Является ли равенство разрешимым на любом типе коиндуктивности?

Question

Это мой первый пост, извиняюсь, если я допустил ошибки.

Я подозреваю, что в Coq коиндуктивные типы, такие как Stream, не имеют разрешимого равенства. То есть, учитывая два потока s и t, невозможно определить, является ли s=t или ~(s=t). Я подозреваю, что это верно для всех коиндуктивных типов в Coq.

Быстрый гугл и поиск через стек обмена не дают никакого подтверждения. Кто-нибудь может подтвердить это или исправить меня?

Answer 1

Я думаю, вы правы. Насколько я знаю, вы даже не можете правильно заявить, что означает, что два потока равны, поскольку это может означать, что вы можете проверять их за конечное время, но они являются бесконечными терминами.

Что вы могли бы сделать, это заявить, что любая конечная проверка ваших коиндуктивных терминов одинакова, или определить "коиндуктивное" понятие равенства, как это делается в стандартной библиотеке:

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