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

[Daniel Fischer]

Am Samstag, 14. März 2009 21:45 schrieb R J:
> 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

(R)    foldl f e (x : xs)     =  foldl 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.
>

Consider a one-element list.
foldl (-) (x-y) [z] = (x-y)-z
(foldl (-) x [z]) - y = (x-z)-y

So a necessary condition for the identity to generally hold is that the Num 
instance obeys the law

(L)   forall u v w. (u - v) - w = (u - v) - w

Then take as inductive hypothesis that zs is a list such that 
forall a b. foldl (-) (a-b) zs = (foldl (-) a zs) - b

Let z be an arbitrary value of appropriate type, x and y too.
Then

foldl (-) (x - y) (z:zs)
   = foldl (-) ((x-y)-z) zs		(R)
   = (foldl (-) (x-y) zs) - z		(IH, a = x-y, b = z)
   = ((foldl (-) x zs) - y) - z		(IH, a = x, b = y)
   = ((foldl (-) x zs) - z) - y		(L, u = foldl (-) x zs, v = y, w = z)
   = (foldl (-) (x-z) zs) - y		(IH, a = x, b = z)
   = (foldl (-) x (z:zs)) - y		(R)

The trick is to formulate the inductive hypothesis with enough generality, so 
you have strong foundations to build on.