# 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
• @AndrejBauer This is natural induction on the length of the list, not structural induction. His inductive hypothesis is that P(k) is true, namely, f . foldl g a = foldl h b :: [C] -> B for the list of length k, and he must prove P(k+1) is true. Structural induction is used for things like trees or any recursively-defined data structure. You could say it's applicable to a cons-list depending on how it's defined, but that's like using integrals to find the area of a square. Structural induction is a generalization of natural induction. Note, the OP did use structural induction. – BrainFRZ Nov 25 at 18:05
• @BrainFRZ: I think I am well aware of what kind of induction is being used where. This answer says that it's using induction on the length of the list, but the induction step has the form of a structural induction: the induction hypothesis is used for xs and the result is then concluded for x : xs. That's structural induction. And you are quite mistaken with your analogy. Structural induction is more basic and prior to induction on the lenght of lists. This is an example from Haskell where lists are defined as a (co)inductive datatype, and that directly gives us structural induction. – Andrej Bauer Nov 25 at 19:23