[Haskell-cafe] Proof of induction case of simple foldl identity.
Dean Herington
heringtonlacey at mindspring.com
Sat Mar 14 17:22:55 EDT 2009
At 8:45 PM +0000 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 : 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).
Careful. Your introduced variables y and ys already appear in the
equation to be proved. Try introducing fresh variables.
>
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090314/778c726e/attachment.htm
More information about the Haskell-Cafe
mailing list