ocaml - 把coq类型的nat提取到哪个类型的ocaml这样我就可以有一个认证的程序了

Question

在Coq中，从类型中提取nat或未int经过big_int认证（它们是有效的）。如下面的链接所示：

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

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

两者都说： 免责声明：试图通过将 nat 提取到 big_int 来获得有效的认证程序不一定是一个好主意。请参阅 ExtrOcamlNatInt.v 中的评论。

如果我有coqtypes: nat, Z, N, 以及我应该选择positive哪些ocaml类型来提取我可以拥有认证（更安全）程序的类型（我可以忽略高效）？

目前，我选择将它们全部提取到int. 然后在里面ocaml int我用Int64hack 里面（获取边界min_intand max_int，如果k < min_intthen min_int，否则），for Zand positivenumber 我检查：如果(i:int) < 0然后返回类型非负整数，如果i <= 0那么它是类型positive

Answer 1

如果您不关心效率，则不应尝试将 Coq 的类型绑定到 Ocaml 的类型，只需按原样提取它们（归纳类型），您将是安全的。但是，对（一元数）进行计算nat会非常慢。例如：

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

提取Z会更加冗长。