11. Induction

16/03/23

Induction on Numbers

data Nata = Zero | Succ Nat

Induction used to break down a problem. Need to prove a base case E.g $\forall n. P(n)$ Base Case: $P(zero)$ Inductive Case: $\forall n. [P(n) => P(Succ)]$

Example: given

add :: Nat -> Nat -> Nat
add Zero m = m
add (Succ n) m = Succ (add n m)

Show that

add n Zero = n

P(n) = add n Zero = n

Base Case: P(zero)

add Zero Zero = Zero

???????

Example: show that

Start reasoning with the largest sub-expression. Good approach because large things can usually be simplified by applying definitions

add x (add y z) = add (add x y) z

X appears twice in the recursive position, y is once, z is none

$P(x) \equiv$ add x (add y z) = add (add x y) z

Base case : P(zero) i.e

Work way down, then when get suck, work way up

add Zero (add y z) = add (add Zero y) z = Hypthoesis

add Zero (add y z) = applying add add y z = unapplying add add (add Zero y) z

Inductive Case

P(x) => P(Succ x) i.e.

add x (add y z) = add (add x y) z => add (Succ x) (add y z) = add (add (Succ x) y) z

add (Succ x) (add y z) -- Can apply the def of addition = Succ (add x (add y z)) = Succ(add (add x y) z) = add (Succ (add x y)) z = add(add (Succ x) y) z

Induction on Lists

Base Case: $P([])$ Inductive Case: $\forall x.\forall xs. [P(xs) => P(xs:xs]$ $\forall xs. P(xs)$

Example: given

rev :: [a] -> [a]
rev [] = []
rev (x:xs) = rev xs ++ [x]

show that rev(rev xs) = xs

Base Case: rev(rev [])) Inductive Case: rev(rev xs) = xs => rev(rev(x:xs)) = x:xs

rev(rev (x:xs)) = rev(rev xs ++ [x]) = rev [x] ++ rev(rev xs) = [x] ++ rev(rev xs) -- Apply inductive hyp = [x] ++ xs = x : xs To not get stuck, use an auxiliary word

Distributivity lemma rev(xs ++ ys) = rev ys ++ rev xs

Singleton list lemma rev [x] = [x]