The Coq Proof Assistant A Tutorial (3) Minimal Logic
今回は，最も基本的な組み込みの最小論理 (Minimal Logic) 推論エンジンの，ほんのさわりだけを見ていきます．
使用するのは，いわゆる三段論法ってやつです (厳密にいうと，この用語はけっこう曖昧なので，あんまり使わないほうが良いのですが…)．A と A → B が成り立つならば，B が成り立つという，アレです．うむ，常識ですな (笑)
# でも，型理論の論文とかで，
とか書いていると，べつにどおってことないことなのに，何だかびびってしまいませんか ? (笑)
まぁ，あたりまえのことを，あたりまえにやっていくのが，論理学ですからね．そして気がつくと，当たり前のことをずっとやってきたはずなのに，とんでもない結論が出てくると w これが論理学の醍醐味です．基本は大事なんですよ．
というわけで，まずは Coq を立ち上げ，セクションを切り替えておきましょう．
そしてとりあえず，命題変数をいくつかグローバルに宣言しておきましょう．
まず始めに，自明なトートロジーではありますが，(A → B → C) → (A → B) → A → C を証明してみましょう．
ここで注意しなければならないのは，-> の意味がオーバーライドされている点です．前回 -> 演算子は，関数構築子でしたが，ここでは論理的な包含関係 (A → B は，A は B は含む (A ⊇ B)，すなわち A ならば B と読みます) をあらわしています．
証明したい論理式 (ゴール) を入力する際には，Goal コマンドを使用します．
コマンドを入力すると，流法(モード)が切り替わり，ゴールの内部ループに入ります．今回は，定理に名前を付けて無いので，Unnamed_them と表示されています．
最初は何もありませんが，証明を行っていくうちに，仮定が増えていきます．二重線の上に，現在のゴール内の局所環境における仮定 (これを judgement と呼ぶそうです) が表示されます．
※ 訂正 : さかいさんからのコメントによると，judgement とは，「ローカルな仮定とゴールの組み合わせ」のことで，「〜の仮定の元，ゴールの〜が成り立つ」という主張(assertion)を表現したもの，なのだそうです．コメントありがとうございました !
証明モードでは，タクティクス (tactics) と呼ばれる，様々な証明戦略を使用することができます．「証明」というと，何やら堅苦しいですが，仮定に対して様々なタクティクスを用いながらゴールを目指す，知的なゲームと考えると，抵抗感がやわらぎ，面白く感じられるようになるのではないかと思います．
たとえば，二重線の下に表示されている，現在のゴール内に，包含関係 ※ が含まれている時は，いつでも intro というタクティクスを使用することができます．
※ P → Q ; ただし，これはメタな表現なので，必ずしも一対一に対応する形でなくとも OK です．
intro を使用すると，包含の左側 (P → Q ならば，P) を，ジャッジメント(ローカルな仮定リスト) (ゴールと仮定の組み合わせ) に加えて，新たな仮定とすることができます．
intro ができるゴールの部分は一意に定まるので，intros を使用すると，まとめて一気に intro を行うことができます．
もうこれ以上は intro ができません．
そこで，kowalski 流に，証明を手続きと解釈してみましょう．
逆に考えるんだ，C を成り立たせるためにはどうすれば良いか ? と考えるんだ．
C を成り立たせるためには，H が成り立てば良いですよね．
今回は一つしかないので，迷う必要はありませんでしたが，一般的には複数の仮定や定義があり，どれを選べば証明が上手くできるのかを見極めるのは難しいです．
そこで，とりあえず一つルールを選んで，上手く行けばベネ (良し) ! 上手く行かないことがわかった，あるいはもっと他の可能性が無いかを調べたい場合には，一つ証明経路を逆戻る (バックトラックする) という方針が考えられます．
これが，kowalski が提唱した，証明を計算と見なすプログラミングパラダイム 「論理プログラミング (Logic Programming)」の基本アイデアです．
代表的な言語である Prolog では，上から公理や定理を眺めて行き，一番最初に見つかった，適用可能な規則を取りあえず用いるという，SLD 導出というアルゴリズムが処理系に組み込まれています．
これは色々と問題もあるのですが，仕様を (無理があるとはいえ) プログラムとして直接動かす，という，当時としては非常に先進的な概念を確立したという点で極めて重要です．
人間は，目で見て，ゴールにルールが適用可能かどうかを区別することができますが， このような構文の比較作業を効率的に行うことができるのが，Robinson が見いだした「単一化」 と呼ばれるアルゴリズムです．これは，パターンマッチングが一般化されたもので，プログラムが双方向性を持つようになると言う，けっこう凄いものです．そのおかげで，論理プログラムは，(私にとっては) 最も読みやすいです．
ただし Prolog は，一般的に，極めてわかりにくい言語でもあります．論理畑の人達は，プログラムの可読性が極めて高いから，とか，双方向性を持つからだ，とか言いますが，私はやはり，本質的に無理があるパラダイムだからだと思います．
この日記を読んでいる人の大部分は，関数畑の方だと思うので，関数型言語に例えるならば，「建前上は，副作用を考えなくても良い」というパラダイムのはずなのに，現実的には，モナドなどがからんでくるので，実際の評価順を考慮したりと，いろいろ頭を悩ませないといけない，というようなことと，同じようなものです．
Prolog も，建前上は，「What is だけを考えて節を書いて行けば良い」はずなんですが，現実的には，SLD 導出，すなわち，バックトラッキングのメカニズムを理解し，頭の中で逆算しながら，節の定義順やアトムの順番を考慮しつつ，プログラミングを行って行く，という離れ業をこなさなければ，まともに動くプログラムを書くことはできません．
しかも，いわば SQL で汎用プログラミングを行っているような言語なので，バックトラッキングを抑制，あるいはコントロールするために，カットオペレータというものを大量に，処理系の挙動を理解しつつ埋めこんでいかなければなりません．
とはいえ，私が思いつく，メジャーなプログラミング言語の中では，一番馴染み深いですし，他人の書いたプログラムを読みやすい言語なので，(実際には使いませんが) 好きな言語ではあります (最近は，ET しか使ってません)．
… っと，思いっきり脱線してしまいました．
ようするに，逆向きに推論を進めていくよ，という話でした．
そこで，C に対して，H を適用します．ここらへんは，始めての方にはけっこうわかりにくいのではないかと思ったので，多少くどく説明してしまいました (そんなことないですか ? 常識 ?)．
こんどは，A -> B を成り立たせる必要があります．そして，A -> B 全体を成り立たせる (真になる) ためには，A を成り立たせる必要があります．ここで，仮定を眺めて見ると… A あるじゃん ! (大げさ)
どう見ても HA は真です．
ほんとうにありがとうございました．
A が成り立ったので，H' をすかさず適用 !
めでたく，仮定から，矛盾することなく，ゴールを証明することができました．
せっかく証明したので，補助定理として保存しておきましょう．もしかしたら，なんかに使えるかもしれません．定理の保存には，Save コマンドを使います．
これで，一応一通りの手順は終りました．
ここからは，ちょっと練習として，いろいろな Coq の機能を使ってみましょう．
まず，証明したい仮説に名前をつけて，証明を始めることができます．
また，さっきは一つずつ intro を行いましたが，実は intros を引数無しで実行すると，できるところまで自動的に intro してくれます．
また，
T1 ; T2
と入力すると，T1 を現在のゴールに対して適用し，それによって生じた全てのサブゴールに対して T2 を適用することができます．
あるいは，
T ; [T1 | T2 | T3 | ...... | Tn]
のように入力すれば，現在のゴールに対して T を適用し，それによって一番最初に生じたサブゴールに対してのみ T1 を，二番目にのみ T2 を… n 番目にのみ Tn を適用することができます．
これによってタクティクスを組み合わせることにより，一発で証明を終らせることもできます．
今回は，最初から名前が付いているので，Save コマンドだけで保存ができます．
いままでは，練習のために，いちいち細かく指示を出して来たので，もう面倒で面倒で，こんなんなら紙とペンで書いた方が良いよ ！ とうんざりしてきた方も多いのでないでしょうか ?
しかし，実は，intro と apply と assumption をいくつか組み合わせた程度の，簡単な証明ならば，全て自動的に Coq が証明してくれます．Auto コマンドを使えば，何の指示も出す必要はありません．
一発で証明が終りました．う〜ん，賢いぞ Coq．
証明の内部ループから，通常の Coq トップレベルループに戻るためには，Abort コマンドを使用します．これは，いつでも使用することができます．
ちなみに，一つ戻る (バックトラック)，あるいは n ステップ戻るためには，Undo n コマンドを使用します．もうゴチャゴチャしてきて，面倒くさくなったら，Restart で，もう一度最初から定理証明を始めることもできます．
最後から数えて，n 個目までの宣言を表示するには，Inspect n コマンドを使用します．グローバルな定義は，先頭に *** とマークが付きます．
ふう… またまた途中で脱線しまくりで，疲れました．
次回からは，ようやく，ようやく，もう少し本格的な命題論理に入れます… こんなペースで，果して依存型にまでたどり着けるのでしょうか ? だんだん不安になってきました (え，依存型までいこうとしてたの !? w)．
# どっかのｽｰﾊﾟﾊｶｰが，「30 日でわかる定理証明器でのコンパイラの書き方」とか書いてくれないかな (そればっか w)
あぁ，それにしても眠い．文章がかなり適当です…
安西先生… Coq で，Coq を書きたいです… (寝言)
使用するのは，いわゆる三段論法ってやつです (厳密にいうと，この用語はけっこう曖昧なので，あんまり使わないほうが良いのですが…)．A と A → B が成り立つならば，B が成り立つという，アレです．うむ，常識ですな (笑)
# でも，型理論の論文とかで，
A A → B
--------
B
とか書いていると，べつにどおってことないことなのに，何だかびびってしまいませんか ? (笑)
まぁ，あたりまえのことを，あたりまえにやっていくのが，論理学ですからね．そして気がつくと，当たり前のことをずっとやってきたはずなのに，とんでもない結論が出てくると w これが論理学の醍醐味です．基本は大事なんですよ．
というわけで，まずは Coq を立ち上げ，セクションを切り替えておきましょう．
Welcome to Coq 8.0pl3 (Jan 2006)
Coq < Section Minimal_Logic.
そしてとりあえず，命題変数をいくつかグローバルに宣言しておきましょう．
Coq < Variables A B C : Prop.
A is assumed
B is assumed
C is assumed
まず始めに，自明なトートロジーではありますが，(A → B → C) → (A → B) → A → C を証明してみましょう．
ここで注意しなければならないのは，-> の意味がオーバーライドされている点です．前回 -> 演算子は，関数構築子でしたが，ここでは論理的な包含関係 (A → B は，A は B は含む (A ⊇ B)，すなわち A ならば B と読みます) をあらわしています．
証明したい論理式 (ゴール) を入力する際には，Goal コマンドを使用します．
Coq < Goal (A -> B -> C) -> (A -> B) -> A -> C.
1 subgoal
A : Prop
B : Prop
C : Prop
============================
(A -> B -> C) -> (A -> B) -> A -> C
Unnamed_thm <
コマンドを入力すると，流法(モード)が切り替わり，ゴールの内部ループに入ります．今回は，定理に名前を付けて無いので，Unnamed_them と表示されています．
最初は何もありませんが，証明を行っていくうちに，仮定が増えていきます．二重線の上に，
※ 訂正 : さかいさんからのコメントによると，judgement とは，「ローカルな仮定とゴールの組み合わせ」のことで，「〜の仮定の元，ゴールの〜が成り立つ」という主張(assertion)を表現したもの，なのだそうです．コメントありがとうございました !
証明モードでは，タクティクス (tactics) と呼ばれる，様々な証明戦略を使用することができます．「証明」というと，何やら堅苦しいですが，仮定に対して様々なタクティクスを用いながらゴールを目指す，知的なゲームと考えると，抵抗感がやわらぎ，面白く感じられるようになるのではないかと思います．
たとえば，二重線の下に表示されている，現在のゴール内に，包含関係 ※ が含まれている時は，いつでも intro というタクティクスを使用することができます．
※ P → Q ; ただし，これはメタな表現なので，必ずしも一対一に対応する形でなくとも OK です．
Unnamed_thm < intro H.
1 subgoal
A : Prop
B : Prop
C : Prop
H : A -> B -> C
============================
(A -> B) -> A -> C
intro を使用すると，包含の左側 (P → Q ならば，P) を，ジャッジメント
intro ができるゴールの部分は一意に定まるので，intros を使用すると，まとめて一気に intro を行うことができます．
Unnamed_thm < intros H' HA.
1 subgoal
A : Prop
B : Prop
C : Prop
H : A -> B -> C
H' : A -> B
HA : A
============================
C
もうこれ以上は intro ができません．
そこで，kowalski 流に，証明を手続きと解釈してみましょう．
逆に考えるんだ，C を成り立たせるためにはどうすれば良いか ? と考えるんだ．
C を成り立たせるためには，H が成り立てば良いですよね．
今回は一つしかないので，迷う必要はありませんでしたが，一般的には複数の仮定や定義があり，どれを選べば証明が上手くできるのかを見極めるのは難しいです．
そこで，とりあえず一つルールを選んで，上手く行けばベネ (良し) ! 上手く行かないことがわかった，あるいはもっと他の可能性が無いかを調べたい場合には，一つ証明経路を逆戻る (バックトラックする) という方針が考えられます．
これが，kowalski が提唱した，証明を計算と見なすプログラミングパラダイム 「論理プログラミング (Logic Programming)」の基本アイデアです．
代表的な言語である Prolog では，上から公理や定理を眺めて行き，一番最初に見つかった，適用可能な規則を取りあえず用いるという，SLD 導出というアルゴリズムが処理系に組み込まれています．
これは色々と問題もあるのですが，仕様を (無理があるとはいえ) プログラムとして直接動かす，という，当時としては非常に先進的な概念を確立したという点で極めて重要です．
人間は，目で見て，ゴールにルールが適用可能かどうかを区別することができますが， このような構文の比較作業を効率的に行うことができるのが，Robinson が見いだした「単一化」 と呼ばれるアルゴリズムです．これは，パターンマッチングが一般化されたもので，プログラムが双方向性を持つようになると言う，けっこう凄いものです．そのおかげで，論理プログラムは，(私にとっては) 最も読みやすいです．
ただし Prolog は，一般的に，極めてわかりにくい言語でもあります．論理畑の人達は，プログラムの可読性が極めて高いから，とか，双方向性を持つからだ，とか言いますが，私はやはり，本質的に無理があるパラダイムだからだと思います．
この日記を読んでいる人の大部分は，関数畑の方だと思うので，関数型言語に例えるならば，「建前上は，副作用を考えなくても良い」というパラダイムのはずなのに，現実的には，モナドなどがからんでくるので，実際の評価順を考慮したりと，いろいろ頭を悩ませないといけない，というようなことと，同じようなものです．
Prolog も，建前上は，「What is だけを考えて節を書いて行けば良い」はずなんですが，現実的には，SLD 導出，すなわち，バックトラッキングのメカニズムを理解し，頭の中で逆算しながら，節の定義順やアトムの順番を考慮しつつ，プログラミングを行って行く，という離れ業をこなさなければ，まともに動くプログラムを書くことはできません．
しかも，いわば SQL で汎用プログラミングを行っているような言語なので，バックトラッキングを抑制，あるいはコントロールするために，カットオペレータというものを大量に，処理系の挙動を理解しつつ埋めこんでいかなければなりません．
とはいえ，私が思いつく，メジャーなプログラミング言語の中では，一番馴染み深いですし，他人の書いたプログラムを読みやすい言語なので，(実際には使いませんが) 好きな言語ではあります (最近は，ET しか使ってません)．
… っと，思いっきり脱線してしまいました．
ようするに，逆向きに推論を進めていくよ，という話でした．
そこで，C に対して，H を適用します．ここらへんは，始めての方にはけっこうわかりにくいのではないかと思ったので，多少くどく説明してしまいました (そんなことないですか ? 常識 ?)．
Unnamed_thm < apply H.
2 subgoals
A : Prop
B : Prop
C : Prop
H : A -> B -> C
H' : A -> B
HA : A
============================
A
subgoal 2 is:
B
こんどは，A -> B を成り立たせる必要があります．そして，A -> B 全体を成り立たせる (真になる) ためには，A を成り立たせる必要があります．ここで，仮定を眺めて見ると… A あるじゃん ! (大げさ)
どう見ても HA は真です．
Unnamed_thm < exact HA.
1 subgoal
A : Prop
B : Prop
C : Prop
H : A -> B -> C
H' : A -> B
HA : A
============================
B
ほんとうにありがとうございました．
A が成り立ったので，H' をすかさず適用 !
Unnamed_thm < apply H'.
1 subgoal
A : Prop
B : Prop
C : Prop
H : A -> B -> C
H' : A -> B
HA : A
============================
A
めでたく，仮定から，矛盾することなく，ゴールを証明することができました．
Unnamed_thm < assumption.
Proof completed.
せっかく証明したので，補助定理として保存しておきましょう．もしかしたら，なんかに使えるかもしれません．定理の保存には，Save コマンドを使います．
Unnamed_thm < Save trivial_lemma.
intro H.
intros H' HA.
apply H.
exact HA.
apply H'.
assumption.
trivial_lemma is defined
これで，一応一通りの手順は終りました．
ここからは，ちょっと練習として，いろいろな Coq の機能を使ってみましょう．
まず，証明したい仮説に名前をつけて，証明を始めることができます．
Coq < Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.
1 subgoal
A : Prop
B : Prop
C : Prop
============================
(A -> B -> C) -> (A -> B) -> A -> C
また，さっきは一つずつ intro を行いましたが，実は intros を引数無しで実行すると，できるところまで自動的に intro してくれます．
distr_impl < intros.
1 subgoal
A : Prop
B : Prop
C : Prop
H : A -> B -> C
H0 : A -> B
H1 : A
============================
C
また，
T1 ; T2
と入力すると，T1 を現在のゴールに対して適用し，それによって生じた全てのサブゴールに対して T2 を適用することができます．
あるいは，
T ; [T1 | T2 | T3 | ...... | Tn]
のように入力すれば，現在のゴールに対して T を適用し，それによって一番最初に生じたサブゴールに対してのみ T1 を，二番目にのみ T2 を… n 番目にのみ Tn を適用することができます．
これによってタクティクスを組み合わせることにより，一発で証明を終らせることもできます．
distr_impl < apply H; [assumption | apply H0; assumption ].
Proof completed.
今回は，最初から名前が付いているので，Save コマンドだけで保存ができます．
distr_impl < Save.
intros.
apply H; [ assumption | apply H0; assumption ].
distr_impl is defined
いままでは，練習のために，いちいち細かく指示を出して来たので，もう面倒で面倒で，こんなんなら紙とペンで書いた方が良いよ ！ とうんざりしてきた方も多いのでないでしょうか ?
しかし，実は，intro と apply と assumption をいくつか組み合わせた程度の，簡単な証明ならば，全て自動的に Coq が証明してくれます．Auto コマンドを使えば，何の指示も出す必要はありません．
Coq < Lemma distr_imp : (A -> B -> C) -> (A -> B) -> A -> C.
1 subgoal
A : Prop
B : Prop
C : Prop
============================
(A -> B -> C) -> (A -> B) -> A -> C
distr_imp < auto.
Proof completed.
一発で証明が終りました．う〜ん，賢いぞ Coq．
証明の内部ループから，通常の Coq トップレベルループに戻るためには，Abort コマンドを使用します．これは，いつでも使用することができます．
distr_imp < Abort.
Current goal aborted
ちなみに，一つ戻る (バックトラック)，あるいは n ステップ戻るためには，Undo n コマンドを使用します．もうゴチャゴチャしてきて，面倒くさくなったら，Restart で，もう一度最初から定理証明を始めることもできます．
最後から数えて，n 個目までの宣言を表示するには，Inspect n コマンドを使用します．グローバルな定義は，先頭に *** とマークが付きます．
Coq < Inspect 3.
*** [C : Prop]
trivial_lemma : (A -> B -> C) -> (A -> B) -> A -> C
distr_impl : (A -> B -> C) -> (A -> B) -> A -> C
ふう… またまた途中で脱線しまくりで，疲れました．
次回からは，ようやく，ようやく，もう少し本格的な命題論理に入れます… こんなペースで，果して依存型にまでたどり着けるのでしょうか ? だんだん不安になってきました (え，依存型までいこうとしてたの !? w)．
# どっかのｽｰﾊﾟﾊｶｰが，「30 日でわかる定理証明器でのコンパイラの書き方」とか書いてくれないかな (そればっか w)
あぁ，それにしても眠い．文章がかなり適当です…
安西先生… Coq で，Coq を書きたいです… (寝言)
