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

R J rj248842 at hotmail.com
Wed Mar 18 07:57:06 EDT 2009

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

More information about the Haskell-Cafe mailing list