<!doctype html public "-//W3C//DTD W3 HTML//EN">
<html><head><style type="text/css"><!--
blockquote, dl, ul, ol, li { padding-top: 0 ; padding-bottom: 0 }
--></style><title>Re: [Haskell-cafe] Proof of induction case of
simple foldl</title></head><body>
<div>At 8:45 PM +0000 3/14/09, R J wrote:</div>
<blockquote type="cite" cite><font face="Courier New">Can someone
provide the induction-case proof of the following identity:<br>
<br>
foldl (-) ((-) x y) ys = (foldl (-) x ys) - y<br>
<br>
If foldl is defined as usual:<br>
<br>
foldl <span
></span> :: (b -> a ->
b) -> b -> [a] -> b<br>
foldl f e
[] =
e<br>
foldl f e (x : xs) =
myFoldl f (f e x) xs<br>
<br>
The first two cases, _|_ and [], are trivial.<br>
<br>
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):<br>
<br>
Case (y : ys).</font></blockquote>
<div><br></div>
<div>Careful. Your introduced variables y and ys already appear
in the equation to be proved. Try introducing fresh
variables.</div>
<div><br></div>
<blockquote type="cite" cite><font face="Courier New"><br>
Left-side reduction:<br>
<br>
foldl (-) ((-) x y)
(y : ys)<br>
= {second equation of
"foldl"}<br>
foldl (-) ((-) ((-) x
y) y) ys<br>
= {notation}<br>
foldl (-) ((-) (x -
y) y) ys<br>
= {notation}<br>
foldl (-) ((x - y) -
y) ys<br>
= {arithmetic}<br>
foldl (-) (x - 2 * y)
ys<br>
<br>
Right-side reduction:<br>
<br>
(foldl (-) x (y :
ys)) - y<br>
= {second equation of
"foldl"}<br>
(foldl (-) ((-) x y)
ys) - y<br>
= {induction hypothesis: foldl
(-) ((-) x y) ys = (foldl (-) x ys) - y}<br>
((foldl (-) x ys) -
y) - y<br>
= {arithmetic}<br>
(foldl (-) x ys) - 2
* y</font><br>
<font face="Courier New"></font></blockquote>
<blockquote type="cite" cite><font face="Courier New">Thanks as
always.</font></blockquote>
</body>
</html>