Mit*_*ley 5 coq decidable coinduction
这是我的第一篇文章,如果我犯了错误就道歉.
我怀疑,在Coq中,像Stream这样的共同类型没有可判定的平等.也就是说,给定两个流s和t,不可能识别s = t或〜(s = t).我怀疑Coq中的所有共同类型都是如此.
快速谷歌和搜索堆栈交换不会透露任何确认.谁能证实这一点或纠正我？
我想你是对的。据我所知，您甚至无法正确说明两个流相等的含义，因为这意味着您可以在有限时间内检查它们，但它们是无限项。
你可以做的是，声明对你的共归纳项的任何有限检查都是相同的，或者定义一个“共归纳”的平等概念，就像在标准库中所做的那样：
https://coq.inria.fr/library/Coq.Lists.Streams.html