Can I extract Positive, Nat to int32, Z to int?

Question

Hi I am writing an extraction from Coq to Ocaml, I would like to convert type:

positive --> int32
N -> int32

but I want to keep type Z is int

Here is the code I am doing to extract these conditions:

Require Import ZArith NArith.
Require Import ExtrOcamlBasic.

(* Mapping of [positive], [N], [Z] into [int32]. *)
Extract Inductive positive => int32
[ "(fun p-> let two = Int32.add Int32.one Int32.one in
    Int32.add Int32.one (Int32.mul two p))"
  "(fun p->
    let two = Int32.add Int32.one Int32.one in Int32.mul two p)" "Int32.one" ]
  "(fun f2p1 f2p f1 p -> let two = Int32.add Int32.one Int32.one in
    if p <= Int32.one then f1 () else if Int32.rem p two = Int32.zero then
    f2p (Int32.div p two) else f2p1 (Int32.div p two))".

Extract Inductive N => int32 [ "Int32.zero" "" ]
"(fun f0 fp n -> if n=Int32.zero then f0 () else fp n)".

Extract Inductive Z => int [ "0" "" "(~-)" ]
"(fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))".

I cannot do it to keep Z -> int because the definition of Z in Coq's library (BinInt.v)

Inductive Z : Set :=
  | Z0 : Z
  | Zpos : positive -> Z
  | Zneg : positive -> Z.

I got an error: (function coq_Zdouble_plus_one)

File "BinInt.ml", line 38, characters 4-5:

Error: This expression has type int but an expression was expected of type int32

BinInt.ml

open BinPos
open Datatypes

(** val coq_Z_rect :
    'a1 -> (int32 -> 'a1) -> (int32 -> 'a1) -> int -> 'a1 **)

let coq_Z_rect f f0 f1 z =
  (fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))
    (fun _ ->
    f)
    (fun x ->
    f0 x)
    (fun x ->
    f1 x)
    z

(** val coq_Z_rec : 'a1 -> (int32 -> 'a1) -> (int32 -> 'a1) -> int -> 'a1 **)

let coq_Z_rec f f0 f1 z =
  (fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))
    (fun _ ->
    f)
    (fun x ->
    f0 x)
    (fun x ->
    f1 x)
    z

(** val coq_Zdouble_plus_one : int -> int **)

let coq_Zdouble_plus_one x =
  (fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))
    (fun _ ->
    Int32.one)
    (fun p ->
    ((fun p-> let two = Int32.add Int32.one Int32.one in
    Int32.add Int32.one (Int32.mul two p))
    p))
    (fun p -> (~-)
    (coq_Pdouble_minus_one p))
    x

If I extract Z -> int32, it is Ok, but it is not what I want.

Answer 1

Your problem is that Z is internally built upon positive.

Inductive Z : Set := Z0 : Z
                   | Zpos : positive -> Z
                   | Zneg : positive -> Z
                   .

This means that whenever you get a Z, you're really getting a positive and some extra info.

If you really want to use different types for Z and positive, you'll have to insert conversion functions between int and int32. You might be able to do that with the extraction feature, but I'm not sure how – or even if – that's possible.

Another problem I see is that code inside a match on Zs will get positives to work with, meaning that you'll be constantly converting between the types and losing any extra precision one of the types might have over the other. If at all possible, I'd use the same type for both.