The Coq mailing list

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

Hi Thorsten,

Consider adding all numbers in an infinite stream of (partial, co-natural) numbers, and applying some function h:

 h (x1 + (x2 + (x3 + ..)))

If h is a morphism from nat to nat (i.e., h 0 ~ 0 and h (i + j) ~ h i + h j), then this should be bisimilar to

 h x1 + (h x2 + (h x3 + ..))

Can't we eliminate the function h and say we have two streams that are pointwise bisimilar (ignoring finite delay) and in this case the sum should be bisimilar? Clearly to define the sum we have to use an auxilliary datatype with a special constructor for + and then flatten.

I thought this just boils down to showing that + is a congruence, but you seem to think this is not so?

The strategy is to define an extension of partial coNat with a special constructor for + and correspondingly an extension of the bisimulation with a congruence rule for +. Now it should be straightforward to show that the statement holds for the extended version of bisimilarity. The missing lemma is to show that if two values in the extended sense are bisimilar then their flattening should be bisimilar?

This seems just to require to extend the flattening lemma to the bisimulations?

 

Right. This is how I tried to prove the lemma (to make the proof that the two sums are bisimilar easy, it is also convenient to have transitivity as an ("inductive") rule in the bisimulation). The fact that add is a congruence I had simply assumed, I hadn't even got that far yet..

Indeed, it
"just" requires to give a flattening lemma for bisimulation extended with sums and transitivity, except
that I have now been trying to exactly that non-stop for the last 6
days or so without making much progress :(

Having said that, I now realize that I don't *quite* do what you suggest, if I understand you correctly: you are suggesting that I prove

  bisimilar_on_extended_conat m n ->
  bisimilar_on_standard_conat (flatten m) (flatten n)

? I have not tried this 'simultaneous' flattening of the bsimulation relation and the conats. Let me give that a try..

Thanks again, much appreciated,

Edsko