# HG changeset patch
# User Markus Kaiser <markus.kaiser@in.tum.de>
# Date 1354133939 -3600
# Node ID bef891fc07b4125ffa6e98fc0bdc09ffaa9299ff
# Parent  0d15fb5d5adeaf3caf570ec357da4e4c90ee7765
week 6 tutorial

diff -r 0d15fb5d5ade -r bef891fc07b4 exercises/src/Exercise_6.hs
--- a/exercises/src/Exercise_6.hs	Wed Nov 21 19:45:54 2012 +0100
+++ b/exercises/src/Exercise_6.hs	Wed Nov 28 21:18:59 2012 +0100
@@ -11,50 +11,84 @@
 {- Aufgabe G6.1 -}
 
 instance Num b => Num (a -> b) where
-    f + g = undefined
-    f - g = undefined
-    f * g = undefined
-    negate f = undefined
-    abs f = undefined
-    signum f = undefined
-    fromInteger x = undefined
+    f + g = \x -> f x + g x
+    f - g = \x -> f x - g x
+    f * g = \x -> f x * g x
+    negate f = \x -> negate (f x)
+    abs f = \x -> abs (f x)
+    signum f = \x -> signum (f x)
+    fromInteger x = const (fromInteger x)
 
 
 
 {---------------------------------------------------------------------}
 {- Aufgabe G6.2 -}
 
+foldl' :: (a -> b -> a) -> a -> [b] -> a
 foldl' f z [] = z
 foldl' f z ( x : xs ) = foldl' f ( f z x ) xs
 
+foldr' :: (c -> b -> b) -> b -> [c] -> b
 foldr' f z [] = z
 foldr' f z ( x : xs ) = f x ( foldr' f z xs )
 
 
 ffoldl = foldl' . foldl'
+{-
+foldl' :: (a -> b -> a) -> a -> [b] -> a
+
+f :: (a -> b -> a)
+
+inner :: a -> [b] -> a
+
+z :: a
+
+xs :: [[b]]
+
+ffoldl' :: (a -> b -> a) -> a -> [[b]] -> a
+-}
+ffoldl' :: (a -> b -> a) -> a -> [[b]] -> a
+ffoldl' f z xs = outer inner z xs
+        where
+        inner = (foldl' f)
+        outer = foldl'
+
 
 oo = (.).(.)
+oo' w = (.) ((.) w)
+oo'' w x = (.) ((.) w) x
+oo''' w x = ((.) w) . x
+oo'''' w x y = (.) w (x y)
+oo''''' w x y = w . (x y)
+
+oo'''''' :: (c -> d) -> (a -> b -> c) -> a -> b -> d
+oo'''''' f g u v = f (g u v)
+
 
 
 
 {---------------------------------------------------------------------}
 {- Aufgabe G6.3 -}
 
-
+-- First vs. second parameter
 a1 = (div 5)
 a2 = (`div` 5)
 
-b1 = (+ 7)
-b2 = ((+) 7)
+-- First vs. second parameter
+b1 = (+7)
+b2 = (7+)
 
-c1 = map (:[])
-c2 = map ([]:)
+c1 = map (:[]) -- [[x] | x <- xs]
+c2 = map ([]:) -- Prepend [] to every list element
 
+o f g x = f (g x)
+flip' f x y = f y x
+-- Both ids, d2 is more general
 d1 = flip . flip
 d2 = id
 
-e1 x y z = [x, y, z]
-e2 x y z = x : y : z
+e1 x y z = [x, y, z] -- z element
+e2 x y z = x : y : z -- z list
 
 
 
@@ -62,14 +96,45 @@
 {- Aufgabe G6.4 -}
 
 {-
-Lemma: reverse = foldl (\xs x -> x : xs) []
+Lemma reverse = foldl (\xs x -> x : xs) []
+Proof by extensionality
+To show:
+  *: reverse xs = foldl (\xs x -> x : xs) [] xs                       for all xs
+Too specialized for an induction!
+
+Generalization
+To show:
+  GEN: reverse xs ++ ys = foldl (\xs x -> x : xs) ys xs           for all xs, ys
+Proof by structural induction on xs
 
 Base case:
-To show:
+To show: reverse [] ++ ys = foldl (\xs x -> x : xs) ys []             for all ys
+reverse [] ++ ys
+== [] ++ ys                             (by reverse_Nil)
+== ys                                   (by append_Nil)
+foldl (\xs x -> x : xs) ys []
+== ys                                   (by foldl_Nil)
 
 Induction step:
-IH: 
-To show: 
+IH: reverse zs ++ ys = foldl (\xs x -> x : xs) ys zs                  for all ys
+To show: reverse (z : zs) ++ ys = foldl (\xs x -> x : xs) ys (z : zs) for all ys
+reverse (z : zs) ++ ys
+== (reverse zs ++ [z]) ++ ys            (by reverse_Cons)
+== reverse zs ++ ([z] ++ ys)            (by append_assoc)
+== reverse zs ++ z : ([] ++ ys)         (by append_Cons)
+== reverse zs ++ z : ys                 (by append_Nil)
+== foldl (\xs x -> x : xs) (z : ys) zs  (by IH with z : ys instead of ys)
+foldl (\xs x -> x : xs) ys (z : zs)
+== foldl (\xs x -> x : xs) ((\xs x -> x : xs) ys z) zs (by foldl_Cons)
+== foldl (\xs x -> x : xs) ((\x -> x : ys) z) zs       (by eval of lambda)
+== foldl (\xs x -> x : xs) (z : ys) zs                 (by eval of lambda)
+
+QED for GEN
+
+To prove * we instantiate GEN with [] for ys and apply append_Nil2.
+
+QED
+
 -}
 
 
@@ -77,20 +142,41 @@
 {---------------------------------------------------------------------}
 {- Aufgabe G6.5 -}
 
-f1 xs = map (\x -> x + 1) xs
+f1 xs = map (+ 1) xs
+f1' = map (+1)
 
-f2 xs = map (\x -> 2 * x) (map (\x -> x + 1) xs)
+f2 xs = map (2 *) (map (+ 1) xs)
+f2' = map (\z -> 2*(z+1))
+f2'' = map ((*2) . (+1))
+f2''' = map (*2) . map(+1)
 
-f3 xs = filter (\x -> x > 1) (map (\x -> x + 1) xs)
+f3 xs = f (g xs)
+        where
+        g = map (+ 1)
+        f = filter (> 1)
+
+f3' = filter (> 1) . map (+ 1)
 
 f4 f g x = f (g x)
+f4' f g x = (f . g) x
+f4'' f g = f . g
+f4''' = (.)
 
-f5 f g x y = f (g x y)
+f5 f g x y = f ((g x) y)
+f5' f g x = f . (g x)
+--
+f5'' = (.).(.)
 
 f6 f g x y z = f (g x y z)
+f6' f g x y = f . (g x y)
+--
+f6'' = (.).(.).(.)
 
 f7 f g h x = g (h (f x))
-
+f7' f g h x = g . (h (f x))
+f7'' f g h = g . h . f
+--
+f7''' = flip ((.).(.)) . flip (.)
 
 
 {---------------------------------------------------------------------}