Theorem Prover Haskellの紹介

この記事はTheorem Prover Advent Calendar 2016の1日目の記事です。

今年も残り1ヶ月になったことを信じたくないと思いつつ、
まあ学生的には4月始まりだから大丈夫と自分に言い聞かせてます。

今回のアドベントカレンダーのネタを必死に1週間くらい前から頑張って探した結果
何も見つからなかったのでHaskellで証明を書きます。

みなさんHaskellで証明を書くのはつらいと思うかもしれませんが
実はEquational Reasoningも使えるし
最近バージョンが上がって少し賢くなったコンパイラの強力なサポートも受けられるので
意外とマシです。(当社比)

さてHaskellで証明をすることについてですが、
ここでは定理証明界のFizzBuzzとも名高い*1、リストのreverse関数が2回やると元に戻ることを示します。

Leanで書いた同じ証明も置いとくので、ぜひ見比べてみてください↓
Leanバージョン

ポイントをいくつか解説します。

cong :: a == b -> f a == f b
cong Refl = Refl

-- fを具体化
congAppend :: Sing x -> a == b -> a ++ Cons x Nil == b ++ Cons x Nil
congAppend _ Refl = Refl

congは上で定義していますが、証明中ではほとんど使っていません。
どうもcongはこの形だとfの曖昧性が残るのでいちいちfを具体的にした命題を置いて使います。

これは、TypeFamiliesで定義した(Reverseとか)type functionはGHC的にはk -> kカインドの関数とは違う(type functionに対しては部分適用を認めない)ようで、fにTypeApplications拡張で直接代入しようとしても引数の数が足りないというエラーになるためです。
ここは型コンストラクタへの部分適用ができるようになればTypeApplicationsでなんとかなるはずです。

data instance Sing (typ :: List a) where
  SNil :: Sing Nil
  SCons :: Sing x -> Sing xs -> Sing (Cons x xs)

singleton typeです。

Listカインドの型を保持したままListの項と同型な構造を持つデータを定義します。
これは帰納法を回すときに"xsの内部の項"を引数でとるために使っています。

Haskell依存型プログラミングでは頻出のテクニックであり、
この辺はsingeltonsパッケージあたりを使うとちょっと楽になれます多分。

(===) :: Sing a -> Sing b -> Sing (Mk2 a b)
(===) a b = STuple a b

infixl 3 `by`
by :: Sing (Mk2 a b) -> a == b -> b == c -> a == c
by _ = trans

qed :: forall a. a == a
qed = refl

ex :: Sing a -> Sing b -> Sing c -> Sing d -> a == b -> b == c -> c == d -> a == d
ex a b c d ab bc cd =
  a === b `by`ab $
  b === c `by` bc $
  c === d `by` cd $ qed