coq - 矛盾による証明の否定を仮定

Question

私はいくつかの規則を持っていますが、それは基本的に、いくつかの命題 P が決して真ではないということを伴います。Coq を使用して、P が偽であることを証明する必要があります。紙の上でそうするために、私は P が成り立つと仮定し、それから矛盾に到達し、それによって P が成り立たないことを証明します。

P がこの証明に適していると仮定する方法がよくわかりません。これが私が助けを求めていることです。私の現在のコード:

Variables {…} : Prop.
Hypothesis rule1 : … .
Hypothesis rule2 : … .
.
.
.
Hypothesis rule6 : … .
Variable s : P. (* Assume that P holds for proof by contradiction *)
(* other Coq commands *)
(* proof is done *)

誰かが私がこれを正しい方法で行っているかどうかを確認してもらえますか (そうでなければ、どうすればよいですか?)?

Answer 1

あなたがしたいことは、証明することです：

Theorem notP := ~ P.

つまり、次のようになります。

Theorem notP := P -> False.

したがって、タイプ P の変数を使用して、ゴールが False であることを証明する必要があります。

あなたのやり方は受け入れられると思いますが、おそらくそれをVariable s : p.セクションに入れたいと思うでしょう。

Section ProvingNotP.
Variable p : P.
Theorem notP: False.
Proof. ... Qed.
End ProvingNotP.

これはうまくいくはずだと思います。