CoqのtacticをOCamlで書く話
CoqのtacticをOCamlで書いてみたので、同じようなことをしたい人のためにメモ。
なお私はOCamlについてはそれほど詳しくないので、そこの正確性については注意が必要。
同じ事をしているtacticがないか探す
同じようなことを考えている人は必ずいるはず。といっても、網羅的な探し方があるわけではないので、ある程度調べて見つからなかったら自分で書いたほうが効率が良いかもしれない。
- まずCoq自体にないかを調べる。Coqの基本的なtacticsは Tactics Index
に書かれている。
- Coqのcontribution集に似たような内容のものがないかを調べる。contributionは
の「All contribs」というリンクから一覧できる。
- 特に、AACTacticsは有用らしく、Ubuntuのパッケージにもなっているようだ。
- ssreflectには有用なtactic/tacticalが大量にある。ただし、ssreflectはデータ構造や証明手順の提示方法が、普通のCoqとかなり異なるので、その点には気をつけなければいけない。 math components —
- ssreflectのtactic/tacticalについてはSSReflect CheatSheet - Proving - kik
が有用。また、ssreflectのドキュメント HAL - INRIA :: [inria-00258384, version 11] A Small Scale Reflection Extension for the Coq system
は網羅的で有用である。
- ssreflectのtactic/tacticalについてはSSReflect CheatSheet - Proving - kik
- また、LibTacticsというtactic集があるようだ。こちらはssreflectと違い、伝統的なCoqの習慣に沿ったtacticを提供しているパッケージのようだ。 LibTactics: A Collection of Handy General-Purpose Tactics
CoqのLtacで実現できないか考える
CoqのLtacは型無しラムダ計算であり、よく理解すればかなりの処理をLtacだけで実現できる。もしOCamlで実装するにしても、Coqに既に存在しているtacticやtacticalなどを把握していれば実装は容易になる。
Ltacの機能については、Coqのリファレンスマニュアルの012番 Chapter 9 The tactic language
まあ、「CoqのLtacでできるはずだが、なぜかできない」(例：Anomalyが発生する)というのはよくある話なので、その機会にCoqの内部構造も理解してしまおうという軽い気持ちでOCamlに手を出すのも悪くはないかもしれない…
ビルド環境を整備する
Windows(Cygwin+MinGWなど)でも頑張ればビルドできないことはないが、大変なのでLinuxなどの使用を強く推奨する。(Windowsでビルドするノウハウについてはそのうち書きたいが…)
OCamlの処理系やCoqのヘッダなどを必要に応じて入れていけばいいだろう。一番簡単なのは、OS標準のOCamlとliblablgtkをインストールした上で、Coq自体は自分でビルドするという方法なのではないかと思う。
開発環境が整ったら、Makeファイルを書く。Makeの例は以下のとおり。
-R . MyPackage -R ../DependentPackage DependentPackage my_ocaml_code.ml my_ocaml_code.mli ocaml_extension_interface.ml4 CoqCode/InternalA.v CoqCode/InternalB.v Foobar.v
MyPackageはパッケージの名前である。この例の場合は、MyPackage.CoqCode.InternalAなどのモジュールが生成される。
普通のOCamlコードはmlとmliに書き、tacticを宣言するところをml4に書くのが一般的なようである。(全てを単一のml4ファイルに集約しても問題はない。)
Makefileを以下のようにして生成する。基本的には、Makeファイルはcoq_makefileへのコマンドライン引数をひとまとめにしたものに過ぎない。
$ coq_makefile -f Make -o Makefile
あとは普通にmakeと打てばビルドされるようになる。
ハローワールドを書く
greeting.ml4ファイルに次のように書く。(以下greetingは任意の名前で置き換えてよい)
TACTIC EXTEND hello | [ "hello" ] -> Tacticals.tclIDTAC_MESSAGE (Pp.str "Hello, world!\n") END
vファイルに次のように書く。
Declare ML Module "greeting". Goal True. hello. auto. Qed.
ゴールの帰結を出力する
ゴールの帰結を出力するようにしてみる。
let hello gl = Tacticals.tclIDTAC_MESSAGE (Termops.print_constr (Tacmach.pf_concl gl)) gl TACTIC EXTEND hello | [ "hello" ] -> hello END
タクティックの基本構造
タクティックはProof_type.tactic型であるが、これはgoal sigma -> goal list sigmaである。
これは、「ゴールと環境を受け取って、ゴールのリストと環境を返す関数」という意味である。
Goal.goalの実体はただの整数である。'a Evd.sigmaは、'aに環境を付加した('a, evar_map)といった感じの型で、'aはEvd.sig_it、環境はEvd.sig_sigで取り出せる。
といっても、goal list sigmaを自分で組み立てることはまずない。Tacticalsモジュール(tactics/tacticals.mli)に、基本的なtacticalが存在しているので、これを使えば大抵の操作は組み立てられる。また、applyなどの基本的なtacticはTacticsモジュール(tactics/tactics.mli)に存在している。
なお、Proofview.tacticは全く異なる型のようであるので注意すること。これはより抽象的なモナドのようだ。
Coqのデータの操作
Coqにおける値はOCaml上ではTerm.constrという型をもつ。「Coqにおける型」を意味するTerm.typesはconstrの別名にすぎない。
constrの基本的な操作はTermモジュール(kernel/term.mli)にある。mkAppなどのmk系、isAppなどのis系、destAppなどのdest系があれば基本的に事足りる。
constr同士の比較は目的に応じて複数の関数があるが、一番身近なのはeq_constrである。自分で比較を作りたいときは、compare_constr関数が便利である。compare_constrを利用して比較を組み立てる方法は、実際にそれを使っているコードをCoq本体から探すのが早い。(eq_constr自身もcompare_constrを使っている。)
帰結の取り出し
ゴールから帰結の型を取り出す関数はTacmach.pf_conclである。ゴールから情報を取り出したいときはまずTacmachモジュールを探せばよいだろう。
ただし、こうして取り出したconstrには、「すでに確定しているevar(existential variable)」が含まれている場合がある。つまり、既に具体的な値が確定しているのに、「?1」のようなexistential variableの形で含まれている部分式が存在しうる。(具体的には、同じ命令の間(ピリオドで区切られたときに同じ区間に属する間)に、以前のtacticで値が確定したevarがこのままの形で残っている。) これを具体的な値で置換する場合は、Evarutil.nf_evarを使えばよい。
Coq内で定義された値を取り出す
いろいろな方法があるようだが、次のようにするのが簡単だろう。
let coq_Permutation = lazy (Coqlib.coq_constant "Coq.Sorting.Permutation.Permutation not found" ["Sorting"; "Permutation"] "Permutation")
