Is equality decidable on any coinductive type?

Question

this is my first post, apologies if it I have made mistakes.

I suspect that, in Coq, coinductive types like Stream do not have decidable equality. That is, given two streams s and t, it is not possible identify whether s=t or ~(s=t). I suspect that this is true of all coinductive types in Coq.

A quick google and search through stack exchange does not reveal any confirmation. Can anyone confirm this or correct me?

Answer 1

I think you are right. To the best of my knowledge, you can't even correctly state what it means for two streams to be equal, since it would imply that you can inspect them in finite time, but they are infinite terms.

What you could do, is state that any finite inspection of your co-inductive terms are the same, or define a "co-inductive" notion of equality, much like it is done in the standard library:

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