如何解决已解决 - 是一个目标打印错误Coq - 列表上的微不足道的归纳不接受假设
在我当前的证明中,我最终需要针对 else
情况下的 case 析取情况得出以下结果。
1 subgoal (ID 28899)
l : list (Concrete.cvalue sem)
============================
match l with
| [] | _ => True
end
因此,我打算通过应用 induction l. apply I.
对我的列表进行微不足道的归纳,最终得到
1 subgoal (ID 28909)
a : Concrete.cvalue sem
l : list (Concrete.cvalue sem)
IHl : match l with
| [] | _ => True
end
============================
match l with
| [] | _ => True
end
然而,一旦到了这里,他不接受assumption
也不接受exact IHl
,说
Error:
In environment
a : Concrete.cvalue sem
l : list (Concrete.cvalue sem)
IHl : match l with
| [] | _ => True
end
The term "IHl" has type "match l with
| [] | _ => True
end" while it is expected to have type
"match l with
| [] | _ => True
end".
您知道可能的原因是什么吗?如何解决?
勘误:它似乎是目标中的打印问题,因为最初的情况是
s : s_constr sem
c0 : Concrete.cvalue sem
============================
match s with
| Etat =>
match c0 with
| ctuple [env] => True
| ctuple [env; exp] => match s with
| Val => eval_lv env exp c0
| _ => True
end
| ctuple (env :: exp :: _ :: _) => True
| _ => True
end
| _ => True
end
之后我申请了 destruct s; simpl; try apply I.
,我应该得到
match c0 with
| ctuple [env] => True
| ctuple [env; exp] =>
match s with
| Val => eval_lv env exp c0
| _ => True
end
| ctuple (env :: exp :: _ :: _) => True
| _ => True
end
,但无论如何打印
match c0 with
| cval_base _ _ | _ => True
end
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。