Coqに入門した感想
最近、定理証明支援のCoqを入門している。というのは、以前の職場にいたときの職場でもCoqをやっている先輩がいて、今回の職場でも定理証明支援系を使っている同僚がいて、しかも最近自分はプログラミング言語実装をやっているためか、Coqや依存型について聞かれることがあるので、一念発起して取り組み始めた。
しかし、案の定、何から始めたらいいのかわからず入門に躓いてしまい、かなり難しいと感じた。しかも一番最初に読み始めた本が、Certified Programming with Dependent Typeという初心者向けではない本だったため、事態は混迷を極めていた。
そんな難関を乗り越えて2ヶ月、ようやく基本的な証明をできるまでたどり着いたので、メモ代わりにどう入門すればよいか残しておこうと思う。
1. 関数型のプログラミング言語を学ぶ
自分は関数型プログラミング言語の処理系を設計・実装したことがあり、型システム、型推論、λ計算についてはある程度知っていたため、Coqで用いる型や式については初見でもなんとなくわかったが、関数型言語について知らない人は厳しいのでまずOCamlかHaskellをやったほうが良いと思う。
例えば、CoqではFixpointという宣言で再帰関数を定義するのだが、これはαコンビネータなどの不動点コンビネータについて知識があると納得するはずである。しかし、これらをしらないと、何なのかさっぱりわからなくなるのではと思う。
2. 形式的証明について学ぶ
この形式的証明も自分はある程度やったことがあるためそれほど困らなかったのだが、そもそも形式的証明について知らない場合、なんのこっちゃわからないと思う。形式的証明については、以下の本がおすすめだと思う。
あたりまえだが、Coqは証明していくためにあるので、そもそも証明とは何かをわかっていないとやっていくのはきつい。
3. Emacsを学ぶ（おまけ）
これはおまけだが、CoqはEmacs上でProof Generalというソフトウェアを動かして使うのが使いやすいように思った。自分はターミナルの中でEmacsを起動して使っている。Coq IDEもあるが、Emacsでバシバシ書けるのは快適なので、Emacsを使ったほうが良いと思う。
4. 適切な入門書を選ぶ
自分が躓いたのはここだった。
入門で利用すべきは、Software FoundationsのVolume 1だったのだ。これは大変わかりやすく、これを読めばだいたい分かるので、まずこれを読んだほうが良い。日本語だと、ソフトウェアの基礎に少し古いバージョンのがあるので、こちらを読めば良いと思う。このどちらかで一通り証明を体験した後、Certified Programming with Dependent Typeを読めば、かなり納得して読めるようになる。間違っても、いきなりこれを読んではいけない。
最近はSSReflect/Mathcompを使うこともあるそうだが、おそらく入門はSoftware Foundationsの方がCoqの基礎がわかって良いと思った。Coqを解説した日本語記事もWebには散見されるが、だいたいわかりにくいので、ソフトウェアの基礎あたりを読んで、演習問題を解いていくのがいいのではないかと思う。
証明の仕方はわかりつつあるので、今後は実際のRunning Codeに活かしていきたい。いまはRust言語でOSを実装しているので、それに対して証明を与えられないかと思っている。それでは皆さん、良いハッキングライフを。
