# Prove foldl fusion law

I have proven the foldr Fusion Law as follows:

Given f is strict, f a = b and f (g x y) = h x (f y) for all x and y, than

f.foldr g a = foldr h b


Case []:

(f . foldr g a) [] = foldr h b [] -- Remove . notation
f (foldr g a [])   = foldr h b [] -- definition foldr
f (foldr g a [])   = b            -- definition foldr
f a                = b            -- This is a given, so stop


Case (x:xs):

(f . foldr g a) (x:xs) = foldr h b (x:xs)       -- remove . notation
f (foldr g a (x:xs))   = foldr h b (x:xs)       -- definition foldr
f (g x (foldr g a xs)) = h x (foldr h b xs)     -- inductive hypothesis
f (g x (foldr g a xs)) = h x (f (foldr g a xs)) -- introduce y
say y = foldr g a xs
f (g x y)              = h x (f y)              -- This is a given, so stop


Now, I would also like to prove the Fusion Law for foldl. This goes like this:

Given f is strict, f a = b and f (g x y) = h (f x) y for all x and y, than

f.foldl g a = foldl h b


However, I don't seem to be able to use the same trick as in the proof for foldr. How can I prove the foldl Fusion Law?

Let me try to answer your question, I may be mistaken, so check it out first:

Let's first state the definition of foldl:

foldl :: (a -> b -> a) -> a -> [b] -> a
foldl h b x = case x of
[]     -> b
(x:xs) -> foldl h (h b x) xs


Now, we aim to prove that, given f:: A -> B, g:: A -> C -> A, h:: B -> C -> B, a:: A b:: B, such that:

f a = b
f (g x y) = h (f x) y, for all x, y
f is strict


Then:

f . foldl g a = foldl h b :: [C] -> B


We are going to prove it by induction on the length of the list:

Case 0:

f.foldl g a []   = foldl h b []
f (foldl g a []) = foldl h b []   -- Definition of .
f a              = b              -- Definition of foldl
True                              -- given


Case n => n+1:

let x:xs be a list of length n+1, then xs has length n, the property holds for xs. Let's check it's true for x:xs:

f (foldl g a (x:xs))   = foldl h b (x:xs)
f (foldl g (g a x) xs) = foldl h (h b x) xs  -- Definition of foldl


Now, let's take f' = f, g' = g, a' = g a x, h' = h, b' = h b x

Clearly, f' is strict, also, f' a' = b':

f' a'     = b'
f (g a x) = h b x  -- Opening the '
h (f a) x = h b x  -- Hypothesis
h b x     = h b x  -- Hypothesis


Now, let's check that f' (g' z y) = h' (f' z) y works for any y, z (I changed the x for a z, because we have a fixed x, the head of the list):

f' (g' z y) = h' (f' z) y
f (g z y)   = h (f z) y   -- Opening the '
-- OK: hypothesis


Now, since the predicate works for lists of length n, and xs has that length, and also f', g', h', a', b' make the premises true, we have that, for any list of size n, in particular xs:

f' . foldl g' a' xs      = foldl h' b' xs
f  . foldl g  (g a x) xs = foldl h (h b x) xs  -- Opening the '
f (foldl g (g a x) xs)   = foldl h (h b x) xs  -- What we were trying to reach

• Instead of saying "induction on the length of the list" it is better to describe what you're doing directly, namely structural induction on lists. – Andrej Bauer Aug 6 at 7:43