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).

      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.

---

Express your personality in color! Preview and select themes for HotmailŪ. See how.