[Agda] Re: [Coq-Club] Need help with coinductive proof

[Edsko de Vries]

Hi Thorsten,

Your suggestion made a world of difference. I have now extended the
flattening lemma to bisimilarity (
www.cs.tcd.ie/Edsko.de.Vries/simultaneous_flattening.v), and it was easy..

My previous attempts fell into two categories. First, I had a bisimilarity
relation on extended co-nats, but one that was much more general than the
one I use now: for example, it related (3 + 2) and 5 -- the new bisimulation
does not do that, because we only have "strong" bisimulation for sums. In
the second category, both the extended bisimulation and the normal
bisimulation were defined over standard co-natural numbers (without a
constructor for addition). In both cases, the discrepancy made life very
difficult. In the new proof, the extensions go hand in hand and the proof is
no longer very hard (of course, it also says less, but that's good: it's
probably the reason why it is easier now).

So, what's left to be able to complete the proof is adding transitivity
rules to the extended relation, and then presumably a translation from the
extended extended relation to the extended relation, and then finally to the
original bisimulation relation. Hopefully, that's not too difficult..

Thanks again, much appreciated (hopefully I should be able to thank you in
person on Sunday at WGP?),

Edsko
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090827/8d8524c0/attachment.html