Laws and Induction

1. Finish the proof of reverse . reverse = id from the lecture.

   -- claim: reverse . reverse = id 
   
   -- by extensional reasoning, it is enough to show that 
   -- (reverse . reverse) zs = id zs 
   -- for all lists zs 
   
   -- we distinguish the cases zs = [] and zs = x:xs 
   -- and prove the claim by induction on zs 
   
   
   -- base case zs = []:
   (reverse.reverse) []
   = -- def (.)
   reverse (reverse [])
   = -- def reverse
   reverse [] 
   = -- def reverse 
   [] 
   = -- def id 
   id [] 
   
   -- inductive case zs = x:xs:
   -- we assume the induction hypothesis (I.H.) (reverse . reverse) xs = id xs
   -- then 
   
   (reverse.reverse) (x:xs)
   = -- def (.)
   reverse (reverse (x:xs))
   = -- def reverse 
   reverse (reverse xs ++ [x])
   = -- lemma 1
   reverse [x] ++ reverse (reverse xs)
   = -- lemma 2
   [x] ++ reverse (reverse xs)
   =  -- def (.)
   [x] ++ (reverse.reverse) xs 
   = -- induction hypothesis
   [x] ++ id xs 
   = -- def id
   [x] ++ xs 
   = -- sugar [x]
   (x:[]) ++ xs 
   = -- def ++
   x : ([] ++ xs)
   = -- def ++ 
   x : xs  
   = -- def id
   id (x : xs)
   
   -- The claim now follows by induction on zs.
   
   -- We used two lemmas in this proof, which we prove next.
   
   -- lemma 2 : reverse [x] = [x]
   reverse [x]
   = -- sugar [x]
   reverse (x : [])
   = -- def reverse
   reverse [] ++ [x] 
   = -- def reverse
   [] ++ [x]
   = -- def ++
   [x]
   
   -- lemma 1 : reverse (zs ++ ys) = reverse ys ++ reverse zs
   -- we prove this lemma by induction on zs, distinguishing the 
   -- cases zs = [] and zs = x:xs 
   
   -- base case zs = []: 
   reverse ([] ++ ys)
   = -- def ++
   reverse ys 
   = -- lemma 3
   reverse ys ++ [] 
   = -- def reverse
   reverse ys  ++ reverse [] 
   
   -- inductive case zs = x:xs 
   -- we assume the induction hypothesis 
   -- reverse (xs ++ ys) = reverse ys ++ reverse xs
   
   
   reverse ((x:xs) ++ ys)
   = -- def ++ 
   reverse (x : (xs ++ ys))
   = -- def reverse
   reverse (xs ++ ys) ++ [x]
   = -- induction hypothesis
   (reverse ys  ++ reverse xs)  ++ [x]
   = -- Lemma 4
   reverse ys  ++ (reverse xs  ++ [x])
   = -- def reverse
   reverse ys ++ reverse (x:xs)
   
   -- Lemma 2 now follows by induction on zs.
   
   
   -- The proof of lemma 1 above depended on a third and fourth lemma, 
   -- which we prove now.
   
   
   -- lemma 3: zs ++ [] == zs
   -- we prove this by induction on zs, ditinguishing the cases
   -- zs = [] and zs = y:ys 
   
   -- base case: zs = [] 
   [] ++ []
   = - def ++
   []
   
   -- inductive case: zs = y:ys
   -- we assume the induction hypothesis ys ++ [] = ys
   (y:ys) ++ []
   = -- def ++
   y : (ys ++ [])
   = -- induction hypothesis
   y : ys 
   
   -- Lemma 3 now follows by induction on ys.
   
   -- Lemma 4: xs ++ (ys ++ zs) = (xs ++ ys) ++ zs 
   -- We prove this by induction on xs, distinguishing the cases xs = [] and xs = w:ws
   
   -- Base case xs = [] 
   [] ++ (ys ++ zs)
   = -- def ++ 
   ys ++ zs 
   = -- def ++
   ([] ++ ys) ++ zs
   
   -- Inductive case xs = w : ws .
   -- We assume the induction hypothesis ws ++ (ys ++ zs) = (ws ++ ys) ++ zs 
   
   ((w:ws) ++ ys) ++ zs 
   = def ++ 
   (w : (ws ++ ys)) ++ zs 
   = def ++ 
   w : ((ws ++ ys) ++ zs)
   = I.H.
   w : (ws ++ (ys ++ zs))
   = def ++
   (w : ws) ++ (ys ++ zs)
   
   -- Lemma 4 now follows by induction on xs.

2. Prove the following laws about list functions.

   • Hint: if you get stuck, the proofs can be found in Chapter 13 of the Lecture Notes.

     -- Laws about list length
     length . map f    = length
     length (xs ++ ys) = length xs + length ys
     length . concat   = sum . map length
     
     -- Laws about sum
     sum (xs ++ ys) = sum xs + sum ys
     sum . concat   = sum . map sum
     
     -- Laws about map
     map f . concat = concat . map (map f)  -- Hard!

3. Prove that sum (map (1+) xs) = length xs + sum xs for all lists xs.

   1. State a similar law for a linear function sum (map ((k+) . (n*)) xs) = ??.
   2. Prove the law from (a).
   3. Which laws from the previous exercise can be deduced from the general law?

4. Prove the following law: if op is an associative operator and e its neutral element, then

   foldr op e . concat = foldr op e . map (foldr op e)

5. Find a function g and a value e such that

   map f = foldr g e

   Prove the equality between both sides.

   -- We claim that
   g x acc = f x : acc 
   e = []
   -- does the trick.
   
   -- By extensional reasoning, it suffices to prove that 
   map f xs = foldr g e xs
   -- for all lists xs 
   
   -- We prove this by induction on xs, distinguishing 
   -- the cases xs = [] and xs = z:zs 
   
   -- Base case: xs = [] 
   map f [] 
   = -- def map 
   [] 
   = -- def e 
   e
   = -- def foldr 
   foldr g e [] 
   
   -- Inductive case: xs = z:zs 
   -- where we assume the induction hypothesis 
   map f zs = foldr g e zs 
   
   map f (z:zs)
   = -- def map 
   f z : map f zs 
   = -- def g
   g z (map f zs)
   = -- I.H. 
   g z (foldr g e zs)
   = -- def foldr 
   foldr g e (z:zs)
   
   -- The claim now follows by induction on xs.

6. Prove that addition is commutative, that is, add n m = add m n.

   • Hint: you might need as lemmas that add n Zero = n and add n (Succ m) = Succ (add n m).

7. Prove that multiplication is commutative, that is, mult n m = mul m n.

   • Hint: you need lemmas similar to the previous exercise.

8. Prove that for all trees size t = length (enumInfix t), where

   data Tree a = Leaf a | Node (Tree a) a (Tree a)
   
   size :: Tree a -> Int
   size Leaf = 0 
   size (Node l x r) = size l + 1 + size r
   
   enumInfix :: Tree a -> [a]
   enumInfix Leaf = []
   enumInfix (Node l x r) = enumInfix l ++ [x] ++ enumInfix r

   • Hint: you might needs some of the laws in exercise 2 as lemmas.

9. Prove that length . catMaybes = length . filter isJust, where

   catMaybes :: [Maybe a] -> [a]
   catMaybes []             = []
   catMaybes (Nothing : xs) = catMaybes xs
   catMaybes (Just x  : xs) = x : catMaybes xs
   
   isJust :: Maybe a -> Bool
   isJust (Just _) = True
   isJust Nothing  = False

   • Hint: proceed by induction on the list, and in the z:zs case distinguish between z being Nothing or Just w.