ひとり勉強会

ひとり楽しく勉強会

forall と -> : カリーハワード (1.3)

Coq

ところで、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に頼らず直接書き下す
証明全体をexactで書いちゃえるほど小さい定理はあんまりない、というか大抵それは auto で片付きますし型付きますが、大きな定理の末端の方だと、ちょくちょくexactは活躍します。Coqさんにいちいちapplyで筋道を教えて上げるより人間がexactで書いてしまった方が速かったりするので。


「この型を持つ値を作ってね！」に対して、他のやり方もあるでしょう。型をみると２引数関数なのはわかるから、まず、そう引数を置いてみて、関数の本体はそれから考える…

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 コマンドを使うと、どういう関数として定義されたかを見ることができます（右下）。