forall と -> (1.1)
Modus Ponens
一番最初の例として
- Anarchy Proof 第1問: http://as305.dyndns.org/aps/problem/view/1
を証明してみよう。古代ギリシャから伝わる "Modus Ponens" とよばれる定理「"PならばQ" であり、しかも "P" ならば、それすなわち "Q" である」です。この定理を Coq で書くと、こうなります。
Theorem Modus_ponens: forall (P: Prop), forall (Q: Prop), (P -> Q) -> P -> Q.
- 「forall ほげ ふが」は「どんなほげについても、ふがが成り立つ」と読 む。
- 「ほげ -> ふが」は「ほげ ならば ふが」と読む。-> は右結合。
- Anarchy Proof には forall (P Q: Prop), (P -> Q) -> P -> Q. と短く書いてありますが、略記法です。連続するforallはまとめて書けます。意味は同じです。
合わせると「どんな命題*1 P と Q を持ってきても、"P->Q" ならば、しかもさらに "P" ならば、"Q" である」。このThorem文の最後もピリオドで終わってますが、基本的に、Coqの文はすべてピリオド終端です。
証明
これを CoqIDE に打ち込んで、Ctrl+Alt+↓ を押すと、こうなる。Ctrl+Alt+↓ は、CoqIDE 上で１つ Coq のコマンドを実行するショートカットキーです。ちなみに Ctrl+Alt+↑ で１つ戻れます。
すると、右上に
1 subgoal ------------------------------------------------ forall (P Q: Prop), (P -> Q) -> P -> Q.
と出る。Coq さんが「対話証明モード」に入りました。「Theorem などと宣言したからには、この forall (P Q: Prop), (P -> Q) -> P -> Q. とやら、証明する覚悟はできているのであろうな？？？？」という問いかけです。証明しましょう。
Theorem Modus_ponens: forall (P: Prop) (Q: Prop), (P -> Q) -> P -> Q. Proof.
Proof. と打って Ctrl+Alt+↓。別に何も起こらないので書かなくていいんですけど、なんとなく気分が出るので Proof. と打ってから証明始めます。気分は重要です。
Theorem Modus_ponens: forall (P: Prop), forall (Q: Prop), (P -> Q) -> P -> Q. Proof. intros.
Ctrl+Alt+↓
対話証明モードに入ったら、「tactic」と呼ばれる、証明コマンドを入力することで証明をすすめます。"intros"は最重要tacticのひとつ。
- intros
- 「"A -> B" を証明しろ」という状態を、「"A" が成り立つものと仮定して "B" を証明しろ」に変える。
- "->" が沢山あっても一気に剥がす。「"A -> (B->C)" を証明しろ」を、「"A"と"B"が成り立つものとして、"C"を証明しろ」に。
まあ、"ならば" の定義みたいなものでしょうか。"A ならば B" を証明するには、「"A"が成り立つと仮定したら"B"が証明できる」ことを言えばよい。そういう方針で証明しますんでよろしくお願いします、とCoqさんに伝えるtacticが、introsです。ここら辺、言葉遊びをしているだけに聞こえるかもしれませんが、まあ先を見てみましょう。
intros. を実行すると、右上のCoqさんの要求がこのように変化します。
1 subgoal P: Prop Q: Prop H: P -> Q H0: P ------------------------------------------------ Q
横線の上が、いま仮定として使ってよいもの、下が証明すべきゴールです。Pという命題があって、「Qという命題があって、P->Qが成り立っていて、Pが成り立っている」 という仮定のもとで、Q を証明せよ、という状態になりました。あ、そうそう、言い忘れてましたが、intros さんは "->" だけでなくて "forall" も全部ひっぺがして仮定に置きます（というか、実は仕組み的には->もforallもCoqの中ではほとんど同じものだったり…）。
元々のゴールから
- "forall (P: Prop), "forall (Q: Prop), (P->Q) -> P -> Q" を証明せよ
- "P: Prop" があったと仮定して "forall (Q: Prop), (P->Q) -> P -> Q" を証明せよ
- "P: Prop" と "Q: Prop" があったと仮定して "(P->Q) -> P -> Q" を証明せよ
- "P: Prop" と "Q: Prop" があって "P->Q" が成り立つと仮定して "P -> Q" を証明せよ
- "P: Prop" と "Q: Prop" があって "P->Q" と "P" が成り立つと仮定して "Q" を証明せよ
まで、4個のひっぺがしが行われました。
さて、お次のtacticは…。
apply H.
Ctrl+Alt+↓。ゴールが変わります。
1 subgoal P: Prop Q: Prop H: P -> Q H0: P ------------------------------------------------ P
違いがわかりますでしょうか。さっきまで "Q" だったゴールが "P" になってます。
- apply H
- 「"A->B"の形の仮定Hがあって、ゴールが"Bを証明せよ"」という状態を「"Aを証明せよ"」というゴールに変える
exact H0.
Ctrl+Alt+↓。さっきの証明目標図をよくみると、仮定に"P"があって、ゴールも"P"です。「"P"が成り立つことを仮定して、"P"が成り立つことを証明せよ」と言われているわけです。おまえさん、それはもう、仮定そのまんま(exact)じゃん！！とCoqさんに伝えるtacticが、exactです。
はい、これで証明完了しました。ゴールが "Proof completed." になるはずです。
最後に、"Qed." と打ち込んで締めます。これは"Proof."と違って気分の問題ではなく、打ち込まないと証明が終わりません。
Qed.
Ctrl+Alt+↓。
証明完了！
