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