问题标签 [coq]

我有一个生成文件：

添加命令：coqtop -R coqdir我必须在我的计算机中给出一个物理路径，但是这个目录取决于用户目录。( ~/color/trunk/color/devel/gwen Devel and ~/color/trunk/color CoLoR)。

在没有给出物理路径的情况下，是否有另一种方法可以调用和组合程序？

有没有办法在 coq 中取消导入或隐藏基础库？

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

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

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

我得到了同样的错误。

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

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

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

我正在写一篇关于使用 Coq 系统对快速排序算法进行程序验证的论文。我在 Coq 中定义了一个快速排序，但我的主管和我自己都不太习惯使用策略来编写实际的证明。有没有人可以帮助解决 coq 证明的那一部分？以下是我们迄今为止提出的建议：

我知道要证明有效，我们需要引理或定理，但是我不确定在那之后从哪里开始。谢谢您的帮助 ：）

我有文件：

• 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？非常感谢你。

这个问题与在 Emacs 中的 Proof General 中配置 Coq 模式有关。

我试图让 Emacs 用相应的 Unicode 字形自动替换 Coq 中的关键字和符号。我设法将其定义fun为希腊小写 lambda λ、forall通用量词符号 ∀ 等。我在定义单词符号时没有遇到任何问题。

问题是当我尝试为它们的 Unicode 符号 ⇒→↔ 定义运算符=>时->，<->它们不会被 Coq 中相应的 Unicode 字形替换。*scratch*但是，当我测试它们时，它们会在缓冲区中被替换。我使用相同的机制将 Unicode glyps 与 Coq 表示法匹配：

我怀疑问题在于 Coq 模式将某些标点符号标记为特殊，因此 Emacs 忽略了我的代码以将它们替换为 Unicode 字形，但我不确定。有人可以为我解释一下吗？

我正在尝试在 Coq 中定义 Ackermann-Peters 函数，但收到一条我不理解的错误消息。如您所见，我a, b将 Ackermann 的论点打包成一对ab；我提供了一个为参数定义排序函数的排序。然后我使用Function表单来定义 Ackermann 本身，并为它提供参数的排序函数ab。

我得到的是以下错误消息：

错误：没有这样的部分变量或假设：ack。

我不确定是什么困扰了 Coq，但是在搜索互联网时，我发现了一个建议，使用通过排序或度量定义的递归函数可能存在问题，其中递归调用发生在匹配中。但是，使用投影fst和生成不同的错误消息snd。if-then-else有人可以建议如何在 Coq 中定义 Ackermann 吗？

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

但我想保留类型Z是int

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

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

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

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

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

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

我正在尝试编写一个专门用于证明偶数属性的归纳假设。我制定并证明了以下内容：

尽管它已被证明，但任何使用它的尝试都会导致错误消息：“错误：不是正确数量的归纳参数。”

有人可以告诉我归纳假设有什么问题，或者如何应用它？

谢谢，

迈耶