Coqの世界から現実世界へ
Coqの中で定義したり証明の対象にした関数を、ふと日常生活で使いたくなるときがある。
そんなときはExtractionコマンドが大変便利である。
文法 [Extraction 関数名]
例えば次のような恒等関数を作ってExtractionしてみる
Coq < Definition id (A:Set)(x:A) := x. id is defined
Coq < Extraction id.
let id x = x
また、出力結果をocamlのソースファイルとして引き出すことができる。まさにextractだ。
文法 Extraction "ファイル名.ml" 関数名.
ファイル名をダブルクォーテイションで挟むことを忘れないようにしよう。
関数を複数記述すれば、複数の関数を出力することもできる。
このようにCoqではOCamlのコードを出力することができるが、実はOCaml以外でもHaskellや、Schemeなどの言語のコードを出力できるそうだ。