柯克证明助手中的双重否定假说？

Question

有人能向我解释为什么我们要证明~A在elim Ha.之后

在“爱丽姆哈”之前

1 subgoals
 A : Prop
 Ha : ~ ~ A
______________________________________(1/1)
 A

之后

1 subgoals
 A : Prop
 Ha : ~ ~ A
______________________________________(1/1)
 ~ A

对吗，意思是~~A true, ~A true -> A true

据我所知，我只知道~E的规则是~A true, A true -> FalseHood true

Answer 1

在Coq中，~ P是P -> False的表示法。如果我没有弄错的话，对形状为elim的假设使用~ P与直接使用False_rect (您可以Print False_rect获取更多信息)和使用P作为输入是一样的。

这样，您就会对Coq说“我知道P持有，所以使用P -> False，我可以得到False的证明”，它通过矛盾来结束目标。这就是为什么每次您elim一个~ P，Coq要求您提供一个P的证据。在您的例子中，P是~ A。