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

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

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

Coqの型とOCamlの型

引き出し Extraction

Coqは非常に疑り深いのでOCamlなどの普通のプログラミング言語の型を全然信頼しない。
このため、CoqからExtractionで引き出した関数を使う場合はCoqの型からOCamlの型への変換をしなければならないことがある。
それはint, nat, stringなどの基本的な型である。
これらはいったん変換関数をOCaml側で作ってしまえば、それを使えば問題ないが、この変換が間違っていれば、Coqでいくら正確に証明しても、実行時エラーになってしまうので十分注意してほしい。いずれも単純な変換なので、心配であれば紙で証明するのもよいだろう。

欲しい関数はだいたい次があげられる。

int_of_z : Coq.z -> int
z_of_int : int -> Coq.z
int_of_nat : Coq.nat -> int
nat_of_int : int -> Coq.nat
string_of_coqstring : Coq.string -> string
coqstring_of_string : string -> Coq.string

ただしここでCoq.〜はCoqからのExtractionで得られたモジュール内のものであるとする。