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

你能详细解释这个答案吗？ –

回答