Proving the fusion law for unfold

Viewed 209

I was reading Jeremy Gibbons' article on origami programming and I got stuck on exercise 3.7, which asks the reader to prove the fusion law for list unfolds:

unfoldL p f g . h = unfoldL p' f' g'

if

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

The function unfoldL, unfold for lists, is defined as follows:

unfoldL :: (b -> Bool) -> (b -> a) -> (b -> b) -> b -> List a
unfoldL p f g b = if p b then Nil else Cons (f b) (unfoldL p f g (g b))

Here is my current attempt at a proof:

(unfoldL p f g . h) b
=   { composition }
unfoldL p f g (h b)
=   { unfoldL }
if p (h b) then Nil else Cons (f (h b)) (unfoldL p f g (g (h b)))
=   { composition }
if (p . h) b then Nil else Cons ((f . h) b) (unfoldL p f g ((g . h) b))
=   { assumptions }
if p' b then Nil else Cons (f' b) (unfoldL p f g ((h . g') b))
=   { composition }
if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
=   { ??? }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
=   { unFoldL }
unFoldL p' f' g'

I am not sure how to justify the step marked with ???. I should probably use some sort of induction on function application on b? Related question: what are some good resources that explain and motivate various induction techniques, such as structural induction?

2 Answers
Related