Can someone provide the induction-case proof of the following identity:
foldl (-) ((-) x y) ys = (foldl (-) x ys) - y
If foldl is defined as usual:
foldl :: (b -> a -> b) -> b -> [a] -> b
foldl f e [] = e
foldl f e (x : xs) = myFoldl f (f e x) xs
The first two cases, _|_ and [], are trivial.
Here's my best attempt at the (y : ys) case (the left and right sides reduce to
expressions that are obviously equal, but I don't know how to show it):
Case (y : ys).
Left-side reduction:
foldl (-) ((-) x y) (y : ys)
= {second equation of "foldl"}
foldl (-) ((-) ((-) x y) y) ys
= {notation}
foldl (-) ((-) (x - y) y) ys
= {notation}
foldl (-) ((x - y) - y) ys
= {arithmetic}
foldl (-) (x - 2 * y) ys
Right-side reduction:
(foldl (-) x (y : ys)) - y
= {second equation of "foldl"}
(foldl (-) ((-) x y) ys) - y
= {induction hypothesis: foldl (-) ((-) x y) ys = (foldl (-) x ys) - y}
((foldl (-) x ys) - y) - y
= {arithmetic}
(foldl (-) x ys) - 2 * y
Thanks as always.
_________________________________________________________________
Express your personality in color! Preview and select themes for Hotmail®.
http://www.windowslive-hotmail.com/LearnMore/personalize.aspx?ocid=TXT_MSGTX_WL_HM_express_032009#colortheme_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
