先週の土日にこのオンラインセミナーに参加してみた。

• 定理証明支援系 Coq チュートリアル - connpass

定理証明は、名前は聞くけど触ったことはなくて、興味はあるけど本を買うほどのモチベーションはないし、誰か詳しい人が要点だけ教えてくれたりしないかな〜。と思っていたところ、まさにぴったりのイベントが。なんていうか、昔ならこういうのは東京まで行かないと参加できなかった気がするけど、家からオンラインで参加できるようになったのは嬉しいね。

日程は5時間 x 2日という長丁場で、説明だけでなく練習問題もあるのでとっても疲れた！でもこういうのって自分で手を動かさないと「わかったような気になった」だけで終わりがちだから、演習があるのはとてもありがたい。

Coqの感想

これまでいろんなプログラミング言語を触ってきたけど、証明とプログラムが一体になった環境は新鮮で面白かった。「整数」「文字列」みたいな普通の型以外に、「命題」や「証明」を表すデータがあるんだよね。例えば

P, Q : Prop

とあればPとQは命題(proposition)。P, Qは値であると同時に型でもあるのでそれらのインスタンスもあって、例えば

HP : P
HQ : Q

とあればHPは「命題Pが成り立つという証明」、HQは「命題Qが成り立つ証明」を表す。つまり命題Pを証明するとは、Pのインスタンスを何か一つ見つけるということ。

で、Coqで出てくる「P -> Q」は論理の世界から見ると「PならばQ」だけど、プログラムの世界から見ると「Pのインスタンスを受け取ってQのインスタンスを返す関数、という型」で、それは言い換えると「Pが成り立つ(Pの証明が存在する)ときにそこからQの証明をつくる関数」とも言える。いやあ、かっこいいよね。

知らなかったこと

新たに知ったことが2つあって、ひとつめはCoqからプログラムを生成できるということ。プログラムと証明が一体となったものから、証明部分を除いたものをOCamlやHaskellのコードとして書き出せるらしい。

もう一つはCoqIDEという開発環境があること。これを使うと、証明の1ステップごとにどんな式変形が起きて、あと何が残っているのかをわかりやすく表示してくれる。実際の.vファイル(例)を見ても大枠くらいしか何をやってるのかわからないけど、それはそういうもので、細かいところはこういったツールで見るということだね。