使用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

感謝您的留言。我在發佈問題後大概一個小時就想出了它。該解決方案發布如下。哈哈！ – 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

你能詳細解釋這個答案嗎？ –

回答