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

StackExchange Computer Science Q#68922, answer score: 7