问题标签 [induction]

I have just run into the issue of the Coq induction discarding information about constructed terms while reading a proof from here.

The authors used something like:

to rewrite a hypothesis H before the actual induction induction H. I really don't like the idea of having to introduce a trivial equality as it looks like black magic.

Some search here in SO shows that actually the remember trick is necessary. One answer here, however, points out that the new dependent induction can be used to avoid the remember trick. This is nice, but the dependent induction itself now seems a bit magical.

I have a hard time trying to understand how dependent induction works. The documentation gives an example where dependent induction is required:

I can verify how induction fails and dependent induction works in this case. But I can't use the remember trick to replicate the dependent induction result.

What I tried so far to mimic the remember trick is:

But this doesn't work. Anyone can explain how dependent induction works here in terms of the remember-ing?

任何归纳类型都是这样定义的

induction有类型(f a -> a) -> Ind f -> a。这有一个双重概念，称为共导。

coinduction有类型(a -> f a) -> a -> CoInd f。注意induction和coinduction是如何对偶的。作为归纳和共归纳数据类型的示例，请查看此函子。

没有递归，Ind StringF是一个有限字符串，CoInd StringF是一个有限或无限字符串（如果我们使用递归，它们都是有限或无限或未定义的字符串）。一般来说，可以转换Ind f -> CoInd f为任何 Functor f。例如，我们可以将函子值包裹在一个协约类型周围

Maybe此操作为每个步骤添加了一个额外的操作（模式匹配）。这意味着它会产生O(n)开销。

我们可以对Ind f和使用归纳wrap法来得到CoInd f。

这是O(n^2). （获得第一层是O(1)，但第 n 个元素是O(n)由于嵌套Maybe的 s 造成的，因此是O(n^2)总数。）对偶，我们可以定义cowrap，它采用归纳类型，并显示其顶部 Functor 层。

induction总是O(n)如此，如此如此cowrap。

我们可以使用和来coinduction生产。CoInd fcowrapInd f

每次我们获得一个元素时都会再次出现这种情况O(n)，总共O(n^2).

我的问题是，不使用递归（直接或间接），我们可以及时Ind f转换吗？CoInd fO(n)

我知道如何使用递归（先转换为Ind f，然后Fix f再转换Fix f为CoInd f（初始转换为O(n)CoInd fO(1)O(n)O(n) + O(n) = O(n)

观察这一点convert，convert'从不直接或间接使用递归。漂亮，不是吗！

我必须通过归纳证明

在哪里 ：

所以，我认为以下是我的假设和我的主张：

我开始尝试证明基本情况（空列表）：

但是我不确定它是否正确，因为我已经证明它们都是 True 而不是如果左边部分是 True 而第二部分是 False，那么暗示是 False （即 ==> 的定义）。这个对吗？我怎样才能继续证明？我不清楚如何使用归纳来证明含义...

先感谢您！

以下是我已经做过的作业，但做错了。我不明白为什么解决方案就足够了。（经过一周的阅读和谷歌搜索后，我转而询问。）

该示例类似于 Hutton 关于 Haskell 的书中使用的示例。

我看不到的是为什么允许感应箱在它停止的地方停止。它使用假设，然后取消应用添加以生成作为归纳案例假设版本的东西。

换句话说，另一个版本的假设是通过假设假设成立而产生的。

足够了？当我找到一个可行的假设时，我是否总是将假设视为有效？对于归纳案例，如果我可以通过假设假设本身已经被证明来生成应用于归纳案例的假设版本就足够了？

我很难将感应从数字转移到功能。请不要让我愚蠢地死去。谢谢。

COQ 中的一个证明陈述如何类似于以下一个。

或者，假设您有一个给定的数字列表，并且您想证明没有数字在该列表中出现两次。

也许必须编写一个以引理为类型的算法。但我不知道如何做到这一点。

顺便说一句，这不是家庭作业。

如果我有这样的谓词：

然后我可以简单地使用归纳法来证明一些虚拟引理：

但是，对于具有产品类型参数的谓词：

几乎相同引理的类似证明被卡住了，因为所有关于变量的假设都消失了：

为什么会这样？如果我用 替换induction，inversion那么它的行为符合预期。

引理仍然可以证明，induction但需要一些解决方法：

不幸的是，这种方式的证明变得非常混乱，并且对于更复杂的谓词是不可能遵循的。

一个明显的解决方案是这样声明bar：

这解决了所有问题。然而，就我的目的而言，我发现以前的（“元组”）方法更加优雅。有没有办法保持谓词不变并且仍然能够进行可管理的归纳证明？问题甚至来自哪里？

老实说，我对数学归纳的了解如下：

这是我现在正在努力解决的归纳问题的图像（请点击）

我目前正在尝试从上图中解决问题，但我做不到。我刚接触这种东西，我不知道，我也无法从我仅有的一点知识中推断出任何东西。

我不知道如何开始，我也不知道如何将我上面描述的小知识应用到那个问题上。

如果您能通过仔细的解释帮助我解决上述问题，非常感谢您。

我如何进行归纳以建立陈述moll n = doll n，与

我试图证明 n = 0 的基本情况

现在n+1，证明

但是现在呢？我怎样才能进一步简化它？

我一直在研究 Dafny 中引理的使用，但发现很难理解，显然下面的示例无法验证，很可能是因为 Dafny 没有看到归纳法或类似引理的东西来证明计数的某些属性? 基本上，我不知道我需要如何定义或定义什么来帮助说服 Dafny 计数是归纳性的等等。一些确保和不变量规范不是必需的，但这不是重点。顺便说一句，这在 Spec# 中更容易。

给定以下功能：

证明以下性质：

• foo (foo xs ys) zs = foo ys (xs@zs)

到目前为止，我已经完成了基本案例和归纳案例，但不知道如何开始证明：

基本情况：

• foo (foo [] ys) zs = foo ys ([]@zs)
• foo ys zs = foo ys zs

归纳案例：

• foo (foo (x::xs) ys) zs = foo ys ((x::xs)@zs)