问题标签 [coqide]

我知道 Coq 允许定义相互递归的归纳类型。但是有没有办法在 Coq 中编写递归定义？

例如，我想写一个定义为：

Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).

上述定义中的重要部分是myDefinition B，它在另一个参数上递归调用相同的定义。在 Coq 中可以做到这一点吗？

我正在尝试在 Coq 中模拟全局和局部变量，但我什至不知道如何开始。有没有人可以给我一个提示或一些建议？我阅读了很多关于这种编程语言的文档，但我无法弄清楚。先感谢您！

我正在使用 Coq 8.10.0。以下证明脚本似乎在 Mac 中工作（忽略警告）：

但是 Linux (Ubuntu) 和 Windows 不接受相同的证明脚本。它抛出以下错误：

（在证明 plus_comm 中）：尝试保存放弃目标的证明。如果这确实是您想要做的，请使用 Admitted 代替 Qed。

知道这里发生了什么吗？

PS：我知道理想情况下，承认的证明应该以 Admitted 而不是 Qed/Defined 结尾。我正在尝试调试证明脚本。

我正在尝试解决关于长度交替附加定理和子列表长度定理的 coq 列表分配。我想通过 coq 证明辅助来证明这些引理。我怎样才能做到这一点？

我有一个明显错误的假设，我想用它来证明错误。在这种情况下，我有Hx: 0 * 0 = 2而且我有False我的目标。我该如何开始呢？

图片来自 CoqIDE：

我无法解决应该使用指称语义的 Coq 定理。如果我从这一点继续前进，我总是陷入无限循环。

在这种情况下应该使用什么策略？我在哪里做错了这个？我应该以不同的方式开始吗？

我最近用 opam 安装了 Coq 版本 8.12.2。我已经使用以下命令安装了 Coq 的所有软件包：

opam repo 添加 coq-released https://coq.inria.fr/opam/released

但是当我尝试在 Coqide 中编译包时，它无法识别 coquelicot。

我收到这些错误：
Cannot find a physical path bound to logical path matching suffix <> and prefix Coquelicot

和

我正在通过 Coq 8.12.0 参考手册学习 Coq，但无法证明以下引理。

然后我被卡住以完成证明。有任何想法吗 ？

我目前正在编写 Software Foundations 教科书 Verified Functional Algorithm 的第 3 卷，但我一直坚持一个练习的证明。

您可以在此处找到我目前正在处理的有关 Mergesort 的章节：https ://softwarefoundations.cis.upenn.edu/vfa-current/Merge.html

到目前为止，这是我被困的地方：

这是我最后一个策略“inv H”的结果。

关于我应该如何继续证明我的目标的任何线索？Permutation (x1 :: x2 :: l1') (l1 ++ l2)

我在理解 Coq 中强规范和弱规范之间的区别时遇到了一些麻烦。例如，如果我想使用强规范方式编写复制函数（给定一个数字 n 和一个值 x，它会创建一个长度为 n 的列表，所有元素都等于 x），我将如何做到这一点? 显然我必须编写函数的归纳“版本”，但如何？

Haskell 中的定义：

弱规范的定义：

用弱规范定义这些函数，然后添加伴随引理。例如，我们定义了一个函数 f : A->B 并证明了一个形式为 ∀ x:A, Rx ( fx ) 的语句，其中 R 是编码函数预期输入/输出行为的关系。

强规范的定义：

给出函数的强说明：这个函数的类型直接说明输入是类型 A 的值 x，输出是类型 B 的值 v 和 v 满足Rxv的证明的组合。这种规范通常依赖于依赖类型。

编辑：我收到了老师的回复，显然我必须做类似的事情，但对于复制案例：

“例如，如果我们想从它的规范中提取一个计算列表长度的函数，我们可以定义一个关系 RelLength 来建立预期输入和输出之间的关系，然后证明它。像这样：

用于证明的函数必须直接使用列表“recursor”（这就是fixpoint 不会显示的原因——它隐藏在list_rect 中）。

所以你不需要编写函数本身，只需要编写关系，因为函数将由证明定义。”

知道了这一点，我如何将其应用于复制功能案例？