coq我应该使用什么战术？A:Prop,A - > ~~ A

Question

我不知道我用什么策略来证明这个结构.我尝试了两种方法,但我陷入了两种方法.

Lemma Exo17 : forall A : Prop, ~~(A \/ ~A).
Proof.

Methode 1
intro.
unfold not.
intro.

Methode 2
intro.
intro.
case H.

Answer 1

这种情况的最佳策略称为"笔和纸".实际上,你应该首先尝试手工建立证据[ 直觉主义后续微积分LJ应该可以正常工作].

一旦你清楚地了解了证明的工作原理,在Coq中编码它将是微不足道的.