2

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

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
Quyen
  • 1,363
  • 1
  • 11
  • 21

1 Answers1

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.

Vinz
  • 5,997
  • 1
  • 31
  • 52
  • In my program, I need to bind it to ocaml ones. If I have to use the ocaml types, which type is safer in this case (is it big_int because I need to deal with a big integers?). Thanks. – Quyen Aug 29 '14 at 10:57
  • I really don't know, sorry. What do you mean by "safer" ? – Vinz Aug 29 '14 at 12:48
  • 3
    `big_int` is safer than `int` because `nat`, `positive`, `N`, and `Z` can get arbitrarily large, and `Z` can also get arbitrarily small. With large numbers, `int` would just wrap around or get capped, so your proofs wouldn't be valid. Mapping Coq numbers to Ocaml numbers doesn't require special care, but mapping operations does. For example, `Extract Constant pred => "fun n -> Big.max Big.zero (Big.pred n)"`. –  Aug 29 '14 at 13:37