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などの言語のコードを出力できるそうだ。