The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Hello,

Arnaud Spiwack escribió:
> 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).

That's right. Coq does not ensure the subject reduction property when
using co-inductive types because a term (CoFix f.e) does not simply
reduce to its body e, as this would lead to an infinite chain of
reductions. Instead of this, the only reduction strategy that is
authorized is

match Cofix f.e with .. end --> match e[f<-Cofix f.e] with .. end.

This is what jeopardizes subject reduction in Coq's theory. However,
subject reduction is preserved in a theory adding free expansions of
CoFix, which should be still sound because of the guardedness condition,
but hardly implementable in the traditional way, as you not longer have
"normal forms" (ie, a term which cannot further reduced). All this is
explained in my PhD thesis.

In my personal experience, I never found a "practical case" in which the
proof about co-inductive objects I was searching for remained blocked
for this reason. This is mainly because, even though Cofix f does not
reduce to e[f<-Cofix f.e], you can prove that Cofix f=e[f<-Cofix f.e],
where "=" denotes Coq's propositional equality. Therefore, you can
rewrite Cofix f to e[f<-Cofix f.e] in your proofs when necessary.

This state of things is obviously unsatisfactory. The problem is still
waiting for a smart PhD student that provides a good and clean
theoretical solution to it. :-)

Best regards,
Eduardo Giménez.

> 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
> <mailto: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
> 
>