# [Haskell-cafe] Proof of induction case of simple foldl identity.

R J rj248842 at hotmail.com
Sat Mar 14 16:45:04 EDT 2009

```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
-------------- next part --------------
An HTML attachment was scrubbed...