问题标签 [induction]

对于我的计算理论课，我们应该做一些复习/练习题来消除生锈并确保我们为课程做好准备。其中一些问题是归纳证明。我曾经这样做过，但显然它已经完全逃脱了我。我看过几个教程，但仍然不能做问题'a'。如果有人能引导我解决第一个问题，我很确定我可以自己解决第二个问题。任何帮助，将不胜感激！

我如何通过归纳来解决这个问题？

假设给你一个算法作为一个黑盒子，你看不到它是如何设计的，它具有以下属性：如果你输入任何实数序列和一个整数 k，算法将回答 YES 或 NO，指示是否存在子集总和正好为 k 的数。展示如何使用这个黑盒来找到给定序列 {X1, ...., Xn} 的子集，其和为 k。您可以使用黑盒 O(n) 次。

任何想法？

假设我有

• T型
• 有根据的关系 R：T->T->Prop
• 函数 F1：T->T 使参数“更小”
• 条件 C：T->Prop 描述 R 的“起始值”
• 函数 F2：T->T 使参数“更大”

如何使 Fixpoint 看起来与此类似：

以及如何使战术“归纳”（或类似）的以下用法成为可能：

我尝试使用 nz 类型来做到这一点：{n:nat | n<>O}（查看 Certiified Programming with Dependent Types 的第 7.1 章），但仅此而已：

我无法理解进一步发生了什么，因为这对我来说太复杂了。

PS 正如我所见——对于初学者来说，关于 Coq 中的一般递归和归纳的教程还不够好。至少我能找到。:(

基本上，我想证明以下结果：

这就是所谓的双重归纳的递归方案。

我试图两次应用归纳来证明它，但我不确定我会以这种方式到达任何地方。确实，我当时就卡住了：

我正在使用一个搜索一系列值的函数。

我希望能够对这个功能进行推理。

但是，我似乎无法让 coq 的内置感应原理工具工作。

看起来 coq 是为处理相互递归而不是嵌套递归而设置的。在这种情况下，我基本上有 2 个嵌套的 for 循环。

然而，翻译成相互递归也不是那么容易：

但这会产生错误

对内部的递归调用具有等于“ n + n”而不是“ i1”的主要参数。

所以，看起来我需要使用 measure 让它直接接受定义。我有时会重置 j 很困惑。但是，在嵌套设置中，这是有道理的，因为 i 减少了，而 i 是外循环。

那么，有没有一种处理嵌套递归的标准方法，而不是相互递归？有没有更简单的方法来推理这些案例，而不涉及制作单独的归纳定理？由于我还没有找到自动生成它的方法，我想我还是坚持直接写归纳原理。

我正在尝试为明天的测试学习归纳证明。我试图理解书中问题的解决方案，但我的数学有点生疏。有人可以解释这些都是平等的吗？我不明白如何从第一个方程中找到最后一个方程。

n(n+1)/2 + (n+1) = n(n+1) + 2(n+1)/2 = (n+1)(n+2)/2

我想知道这种归纳证明的变体是否正确

归纳的标准证明表明，如果一个方程/算法适用于 n，并且您可以证明它适用于 n+1，那么您可以假设它适用于每个大于或等于 n 的整数。

现在，如果你有 2 个基本情况（例如：2 和 3）并且你要证明它适用于 n+2，你能说它适用于每个大于 2 的整数吗？

因为假设你可以证明它对 n+2 是正确的，

等等，所以你覆盖了每个大于 2 的整数

谢谢你的帮助^^

（如果+2版本是正确的，这意味着如果你有m个连续的基本情况并且证明它适用于n+m，那么它将适用于每个大于n的整数）

我想知道最长公共子序列问题的一个特例 http://en.wikipedia.org/wiki/Longest_common_subsequence_problem 如果我们有两个 n 符号字符串，并且保证它们都只有 1 个符号并且每个符号来自字母表的前 n 个符号。普通算法如何改进？

尝试对函数的结果（返回归纳类型）执行案例分析时，我在 Coq 中遇到了一些麻烦。当使用通常的策略时，如elim, induction,destroy等，信息会丢失。

我举个例子：

我们首先有一个这样的函数：

现在，假设我们正处于证明特定定理的这一步：

当我应用一种策略时，比如说，induction (f n)，会发生这种情况：

但是，我想要的是这样的东西：

在它实际工作的方式中，我丢失了信息，特别是我丢失了关于f n. 在我处理的问题中，我需要使用f n = true或的信息，f n = false与其他假设一起使用，等等。有没有办法做第二个选项？我尝试使用类似的东西，cut(f n = false \/ f n = true)但它变得非常烦人，特别是当我连续有几个这样的“特殊”感应时。我想知道是否有一些基本上与cut上述完全一样的东西，但策略/证据较少

我试图证明将函数 f 应用于两个列表的每个元素会产生相似的rel_list列表，如果它们最初是相关的。我rel在列表的元素上有 a 并且已经证明了一个引理Lemma1，即如果两个元素在 中rel，那么在rel函数 f 应用于两个元素之后它们就在。我尝试对列表进行归纳，rel_list但在基本情况解决后，我最终得到类似情况xL :: xL0 :: xlL0 = xL0 :: xlL0或进入循环。请有人建议我如何关闭证明。谢谢，