问题标签 [logical-foundations]

我正在通过逻辑基础课程并面临以下错误：

未定义的字符串

Lists.v，代码：

回复：

错误：在当前环境中找不到引用字符串。

在我添加Require Import String.到文件的开头后，错误消失了。但为什么我需要这样做？我想，该课程必须按原样进行。

警告错误

代码：

回复：

错误：没有选项警告。

我无法修复它。

空列表“[]”符号未定义错误

在文件 Logic.v

[] 错误：

语法错误：在 '<>' 之后需要 [constr:operconstr]（在 [constr:operconstr] 中）。

我无法修复它。

怎么了？请帮忙。

Poly 模块中有 4 个与教堂数字相关的练习：

据我了解，cnat 是一个接受函数 f(x) 的函数，它是参数 x 并返回它的这个参数的值：f(x)。

然后有 0、1、2 和 3 的 4 个示例以教会符号表示。

但是如何解决这个问题？我知道我们必须再次应用该功能。cnat 返回的值将作为参数。但是如何编码呢？使用递归？

更新

我试过这个：

试图解决 eqb_trans 我卡住了：

显然，我们应该使用 eqb_true 来解决它：

此时我们有：

现在我想在目标上使用 eqb_true ：

但是在这里我们得到一个错误：

为什么它不起作用？怎么修？

这是我到目前为止得到的：

在这里我被困住了。归纳假设有什么特别值得我注意的？

试图从逻辑章节中解决 In_app_iff excersize 我来到了这个怪物：

这是我最后得到的：

我怎样才能从中得到H12事实IHl呢In a (t ++ h' :: t')？

因为 H12 处于析取状态。并且足以推断结论。

apply H12 in IHl.不起作用。

请帮忙。

这是书中的代码：

Aftersimpl. In转换为 3 个元素的析取：

但我完全不明白如何阅读：

它产生了这个：

我的理解：

1. 它将 n fromforall放入上下文中。
2. 它将 3 个元素的析取分解为 2 个子目标，忽略 False：
3. 根据拆分的数量创建了 2 个子目标。

底部还有一个提示：

En passant（法语：[ɑ̃ paˈsɑ̃]，点燃。顺便说一句）是国际象棋中的一步。这是一种特殊的棋子捕获，只能在棋子从其起始格移动两个格子后立即发生，并且如果它只前进一个格子就可能被敌方棋子捕获。

看着这个：

有人可以解释一下吗：

1. 这种形式的命令应该用于破坏forall吗？这个任务还有别的吗？
2. 如何用英文阅读这个命令？
3. 为什么要[H | []]放在另一对括号中？
4. 如何[]告诉 coq 忽略 False 语句？
5. 一般什么时候应该使用这个命令？

我面临一个非常奇怪的问题：coq 不想将 forall 变量移动到上下文中。

在过去，它是这样的：

它生成：

但是当我们在 forall 里面有 forall 时，它就不起作用了：

在此之后我们得到：

但是如何将 x 移出 H 并将其分解成更小的部分？我试过了：

但它给出了一个错误：

它是什么？怎么修？

这是任务：

从 [In] 中汲取灵感，编写一个递归函数 [All]，说明某个属性 [P] 包含列表 [l] 的所有元素。为确保您的定义正确，请证明下面的 [All_In] 引理。（当然，您的定义不应该只是重述 [All_In] 的左侧。）

In是这样定义的：

起初我All以类似的方式定义：

但后来我认为这是不正确的，因为连词末尾的 False 总是会给出 False。

如果列表的最后一个 nil 元素不为空，我们需要忽略它（这不起作用，只是一个想法）：

错误，我不知道如何解决：

错误：术语“l' = []”的类型为“Prop”，它不是（共）归纳类型。

然后我回到第一种情况：

并尝试证明 All_In 定理：

现在我们被困住了：

因为我们在结论中有 False，但前提中没有 False 假设，整个陈述都是谎言。

1. 如何正确定义All？
2. 我的证明有什么问题？

在逻辑章节中，介绍了反向列表函数的尾递归版本。我们需要证明它可以正常工作：

但在证明之前，我想证明一个引理：

我在这里卡住了：

接下来做什么？

我在这里卡住了：

我们可以使用归纳假设将 (double k) 重写为 n'，也可以对目标使用注入，然后应用归纳假设。

但我不能做这些，因为exists。

rewrite <- IHn'给出：

错误：找不到要重写的同类关系。

injection给出：

错误：Ltac 调用“注入”失败。不是否定的原始平等。

该怎么办？