Proving the fusion law for unfold

Question

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?

Answer 1

I haven't read Gibbons's article, and there might be other techniques that he's relying on, but here's what I know.

It's a good intuition that you are looking for some kind of induction, because what you need is very similar to what you are trying to prove. But you actually need coinduction here. It's because unfoldL can produce infinite lists. In formal type systems, it's very rare that you can prove that two infinite structures are "equal" -- formal equality is much too strong to prove most results. Instead, we prove bisimilarity, which in informal circumstances might as well be equality.

Bisimilarity is tricky theoretically, and I won't go into it (partially because I don't fully understand the underpinnings), but working with it in practice is not too hard. Basically, to prove that two lists are bisimilar, you prove that they are either both Nil, or that they are both Cons with the same head and their tails are bisimilar, and you may use the coinductive hypothesis when proving the bisimilarity of the tails (but not elsewhere).

So for you, we prove by coinduction that for all b (because we need to use the coinductive hypothesis for different bs):

(unfoldL p f g . h) b ~~ unfoldL p' f' g' b

So far we have

(unfoldL p f g . h) b
= { your reasoning }
if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))

Analyzing by cases on p' b, if p' b is True then

if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
= { p' b is True }
Nil
~~ { reflexivity }
Nil
= { p' b is True }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
= { unfoldL }
unfoldL p' f' g'

; if p' b is False then

if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
= { p' b is False }
Cons (f' b) ((unfoldL p f g . h) (g' b))
*** ~~ { bisimilarity Cons rule, coinductive hypothesis } ***
Cons (f' b) (unfoldL p' f' g' (g' b))
= { p' b is False }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
= { unfoldL }

The line marked with *** is the key one. First, note it's a ~~ instead of an =. Also, we were allowed to use the coinductive hypothesis only underneath the Cons constructor. If we were allowed to use it anywhere else, then we could prove that any two lists are bisimilar.

Answer 2

After some googling I've found a paper by the same Jeremy Gibbons (and Graham Hutton) that presents proof methods for corecursive programs; the article includes a section on bisimulation and coinduction, the proof technique used by @luqui in the accepted answer. Section 6 has a proof of the fusion law using the universal property of unfold. For completeness, I've copied the proof below.

---

The universal property of unfoldL:

h = unfoldL p f g
<=>
∀ b . h b = if p b then Nil else Cons (f b) (h (g b))

Proof of the fusion law:

unfoldL p f g . h = unfoldL p' f' g'
<=> { universal property }
∀ b . (unfoldL p f g . h) b = if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
<=> { composition }
∀ b . unfoldL p f g (h b) = if p' b then Nil else Cons (f' b) (unfoldL p f g (h (g' b)))
<=> { unfoldL }
∀ b . if p (h b) then Nil else Cons (p (h b)) (unfoldL p f g (g (h b))) = if p' b then Nil else Cons (f' b) (unfoldL p f g (h (g' b)))
<=> { composition }
∀ b . if (p . h) b then Nil else Cons (p . h) b (unfoldL p f g ((g . h) b)) = if p' b then Nil else Cons (f' b) (unfoldL p f g ((h . g') b))
<=  { assumptions }
(p . h = p') ^ (f . h = f') ^ (g . h = h . g')