问题标签 [coq-extraction]

我有一个tmp从 coq 提取到 ocaml 后生成的文件夹。

main.ml是我用来调用一个函数的文件cpf0：

我得到一个错误说Cpf0.proof是未绑定的。我尝试使用：（proof存在于Cpf0）。

我得到了同样的错误。

Ocaml 链接：ocamlc -I tmp -c main.ml

我不明白为什么它不接受Cpf0？

但open Cpf0;;仅此而已，链接不会给我任何错误。我用另一个文件进行了测试tmp，它能够使用该文件的所有功能。

我有文件：

• String0.ml提取自String.v（来自 Coq 库）

• String.ml：是Ocaml的字符串库

将我的测试文件从 Coq 提取到 Ocaml 后，我想String.ml在 Ocaml 的库中使用，所以我编写了一个替换命令将所有替换String0为String.

问题出在文件test.v中，我使用了以下定义之一：

string_decOcaml 的库中没有这个函数，但 Coq 的字符串库中有

所以我编译的时候出错了test.ml

错误：未绑定的值 string_dec

我想将 Ocaml 的字符串库用于我的所有提取文件。我怎样才能编译string_dec？

我正在提取转换nat为big_int

当我使用库时：ExtrOcamlNatBigInt，它没有返回正确的类型big_intinOcaml

所以我修改了它（文件 ExtrOcamlNatBigInt），但我找不到定义函数的方法，nat_case因为在Big_intOcaml 的库中它们没有函数nat_case。

我尝试为nat_caseby 定义第二个定义：

这是使用第二个定义后的结果：

我n在行出现错误else f0 (n - one)：

文件“Datatypes.ml”，第 68 行，字符 51-52：错误：此表达式的类型为 Big_int.big_int，但表达式应为 int 类型

我认为是因为minus( -)

我还修改了minus提取：

你能帮我定义函数nat_case吗Big_int？非常感谢你。

嗨，我正在编写从 Coq 到 Ocaml 的提取，我想转换类型：

但我想保留类型Z是int

这是我为提取这些条件所做的代码：

我无法保留它，Z -> int因为ZCoq 库 ( BinInt.v )中的定义

我收到一个错误：（函数 coq_Zdouble_plus_one）

文件“BinInt.ml”，第 38 行，字符 4-5：

错误：此表达式的类型为 int，但预期的表达式为 int32 类型

如果我提取Z -> int32，没关系，但这不是我想要的。

我在这个模块中有一个模块结构我声明了一个用于内部某些函数的变量module A。

然后我使用提取机制。

要不就

它为我生成了带有警告的代码：“必须在提取的代码中实现以下公理：Aa”

在这里，我收到a了failwith "AXIOM TO BE REALIZED" 我无法成功运行我的功能，因为这个failwith

因为我必须使用a模块内部的变量。failwith我想知道有没有办法定义提取后不会生成的模块？还是与不会生成此failwith功能的提取有关？

我有一个功能PolyInterpretation（http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt.html）

和一个模块签名TPolyInt（http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt_MA.html）

然后在我的文件rainbow.v中，我定义了一个TPolyInt_imp使用仿函数的模块用途PolyInt

哪里fun_of_pairs_list有类型：forall f: Cpf0.symbol, list {g : symbol & poly (arity g)} -> poly (arity f)

然后我定义一个模块P：

Coq证明助理接受了上述定义P。

然后我使用提取来提取到OCaml.

我把它写在另一个文件中：extraction.v

它工作正常。

这是提取后的代码

TPolyInt_imp因为在他们包含Variable并生成的仿函数内部，failwith AXIOM我决定定义一个新的签名来包含所有这些变量。

Arity然后定义一个以 ( ) 作为参数的新函子。在这个函子中我定义了模块TPolyInt_imp（像TPolyInt_imp以前一样）。

然后我使用提取将其提取到Ocaml.

然后我收到一条错误消息：

提取后的代码：

提取有什么问题？以及他们出现此错误的原因？如何更正我的代码，以便在提取后成功编译？

另外我不想定义一个实现签名的新模块Arity。

我很抱歉我的代码缺少类型并且无法编译。我试图给出我的问题的想法。

我想将一个函数提取foo到Coq一个OCaml文件中。因为我真正的函数必须使用 . Recursive Extraction，所以当我运行程序时，它会在cmd. 但我想将其输出到文件中，例如：foo.ml

当我尝试时：

或者Recursive Extraction foo "foo.ml"

我收到一个错误：Syntax error: "." expected after [vernac:command] (in [vernac_aux]).

我的问题是：我是否能够foo使用Recursive Extraction语法将函数提取到文件中？谢谢您的帮助。

在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

我使用从 Coq 到 OCaml 的提取，其中我有 type Z, N,positive

我不用来提取它int不习惯从 OCaml 中提取它。

那么我提取后的类型是：

我在 OCaml 中有一个程序，其中一些函数使用 OCaml 类型string。

在我的 OCaml 程序中，我需要编写一些函数来转换类型：string -> coq_N, string -> coq_Z,string -> positive

我尝试在 Coq 中编写函数，然后使用提取来获取 OCaml 类型，但 Coqstring与 OCaml 不同string。

例如：

函数coq_N_of_ascii的提取在哪里。coqN_of_ascii

当我应用函数string_of_coqN时，例如：

我得到了抱怨

您能否帮我找到一种编写转换函数的方法string -> coq_N：string -> coq_Z和string -> positive？

我目前正在尝试从我的程序验证引理生成 Haskell 代码，如下所示：

在结束我的部分后，我会：

它似乎对某事并不满意，因为它返回以下错误：

我有另一个引理，它似乎可以很好地导出，但我无法弄清楚问题到底出在哪里。有关如何解决该错误的任何线索？