= Solution
Use <structural induction> on the finite <list> `xs`, with the assertion quantified over every accumulator `e` and every <list> `ys`. The equations of the <left fold> are `foldl f e [] = e` and `foldl f e (x:xs) = foldl f (f e x) xs`.
For `xs = []`, both sides reduce to `foldl f e ys`. For the constructor case, <equational reasoning> gives
``
foldl f e ((x:xs) ++ ys)
= foldl f e (x : (xs ++ ys))
= foldl f (f e x) (xs ++ ys)
= foldl f (foldl f (f e x) xs) ys
= foldl f (foldl f e (x:xs)) ys
``
The third equality uses the <induction hypothesis> with accumulator `f e x`. Hence \b[the stated identity holds]. No inspection of `ys` was required: in <Haskell> this equality also permits infinite or partially defined `ys`, with both expressions denoting the same possibly undefined result.
Back to article page
