定理証明系、はじめました

とりあえずCoqをインストールしていくつか証明を書いたのでそのメモ。
分かりやすい参考文献集


まずはCoqのインストール。Winならhttp://coq.inria.fr/downloadからダウンロード、Debian系OSならaptでcoqideをインストールする。

CoqIdeを起動すると、左側にファイルの編集画面、右側に実行結果などが表示される。まずはファイルに何か関数定義でも打ち込む。


画面上のボタン類から下向きの矢印を押すと、一行ずつ実行される。ショートカットはCtrl+Alt+Down(のはずが何故か効かない)

カリー＝ハワード同型対応より、命題は型として、証明はプログラムとして扱えるらしいけれども詳しい事はよく分かってない。
ここで簡単な証明、任意の命題A, Bに対し、A -> (A -> B) ->B を証明してみる。つまりこれを満たす関数を書く。



forall A B : Prop, A -> (A -> B) -> Bとなるような関数を書けば良い。PropはA, Bの型。今回は無名関数の定義である fun を使う。
forallのA, Bも引数として取らなければいけないので、最初の引数は A B 、次にA型の値x、A -> B型の関数fを取って、fにxを適用すればBが帰ってくる。
関数が正しく定義出来ると、prop1 is definedのように表示される。

次にド・モルガンの定理の証明をしてみる。
先ほどのように簡単な証明だと関数を書けば終わるけれども、複雑な定理とかになってくるとそうもいかない。まずは証明する命題を示し、次にその命題をCoqに用意された様々なタクティクを利用して証明していく。タクティクについてはよく分かってないので上の参考文献集とかを適当に読んで下さい。おすすめはCoqの入門記事を書く会の記事。
まずは定理を示す。LemmmaとかTheoremとかを適当に選んで名前を付けたり、あるいは名前を付けずにGoalと書いてから命題をいきなり書くことも出来る。
次にapplyとかexactとかconstructorとか色々タクティクを使い倒して、目的の証明まで持っていく。
intros.はA->Bがゴールである時に、Aを前提にしてBをサブゴールにするタクティク。
applyは使える前提にA -> Bがあって、証明すべきゴールがBの時に、ゴールをAに変えるタクティク。
ド・モルガンの定理、forall P Q: Prop, ~(P\/Q) -> (~P/\~Q)の証明は次の通り。

Coqの証明を見つけたら、とりあえずIDEで実行してみると、大体の流れがつかめると思う。
ここで、Coqは排中律を認めないので、forall P Q:Prop, ~(P /\ Q) -> (~P \/ ~Q)とかは排中律を公理として追加しないといけないことにも注意が必要。


他にもCoq-99 : Part 1の証明を書いたりした。