2

Coq で証明しようとしていますが、すでに定義および証明されている補題を使用したいと考えています。以下のコードは可能ですか？

Lemma conj_comm:
forall A B : Prop, A /\ B -> B /\ A.
Proof.
intros.
destruct H.
split.
exact H0.
exact H.
Qed.


Lemma not_conj_comm:
forall A B : Prop, ~(A /\ B) -> ~(B /\ A).
Proof.
intros.
intro.
unfold not in H.
apply H.
use H0.

上記では、~(A /\ B) が ~(B /\ A) と同じであることを証明するために、A /\B が B /\ A と同じであるという事実を使用したいと考えています。私の証明された補題を使用することは可能ですか?

4

1 に答える 1

3

あなたが使用することができますapply<lemma>.

ここに例があります

http://blog.mikael.johanssons.org/archive/2007/08/coq-and-simple-group-theory/

言う行を参照してくださいapply unit_uniq

于 2012-11-25T17:02:04.067 に答える