= Solution
Prove the stronger equation, quantified over the accumulator:
$$
f(\operatorname{foldl}\ g\ a\ xs)=\operatorname{foldl}\ h\ (f\ a)\ xs\qquad\text{for all }a,xs.
$$
For `[]`, both sides are `f a`. For the <bottom value>, both sides are bottom because `f` is a <strict function>. For the cons step, the universal <induction hypothesis> allows the accumulator to become `g a x`:
``
f (foldl g a (x:xs))
= f (foldl g (g a x) xs)
= foldl h (f (g a x)) xs
= foldl h (h (f a) x) xs
= foldl h (f a) (x:xs).
``
Thus <structural induction> proves the claim for finite and finite partial spines; definable continuity extends it to infinite <lazy lists>. Pointwise equality is exactly the asserted equality of <function compositions>. This is the <left-fold fusion law>.
Back to article page
