Coq Proof Assistant를 사용하여 (p-> q) -> (~ q -> ~ p)를 증명하십시오.

저는 Coq을 처음 접했고 Ruth와 Ryan의 샘플 보조 정리를 시험 중입니다. 자연 공제를 사용한 증명은 매우 사소한 것이며, 이것이 내가 Coq를 사용하여 증명하고자하는 것입니다.Coq Proof Assistant를 사용하여 (p-> q) -> (~ q -> ~ p)를 증명하십시오.

assume p -> q. 
    assume ~q. 
    assume p. 
     q. 
     False. 
    therefore ~p. 
    therefore ~q -> ~p. 
therefore (p -> q) => ~q => ~p.

나는 3 행에 붙어있다. assume p.

자연 공제에서부터 Coq 키워드까지 일대일 매핑이 있는지 누군가가 말해 줄 수 있습니까?

이 같은 증명서를 시작할 수 있습니다

Section CONTRA. 
Variables P Q : Prop. 

Hypothesis PimpQ : P -> Q. 
Hypothesis notQ : ~Q. 
Hypothesis Ptrue : P. 

Theorem contra : False. 
Proof.

그 시점에서 환경 :

1 subgoal 

    P : Prop 
    Q : Prop 
    PimpQ : P -> Q 
    notQ : ~ Q 
    Ptrue : P 
    ============================ 
    False

당신은 증거를 계속 할 수 있어야한다. 귀하의 증거보다 좀 더 자세한 내용이 될 것입니다. (방금 4 번째 줄에 방금 쓴 q, 여기에 PimpQ과 Ptrue을 결합하여 증명해야합니다.) trivial ...

2013-02-01 16:16:12 Ptival

게시물 주셔서 감사합니다. 질문을 게시 한 후 약 1 시간 만에 알아 냈습니다. 솔루션은 아래에 게시됩니다. 하하! – user1791452

그래, 나는 쉬운 해결책이고 당신이 배우는 방법이기 때문에 전체 해결책을주고 싶지 않았다. :) – Ptival

그리 어렵지 않습니다. , 사실은.

방금 놀아서 두 번 부정을 도입하고 물건이 자동으로 넘어졌습니다. 이것이 증명의 모습입니다.

Theorem T1 : (~q->~p)->(p->q). 
Proof. 
intros. 
apply NNPP. 
intro. 
apply H in H1. 
contradiction. 
Qed.

Ta daaaa!

2013-02-02 05:45:43 user1791452

NNPP은 쓸모가 없습니다.

Theorem easy : forall p q:Prop, (p->q)->(~q->~p). 
Proof. intros. intro. apply H0. apply H. exact H1. Qed.

2013-10-04 00:45:18 STyx

이 대답에 대해 자세히 설명해 주시겠습니까? –

답변