The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Hello,

It's a bit difficult to say with precision what is "wrong" with coinductive types in Coq. It gets a tad philosophical I guess. They are somewhat too powerful to be correct, that's about clear. One theory, which I personnally advocate, is that the trouble is dependent pattern matching on coinductive type, which tells, in the case of streams "a stream necessarily starts with a 'cons' ". Which is not entirely true (not every streams are convertible to a stream starting with a cons, probably very few one would build actually), but because of dependent pattern matching, it is actually a provable fact (forall s:stream, exists a, exists s', s = cons a s'). A variant fact by the way is that which allows to cheat type preservation (if I remember correctly).

So generally speaking, and according to this point of view, dependent pattern matching is what one should avoid when using CoInductive types. Bisimilarity dependent doesn't require dependent pattern matching. I'd say you're safe using it.

It is by the way partly because of the above rational that the "record" syntax for coinductive was added to Coq v8.2 (though it also exists for inductive types). My suggestion would be as follows :

- Streams (and generally coinductive types) should be defined something along the lines of :
CoInductive Stream (A:Type) := { hd : A ; tl : Stream A }

- Do not use destruct or case or intros [ ] or whatever similar on a string object

And you will not run into the strange corner cases.




Arnaud Spiwack

2009/4/30 Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>

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