The extraction of coq type nat into which type of ocaml so that I can have a certified program

Question

In Coq, the extraction from type nat into int or big_int are not certified (they are efficient). As in these links below:

http://coq.inria.fr/V8.3/stdlib/Coq.extraction.ExtrOcamlNatBigInt.html and

http://coq.inria.fr/distrib/8.3/stdlib/Coq.extraction.ExtrOcamlNatInt.html

Both saying that: Disclaimer: trying to obtain efficient certified programs by extracting nat into big_int isn't necessarily a good idea. See comments in ExtrOcamlNatInt.v.

If I have coq types:nat,Z, N, and positive which ocaml types should I choose to get the type extracted that I can have a certified (safer) program (I can ignore the efficient)?.

Currently, I chose to extract all of them into int. And then inside ocaml int I used the Int64 to hack inside (get the boundary min_int and max_int, if k < min_int then min_int, and otherwise), for Z and positive number I check that: if (i:int) < 0 then return type non-negative int, if i <= 0 then it is of type positive

Answer 1

If you don't care about efficiency, you should not try to bind Coq's type to Ocaml ones, just extract them as they are (inductive types) and you will be safe. However using computation over nat (unary numbers) will be really slow. For example:

Extraction nat.
(*
  type nat =
   | O
   | S of nat
 *)

Extracting Z will be a bit more verbose.