The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

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