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

[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))

      Right-side reduction:

         foldl (flip f) e (reverse (x : xs))
      =  {second equation of "reverse"}
         foldl (flip f) e (reverse xs ++ [x])
_________________________________________________________________
Hotmail® is up to 70% faster. Now good news travels really fast. 
http://windowslive.com/online/hotmail?ocid=TXT_TAGLM_WL_HM_70faster_032009
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090318/a5770695/attachment.htm