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

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

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

At 8:45 PM + 3/14/09, R J wrote: 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 :

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

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)

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

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 -

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

Am Samstag, 14. März 2009 22:44 schrieb Marcin Kosiba: (L) forall u v w. (u - v) - w = (u - v) - w Typo? :) (L) forall u v w. (u - v) - w = (u - w) - v Sure. Thanks for spotting it. I had (x-y)-z = (x-z)-y first, then decided it would be better to use different variable names...