<html>
<head>
<style>
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 10pt;
font-family:Verdana
}
</style>
</head>
<body class='hmmessage'>
<font style="" face="Courier New">Can someone provide the induction-case proof of the following identity:<br><br>&nbsp;&nbsp; foldl (-) ((-) x y) ys = (foldl (-) x ys) - y</font><font style="" face="Courier New"><br></font><font style="" face="Courier New"><br></font><font style="" face="Courier New">If foldl is defined as usual:<br><br>&nbsp;&nbsp; foldl&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &nbsp;&nbsp; :: (b -&gt; a -&gt; b) -&gt; b -&gt; [a] -&gt; b<br>&nbsp;&nbsp; foldl f e []&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &nbsp;&nbsp; =&nbsp; e<br>&nbsp;&nbsp; foldl f e (x : xs) &nbsp; &nbsp; =&nbsp; 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></font><font style="" face="Courier New">&nbsp;&nbsp; Case (y : ys).</font><font style="" face="Courier New"><br></font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Left-side reduction:</font><font style="" face="Courier New"><br></font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; foldl (-) ((-) x y) (y : ys)</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =&nbsp; {second equation of "foldl"}</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; foldl (-) ((-) ((-) x y) y) ys</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =&nbsp; {notation}</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; foldl (-) ((-) (x - y) y) ys</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =&nbsp; {notation}</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; foldl (-) ((x - y) - y) ys</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =&nbsp; {arithmetic}</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; foldl (-) (x - 2 * y) ys</font><font style="" face="Courier New"><br></font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Right-side reduction:</font><font style="" face="Courier New"><br></font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (foldl (-) x (y : ys)) - y</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =&nbsp; {second equation of "foldl"}</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (foldl (-) ((-) x y) ys) - y</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =&nbsp; {induction hypothesis: foldl (-) ((-) x y) ys = (foldl (-) x ys) - y}</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ((foldl (-) x ys) - y) - y</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =&nbsp; {arithmetic}</font><font style="" face="Courier New"><br></font><font style="" face="Courier New">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (foldl (-) x ys) - 2 * y</font><font style="" face="Courier New"><br></font><font style="" face="Courier New"><br>Thanks as always.<br></font><br /><hr />Express your personality in color! Preview and select themes for HotmailŪ.  <a href='http://www.windowslive-hotmail.com/LearnMore/personalize.aspx?ocid=TXT_MSGTX_WL_HM_express_032009#colortheme' target='_new'>See how.</a></body>
</html>