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

[Thorsten Altenkirch]

On 26 Aug 2009, at 17:29, Edsko de Vries wrote:

> 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?

Cheers,
Thorsten

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.