資料は下の方にあるので確認しておいてください。
Coqをダウンロードして、実行できるようにせよ。
ヒント
CoqIDEを起動し、以下のコードを打ち込め。(Emacsに慣れている場合は、CoqIDEではなくProofGeneralを用いるほうがよいかもしれない。)
Theorem tautology : forall P : Prop, P -> P.
Proof.
intros P H.
assumption.
Qed.
次のことを確認せよ。
また、同様に次のコードを打ち込め。
Theorem wrong : forall P : Prop, P.
Proof.
intros P.
Qed.
これを最後まで実行しようとするとどのようになるか調べよ。
次の定理を証明せよ。ただし、全自動で証明できてしまうautoやtautoなどのコマンドは使わないこと。
Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
(* ここに証明を書く *)
Qed.
ヒント
矢印で P -> Q と書いてあるものは「PならばQ」という意味だと思ってください。
例えば、applyコマンドとintrosコマンドを使うことで証明することができます。
applyコマンドとintrosコマンドのもっとも基本的な使い方は以下の通りです:
はじめのうちは、「初手はintros」と思ってしまってもよいかもしれません。
次の定理を証明せよ。ただし、全自動で証明できてしまうautoやtautoなどのコマンドは使わないこと。
Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
(* ここに証明を書く *)
Qed.
ヒント
必要なコマンドについては下の方を参考に調べてみてください。(調べるのも練習のうちということで……わからなかったら直接質問してもOKです。)
スラッシュとバックスラッシュの組は論理積「PかつQ」をあらわします。これは∧という記号を半角文字だけで表したものです。
チルダ記号は論理否定「Pでない」をあらわします。また、「False」は矛盾(別の言い方をすると、ある命題が偽であること)を意味します。
次の定理を証明せよ。ただし、全自動で証明できてしまうautoやtautoなどのコマンドは使わないこと。
Theorem Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q.
Proof.
(* ここに証明を書く *)
Qed.
ヒント
バックスラッシュとスラッシュの組は論理和「PまたはQ」をあらわします。これは∨という記号を半角文字だけで表したものです。
次の定理を全て証明せよ。ただし、全自動で証明できてしまうautoやtautoなどのコマンドは使わないこと。
Theorem DeMorgan1 : forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q).
Proof.
(* ここに証明を書く *)
Qed.
Theorem DeMorgan2 : forall P Q : Prop, ~P /\ ~Q -> ~(P \/ Q).
Proof.
(* ここに証明を書く *)
Qed.
Theorem DeMorgan3 : forall P Q : Prop, ~(P \/ Q) -> ~P /\ ~Q.
Proof.
(* ここに証明を書く *)
Qed.
ヒント
対称性より、もう一つのドモルガン則も存在しますが、これは無仮定では証明できないことが知られています。これについては後日扱う予定です。
次の定理を証明せよ。ただし、全自動で証明できてしまうautoやtautoなどのコマンドは使わないこと。
Theorem NotNot_LEM : forall P : Prop, ~ ~(P \/ ~P).
Proof.
(* ここに証明を書く *)
Qed.
証明はProofで始まってQedで終わります。この間、CoqIDEの右上の画面は例えば次のようになっています。
1 subgoals
P : Prop
H : P
______________________________________(1/1)
P
水平線の上と下では意味が真逆なので注意してください。
「AかつB」を証明する場合などで、複数の命題を証明する場合があります。これをサブゴールが複数あるといいます。このときは水平線がサブゴールの数だけ出てきます。使ってよい仮定はサブゴールによって異なりますが、一番上のサブゴールの仮定のみ表示されます。タクティックは一番上のサブゴールに対して実行されます。
記号論理学経験者向けの説明: Coqの証明は基本的に「証明図(証明木)を下から書く」という手順になります。このイメージを持っておくとわかりやすいかもしれません。
さて、今回は命題論理の証明です。
まず、ドキュメントとして次のページはよく使うので覚えておきましょう。
また、Coqの日本語資料はいくつか存在しますので、いろいろGoogle検索で頑張って調べてみてください。
今回の課題は、少なくとも以下のタクティック(証明用のコマンドのこと)を覚えていれば証明できると思います
そのほか、次のタクティックも覚えておくとよいでしょう。
また、今回は禁止ですが、次の自動証明コマンドもよく使われます。