이미 입증 된 lema/theorem/corollary in coq를 사용합니다.

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가)와 같은 증명하기 위해 A/\ B는 B/\ A와 동일하다는 사실을 사용할 ~ (B/\ 에이). 내 입증 된 보조 정리를 사용할 수 있습니까?

Answer 1

당신은

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

이 apply unit_uniq

를 말한다 라인을 참조

여기 예를 들어 거기 apply <lemma>.

사용할 수 있습니다