形式的定理証明をするためのプログラミング言語と開発環境のセットです。
数学の定理の証明を形式的な記法を用いて記述し、その証明の正当性を検査することができます。
Coqはプログラミング言語なので、Coqで書かれたプログラムの動作に対して証明をつけることができます。
CoqIDE を利用するので、CoqIDEが同梱されているものをダウンロードして、インストールしてください。
CoqIDEを起動してください。
CoqIDEのメインのエディタ欄に以下のように入力してください。
Eval lazy in (1+1).
Eval lazy in (2*2).
Eval lazy in ( (fun x => x*2) 3).
CoqIDEでは、処理をソースコードの途中まで進めたり、戻ったりすることで証明を書いていきます。
ツールバー上の矢印ボタンをいじって、遊んでみてください。
矢印ボタンは5つありますが、左から順に
- 1ステップ進む
- 1ステップ戻る
- カーソルのある場所まで進む/戻る
- 一番下まで進む
- 一番上まで戻る
です。
各種説明は後回しにして、まずは簡単な証明を書きます。
Theorem Modus_Ponens: forall P Q:Prop, (P -> Q) -> P -> Q.
Proof.
Qed.
これを入力し、Qed.の位置まで進めてください。
まだ証明は終了していないので、Qed.の位置でエラーが出るはずです。
この、ProofとQedの間に証明を書きます。(Proof.は無くても良いです)
このように書いてください。
intros.
apply H.
exact H0.
すると証明が完了し、Qed.のところまで進めるようになります。
それでは、一個ずつ見ていきます。画面の右上に進捗状況が書かれています。証明をするときはこれを見ながら証明を書くことになります。
証明を開始した段階では
1 subgoal
______________________________________(1/1)
forall P Q : Prop, (P -> Q) -> P -> Q
となっています。この水平線が大きな意味を持ちます。
- 水平線の上側…持ち物を表します。上にあるものを使って下にあるものを証明します。
- 水平線の下側…ゴールを表します。下にあるものは持ち物ではありません。これを今から得ることが目標になります。
現在は、手持ちが全くない状態から、「forall P Q : Prop, (P -> Q) -> P -> Q」を証明したいという意味になります。
まず、introsをします。 証明の最初の一歩はintrosだと思って差し支えありません。
すると、以下のようになります。
1 subgoal
P : Prop
Q : Prop
H : P -> Q
H0 : P
______________________________________(1/1)
Q
これは、手持ちとしてP,Q,H,H0があるということを意味します。ただし、P,Qが命題論理において命題に対応するのに対し、H,H0は命題論理において証明に対応するものであり、両者の性質は違います。ここでは、H,H0のみに注目すればよいです。
つまり、「P」と「PならばQ」から「Q」を得ればよいというわけです。
ここでは、次のように考えます。
- Qを証明したいわけだが、「PならばQ」ということがわかっている。とすれば、Pを証明してやれば、Qを証明したことになるのではないか。
これに対応するのが、applyです。apply Hをすると、次のように状況が変わります。
1 subgoal
P : Prop
Q : Prop
H : P -> Q
H0 : P
______________________________________(1/1)
P
さて、ここで、H0こそ、今得ようとしているPという型をもっています。そこで、ちょうどH0が条件を満たしているということを示すために、exact H0と命令します。
すると
Proof completed.
となり、証明に成功したことがわかります。
続いて、「かつ」の可換性を証明しましょう。
Theorem and_comm: forall P Q:Prop, P /\ Q -> Q /\ P.
Proof.
Qed.
これは、「どのような命題P,Qについても、(PかつQ)ならば(QかつQ)」という意味です。
この証明は以下のようになります。
intros.
destruct H.
split.
exact H0.
exact H.
注目すべきは「destruct」と「split」です。
splitは次のような意味です。
- 「QかつP」を証明したいのだから、「Q」を証明して、それが終わったら今度は「P」を証明しよう。両方証明できたら「QかつP」も正しい。
splitを実行したさい、Subgoalの数が増えていることに注目してください。これは、これらのゴールそれぞれを証明する必要があるが、とりあえず一番上を証明しようとしているということを意味しています。(一番上以外については、ゴールのみが見えていて、手持ちは表示できないようです。)
destructの意味は場面によって違いますが、ここでは次のような意味です。
- 「PかつQ」が手元にあるのだから、それを分解してPとQを得ることができる。
続いて、「または」の可換性を証明しましょう。
Theorem or_comm: forall P Q:Prop, P \/ Q -> Q \/ P.
Proof.
intros.
destruct H.
right.
exact H.
left.
exact H.
Qed.
これで証明できます。
ここでは、destructとleft/rightが登場しています。
ここでのdestructは次のような意味です。
- 「PまたはQ」だから、Pだった場合と、Qだった場合を考えて、それぞれ証明すれば良さそうだ。
left/rightは次のような意味です。
- 「QまたはP」を示したいわけだが、要するにどちらか片方を示せば良い。
さて、このように「または」が登場する場合、以下のようなハマりポイントがあります。
Theorem or_comm: forall P Q:Prop, P \/ Q -> Q \/ P.
Proof.
intros.
left.
destruct H.
(* 先に進めない *)
一般に、「または」や「存在する」など、情報を含んでいるタイプのものが出現する場合、手持ちにあるそれを先に処理する必要があります。このことに注意して証明しましょう。
命題論理に限って言えば、証明に必要なタクティックスは、その命題の形でほぼ決まっていきます。
それが以下の表です。
| 命題の形 | 手持ちの中にある場合 | ゴールにある場合 |
|---|---|---|
| A ∧ B | destruct H. | split. |
| A ∨ B | destruct H. | left. / right. |
| A → B | apply H. | intro. |
| False | destruct H. | 手持ちから作るしかない |
なお、否定 ~A は、(A->False) とほぼ同じ意味です。
Falseは論理の世界では⊥と書き、矛盾を意味します。(真偽値を意味するbool型の値はfalse/trueであり、これらとは意味上の対応関係はありますが、基本的には別物です。)
また、場合によっては以下のタクティクスが便利です。
- apply H in H0. -- Hが(P->Q)という型で、H0がPという型のとき、H0をQに変えます。
- assert (補題). -- まず先に「補題」を示します。補題の証明が終わると、「補題」が手持ちとして手に入るので、これを使って元の命題を証明します。
- exfalso. -- Pを証明するかわりに、矛盾⊥を証明することにします。
適当に選んで解けばいいと思います。
Theorem and_assoc: forall P Q R:Prop, ((P /\ Q) /\ R) -> (P /\ (Q /\ R)).
Theorem or_assoc: forall P Q R:Prop, ((P \/ Q) \/ R) -> (P \/ (Q \/ R)).
Theorem and_or_dist: forall P Q R:Prop, ((P /\ Q) \/ R) -> (P \/ R) /\ (Q \/ R).
Theorem or_and_dist: forall P Q R:Prop, ((P \/ Q) /\ R) -> (P /\ R) \/ (Q /\ R).
Theorem de_morgan_1: forall P Q:Prop, ~P /\ ~Q -> ~(P \/ Q).
Theorem de_morgan_2: forall P Q:Prop, ~(P \/ Q) -> ~P /\ ~Q.
Theorem de_morgan_3: forall P Q:Prop, ~P \/ ~Q -> ~(P /\ Q).
Coqは、デフォルトでは直観主義論理を採用しています。以下のような命題は、正しそうにも見えますが、Coqでは証明できません。
- 排中律: forall P, P / ~P
- 二重否定除去: forall P, ~~P -> P
- パースの法則: forall P Q, ((P->Q)->P)->P
ここからは、少し命題論理を超えた話に入ります。
証明したいのは、「排中律が正しいならば、二重否定除去は正しい」です。
Theorem EM_then_NNPP: (forall P, P \/ ~P) -> (forall P, ~~P -> P).
これをintrosすると、手持ちにforallが残ることがわかります。
これは「全てのPについて、ほにゃらら」という意味なので、自分が使いたい値を代入して使うことができます。例えば、この場合、(H P)という式は P / ~P という型をもちます。
これを用いると、以下のように証明できます。
intros.
destruct (H P).
exact H1.
exfalso.
apply H0.
exact H1.
つまり、Pか~Pが言えるので、それぞれについて考えています。
こちらも、考え方は同じですが、少々厄介です。
Theorem NNPP_then_EM: (forall P, ~~P -> P) -> (forall P, P \/ ~P).
最初の2行は、次のようにすると良いでしょう。
intros.
apply H.
このときのapply Hは、自動的にforall Pに代入するPを決定して利用してくれるというものです。この場合、P := P / ~P となり、apply (H (P / ~P)) と等価です。
全体では以下のような手順になります。難しいけど頑張って理解してみると良いでしょう。
intros.
apply H.
intro.
apply H0.
right.
intro.
apply H0.
left.
exact H1.
Theorem EM_then_Perice: (forall P, P \/ ~P) -> (forall P Q, ((P->Q)->P)->P).
Theorem Peirce_then_NNPP: (forall P Q, ((P->Q)->P)->P) -> (forall P, ~~P -> P).