Functional Programming - Laws and Induction

Laws and Induction

1 atHome

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 inClass

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 atHome

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

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

4 atHome

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 inClass

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 atHome

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 atHome

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

Hint: you need lemmas similar to the previous exercise.

8 inClass

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 atHome

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.