如何简化Coq中形式为真-> P的假设？
如何简化Coq中形式为真-> P的假设？
提问于 2020-03-23 08:19:52
如果我在我的证明上下文中有一个看起来像H: True -> P的假设，并且我想把它转换成H: P，那么最简单的方法是什么？我尝试过simpl in H，但它什么也不做，我找到的唯一方法就是非常不满意的pose proof (H Coq.Init.Logic.I) as H。难道没有更简单的方法吗？
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-03-23 08:32:47
除了使用pose proof之外，还有两种方法来处理这个问题。
使用specialize。
这种策略允许你为你的假设提供论据。在你的情况下，你可以做到
specialize (H I).甚至是
specialize H with (1 := I).如果希望创建副本而不是直接实例化as，则可以使用H。
使用forward。
我想这就是你想要的。forward H.会要求你证明H的第一个假设。所以你会这样做：
forward H.
- auto.
- (* Then resume with H : P *)但你也可以为它提供一种(进球-关闭)战术：
forward H by auto.
(* Now you have one goal, and H has type P *)到目前为止，forward还不是标准库的一部分。但是，可以很容易地定义它(这是来自MetaCoq库的定义)。
Ltac forward_gen H tac :=
match type of H with
| ?X -> _ => let H' := fresh in assert (H':X) ; [tac|specialize (H H'); clear H']
end.
Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.请注意，这里的simpl不起作用，因为它并不是一种在通常意义上简化假设的策略，它实际上只是一种应用一些计算规则的策略，它基本上是评估目标或应用它的假设。True -> P不会简化为P，因为这样就会少使用一个参数。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/60817497
复制相关文章
相似问题
腾讯云开发者
