问题标签 [coinduction]

我正在尝试编写一个 Coq 函数，该函数接受 aStream和一个谓词，并以 a 的形式返回list该属性所包含的流的最长前缀。这就是我所拥有的：

但是当我尝试用这个函数进行计算时，我得到了一个非常大的术语，所有的定义都被扩展了。我不知道为什么，但我猜 Coq 不愿意展开共归纳Stream论证。这是一个例子：

鉴于此，该命令Eval compute in take_while (fun s => lt_dec (hd s) 5) (nats 0) (increasing_nats 0 5)会导致一个非常大的术语，正如我上面提到的。

谁能给我一些指导？

在 Prolog 中，统一X = [1|X]是获得无限列表的明智方法吗？SWI-Prolog 没有任何问题，但 GNU Prolog 只是挂起。

我知道在大多数情况下，我可以将列表替换为

但我的问题是明确地是否可以X = [1|X], member(Y, X), Y = 1在“理智的”Prolog 实现中使用该表达式。

Morte旨在用作超级优化功能程序的中间语言。为了保持强归一化，它没有直接递归，因此，列表等归纳类型表示为折叠，而无限列表等传导类型表示为流：

我想enumFromTo在 Morte 上重写 Haskell，这样：

归一化为：

那可能吗？

我试图在 Coq的“Practical Coinduction”中证明第一个例子。第一个例子是证明无限整数流上的字典顺序是可传递的。

我无法制定证明来绕过Guardedness 条件

这是我到目前为止的发展。首先是无限流的通常定义。然后定义字典顺序称为lex。最后是传递性定理的失败证明。

这是我要证明的引理。我从准备目标开始，这样我就可以应用构造函数，希望最终能够使用cofix.

我该如何从这里开始？感谢您的任何提示！

• 编辑

感谢亚瑟（一如既往！）有帮助和启发性的回答，我也可以完成证明。我在下面给出我的版本以供参考。

我使用cons_ht引理来“扩展” s1and的值s3。lex这里 (with headand )的定义tail更接近于Practical Coinduction中的逐字表述。Arthur 使用了一种更优雅的技术，它使 Coq 自动扩展值 - 更好！

我在用：

我定义了以下CoInductive类型stream：

然后，我尝试定义以下CoFixpoint定义zeros：

但是，我收到了以下错误：

我发现我必须显式实例化变量A：

为什么 Coq 不A自己推断类型？我如何让它推断出的类型A？

I've been writing something similar to a Stream. I am able to prove each functor law but I can not figure out a way to prove that it's total:

Gives:

Is there a trick to proving the functor laws over codata which also passes the totality checker?

下面的代码在 Haskell 中是完全可以的：

Agda 中的类似代码无法编译（终止检查失败）：

a使用的定义在a结构上不是更小，因此是循环。似乎终止检查器不会查看dh.

我试过使用 coduction，设置选项--termination-depth=4- 没有帮助。{-# NO_TERMINATION_CHECK #-}在块内插入会有所mutual帮助，但它看起来像作弊。

有没有一种干净的方法可以让 Agda 编译代码？Agda 的终止检查器是否有一些基本限制？

这是我的第一篇文章，如有错误请见谅。

我怀疑，在 Coq 中，像 Stream 这样的协约类型没有可判定的相等性。也就是说，给定两个流 s 和 t，不可能确定是 s=t 还是 ~(s=t)。我怀疑 Coq 中的所有共归纳类型都是如此。

通过堆栈交换快速谷歌和搜索不会显示任何确认。任何人都可以确认或纠正我吗？

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

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'从不直接或间接使用递归。漂亮，不是吗！

Isabelle 中的这个（修剪掉的）核心递归函数定义

产量

但如果我进一步简化为

有用。

我也尝试使用解构视图，即

现在我收到一条不同的错误消息：Invalid map function at "case undefined of Reg c ⇒ tree Γ v |`| undefined".

可能是什么原因？

使用其他case表达式它可以工作，我没有在文档中找到任何提及限制（数据类型文档中的第 5.1.1 节。）