问题标签 [logical-foundations]

我正在使用在线书籍“软件基础”来了解 Coq。

第二章要求证明“plus_assoc”定理：

我利用了两个先前证明的定理：

我在 n 上使用归纳法证明了 plus_assoc 定理：

此时，上下文（*）为：

我想用 plus_comm 来获取

然后加上_n_sm

然后又是 plus_n_sm

并使用 plus_comm 完成证明两次然后 reflexivity

小问题是我不知道如何将 plus_comm 应用于 (S n' + m)。

最大的问题是：为什么要发行

立即完成证明（在给定的上下文 (*) 中）？

提前感谢您的任何澄清！

法比安·皮克

这是我对回文的归纳定义：

我想证明的定理来自软件基础：

我对证明的非正式概述如下：

假设l0是一个任意列表，使得l0 = rev l0. 那么以下三种情况之一必须成立。l0有：

(a) 零元素，在这种情况下，根据定义它是回文。

(b) 一个元素，在这种情况下，根据定义，它也是一个回文。

(c) 两个或更多元素，在这种情况下l0 = x :: l1 ++ [x]，对于一些元素x和一些列表l1，使得l1 = rev l1.

现在，既然l1 = rev l1，以下三种情况之一必须成立......

递归案例分析将终止任何有限列表l0，因为分析的列表的长度通过每次迭代减少 2。如果它终止于任何 list ln，则它的所有外部列表l0也是回文，因为通过在回文的任一端附加两个相同元素构造的列表也是回文。

我认为推理是合理的，但我不确定如何将其正式化。它可以在 Coq 中变成证明吗？对所使用的策略如何起作用的一些解释将特别有帮助。

我试图apply ... with ...从 Pierce 的“软件基础”中运行一些简单的策略示例。

看来书中的例子对我不起作用：

trans_eq_example'失败并出现错误：

关于 Coq 版本的附加信息：

我该如何解决这个错误？

我正在研究软件基础并遇到错误。

错误：术语“true”的类型为“bool”，而预期的类型为“Datatypes.bool”

为下面的证明。

我发现当我使用Require Import Omega. 对环境中引入
的内容有任何提示、建议或解释吗？Omega

我一直在阅读 Benjamin Pierce 等人的Software Foundations的第 1 卷，并且在 IndProp 一章中遇到了几个问题。不幸的是，我不知道有更好的地方问：有人有任何提示吗？

这些是在线教科书中的练习；请不要提出解决方案。但是有一个地方开始会很有帮助。

我正在研究软件基础并得到了这个例子：

并对这意味着什么感到困惑。例如，我们得到：

或者

第二还是第一？

特别是我试图理解：

“软件基础”中有一个练习，我一直在尝试正确解决一段时间，但实际上我在尝试写下所要求的功能方面遇到了困难。这是练习的相关部分

考虑使用二进制而不是一元系统的自然数的不同、更有效的表示。也就是说，与其说每个自然数要么是零要么是自然数的后继，我们可以说每个二进制数要么是

• 零，
• 二进制数的两倍，或
• 一个二进制数的两倍多。

(a) 首先，写出对应于二进制数描述的类型 bin 的归纳定义。

幼稚的定义不太适用，因为您最终能够构建将 1 加到已经加了 1 的数字或无缘无故地将 0 乘以 2 的术语。为了避免那些我想我会在构造函数中编码某种状态转换以避免这些，但这有点棘手所以这是我能想到的最好的

通过上述表示，我避免了没有意义的术语问题，但现在每当我乘以 2 时我都必须携带证明。我实际上不知道如何在递归函数中使用这些东西。

我知道如何构建证明和术语，它们看起来像这样

我还可以写下我想要对应于函数的定理的“证明”，但我不知道如何将其实际转换为函数。这是转换函数的证明

我知道这个术语是我想要的函数，因为我可以验证当我用它计算时我得到了正确的答案

所以最后的问题是，有没有一种简单的方法可以以简单的方式将上述证明项转换为实际函数，还是我必须尝试对证明项进行逆向工程？

我正在通过 coq 课程“逻辑基础”。解决问题：

具有较少或相等的功能：

创建“小于”功能：

据我了解，它应该像这样工作：

我创建了这个：

但它不起作用 - 输出：“错误：此子句是多余的。” 对于该行：

请帮忙。

我正在通过逻辑基础课程并被困在基础知识的最后一个练习中：

让二进制数将转换器写入它的一元表示：

我用 C 中的递归函数解决了这个问题。唯一的事情是，我使用“0”而不是“A”和“1”而不是“B”。

我现在的问题是如何在 coq 中编写这段代码：

我是 Coq 的新手，目前正在阅读 Software Foundations 系列教程。

然而，我一直发现自己Require Export在第一次尝试时很难让零件工作，每个文件似乎都需要一个新的策略才能工作。然而，这一次，我完全被困住了。

在一个文件（Lists.v）中，我可以简单地编写 From LF Require Export Induction.，并且让它工作得很好。

在下一个（Poly.v）中，我根本无法加载 Lists 模块，

除非我先将加载路径添加到当前文件夹：

但是，在下一章中，似乎没有任何效果。

这是我尝试过的：

可以肯定地说：我在这里不知所措，我不知道我在做什么或为什么它不起作用。它以前有效，我在网上找不到任何东西似乎可以给出任何好的答案。

我的 _CoqProject 文件包含-Q . LF

我在 Windows 和 Mac 上都遇到了这个问题。

我正在使用最新版本的 CoqIDE。