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

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Coqの世界から現実世界へ

Coq入門 引き出し Definition Extraction

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