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

[Edsko de Vries]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090827/002ea7d8/attachment.html