问题标签 [induction]

我正在写一门关于函数式编程的课程，课程中的一个模块涵盖列表，另一个模块涵盖树。这两个模块都以对这些数据类型的递归和归纳为中心。我正在寻找一些涵盖这些主题的材料，以便将其作为课程参考书目的一部分。

任何人都可以链接到一个好的资源（最好是一本书），我可以在其中找到这些主题的解释吗？

为便于理解而编辑

我试图证明一种特殊类型树的属性。这棵树如下所示。问题是 Coq 生成的归纳原理不足以证明树的属性。举一个更简单的例子，假设以下类型描述了我所有的“树”：

然后，为了证明所有树的健全性（例如，蕴涵），我需要证明以下引理：

为此，我需要对树的结构进行归纳。但是，如果我这样做了，intros;induction H.那么第一个子目标(E,G,R |= f --> g)就是丢失 f 和 g 所需结构的信息（我想要(E,G,R |= a --> a)）。（此外，对于归纳情况，归纳假设状态(E,G,R |= f --> g)，这对我来说似乎很奇怪）。

我尝试过的另一种方法是记住(G |- f ---> g)，以保持 f 和 g 的结构可用。然后，证明继续进行，intros;remember (G |- f --> g) as stmt in H.induction H.然后，我获得了我对基本案例所期望的目标和环境。但是，为了证明案例 TRA，我获得了以下证明上下文：

虽然我希望归纳假设是

旧文本

我试图证明一种特殊类型树的属性。这棵树可以使用 21 种不同的规则来构建（我不会在这里全部重复）。问题是 Coq 生成的归纳原理不足以证明树的属性。

树的构造如下

这些构造函数之一是

我的目标是证明

为此，我记得makeStatement G f g，否则我会丢失有关 f 和 g 结构的信息。然后我在树上应用归纳。我已经证明所有案例都是单独的引理，我可以成功地将其用于基本案例。然而，对于归纳案例，Coq 提供给我的归纳假设是不可用的。

例如，对于前面提到的 CTX 构造函数，我得到如下归纳假设：

我不能使用。相反，我想要类似的东西

有人可以向我解释如何解决这个问题吗？到目前为止，我已经尝试在 prv_tree 上定义自己的归纳原理，但是这会导致相同的问题，所以也许我做错了？

我自己的归纳原理中对 CTX 的表述如下：

这是给我的练习之一，我在对 l 进行归纳后几乎立即卡住了。我不知道这里还有什么其他断言。

我不允许使用自动、直觉等高级策略。

我们刚刚开始在课堂上学习 prolog，我们的第一个练习如下：

问题：

注意：假设只有两个原子，例如 a 和 b，而不是无限多个。

a) 编写一个prolog 程序，翻译命题逻辑公式的归纳定义（即翻译定义1）。为此，您需要使用：

1.) 一元谓词“at”表示原子公式（因此“at(f)”表示“F 是原子公式”，其中 f 是常数）。

2.) 表示公式的一元谓词“fmla”（因此“fmla(F)”表示“F 是一个公式”）。

3.) 一元运算“neg”表示否定（因此“neg(F)”代表 ¬F）。

4.）二元运算“或”表示两个公式的析取（因此“或（F，G）”代表（F∨G））。

试图：

有效公式示例：(~A v B) ---> or(neg(a), b)。

我相信我构建程序的方式是正确的，但递归部分不起作用（我在那里也遇到了单例错误）。我试图解决这个问题几个小时但无济于事。任何帮助，将不胜感激。

我有一个数组“line”，其中包含一个长度为“l”的字符串，还有一个数组“nl”，其中包含一个长度为“p”的字符串。注意：“l”和“p”不一定是每个对应数组的长度。参数“at”将是在“line”内进行插入的位置。恢复：长度为“p”的数组将插入“line”，将“line”的所有字符在位置（at，i，at+p），'p'位置之间向右移动以进行插入。

我的确保逻辑是检查插入“line”中的元素是否具有相同的顺序并且是否与“nl”中包含的字符相同。

这是代码：

这是 我收到的错误。

谢谢。

我正在使用 Dafny 制作一个删除方法，您会收到：

• 字符数组line

• 数组的长度l

• 一个位置at

• 要删除的字符数p

首先从 at to 删除 line 的字符at + p，然后必须移动at + pto右边的所有字符at。

例如，如果您有[e][s][p][e][r][m][a], and at = 3, and p = 3, 那么最终结果应该是[e][s][p][a]

我试图证明一个有意义的后置条件，例如：

ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]);

确保 at + p 右侧的所有字符都在新位置。

但是 Dafny 输出两个错误：

索引超出范围 7 53

后置条件可能不会在此返回路径上成立。19 2

这是rise4fun上的程序

问题：

证明 ifbasecase p和indstep p, 那么forAllNat p

我不明白的是，如果basecase p和indstep p，那么当然forAllNat p应该是True。

我认为basecase p说那P(0)是真的， indstep p说那P(Succ n)是P(n+1)真的而且我们需要证明那P(n)是真的。我对吗？关于如何做到这一点的任何建议？

我有：T(n) = T(n/2) + T(n/4) + T(n/8) + cn；c > 0。

这是我的归纳步骤：想证明 T(n) 在 O(n) 中，即一些 d > 0 和 n0 使得每个 n > n0 和 T(n) < dn

T(n) = T(n/2) + T(n/4) + T(n/8) + cn <= d(n/4) + d(n/4) + d (n/8) + cn = dn(7/8) + cn = dn(7/8) + cn <= dn ... = 8c <= d

我被基本情况卡住了，但这就是我的老师向我解释的方式：基本情况：需要 n0 足够小以便尝试。尝试 n0 = 8 T(8) = T(4) + T(2) + T(1) + c8 <= 8T(4) + 8T(2) + 8T(1) + C8 < d8

有人可以向我解释基本情况吗？谢谢！

我正在分析不同的方法来查找算法的时间复杂度，并且在尝试通过使用归纳证明来解决这种特定的递归关系时遇到了很多困难。

我的 RR 是：T(n) <= 2T(n/2) + √n

我假设你会假设 n 并证明 n-1？有人可以帮我吗。

我需要通过归纳证明——

在基本案例和归纳假设之后的归纳步骤中，我写道 -

但是为了证明这个运行时间复杂度，我需要证明存在 C,N0 > 0 所以最终的不等式是正确的。

如果有人能告诉我如何找到/或纠正我的归纳。谢谢。