问题标签 [coqide]

我已经写了这个归纳谓词和它的（强）规范的部分证明：

问题是我认为这个定理不正确，因为 Coq 不接受类似{n0 n1: nat | ...}. 有没有办法解决这个问题还是我想错了？

我认为谓词SumPairs是正确的，但由于我不确定，这里有一个它应该如何工作的例子： input [(1,2),(3,4)], expected output[3,7]

是否可以“转换”函数的Fixpoint定义count：

对于Inductive谓词（我第一次尝试如下，但我不确定它是否正确）？（这个谓词应该描述函数的输入和输出之间的关系）

为了确定它是否正确，我定义了这个定理（弱规范）：

但我不知道如何完成它......有人可以帮忙吗？

我的 coq 中有一个目标，其中有“&”号。我该如何处理？

我很感激任何帮助。

问候

我正在尝试编写一个在堆栈程序中执行布尔操作的函数。到目前为止，我得到了下面的代码，但由于某种原因，executeBool它不起作用。Coq 显示错误“无法猜测修复的递减参数”，但我不太清楚为什么，因为它看起来有点“明显” program。

为什么会这样？不管我改变多少功能，我都会得到它......有什么办法可以解决它吗？谢谢！

我正在形式化一个支持一对元组和 nat 作为函数输入的系统。但是，我对 Coq 中的 pair 类型有一些问题。

根据我对 Coq 的了解，pair 被定义为左关联。即(1, 2, 3)并且((1, 2), 3)具有相同类型的nat * nat * nat. 有时，它可以被视为 nat 的 3 元组。另一方面，(1, (2, 3))有 type nat * (nat * nat)，它是一对 nat 和 pair（或 2 元组）。

理想情况下，我想要一个允许nat 和 tuple对以及 tuple 和 nat 对的系统。即两者(1, (2, 3))和((1, 2), 3)都不同于(1, 2, 3)。对于这种模型，Coq 中是否有任何建议的数据类型？

运行以下代码时遇到错误消息。

我想知道我该如何解决它。谢谢。

我目前的目标是这样的：

fun2 是我之前定义的一个函数，它的类型为 forall W ：Type, list W -> list W -> list W 并且还满足 S_fun fun2。如何将 fun2 替换为 fun1 或将 fun1 替换为 fun2 或告诉 Coq fun2 和 fun1 实际上相同以使用自反性完成证明？

使用启用了 VSCoq 和 coq 扩展的 Visual Studio Code 时，单步执行证明效果很好，但 ProofView 窗口显示空白（无内容）。解决此问题的问题和解决方案可能是什么？

我目前的目标是：

我尝试使用rewrite -> (Nat.add_comm (-1) 1).将当前目标更改为x + 1 - 1，但它给了我错误Error: Cannot interpret this number as a value of type nat。我该如何解决这个问题？

这是我想在这里证明的定律：

这是我的代码，直到我不知道该朝哪个方向前进：

显示的子目标和我所拥有的前提似乎是可证明的，但下一步是什么？

我试过用exfalso., 去apply H.之后。这给了我另一个前提x : X和一个子目标px。

不知道以后怎么办。谢谢您的帮助！