logic - 使用 Coq Proof Assistant 证明 (p->q)->(~q->~p)

Question

我对 Coq 还很陌生，正在尝试来自 Ruth 和 Ryan 的示例引理。使用自然演绎的证明非常简单，这就是我想用 Coq 证明的。

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

我被困在第 3 行assume p。

有人可以告诉我从自然演绎到 Coq 关键字是否存在一对一的映射？

score 4 · Accepted Answer

NNPP没用！

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

score 2 · Accepted Answer

你可以像这样开始你的证明：

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...... :)

score 0 · Accepted Answer

其实没那么难。

只是玩了一下，引入了双重否定，事情就自然而然地平息了。这就是证明的样子。

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

呸呸呸！

3 回答 3