対話的定理証明系 Coq では、それ自身でプログラムを書き、性質を証明し、証明したコードを Haskell, OCaml, Scheme といった言語のプログラムとして抽出（Extraction）することができる。
しかし、 Lisp 系の言語で実用的なプログラムというと、 Common Lisp や Emacs Lisp で書かれることが多いのも事実である。
ということで Coq to Scheme Extraction で生成された Scheme コードを Common Lisp や Emacs Lisp （24.1 以降）としても読めるように変換するプログラムを作ってみた。
（変換の仕方は、同様のことを Coq 本体を改造して実現する話を ProofSummit 2014 でしたので、そのときのスライドを参照のこと）
変換プログラムは R7RS Scheme で書かれている。例えばリポジトリ内の example.v をコンパイルして、それを Common Lisp から使う場合には、以下のようにする（ここでは処理系として chibi-scheme を使った）。
% coqc example.v
% chibi-scheme unscheme.scm example.scm example.lisp
これで、 Scheme 版の example.scm を経由して、 example.lisp として Coq の関数が抽出される。このファイルを実行するための補助マクロはリポジトリ内の macros_extr.lisp に定義されている（Emacs Lisp の場合は .lisp を .el に読み替える）。
例えば SBCL を使って次のようにして抽出された関数を実行してみることができる。
% sbcl --load macros_extr.lisp --load example.lisp --script test.lisp
Coq から Extraction されたコードを使う話としては、 Coq で書かれたソート関数を Standard ML から使う、SMLでソート - チラシの裏の記事が参考になるだろう。
また、実際に Extraction されたコードがどのようになるか見てみたい場合は、 Coq から Erlang を Extraction してみる、 Verlang と Coq の Extraction について - Qiita の記事も参考になる。
まとめ
- Coq to Scheme Extraction で抽出された Scheme コードを Common Lisp / Emacs Lisp としても読めるように変換するプログラムを書いた
- 上記変換をしたコードを Common Lisp, Emacs Lisp として実行するための補助マクロを書いた
Coq 自体を改造して Extraction されるコードを変更する方法では、 Coq 本体の変更に追従するのが面倒だったり、そのために、 Coq のバージョンに依存したコードを Extraction するのが面倒だったりという問題があった。
今回の変更でより手軽に証明された Common Lisp / Emacs Lisp プログラムが手に入るようになったと思う。