[Haskell-cafe] Unfold fusion

[Dan Doel]

On Wednesday 06 May 2009 4:26:15 pm Dan Doel wrote:
> unfortunately it looks like I'm doing something wrong in that "coinductive
> hypothesis"

Sorry about the self-reply, but I realized where I went wrong. The principle 
of proof by coinduction for defining a function 'f' goes something like this 
(expressed all point-free like):

  if
    null . f = p'
   (and when not null)
    head . f = f'
    tail . f = f . g'
  then
    f = unfold p' f' g'

now we have:

    null . (unfold p f g . h) = p . h = p'
    head . (unfold p f g . h) = f . h = f'
    tail . (unfold p f g . h) = unfold p f g . g . h
                              = unfold p f g . h . g'
                              = (unfold p f g . h) . g'

now we have a system of equations for (unfold p f g . h) that fits the format, 
so by coinduction we have:

    unfold p f g . h = unfold p' f' g'

And we're done.

-- Dan