问题标签 [coq]

我有类型

我想option d从列表的顶部获取类型，然后检查整个列表。我的代码如下所示：

我的问题是if forallb (fun li => forallb (fun ci =>do_something ci d))ls)l'我添加的测试是forallb (fun li =>...)因为我希望它在整个列表中进行测试l'。但我根本没有使用这个论点li。

编辑：我的问题集中在if forallb (fun li => forallb (fun ci => do_something ci d))ls)l'. 我添加forallb (fun li =>是因为我想对列表的其余部分进行测试l'。如果没有forallb (fun li我可以存档此测试if (forallb (fun ci => do_something ci d))ls，但我不知道如何在列表中再次测试此条件l'。

编辑

我收到一条错误消息：递归调用 dpProof 的主要参数等于

如果我不使用相互递归并使用嵌套固定点，它将结合并通过终止检查器。这是成功组合的代码。

我想更深入地了解它无法通过终止检查的原因？是因为他们无法猜测参数递减吗？有什么方法可以使用相互递归来表达我的功能dpGraphProc？

另外我如何编写dpGraphProc检查整个列表的函数？这里的说法不知怎么用cs'。

我有一个 Coq 项目，其中包含许多文件（例如 x1.v、x2.v、... xn.v），包括存储在文件夹“C:\Users\WK\Desktop\Personal\coq-project”中的 Makefile 和在我的 Windows 7 机器上的“C:\Coq”中安装了 Coq 8.3。

Coq 程序（文件）相互依赖。如何在 Coq 中执行单个程序（比如 x1.v）？我想在 Coq 中打开一个文件并逐行编译以理解它，但它会给出错误，因为每个文件中有许多导入的文件，而没有一个 (.vo) 格式的文件。我认为命令 coqc、coqtop、make 或这些命令的任何组合都有一些用途，但我不知道命令、参数和顺序的确切格式。请让我给出完整路径的完整命令记住上述路径。

谢谢，

维拉亚特

• 自从我学了一点 Coq 之后，我就想学习写一个所谓的除法算法的 Coq 证明，这实际上是一个逻辑命题：forall n m : nat, exists q : nat, exists r : nat, n = q * m + r
• 我最近使用从Software Foundations中学到的知识完成了这项任务。
• Coq 是一个用于开发建设性证明的系统，我的证明实际上是一种从值q和.rmn
• Coq 有一个有趣的工具，可以将 Coq 的算法语言 (Gallina) 中的算法“提取”为包括 Haskell 在内的通用函数式编程语言。
• 另外，我设法将 divmod 操作编写为 GallinaFixpoint并提取它。我想仔细指出，该任务不是我在这里考虑的。
• Adam Chlipala 在Certified Programming with Dependent Types中写道：“Curry-Howard 通信的许多粉丝都支持从证明中提取程序的想法。实际上，很少有 Coq 和相关工具的用户会做这样的事情。”

甚至有可能提取我对 Haskell 的证明中隐含的算法吗？如果可能，将如何实现？

我正在尝试为二进制自然数（位列表）定义前置函数。我想将我的函数的输入限制为修剪过的数字（没有前导零）并且是正数（所以，我不必担心零的前身）。

这是运算符的定义pred：

我的第一个义务如下：

但是，我不知道如何解决它。

矛盾显然在H2。但是，因为它取决于H1，所以我不能只rewrite nat1使用Empt，然后(is_pos Empt H1)使用False。

我应该如何证明这一点？

我试图在 Coq 中证明一个定理，但我无法解决出现的问题。我正在尝试解决：

我是 Coq 的新手，所以我不知道这到底意味着什么。我在互联网上做了一些研究，但我没有设法找到解决方案。有谁知道这个问题来自哪里？

我正在尝试在 Coq 中进行证明，并且我想使用我已经定义和证明的引理。下面的代码可以吗？

在上面我想使用 A /\B 与 B /\ A 相同的事实来证明 ~(A /\ B) 与 ~(B /\ A) 相同。是否可以使用我证明的引理？

我被困在一个关于归纳谓词的简单证明上。我必须证明自然 0 不是正数，其中自然是位列表，而 0 是任何只有位为 0 的列表。

Certified Programming with Dependents Types这一章似乎建议我使用inversion，但我收到一条错误消息。

我目前正在阅读《软件基础》一书。当定理被定义时，我经常看到我认为连词更有意义的含义链。例如，在定义鸽巢原则时，作者写道：

如果它看起来更像这样，这个定义对我来说会更有意义：

为什么第一个版本是正确的？为什么连词不更合适？

这只是一个例子。更一般地说，我在问为什么在 coq 中似乎回避连词以支持含义链。

之前，我能够证明forall nat1: Nat, Trim nat1 -> Trim (pred nat1)的以下定义pred。

但是用下面的新定义pred我不知道如何证明forall nat1: {nat2: Nat | Trim nat2 /\ Pos nat2}, Trim (pred nat1)。

有人可以给我一个提示吗？我不知道用sig. 或者，也许我做错了什么。我不知道。完整的代码在这里。之前的代码在这里。