问题标签 [coinduction]

在 Coq 中，联合归纳采用证明 A -> A 的形式受到保护约束，以确保有进展。这个公式很容易出错，因为它看起来就像你一开始就到达了目的地，并且根据证明中的当前状态不容易看到防护性。是否有更接近于通常指定归纳的替代公式，您必须得出与前提不同的结论？

一个例子：

在 cofix 之后，你会得到这个奇怪的状态：

apply f更糟糕的是，如果您尝试使用 Qed 关闭它，它不会检测到错误。

那么，基本上，有没有共同归纳的公式可以尽早发现这个错误，而不是等待整个证明完成并检查警戒性？

I recently decided to fool around with coinduction in Agda, and found the "copattern" machinery to be fairly brittle. I decided to cut to the chase and define M types, which more-or-less generalize all the coinductive types (setting coinduction-recursion aside). My hope was to sidestep the whole copattern mess entirely, but to my surprise, it seems that copatterns aren't capable of handling the M constructor:

produces:

I tried a couple of minor variations, to no avail. Is there an incantation that causes safe agda to accept some variant of M?

For the record, I'm aware that I have a number of options available to me, including:

• turning on --sized-types and indexing M on a size
• turning off --safe and promising the compiler that unroll is productive
• maybe try "old-style coinduction", which may or may not be consistent (?)

I find all of these at least mildly unpalatable, and am surprised that vanilla safe agda cannot handle this case (given that it's the one case that, if handled, leaves the user an escape hatch). Am I missing something?

嗨，我是一个新手，试图学习如何在伊莎贝尔中使用共归纳法。我一直在查看 HOL/Datatype_Examples/Process.thy (Andrei Popescu) 2012。随着 2019 年 Isabelle 的进步很大（而不是因为任何个人技能），我已经简化了证明，但仍然不明白他们为什么决定做第一个步。

工作简化证明是

我失败的天真方法是：

两个问题：

1. 语法 {fix q 假设 "q = solution sys (PROC p)" .....} 是本地引理的旧语法吗？

更重要的是 2. 我怎么知道什么时候尝试这种技术？

非常感谢大卫

我定义了无限流如下：

和一个归纳类型，它表明流中的某些元素最终满足谓词：

我想编写一个函数，它会跳过流的元素，直到流的头部满足谓词。为了确保终止，我们必须知道一个元素最终满足谓词，否则我们可能会永远循环。因此， 的定义Eventually必须作为参数传递。此外，该函数在计算上不应该依赖于Eventually谓词，因为它只是用来证明终止，所以我希望它是一个已删除的参数。

这就是问题所在 - 我想填补定义中的漏洞。从contra范围内，我们知道流的头部不满足P，因此根据最终的定义，流尾部的某些元素必须满足P。如果Eventually在这种情况下没有被删除，我们可以简单地对谓词进行模式匹配，并证明这种here情况是不可能的。通常在这些情况下，我会编写一个已擦除的辅助函数，如下所示：

这种方法的问题在于Eventually证明是结构递归参数 in dropUntil，并且调用这个辅助函数不会通过终止检查器，因为 Agda 不会“查看”函数定义。

我尝试的另一种方法是将上述已擦除函数内联到dropUntil. 不幸的是，我对这种方法也没有运气 - 使用case ... of此处描述的类似定义https://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html也没有通过终止检查器。

我在 Coq 中编写了一个等效的程序，它被接受（使用Prop而不是擦除类型），所以我相信我的推理是正确的。Coq 接受定义而 Agda 不接受的主要原因是 Coq 的终止检查器扩展了函数定义，因此“辅助擦除函数”方法成功了。

编辑：

这是我使用大小类型的尝试，但是它没有通过终止检查器，我不知道为什么。

我一直在用“旧”和“新”方法在 Agda 中处理共归纳法进行一些实验，但我认为我仍然遗漏了一些关于 Agda 在不使用Size时对核心递归函数的终止检查行为的重要事实。

例如，考虑 和 的以下Stream定义repeat：

粗略地说，协约记录类型∞Stream是专门Thunk用于流的。我在很多 Agda 形式化中看到了类似的定义，尽管它们通常被改进为 aSize以获得更好的精度。无论如何，上面的定义repeat被 Agda 接受，没有任何Size注释。

问题是当我尝试将∞Stream记录分解为 aThunk时，以便我可以Thunk在其他地方重用以定义其他可能无限的数据类型：

注意：

• 两种情况下的代码repeat完全相同，
• repeat在每种情况下，都会在构造函数的下方找到递归调用cons，
• 在每种情况下都会repeat产生一个共归纳记录类型的值，

然而 Agda 接受第一个定义repeat但拒绝第二个定义（以下函数的终止检查失败：repeat）。

我知道使用Thunk标准库中的大小可以修改第二个版本，以便被 Agda 接受。尽管如此，我想了解是什么让上面的第一个版本与第二个版本如此不同，以至于它通过了​​终止检查器。在我看来，它们基本相同。

谢谢！

换种说法：如果我们要分别删除终止检查和使用归纳和共归纳数据类型的保护条件，那么归纳/共归纳和修复/共定之间是否会不再存在根本区别？

我所说的“根本差异”是指 Coq 核心演算的差异——而不是语法和证明搜索等方面的差异。

这似乎最终归结为一个关于构造微积分的问题。

注意：我知道一个跳过终止检查/递归/核心递归的保护的定理证明器可以证明——False所以，如果它有帮助，请将其视为关于非完全编程而不是证明的问题。

我有一个简单的惰性二叉树实现：

以及以下属性：

我想证明一个定理，即有限树没有任何无限分支：

...但是在最初的几次战术之后我迷路了。这个假设本身似乎很微不足道，但我什至不能从它开始。这样一个定理的证明会是什么样子？

我可以证明关于互归纳类型的“互归纳原理”吗？例如，流类型的协约原理的伪代码如下所示：

我的感觉是这是正确的，但我想不出在 Coq 或 Agda 中证明它的方法。

我试图证明流谓词（在标准库中定义）的以下原则。

根据我对 施加的句法保护条件的理解cofix，我将永远无法以这种方式完成证明，因为在证明术语中，Cof s必须出现在 下H，它既不是构造函数也不是匹配项等。

在 Coq 中还有其他方法吗？我用pacoForAll定义了一个明确的固定点，并试图证明这个原理，但没有成功（我根本无法实例化）。H

编辑：这个引理是不可证明的，因为False可以从它推导出来P := fun s => False（谢谢 Maëlan）。

我了解如何在 Haskell 中定义同构和异构流。

我们如何将恒定流定义为异构流的特例？如果我尝试定义常量类型流的类型族，则会收到“减少堆栈溢出”错误。我想这与类型检查算法不够懒惰并试图计算整个Constant a类型流有关。

有什么办法可以解决这个问题并定义恒定的异构流？我应该尝试其他类似的结构吗？