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

Better make that skeleton-defined finite lists:

Prelude> foldr (++) [] ("this":" goes":" so":" far":undefined)
"this goes so far*** Exception: Prelude.undefined
Prelude> foldl (flip (++)) [] (reverse ("this":" goes":" so":" 
far":undefined))
"*** Exception: Prelude.undefined


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