Можно ли извлечь Positive, Nat для int32, Z для int?

Question

Привет, я пишу извлечение из Coq в Ocaml, я хотел бы преобразовать тип:

positive --> int32
N -> int32

но я хочу сохранить тип Z является int

Вот код, который я делаю, чтобы извлечь эти условия:

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))".

Я не могу сделать это, чтобы сохранить Z -> int потому что определение Z в библиотеке Coq ( BinInt.v)

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

Я получил ошибку: (функция coq_Zdouble_plus_one)

Файл "BinInt.ml", строка 38, символы 4-5:

Ошибка: это выражение имеет тип int, но ожидалось выражение типа 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

Если я извлекаю Z -> int32Это нормально, но это не то, что я хочу.

Answer 1

Ваша проблема в том, что Z внутренне построен на positive,

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

Это означает, что всякий раз, когда вы получаете Zты действительно получаешь positive и немного дополнительной информации.

Если вы действительно хотите использовать разные типы для Z а также positiveВам нужно будет вставить функции преобразования между int а также int32, Вы могли бы сделать это с помощью функции извлечения, но я не уверен, как - или даже если - это возможно.

Другая проблема, которую я вижу, состоит в том, что код внутри совпадения на Zs получит positives для работы, это означает, что вы будете постоянно конвертировать между типами и теряете дополнительную точность, которую один из типов может иметь по сравнению с другим. Если это вообще возможно, я бы использовал один и тот же тип для обоих.