Write Yourself a Theorem Prover in 48 Hours (その4)

去年のアドベントカレンダーの続きです！

Coqみたいな定理証明器のおもちゃみたいなのをHaskellを使って1年と48時間ぐらいで作れるかな？って話です。

去年の記事は
http://qiita.com/kikx/items/10d143edc090bdfec477
http://qiita.com/kikx/items/b0eda41bc7b9036ac18d
http://qiita.com/kikx/items/57aad1867b89f8955611
です。

去年の記事で型検査と計算はできたので、証明支援を行う部分を作っていきます。

対話環境の作成

対話的にコマンドを実行するコードを書くのは本質とは関係ないので、なるべく手抜きで作りましょう。ghciをそのまま使う方法もありますが、グローバルなIORefを引数で渡して回ったりしないといけないのでちょっと使いにくいです。簡単な方法としてHaskellのソースファイルに実行したいコマンドを順番に書いた関数を書いて、更新するごとにghciで呼び出す方法です。最初はなかなかまともに動作しないのでこの方法がおすすめです。

test_proof :: IORef GlobalState -> IO ()
test_proof g = runProver g $ do
  command1 param1 param2
  command2 ...
  ...

みたいな感じに使えるモナドを作りましょう。単純にやるならgを読み出すReaderTとIOの合成でできます。

グローバルな環境

すでに証明が終わった定理を他の定理の証明で使いたいので、グローバル環境に保存しておく必要があります。ローカル変数と違いこちらは名前で参照します。

data Binding = Decl Type
             | Def  Type Term
             deriving (Show, Eq)
 
type Local = [(Maybe String, Binding)]
type GlobalBindings = [(String, Binding)]

ローカル変数は番号で参照していますが、証明の途中やデバッグでは表示用の名前があったほうが便利なのでなるべく残しておいたほうがいいです。グローバル変数を参照する項を追加しましょう。

data Term = ...
          | TmConst String
          | ...

これにより型検査等にはGlobalBindingsも渡さないといけなくなります。

対話環境の状態はこのグローバルな環境と証明中のときはその状態を持たせることにします。

data GlobalState = GlobalState GlobalBindings (Maybe ProofState)

コマンドの型は簡単に次のモナドにしましょう。

type ProverCommand a = ReaderT (IORef GlobalState) IO a

コマンドによってはGlobalBindingsを変更するものやProofStateを更新するもの、GlobalBindingは読むだけのものなど色々と分類できるので、細かく便利関数を作って工夫しましょう。

証明環境

証明を開始するには、証明したい命題の型と命題の名前を渡します。この型を持つ証明項を作っていくわけです。

証明が完成すると、出来上がった証明項が命題の型を持つことを検査して、グローバル環境に追加しましょう。今回は簡単のために証明の途中では型検査を完全にはしないことにします。

証明の途中では作りかけの項が存在します。作りかけの項を表すデータ型が必要ですが、ここでは単純のために、Termに穴を追加しましょう。

data Term = ...
          | TmHole Int
          | ...

穴の番号は各定理の証明が始まるごとに0から付け始めればよいでしょう。型検査中などの途中で穴の存在はバグです。本当は穴のある項かどうか型で区別できるべきですが手抜きしましょう。

証明中の環境は以下のようになります。

data Goal = Goal Int Type Local

data ProofState = ProofState { goals :: [Goal]
                             , proof :: Term
                             , lemmaName :: String
                             , mainGoal :: Term
                             , nextHoleId :: Int
                             }

mainGoalとlemmaNameは開始時に与えられた値で一定です。nextHoleIdで次に割り当てる穴の番号を管理します。proofは穴がいくつかある項です。証明が完了して穴がなくなると、これが証明項になります。goalsにはサブゴールのリストが入ります。リストの長さはproofの穴の数に等しくします。各サブゴールは穴の番号とこのサブゴールの型とローカル環境を持っています。

証明の開始時に、proofは穴がひとつの項 TmHole 0にします。そしてサブゴールは1つだけで、Goal 0 mainGoal []になります。

証明コマンドtacticはgoalsの先頭のサブゴール「Goal n ty Γ」に作用します。コマンドはtyを見て適用可能なものか判断されます。引数として項を取るコマンドの場合は、ローカル環境Γにある変数を参照したりグローバル環境を参照したりできます。コマンドの結果は、穴「TmHole n」を埋める新しい項と、新しい項に含まれる新しい穴に対応するサブゴールのリストになります。

例えば、「exact 項」コマンドは先頭のサブゴールを完了するので、引数の項をそのまま返して、新しく増えるサブゴールは空になります。その結果、サブゴールはひとつ減ります。

ほとんどのコマンドはサブゴールの数を変えません。例えば「intro」コマンドが返す項は穴がひとつある項を返すので、サブゴールの数は変わりません。「intro」の生成する項は関数なので「TmAbs ty' (TmHole newId)」になります。新しい穴newIdではローカル変数がひとつ増えるので、Γが増えたサブゴールをひとつ返しましょう。

簡単な証明

簡単な定理を証明してバグを取りましょう。最初に証明すべき定理は

Univ 0 = Univ 0

ですね。次は

forall t : Univ 0, forall x : t, x = x

です。他にも

forall P : Univ 0, P -> P

等色々とあります。頑張ればEckmann-Hiltonの定理まで証明できると思いますが、どんどん複雑になっていくので、tacticを増やしながら進めていくことになります。

次回予告

TmEqをデストラクトするtacticはとんでもなく難しいです。次回はそれを頑張って実装して、Eckmann-Hiltonの定理まで証明できるようにしたいなあ。