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

Question

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

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

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

score 5 · Accepted Answer

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

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

1 回答 1