L'uguaglianza è decidibile su qualsiasi tipo di tipo coinduttivo?

Question

questo è il mio primo post, mi scuso se ho commesso degli errori.

Sospetto che, in Coq, tipi di tipo coinduttivo come Stream non abbiano uguaglianza decidibile. Cioè, dati due flussi s e t, non è possibile identificare se s = t o ~ (s = t). Sospetto che questo sia vero per tutti i tipi di coinduzione in Coq.

Un rapido google e la ricerca attraverso lo scambio di stack non rivela alcuna conferma. Qualcuno può confermare questo o correggermi?

Answer 1

Penso che tu abbia ragione. Per quanto ne sappia, non puoi nemmeno dire correttamente che cosa significhi per due stream essere uguali, dal momento che implicherebbe che puoi controllarli in un tempo finito, ma sono termini infiniti.

cosa si potrebbe fare, è stato che ogni finita ispezione dei tuoi termini di co-induttiva sono gli stessi, o definire una nozione "co-induttiva" di uguaglianza, proprio come si è fatto nella libreria standard:

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