The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Keiko Nakata wrote:
> Hello,
>
> Are there any potentially bad consequences of having 
> "Add Relation sequence bisimilar", 
> where sequence and bisimilar are defined coinductively, 
> i.e. infinite lists and the bisimilar relation on them?
>
> I am aware of an issue concerning type preservation discussed: 
>
> http://logical.saclay.inria.fr/coq-puma/messages/b35593715e6cbad3#msg-b35593715e6cbad3
>
> I also remember someone told me that he suspect that there might be
> some bad interactions between Coq's criterion of guardedness and Setoids.
>
> I was thinking if, with "Add Relation sequence bisimilar", 
> any predicate on sequences will not distinguish bisimilar lists; 
> this sounds interesting to me.
>
> Best regards,
> Keiko
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>   
I don't know if this is relevant, but Christine Paulin has a development 
where she uses streams and and coinductive relations in the framework of 
setoids.  You can have a look at it by following these links:

http://www.lri.fr/~paulin/PUBLIS/paulin07kahn.pdf
http://www.lri.fr/~paulin/KahnNetworks/library.pdf
http://www.lri.fr/~paulin/KahnNetworks/HTML/all-gal.html
http://www.lri.fr/~paulin/KahnNetworks/kahn-networks.tgz

I hope this helps,

Yves