読者です 読者をやめる 読者になる 読者になる

CoqのtacticをOCamlで書く話

CoqのtacticをOCamlで書いてみたので、同じようなことをしたい人のためにメモ。

なお私はOCamlについてはそれほど詳しくないので、そこの正確性については注意が必要。

同じ事をしているtacticがないか探す

同じようなことを考えている人は必ずいるはず。といっても、網羅的な探し方があるわけではないので、ある程度調べて見つからなかったら自分で書いたほうが効率が良いかもしれない。

CoqのLtacで実現できないか考える

CoqのLtacは型無しラムダ計算であり、よく理解すればかなりの処理をLtacだけで実現できる。もしOCamlで実装するにしても、Coqに既に存在しているtacticやtacticalなどを把握していれば実装は容易になる。

Ltacの機能については、Coqのリファレンスマニュアルの012番 Chapter 9 The tactic language にまとまっている。なお、Ltacに関連するコマンドとしては、"Ltac"と"Tactic Notation"が扱えればよい。これらのコマンドについては、コマンド一覧 Vernacular Commands Index を参照。

まあ、「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")

まとめ

とりあえず自分の使った範囲では以上のようなテクニックがあった気がする。

高度な証明生成がしたくなったら、OCamlコードを書いて快適なCoqライフを送ろう。