Idrisで定理証明をやっていく - p ならば p の証明
Idris 処理系のインストール
バージョン2もあるらしいですが、ウェブ上の情報が多い1.3系でやっていきます。
Ubuntu 20.04 の環境で
apt install ghc
cabal install idris
とかでインストールできた記憶（超適当
親切で詳しい方の記事をご参考にしてください。
(インストール方法に限らず、まじめにIdrisを学びたい方はまずkeenさんの本を読まれた方がいいと思います。)
証明が終わった決め台詞を表示するだけのプログラム
テキストエディタで.idrの拡張子でファイルを作ります。
（Vim ではソースコードカラーリングのために設定がひと手間必要でした）
%default total -- 関数定義（証明）に漏れがないかチェックする設定
main : IO () -- Haskell とは違い、型宣言は : を使い、また、型宣言を省略できません
main = do
putStr "Q.E.D."
せっかくなので、人生でほぼ使う機会がない 「Q.E.D.」（証明終）を表示します。
Idrisでは型が命題で、関数定義が証明で、警告なくコンパイル出来たらすべての証明ができたことを意味するので、プログラムの実行自体はしなくてもコンパイルすれば定理証明ができます。
実行
Vim の QuickRun プラグインを使っているためビルド方法を忘れました汗
コンパイルしてできたバイナリファイルを実行すればいいだけです。
p ならば p の証明
ある命題 p があって、p が真なら当然 p は真です。（繰り返しているだけ）
論理式で書くと「p ならば p」(p => p)です。
この当たり前のことをIdrisで証明します。
型が命題で、型から型への写像である関数を定義できれば、命題から命題への推論ができたことになります。（何を言っているのか）
p という任意の型から、同じ p という型への写像である関数は、以下のように定義できます。
%default total -- 関数定義（証明）に漏れがないかチェックする設定
myFirstProof : p -> p
myFirstProof hp = hp -- 命題 p の仮説には Hypothesis の h をつける慣習があるらしい
main : IO ()
main = do
putStr "Q.E.D."
上記プログラムをコンパイルすると、何も怒られないので、 p -> p 、つまり p ならば p の証明ができました。（Q.E.D.）
ならば(=>)の推移律もやってみる
p => p というのは証明しても意味があまり感じられないので、ならばの推移律もやってみましょう。
p=>q かつ q=>r なら、pが真のときにqも真になってrも真になるので、p=>rになるはずです。
ここで、かつ（論理積）は、Idrisではタプルで(p, q)と表現できます。
（pとqを同時にタプルにできるということは、両方に証明があるということ）
以下のコードで証明ができます。
ならば推移律 : (p->q, q->r) -> (p->r)
ならば推移律 (hpq, hqr) = \hp => hqr (hpq hp)
-- 作りたいのは、型pの値を受け取って型rの値を作り出す関数
-- 受け取ったhpから、p->qの関数、q->rの関数を使って型rの値を作り出す
ちょっと実用的な定理も証明できましたね。
理論的な補足
型と命題、関数と証明が対応することは、カリー・ハワード同型対応というしっかりした理論的根拠があるらしいです。
Discussion