2

私は 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 キーワードへの 1 対 1 のマッピングがあるかどうか誰か教えてもらえますか?

4

3 に答える 3

4

NNPPだめです！

Theorem easy : forall p q:Prop, (p->q)->(~q->~p).
Proof. intros. intro. apply H0. apply H. exact H1. Qed.
于 2013-10-04T00:45:18.920 に答える
2

次のように証明を開始できます。

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 を書きました。ここでは、PimpQandを組み合わせて証明するPtrue必要があります。ただし、公平なはずtrivialです... :)

于 2013-02-01T16:16:12.500 に答える
0

実際、それほど難しくはありません。

遊んだだけで、二重否定が導入され、状況は自動的に横ばいになりました。これが証明の様子です。

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

タダアア！

于 2013-02-02T05:45:43.837 に答える