assume p
是毫无用处的!
NNPP
Theorem easy : forall p q:Prop, (p->q)->(~q->~p).
Proof. intros. intro. apply H0. apply H. exact H1. Qed.
当时的环境是:
Section CONTRA.
Variables P Q : Prop.
Hypothesis PimpQ : P -> Q.
Hypothesis notQ : ~Q.
Hypothesis Ptrue : P.
Theorem contra : False.
Proof.
您应该能够继续证明。它比您的证明要多一些(在第4行,您刚刚编写Q,在这里您必须通过组合
1 subgoal
P : Prop
Q : Prop
PimpQ : P -> Q
notQ : ~ Q
Ptrue : P
============================
False
PimpQ
来证明这一点。但是,它应该是相当
Ptrue
...::)
实际上并不困难。刚打球,引入了双重否定,事情会自动下降。这就是证明的样子。
trivial
ta daaaa!
示例使用功能来证明。
Theorem T1 : (~q->~p)->(p->q).
Proof.
intros.
apply NNPP.
intro.
apply H in H1.
contradiction.
Qed.