Czy równość jest rozstrzygalna w przypadku dowolnego typu koindukcyjnego?

Question

to jest mój pierwszy wpis, przepraszam, jeśli popełniłem błędy.

Podejrzewam, że w Coq typy koindukcyjne, takie jak Stream, nie mają decydującej równości. Oznacza to, że biorąc pod uwagę dwa strumienie s i t, nie jest możliwe określenie, czy s = t czy ~ (s = t). Podejrzewam, że dotyczy to wszystkich typów indukcyjnych Coq.

Szybkie wyszukiwanie google i wyszukiwanie za pomocą stosu nie ujawnia żadnego potwierdzenia. Czy ktoś może to potwierdzić lub poprawić?

Answer 1

Myślę, że masz rację. Zgodnie z moją wiedzą, nie można nawet poprawnie stwierdzić, co to znaczy, że dwa strumienie są równe, ponieważ oznaczałoby to, że można je kontrolować w skończonym czasie, ale są one nieskończonymi terminami.

Co można zrobić, to stan, że każdy skończony inspekcję swoich współpracowników-indukcyjny względem są takie same, lub zdefiniować „współ-indukcyjny” pojęcie równości, podobnie jak to się robi w bibliotece standardowej:

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