The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Monday 24 November 2008 5:19:37 pm Aaron Bohannon wrote:
> 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?

I believe, though I am not sure, that he is referring to a fact that if you 
can prove bisimilarity of two values, like:

  i ~ cosuc i

  j = anaConat inr 5

Then you can also imagine performing a(n infinite) series of reductions of 
said 
values to demonstrate that they are, in fact, intensionally equal as Coq/Agda 
defines it. Namely, both have a 'normal form' of:

  cosuc (cosuc (cosuc (cosuc ...)))

You can't actually achieve this for infinite values like the above, so to 
usefully prove their equality, you'd have to add an extensionality axiom like 
you suggest. But in principle, bisimilarity means that you could prove two 
values intensionally equal through evaluation (the equality just isn't 
decidable).

-- Dan