ちょっと証明を
Coqの証明で遊びたくて、うずうずしている人もいるでしょうから、まずは 詳しい説明はとばして
をCoqで証明してみましょう。ここでA, B, Cは任意の命題です。「A \/ B」は「A または B」の意味です。「A /\ B」は「A かつ B」の意味です。そして、「->」は、「ならば」を意味する記号で、「A -> B」の場合は「A ならば B」を意味します。ですから、
では（CoqIdeではなく）Coqを起動してください。
| Welcome to Coq 8.1pl3 (Dec. 2007) Coq < |
コマンドプロンプトのような窓がでて、その中に上記のような文字が表示されているでしょうか（数字は多少違うかも）。
説明は省きますが、MLと名前をつけてSectionの中に入ります。命令はSeciton ML.です。（名前のMLは勝手な他の名前でも結構です。）
| Welcome to Coq 8.1pl3 (Dec. 2007) Coq < Section ML. Coq < |
つぎに、これから使う変数A, B, Cが、命題（Prop）であることをCoqに教えないといけません。それはVariable命令を使います。また、後々の説明のために、まったく使用しない変数 D も一緒に宣言しておきます。
| Welcome to Coq 8.1pl3 (Dec. 2007) Coq < Section ML. Coq < Variables A B C D:Prop. A is assumed B is assumed C is assumed D is assumed Coq < |
変数A, B, C, Dの間の空白は重要です。もし、「Variables ABCD:Prop.」としてしまうと、変数名がABCDの１つの変数だとCoqは解釈します。（実際にCoqにその命令Variables ABCD:Prop.を与えると、変数が1つなのにVariablesと複数形になっているので、Coqに叱られます。Variable ABCD:Prop.とすれば、Coqに叱られることなく変数ABCDを設定できます。）
さあ、いよいよ１．を定理（Theorem）として宣言します。定理の名前はOrtoAndにしましょう。（まったくセンスのない名前ですがご勘弁を。）
|
Coq < Variables A B C D:Prop. A is assumed B is assumed C is assumed D is assumed Coq < Theorem OrtoAnd : ((A \/ B) -> C) -> ((A /\ B) -> C). 1 subgoal A : Prop B : Prop C : Prop D : Prop ============================ (A \/ B -> C) -> A /\ B -> C OrtoAnd < |
プロンプトがOrtoAnd <に変わり、証明モードに入りました。またフォントの関係で、「 \ 」は「 \ 」と表示されています。さて、上記の
|
1 subgoal A : Prop B : Prop C : Prop D : Prop ============================ (A \/ B -> C) -> A /\ B -> C |
の部分ですが、============================を境に、上段が仮定の部分、下段が結論（goal又はsubgoal）の部分になります。上記は、A, B, C, Dが命題であるという以外には仮定は何もなく、結論が(A \/ B -> C) -> A /\ B -> Cとなっています。Coqの中では論理記号の結合の強さがはっきりと決まっているので、括弧が勝手に省略されています。また、「->」は右に結合的というやつで、「A -> B -> C」と書くと、「A -> (B -> C)」のことになります。
Coqはいわゆる証明支援というやつで、証明したい命題から始めて、さかのぼっていくスタイルをとります。つまり、「2辺とその間の角が等しいことがわかったから、よって、合同であることが言えた。」というスタイルではなく、「合同であることを示したいんだけど、そのためには何を言えばいいかな。」という風に逆に考えるスタイルをとります。
では、さかのぼることにしましょう。まずはProof.命令を実行します。
|
Coq < Theorem OrtoAnd : ((A \/ B) -> C) -> ((A /\ B) -> C). 1 subgoal A : Prop B : Prop C : Prop D : Prop ============================ (A \/ B -> C) -> A /\ B -> C OrtoAnd < Proof. OrtoAnd < |
実はこのProof.命令は何もしないのだそうです。つまりこのProof.命令は省略しても構わないそうです。「これから証明するぞ」という意気込みを表すのでしょうか。
示したい命題（subgoal）が「P -> Q」のような形をしているときは、introという命令（このような命令のことを証明モードではtacticと呼びます。）で、Pの部分に名前をつけて仮定の方（上段）に持っていきます。名前は H にしましょう。
| OrtoAnd < Proof. OrtoAnd < intro H. 1 subgoal A : Prop B : Prop C : Prop D : Prop H : A \/ B -> C ============================ A /\ B -> C OrtoAnd < |
どのようにさかのぼったのか、おわかりでしょうか。(A \/ B -> C) -> A /\ B -> Cを証明するには、H : A \/ B -> Cを仮定してA /\ B -> Cを示せばよい、というわけです。
subgoalがまだ「P -> Q」の形をしていますね。今度は仮定に H0 と名前をつけましょう。
| OrtoAnd < intro H0. 1 subgoal A : Prop B : Prop C : Prop D : Prop H : A \/ B -> C H0 : A /\ B ============================ C OrtoAnd < |
仮定の「H0 : A /\ B」は、「A」と「B」の2つの仮定に分けてもいいですね。これは少し手間がかかりますが、次のようにします。まずは、仮定の「H0 : A /\ B」に、消去命令であるelimを実行します。（消去命令とは言いながら H0 は消えません。ここで消去するのは、H0そのものというよりも、論理記号の「/\」です。）
| OrtoAnd < elim H0. 1 subgoal A : Prop B : Prop C : Prop D : Prop H : A \/ B -> C H0 : A /\ B ============================ A -> B -> C OrtoAnd < |
この後、intro a.に続いてintro b.を実行して、仮定に「a : A」と「b : B」を追加したいのですが、これは一度にintros a b.で実行できます。
| OrtoAnd < intros a b. 1 subgoal A : Prop B : Prop C : Prop D : Prop H : A \/ B -> C H0 : A /\ B a : A b : B ============================ C OrtoAnd < |
これで、H0が「a : A」と「b : B」の2つに分かれました。仮定の「H0 : A /\ B」は本当にいらなくなりました。clear命令の練習のために、本当に消去してみましょう。 ここでの証明程度のときは、そんなことは普通しませんが、長い命題を証明しているときなどは、画面上からそのような「ゴミ」を消去することで、随分見やすくなります。
| OrtoAnd < clear H0. 1 subgoal A : Prop B : Prop C : Prop D : Prop H : A \/ B -> C a : A b : B ============================ C OrtoAnd < |
ここで、後の説明のために、普通はしないことをここでさせてください。それは仮定「b : B」の消去です。繰り返しますが、普通はそんなことしません。仮定を減らしてしまったら、証明できるものもできなくなるかもしれません。clear命令をするときは、十分気をつけてください。 心配な人は次のclear b.命令を実行しなくても構いません。それでももちろん最後までうまく証明を続けることができます。
| OrtoAnd < clear b. 1 subgoal A : Prop B : Prop C : Prop D : Prop H : A \/ B -> C a : A ============================ C OrtoAnd < |
さらに証明をさかのぼりましょう。仮定 H を使ってさかのぼろうと思います。 H が「P -> Q」の形をしているときのさかのぼる命令（tactic）はapplyです。
| OrtoAnd < apply H. 1 subgoal A : Prop B : Prop C : Prop D : Prop H : A \/ B -> C a : A ============================ A \/ B OrtoAnd < |
何が起きたかお分かりでしょうか。証明をさかのぼっているということに注意して考えると、上記で起きたのは、
「H : A \/ B -> Cが仮定されている状況で C を証明したいなら、同じ仮定のもとで、 A \/ B を証明すればよい。」
ということになります。
さて、「A \/ B」を証明するためには何を証明すればよいでしょうか。「A \/ B」は「A または B」のことですから、 「A」あるいは 「B」の一方のみ が証明されれば十分です。そして、仮定の中に 「a : A」 があります。 ということで、「A \/ B」のうち、「B」を切り捨てて、「A」のみの証明にさかのぼりましょう。それにはleft.命令を使います。（「A」を切り捨てて、「B」を残すならright.命令です。）
| OrtoAnd < left. 1 subgoal A : Prop B : Prop C : Prop D : Prop H : A \/ B -> C a : A ============================ A OrtoAnd < |
ここまでくるとゴールが見えてきたと思います。仮定の中に「 a : A 」があり、証明するのは「A」です。つまり、仮定にある命題がそのままsubgoalになっているわけです。こういうときはassumption.命令で証明が完了します。証明が完了したら、Qed.命令で証明モードを抜けましょう。
| OrtoAnd < assumption. Proof completed. OrtoAnd < Qed. intro H. intro H0. elim H0. intros a b. clear H0. clear b. apply H. left. assumption. OrtoAnd is defined Coq < |
上記のProof completed.の部分が、証明が完了したことを表しています。しかし、その時点ではまだプロンプトがOrtoAnd <になっています。この状態ではまだ証明モードを抜けていないので、定理OrtoAndも、この後使用することはできません。そこでQed.命令です。その命令の後、今までの証明で使われた命令（tactics）が列挙され、OrtoAnd is definedなる宣言も出て、プロンプトがCoq <に戻りました。
定理OrtoAndが存在するか確かめたかったらCheck命令、 定理OrtoAndの証明も見たいならPrint命令です。
| OrtoAnd is defined Coq < Check OrtoAnd. OrtoAnd : (A \/ B -> C) -> A /\ B -> C Coq < Print OrtoAnd. OrtoAnd = fun (H : A \/ B -> C) (H0 : A /\ B) => and_ind (fun (a : A) (_ : B) => H (or_introl B a)) H0 : (A \/ B -> C) -> A /\ B -> C Coq < |
Print命令でCoqが表示する内容のうち、最後の行はCheck命令で表示されたものと同じはずです。そして、Check命令では表示されない部分が証明です。とはいっても、表示されているのは「Curry-Howard同型によって証明に対応する（型付き）λ式」です。しかも普通の（型付き）λ式と少し表示が違っています。ですから、（型付き）λ式から証明への直し方を知らないと、Print命令の表示からは証明を再構成できないと思います（というか、Print命令のこの表示以外に証明を表示する方法を私は知りません）。と言うことで、その直し方知りたいですよねえ。
その直し方は、話が長くなるので後にしましょう。とりあえずSection MLから出ようと思いますが、Sectionの中と外でどう違うかについて少し体験するために、 最初に宣言した変数 A, D をCheckコマンドで見てみましょう。
|
Coq < Print OrtoAnd. OrtoAnd = fun (H : A \/ B -> C) (H0 : A /\ B) => and_ind (fun (a : A) (_ : B) => H (or_introl B a)) H0 : (A \/ B -> C) -> A /\ B -> C Coq < Check A. A : Prop Coq < Check D. D : Prop Coq < |
A : Prop及びD : Propと出ています。つまり変数 A, D はProp（命題）である、 と言うわけです。ではSection MLから出ましょう。命令はEnd ML.です。
| Coq < Check D. D : Prop Coq < End ML. Coq < Check A. Toplevel input, characters 6-7 > Check A. > ^ Error: The reference A was not found in the current environment Coq < Check D. Toplevel input, characters 6-7 > Check D. > ^ Error: The reference D was not found in the current environment Coq < Check OrtoAnd. OrtoAnd : forall A B C : Prop, (A \/ B -> C) -> A /\ B -> C Coq < |
Section MLの外に出てから、即ちEnd ML.命令の後のCheck A.コマンドに対するCoqの出力を見てください。今度は
Error: The reference A was not found in the current environment
などとエラーが出ています。しかも、「 A なんて知らない」という内容のエラーです。変数 D に対しても同様です。 実は、Sectionの中におけるVariable命令は、いわゆる「局所変数」を定義することになっているのです。ですから、Sectionの外に出たとたん「 A なんて知らない」「 D なんて知らない」になったわけです。
さらに、Section MLの外に出てからもう一度Check OrtoAnd.命令を実行してみました。ちょっと表示されるものが増えていますね。そうです、forall A B C : Prop, の部分が増えています。つまり、
任意の命題 A, B, C に対して((A \/ B) -> C) -> ((A /\ B) -> C)が成立する。
という内容に変わっています。Section MLの外では変数 A, B, C すべてが存在しない変数ですから、裸の
((A \/ B) -> C) -> ((A /\ B) -> C)
のままではまずいわけです。それで上記のようになったというわけです。
ここで注意することがあります。それは変数 D のことです。Section MLの外に出てからCheck OrtoAnd.命令を実行すると、定理OrtoAndの表示が増えていましたが、それはforall A B C D : Prop, ではなくforall A B C : Prop, でした。つまり、変数 D はまったく消えてしまっているわけです。Coqは定理の証明の際、Sectionの中で不必要な局所変数を定義してしまっても、Sectionの外に出たときはそれが最初からなかったかのように忘れてくれるのです。
型
ここで、Checkコマンドについて思い出してもらいたいことがあります。 「まずはいじってみる」で、命令Check 3.を実行した ときのCoqの出力を思い出してください。Coqは
| Welcome to Coq 8.1pl3 (Dec. 2007) Coq < Check 3. 3 : nat Coq < |
なる表示を返してきました。 この「3 : nat」は「3の型はnatである」と読めるのでした。では、このページでした 最初のCheck命令を見てください。そこではCheck OrtoAnd. 命令を実行しました。そのときのCoqの出力は
| OrtoAnd is defined Coq < Check OrtoAnd. OrtoAnd : (A \/ B -> C) -> A /\ B -> C |
でした。実はこれも 「OrtoAndの型 は((A \/ B) -> C) -> ((A /\ B) -> C)である」と読めるのです。 つまり「Theorem OrtoAnd : ((A \/ B) -> C) -> ((A /\ B) -> C).」 なる命令からはじめた証明の作業は、実は、 「（命題変数 A,B,C,D から、）型が ((A \/ B) -> C) -> ((A /\ B) -> C)であるλ式を作る作業」だったのです。 そして、 どんな形かわからないλ式を、OrtoAndなる変数名の変数で表したのでした。 もちろん勝手な型に対して、必ずそういう型を持つλ式を作れるとはかぎりません。 作れないというのは、証明で言えば証明できなかったということなのです。
また、「a:A」の別の読み方として、「aは、論理式Aの証明である」という読み方もあります。それについては、ここで説明しています。