On Saturday 14 March 2009, Daniel Fischer wrote:

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

Typo? :) (L) forall u v w. (u - v) - w = (u - w) - v

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.

-- Pozdrawiam, Marcin Kosiba