[Agda] Re: [Coq-Club] Re: Agda beats Coq

[Aaron Bohannon]

I reviewed the previous coq-list thread on coinduction and I
understand why people are not completely happy with the current
situation.  Among the proposals for remedying the situation was the
suggestion that we add an axiom asserting that bisimilarity implies
intentional equality for each datatype.  I take this to mean that some
people believe this to be sound, although I am apparently not the only
to stop and question it.  Of course, this is a moot point for
datatypes where you could actually build a proof in Coq of such a
proposition.  Does the proof rely on some other axioms?  Do you mind
sharing your proof or a reference to one?

 - Aaron

On Mon, Nov 24, 2008 at 3:45 PM, Arnaud Spiwack
<Arnaud.Spiwack at lix.polytechnique.fr> wrote:
> 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
>>
>>
>
>