andとorとnot: カリーハワード (2.2)

「プログラミング言語としてみると」さっきの証明は何をやっていたことになるんでしょう。

"Inductive"は、ユーザー定義の新しい命題を定義するのでした。そして、命題＝型です。つまり、ユーザー定義の新しい型を作る機能が対応します。Haskell だと "data" ですね。

data And a b = 
 Conj a b

data Or a b =
   OrIntroL a
 | OrIntroR b

Inductiveによるandとorの定義をHaskellで書き直すと、↑こうなります。公理とは、要するにコンストラクタです。はい。

class And<A,B> {
  public And(A a, B b) { ... }
}

class Or<A,B> {
  public Or(A a) { ... }
  public Or(B b) { ... }
}

Javaで書くとこんな感じです。Andは、2引数のコンストラクタを1つ持つ型です。Orは、1引数のコンストラクタが2つ。どっちを使っても作れますが、どっちかを使わないと作れません。

ちなみに False は、Coq.init.Logic.False:

Inductive False : Prop :=.

公理が一つもない…つまり証明する手段が１つも用意されていない命題、それがFalse、という定義です。Haskellでも

{-# OPTIONS_GHC -XEmptyDataDecls #-}
data False

こう、こういう変な型を定義するには追加オプションが要りますけど、作れます。

さて、あらためて、ド・モルガンの証明とはなんだったかというと…

de_morgan :: (Or a b -> False) -> And (a -> False) (b -> False)

Haskellで「この型を持つ値を作ってね！なんでもいいから！」と言われたら、どうしますか？

de_morgan f =
 Conj (\x -> f (OrIntroL x)) (\y -> f (OrIntroR y))

たとえば、こんな風に書けますね。これが、さっきCoqで作った証明です。

andとorとnot: ド・モルガン (2.1)

andとorとnotを分けて説明するのが面倒くさいので、いきなり全部入りの定理を例にしましょう。今回のお題はド・モルガンの法則です。

Lemma De_Morgan:
  forall A B: Prop, ~(A \/ B) -> (~A /\ ~B).
Proof.

「(AまたはB)ではない、ならば、(Aではない、かつ、Bではない）」です。∨ が「または」で、∧ が「かつ」で、「~」が否定の「ではない」です。∨と∧はバックスラッシュを使って書くので、フォント環境によっては円記号に見えてしまっているかも。その場合はすみません、心眼で￥を＼と読んで下さい。

そういえば前回は Theorem Modus_ponens と "Theorem" (定理) で書き始めましたが、今回は "Lemma" (補題) です。Coq 的には違いは何もありません。趣味の問題です。"Proposition" (命題) や "Corollary" (系)、"Fact"、"Remark" など色々ありますが趣味で使い分けて下さい。

notの扱い

さて、まず、否定の ~A は、「A -> False」の省略形です。リファレンスから引用します。Coq.Init.Logic.not:

Definition not (A:Prop) := A -> False.
Notation "~ x" := (not x) : type_scope.

「Aではない」とはすなわち、「Aならば偽」「Aだと仮定すると矛盾が生じる」である。これがCoqでの、そしてCoqがベースにしている論理体系での「~」の定義であります。False の定義はあとで解説しますが、とりあえず単にそういう名前の命題と思っておいて下さい。

「ならば」の扱いなら前回やって慣れてますので、安心ですね。「"not" なんて見慣れない単語を使わないで、全部 "->" の言葉でしゃべってください」と Coq さんに伝えましょう。

  unfold not.

"unfold" tactic を使います。単に、Definition ... := で定義された定義をインライン展開するだけのtacticです。

ついでに intros. しておきました。

andの扱い

示さないといけないゴールの形が、(A→False)∧(B→False) になりました。この ∧ とは何者かというと… Coq.Init.Logic.and:

Inductive and (A B:Prop) : Prop :=
  conj : A -> B -> A /\ B

where "A /\ B" := (and A B) : type_scope.

こんな物体です。なにやら複雑ですが、とりあえず最後の１行は「"A∧B" という中置演算みたいな記法は、(and A B) の略記です」と言ってるだけです。本体は上２行。"Inductive" 宣言を使って、二つのことを宣言しています。

• "A∧B" という新種の命題をこれから使います！
• この "A∧B" の「公理」は A -> B -> A∧B です！

"A∧B"が成り立つのは、Aが成り立って、しかもBが成り立っているとき、その時に限ります。つまり "Aならば(Bならば(A∧B))" が無条件で成立する…そういう∧という命題を使って色々書いたり証明したりするんでよろしくお願いします、とCoqさんに伝えるのがInductive宣言です。

さてさて、定義の話はいいから、証明のやり方はどうするのでしょうか。

実は、もう我々は証明のしかたを知っています。

• ゴールは hoge ∧ fuga という形です
• conj : hoge -> fuga -> hoge ∧ fuga という公理があります

公理はいつでも無条件に使えるので、仮定と同じように、apply することができて…

 apply conj.

"(A->False) ∧ (B->False)" を示すためには、A->False を示して、B->False を示せば、後は conj を使えば証明できます。そういう感じで証明しますんでよろしく、とCoqさんに伝えると

二つのゴールができました。

orの扱い

続いて、一つ目のゴールは "A->False" です。ゴールが "->" の形なので、何も考えず

  intros.

するとゴールが "False" になりますが、仮定を眺めると False を作れるのは "H: A∨B->False" しかないので、これをapplyしておきます。

 apply H.

ゴールは "A∨B" になりました。さてどうしましょう。定義を見ると Coq.Init.Logic.or:

Inductive or (A B:Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B

where "A \/ B" := (or A B) : type_scope.

今度は、公理が２つあります。

• or_introl: "A"が成り立つなら、"AまたはB"が成り立つ
• or_intror: "B"が成り立つなら、"AまたはB"が成り立つ

まあor(または)の意味として納得の行く定義です。

というわけで、ゴールを証明するには "apply or_introl." か "apply or_intror." を使えばよいのですが…どっちが正解でしょうか？

• ゴール A∨B に、or_introl: A->(A∨B) を apply すると、新ゴールは A になります
• ゴール A∨B に、or_intror: B->(A∨B) を apply すると、新ゴールは B になります

どっちなら続きを証明できるかというと、今回は仮定に "H0: A" があるので、新ゴール A なら"exact H0."で証明完了です。というわけで、or_introl の方を使います。

  apply or_introl.
  exact H0.

こういう風に、or のような分岐があると「どっちに行ったら証明できるか」をよく考えて選んでやる必要があります。証明の完全な機械化は難しくて、Coqのように人間が考えて証明記述してやるシステムが必要な理由の一端は、ここにあります。頑張って人類の発想力を発揮しましょう。

apply conj でできたもう一つのゴール "B->False" も、同じように証明できます。こっちは or_intror の方を使います。

  intros.
  apply H.
  apply or_intror.
  exact H0.
Qed.

証明完了！

Coqの入門記事を書く会 (2)

第２回です。前回は「forall」と「->」の扱い方でした。今回は、「ならば (->)」以外の定番の論理演算、「and」「or」「not」のお話です。

実は、Coq の本当に言語組み込みの命題構成子は forall と -> だけで、「and」「or」「not」は、Coq使いなら自分で同じ機能のものを簡単に作れてしまう「ユーザー定義命題」です（もちろん、共通のものがないと不便なので標準ライブラリで真っ先に定義されてますけど）。逆に言うと、もっと本格的なCoqコードで出てくる複雑そうな命題も、全部、「and」「or」「not」と同じユーザー定義型の仕組みで定義されてますので、「and」「or」「not」の扱いさえマスターすれば、他のどんなユーザー定義の命題の証明も同じ道具で書けちゃいますよ。

[Coq] forall と -> : まとめ (1.6)

というわけで、Coq入門編その一、forall と -> だけ使った定理の証明、をお届けしました。気が向いたら「and, or, not を使った定理の証明」「exists を使った定理の証明」「帰納法」「forallと->と依存型について本気出して考えてみた」… の順番で続きます。入門記事を書くのはいいけれど、面白い練習問題が提供できないとつまらないよなーむずかしいなー、と思って長年躊躇していたのですが、最近

• Anarchy Proof

という読者投稿型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に変える

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は、適用される側を消して新しい結果で上書きします。これも、消される仮定が後で要るか要らないかよく考えてから使いましょう。

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.3)

ところで、HaskellやOCamlなどの関数型言語をご存じの方なら100倍高速にCoqを理解できる！というショートカットのご紹介です。以下、この節限定で、説明にHaskellが混じります。Haskellわからんという人はこの節は飛ばしても以降に差し支えはない…はず…たぶん…。

さて、カリー･ハワード同型対応。

• Curry-Howard Isomorphism

をご存じでしょうか。ご存じない方は今すぐググる、上記の記事を読むなどして存じて下さい。論理の「定理」とは要するにプログラミング言語でいう「型」のことであり、「証明」とはその型の「値」のことである、そう見なして完全に整合性がとれる、というお話です。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 コマンドを使うと、どういう関数として定義されたかを見ることができます（右下）。