The Coq mailing list

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

As a matter of fact, the most natural bisimalirity on streams does imply 
intentionnal equality. Which can be considered quite useful, but I've 
got the feeling it's not a good idea. This is actually what makes that 
Coq conversion is not decidable or Coq doesn't have subject reduction 
(choose whichever you want). There are quite some metaphysical issues 
here. ITT, ETT, OTT, whichever intermediate alternative, Impredicative, 
Predicative, ... There is enough to fight over all night long.


Arnaud Spiwack

Xavier Leroy a écrit :
> Aaron Bohannon wrote:
>
>   
> > [...] That is, may I safely assert that a standard definition of
> > bisimilarity on a coinductive data type implies the default
> > (intensional) equality ("=")?  (I don't know if this question is
> > relevant to Agda.)
> >     
>
> Thanks for raising this question, as I've been wondering about it for
> a while.
>
> Let me take streams (infinite lists) as a concrete example of
> coinductive datatype.  My (limited) understanding is that you could
> make a set-theoretic model of streams where a stream of A is a
> function nat -> A, so your property would amount to function
> extensionality, which holds in this model.  However, I'm pretty sure
> that if you assert function extensionality as an axiom in Coq, you
> still cannot prove the extensionality property over streams stated
> above...
>
> Expecting more informed replies from true logicians,
>
> - Xavier Leroy
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.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
>
>