[Haskell-cafe] Proof of duality theorem of fold?

[Daniel Fischer]

Am Mittwoch, 18. März 2009 12:57 schrieb R J:
> I'm trying to prove the following duality theorem of fold for finite lists:
>
>    foldr f e xs         =  foldl (flip f) e (reverse xs)
>
> where
>
>    reverse              :: [a] -> [a]
>
> reverse []           =  []
>
> reverse (x:xs)       =  reverse xs ++ [x]
>
>    flip                 :: (a -> b -> c) -> b -> a -> c
>    flip f y x           =  f x y
>
>    foldr                :: (a -> b -> b) -> b -> [a] -> b
>    foldr f e []         =  e
>    foldr f e (x : xs)   =  f x (foldr f e xs)
>
>    foldl                :: (b -> a -> b) -> b -> [a] -> b
>    foldl f e []         =  e
>    foldl f e (x : xs)   =  foldl f (f e x) xs
>
>
> I'm stuck on the induction case.  Can someone help?  Here's what I've got
> so far:
>
> Proof:
>
>    Case _|_.
>
>       Left-side reduction:
>
>          foldr f e _|_
>       =  {case exhaustion of "foldr"}
>          _|_
>
>       Right-side reduction:
>
>          foldl (flip f) e (reverse _|_)
>       =  {case exhaustion of "reverse"}
>          foldl (flip f) e _|_
>       =  {case exhaustion of "foldl"}
>          _|_
>
>    Case [].
>
>       Left-side reduction:
>
>          foldr f e []
>       =  {first equation of "foldr"}
>          e
>
>       Right-side reduction:
>
>          foldl (flip f) e (reverse [])
>       =  {first equation of "reverse"}
>          foldl (flip f) e []
>       =  {first equation of "foldl"}
>          e
>
>    Case (x : xs).
>
>       Left-side reduction:
>
>          foldr f e (x : xs)
>       =  {second equation of "foldr"}
>          f x (foldr f e xs)
>       =  {induction hypothesis: foldr f e xs = foldl (flip f) e (reverse
> xs)} f x (foldl (flip f) e (reverse xs))

        = (flip f) (foldl (flip f) e (reverse xs)) x

>
>       Right-side reduction:
>
>          foldl (flip f) e (reverse (x : xs))
>       =  {second equation of "reverse"}
>          foldl (flip f) e (reverse xs ++ [x])

Now prove the

Lemma:

foldl g e (ys ++ zs) = foldl g (foldl g e ys) zs

for all g, e, ys and zs of interest.
(I don't see immediately under which conditions this identity could break, 
maybe there aren't any)

Then the last line of the right hand side reduction can be rewritten as the 
new last of the left.