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?