Coqの入門記事を書く会 (1)
証明支援系Coqの遊び方の入門を書いてみるよ。すでに世の中に何個も入門記事ありますけど、増えて困ることはなかろう…ということで。まず、インストール方法については、id:yoshihiro503 による紹介記事
最近パソコンを買ったんだけど、使い方がよく解らない。という人のために、今日はCoqのインストールの方法を紹介しよう。
を参照のこと。現時点では最新の安定版の Coq 8.2 がおすすめ。
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+↓。
証明完了！
forall と -> (1.2)
いくつか細かい捕捉。
- intro
- introsと同じひっぺがし作業を１回だけやる
Theorem Modus_ponens:
forall (P: Prop),
forall (Q: Prop),
(P -> Q) -> P -> Q.
Proof.
intro.
intro.
intro.3回だけで止めると
P: Prop Q: Prop H: P -> Q ------------------------------------------------ P -> Q
こうなるので、ここで exact H. という証明もありです。apply とか要らない分簡単かも。
- intro X
- X という名前をつけつつintroでひっぺがす
- intros X1 X2 ... Xn
- X1 X2 ... という名前をつけつつn個introsでひっぺがす
Theorem Modus_ponens: forall (P: Prop), forall (Q: Prop), (P -> Q) -> P -> Q. Proof. intros P Q P_naraba_Q. exact P_naraba_Q. Qed.
他にも、intro/intros にはいくつか賢いオプション指定ができるので、詳しくはマニュアル参照のこと。
- assumption
- 仮定にあるどれかがゴールそのまんまだからそれでお願い！という証明
Theorem Modus_ponens: forall (P: Prop), forall (Q: Prop), (P -> Q) -> P -> Q. Proof. intros. apply H. assumption. (* exact H0. の代わり *) Qed.
実は、"exact H" や "exact H0" のように名前を指定しなくても、そのくらい自動で探してこいよ！というとCoqさんちゃんと見つけてくれます。賢いですね。
賢いと言えば
- auto
- Coqさんならできる！頑張れよ！もっと熱くなれよ！！
Theorem Modus_ponens: forall (P: Prop), forall (Q: Prop), (P -> Q) -> P -> Q. Proof. auto. Qed.
実はCoqさん十分賢いのでこの程度の証明は、auto. って書くと勝手に全部やってくれるんですが、それだとあんまりCoq入門にならないので、この記事ではできるだけautoを使わないようにします。
forall と -> : カリーハワード (1.3)
ところで、HaskellやOCamlなどの関数型言語をご存じの方なら100倍高速にCoqを理解できる！というショートカットのご紹介です。以下、この節限定で、説明にHaskellが混じります。Haskellわからんという人はこの節は飛ばしても以降に差し支えはない…はず…たぶん…。
さて、カリー･ハワード同型対応。
をご存じでしょうか。ご存じない方は今すぐググる、上記の記事を読むなどして存じて下さい。論理の「定理」とは要するにプログラミング言語でいう「型」のことであり、「証明」とはその型の「値」のことである、そう見なして完全に整合性がとれる、というお話です。Coqも、この対応関係に基づいて作られた証明系です。
「定理」＝「型」、「証明」＝「値」ということは、
Theorem Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q.
「この定理を証明します」、という宣言は、「この型をもつ値を作ります」という宣言に他なりません。なので、上のTheorem文をHaskellで言い換えると、こう書いてあるのと全く同じことです。
modus_ponens :: (p -> q) -> p -> q
"->" (ならば) とはつまり関数であり、"forall (_:Prop)" とは、多相型です。
（さっきちょっと述べた「forallも->もCoqの内部的にはほとんど同じ」は、多相型と考えると理解できてくる人もいらっしゃるかもしれません。forallも、要するに型を受け取ってなんか返す"関数"なのです。ただしCoqのforallはHaskellの多相型よりも強力で、型/Prop以外のなんでもforallできます。いわゆる依存型というやつで、自然数 forall (x:nat), でも関数 forall (x:A->B), でもなんでもかんでも。使用例はそのうち出てくるかも来ないかも…）
関数型言語と思って証明を作る
さて。
modus_ponens :: (p -> q) -> p -> q
Haskellで「この型を持つ値を作ってね！なんでもいいから！」と言われたら、どうしますか？
まあ見るからに、関数と、値を受け取って、適用して返す関数ですよね…
modus_ponens = (\ f x -> f x)
はいそうです。Haskell だと modus_ponens=($) でも正解ですね。この、一発で「こういう値ですよね」って証明/値を書き下しちゃうスタイルの証明は、"exact" tactic でできます。
Theorem Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q. Proof. exact (fun p q f x => f x). Qed.
Coqだとforallも普通の関数みたいなものなのでその分の引数(p,q)も明示的に書かないといけなくて、ちょっと長くなってますが、Haskellの(\ f x -> f x)と同じ関数です。
- exact t
- ゴールの型を持つ値/証明 t を、これ以上tacticに頼らず直接書き下す
「この型を持つ値を作ってね！」に対して、他のやり方もあるでしょう。型をみると２引数関数なのはわかるから、まず、そう引数を置いてみて、関数の本体はそれから考える…
modus_ponens :: (p -> q) -> p -> q modus_ponens f x = ???
あとは、??? のところに、q型の式をなんとかして埋めればよいわけです。実は intros のやっていることは、ずばり、この作戦なのです。
Theorem Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q. Proof. intros p q f x. (* とりあえず p と q と p->q型の引数fとp型の引数xを導入してみて細かいことはあとで… *)
返値の型はqだから…あ、わかった、f x で作れる！と、ここでわかったらexact。
exact (f x). Qed.
まだ閃けなかったらどうしましょう。f が p->q 型の変数だから、最終的に q 型の値を作るには、この関数を使えば作れるな…
modus_ponens :: (p -> q) -> p -> q modus_ponens f x = f ???
と、とりあえず関数適用を書いてみる。引数のことは後で考える。これが apply です。
Theorem Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q. Proof. intros p q f x. (* とりあえず p と q と p->q型の引数fとp型の引数xを導入してみて細かいことはあとで… *) apply f. (* f:p->q を使ってq型の値を作る、という方針で頑張ります *)
あとはなんとかして p型の値（命題pの証明）を作れば完成！と。
assumption. Qed. Print Modus_ponens.
証明したあとに Print コマンドを使うと、どういう関数として定義されたかを見ることができます（右下）。
forall と -> : ゴールが２つ (1.4)
別の例をやってみたいと思います。Sコンビネータと呼ばれる定理です。
Theorem S: forall (P Q R: Prop), (P->Q->R) -> (Q->P) -> Q -> R.
いきなりexactで書いてもいいんですが、順を追ってやっていきましょう。
intros.
「ゴールにforallや->があったら、とりあえず何も考えずintrosする」というのはかなり成功率の高い戦略です。
略 H: P->Q->R 略 ---------------------------------- R
こうなってると思うので、R を作るには apply H しましょう。他に R が仮定にないですし。これしかない。
さて、見慣れないことが起きました。右側に、"2 subgoals" と出ています。Hは二つ前件がある"ならば"なので（カリーハワード対応的にいうと、2引数の関数なので）、Hを使って"R"を示すには、"P"の証明と"Q"の証明の、二つの証明が必要です。というわけで、Coqさんからの要請として、「証明するものが２つになりましたよー」と言ってきているわけです。"P"と"Q"です。まずは(1/2)のゴールである"P"から片付けます。
apply H0. apply H1. (* exact H1. でも assumption. でも同じ *)
H0 が Q->P で、P を作るには H0 を使えばよい。あとは Q の証明が必要…と思ったら、H1 が Q そのものでした。おしまい。仮定にゴールそのものがあるときは、exactではなくてapplyでもいいです。何も前提条件のない"ならば"（0引数の関数）とみなしてapplyしている感覚です。
Pの証明が終わると自動的にもう一つのゴール"Q"に移るので
assumption. Qed.
こちらも終わらせます。証明完了！
Print S. ==> S = fun P Q R H H0 H1 => H (H0 H1) H1 (型情報略)
forall と -> : 仮定側の変形 (1.5)
ここまでに紹介した apply と intro(s) は、どちらも、証明のゴールを変形する tactic でした。なのですが、これってあまり直感的ではない気がするのですよね。私見ですが。
- 「A と B と C を仮定して Z を証明して下さい！」
って言われたときに
- 「Cが使えるから、Zを言うためにはYを証明すれば言えるな。」てことは、「AとBとCを仮定して、Yを証明」すれば終了だ
という考え方は、勿論しないことはないですけど、自分の場合それよりはむしろ
- 「AとB からは、D が言えるな。」てことは「AとBとCとD から、Zを証明」できればOKだ
- 「あ、CとDからE も示せる。」つまり「AとBとCとDとE から、Z」が言えれば…
と、仮定の方をどんどんリッチにしていって、そのうちZが出てくる、と考えることが多いです。というわけで、仮定の方を変形する証明スタイルをやってみます。お題はさっきの S コンビネータで。
Theorem S: forall (P Q R: Prop), (P->Q->R) -> (Q->P) -> Q -> R. Proof. intros.
introsは仕方ないので何も考えず脊髄反射でintros。そうすると、ゴールはこうなります。
H : P -> Q -> R H0 : Q -> P H1 : Q ------------------- R
H0: "QならばP" と H1: "Q" があるから、これを使って、まず "P" が証明できますよね。H0 に H1 を適用すれば証明できる。
assert (Proof_of_P := H0 H1).
- assert (X := t)
- 証明tによって証明された命題を、名前Xの仮定として追加
すると、Proof_of_P: "P" と、H1: "Q" と H: "Pならば(QならばR)" が仮定にあるのだから、"R" が証明できますね。
assert (PrR := H Proof_of_P H1).
おや、いつの間にやら仮定に R があって、ゴールも R です。証明完了ですね。
exact PrR.
Qed.
Print S.
==>
S = fun P Q R H H0 H1 =>
let Proof_of_P := H0 H1 in
let PrR := H Proof_of_P H1 in
PrR. (* 型情報略 *)証明項をPrintしてみると、このスタイルの証明は、こんな風な、let を使ったプログラムになります。
その他の仮定側変形tactic
さきほどは、H0: Q->P で H1: Q のときに、この２つから P が証明できるよね、と、assert を使ってPを出しました。違うtacticを使う方法もあります。
- specialize (A B)
- 仮定Aを、A B に置き換え
Theorem S: forall (P Q R: Prop), (P->Q->R) -> (Q->P) -> Q -> R. Proof. intros. specialize (H0 H1).
こうすると、さっきまで "H0: Q->P" だったのが "H0: P" に変化します。assertと違って、
- 仮定の名前 X := を書かなくていいので楽
- その代わり、もとあった仮定 Q->P が消えてしまう。複数回 Q->P を使いたい場合は specialize してはいけない
- 逆に考えると、もう二度と使わない仮定なら消えた方が画面が広くて綺麗なので、specialize しちゃってよい
その名の通り、H0という"ならば"型の仮定を、H1 という特殊な場合に限定(specialize)して使うよ、という方針をCoqさんに伝えるのが、このtacticです。
さて、今の仮定は H:P->Q->R、H0:P、H1:Q です。ここから R が出せますね。もう一つ、別の仮定変形があります。
- apply A in B
- 仮定Bを、A B に置き換え
Theorem S: forall (P Q R: Prop), (P->Q->R) -> (Q->P) -> Q -> R. Proof. intros. specialize (H0 H1). apply (H H1) in H0.
こうすると、さっきまで "H0: P" だったのが "H H1: Q->R" を適用(apply)されて、"H0: R" に変化します。specializeは適用する"ならば"仮定の方を消してしまうのに対し、こちらのapply〜inは、適用される側を消して新しい結果で上書きします。これも、消される仮定が後で要るか要らないかよく考えてから使いましょう。
[Coq] forall と -> : まとめ (1.6)
というわけで、Coq入門編その一、forall と -> だけ使った定理の証明、をお届けしました。気が向いたら「and, or, not を使った定理の証明」「exists を使った定理の証明」「帰納法」「forallと->と依存型について本気出して考えてみた」… の順番で続きます。入門記事を書くのはいいけれど、面白い練習問題が提供できないとつまらないよなーむずかしいなー、と思って長年躊躇していたのですが、最近
という読者投稿型Coqの問題集サイトができて、面白い練習問題はここを見ろ！と言えるようになったので、まあいいかなという気分になりました。
今日のまとめ。少なくとも最初のうちは、ゴールにforallや->がいたら何も考えずintros。
- intro
- 「"A -> B" を証明しろ」という状態を、「"A" が成り立つものと仮定して "B" を証明しろ」に変える。forallも同様に仮定に移す
- intros
- introをできるかぎり繰り返す
- apply H
- H:A->B で、ゴールがB なら、ゴールをAに変える
- exact t
- 現在のゴールの型をもつ値/証明 t を直書きする
- assumption
- exactな仮定があるとき自動で探してそれを使う
- auto
- Coqさんは賢い
- assert (X := t).
- 証明tで証明できた事実を新しい仮定Xとして増やす
- specialize (A B).
- 仮定AをA Bに変える
- apply A in B.
- 仮定BをA Bに変える
