coq - 是否可以在任何共归纳类型上确定相等性？

Question

这是我的第一篇文章，如果我犯了错误，请道歉。

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

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

Answer 1

我想你是对的。据我所知，您甚至无法正确说明两个流相等的含义，因为这意味着您可以在有限时间内检查它们，但它们是无限项。

你可以做的是，声明对你的共归纳项的任何有限检查都是相同的，或者定义一个“共归纳”的平等概念，就像在标准库中所做的那样:

https://coq.inria.fr/library/Coq.Lists.Streams.html