Idrisで定理証明をやっていく

定理証明

プログラムで数学的な正しさを証明できる、定理証明システムというものがあります。

学生の頃、定理証明システムの講義があってそれがとても楽しかったです。
素数の無限性の証明だけできなかったのだけ心残りでした。

それ以来、10年以上経っても心のどこかでずっと定理証明システムをやりたかったのですが、Idrisという魅力的なものを見つけたので、ついにやっていくことにしました。

なぜ Coq ではないのか

定理証明システムには色々あって、いちばん有名なのはCoqだと思いますが、個人的には以下の理由で、Coqをやる気は起きませんでした。

• 独自のGUIツールを使う必要がありそうなので、自分が好きなエディタ（Vim）でできない
• いろんな言語やシステムの組み合わせでできていて複雑そう

Idris

調べていると、Idrisという定理証明ができるプログラミング言語があり、

• ベースがHaskellなので入りやすい（ついでにHaskellの勉強にもなる）
• 証明支援機能もあるが必ずしもそれを使わなくてよい
• エディタでテキストファイルのプログラムを書けば、証明ができる　→　Vimでできる！
• 証明付きプログラムも書ける

というところに魅力を感じました。

やっていく

定理証明システムや関数型言語の界隈では、賢そうな人たちがむつかしそうなことをやっている印象がありますが、そういうことはあまり気にしないようにしたいです。
（単に私が知らないというのもあります）

プログラムで定理を証明していきたい。
証明がついた安全なプログラムの書き方を学びたい。

という気持ちを大事にして、やっていきたいと思います。

方針

• REPL（対話型インターフェース）や証明補助機能は使わない
• つまり、Vim とIdrisコンパイラだけでやっていく
• あらかじめ用意されたライブラリ（Prelude）はできるだけ使わずに理解を積み上げていく
• 識別子名に日本語はバンバン使う
  　交換則って英語でなんて言うんだっけ？ってググって無理に英語名つけても、読みづらいし本質的じゃないところでモヤモヤします。
• 関数型言語の難しい機能（モナドなどなど）は、必要がなければ触れない
• とにかくやっていきたい