Coqの型とOCamlの型

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で得られたモジュール内のものであるとする。