The Coq mailing list

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

On 18 Aug 2009, at 15:36, Adam Chlipala wrote:

> Edsko de Vries wrote:
> > Example: suppose we define coinductive trees as
> >
> > CoInductive cotree : Set :=
> > | coleaf : cotree
> > | cobranch : cotree -> cotree -> cotree.
> >
> > Consider a function to count the number of leaves in a tree
> >
> > leaves : cotree -> conat
> >
> > (the domain is conat because there might be infinitely many  
> > leaves). This function is "obviously not productive": there are  
> > infinitely large trees that don't have any leaves but simply keep  
> > on branching forever.
>
> Since you haven't defined [conat], it's not clear to me that you  
> can't write this function. A reasonable definition of [conat], tuned  
> to this application, could include an "add zero" constructor.

Ah, very interesting. Yes, I guess that's possible. With a suitably  
modified bisimulation relation for conat' (which allows to ignore  
addzero constructors) we can then prove that the result of leaves when  
applied to the infinite tree is bisimilar to both zero and infinity (I  
just tried it, it works :). Nice.

Thanks for the suggestion.

-E