coq - 在 coq 中使用已经证明的 lema/theorem/corollary

Question

我正在尝试在 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) 相同。是否可以使用我证明的引理？

Answer 1

您可以使用apply<lemma>.

这里有一个例子

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

看到上面写着的那一行apply unit_uniq