Induction Proofs
Table of Contents
Here are the demo proofs by induction we looked at in the lecture.
Firstly, the Haskell definitions of the functions of interest:
module Induct where -- Example recursive functions, used as examples in some -- illustrative inductive proofs. -- sum the numbers from 1 to n sum_to :: Int -> Int sum_to n = if n <= 0 then 0 else sum_to (n - 1) + n -- The Peano representation of natural numbers. data Nat = Z | S Nat deriving (Read, Show) -- Mapping from regular ints to Peano naturals. int_to_nat :: Int -> Nat int_to_nat n = if n <= 0 then Z else S (int_to_nat (n - 1)) -- Various recursive definitions of addition. add :: Nat -> Nat -> Nat add Z y = y add (S x) y = S (add x y) add2 :: Nat -> Nat -> Nat add2 Z y = y add2 (S x) y = add2 x (S y) add3 :: Nat -> Nat -> Nat add3 x Z = x add3 x (S y) = S (add3 x y) -- Hand-written versions of the library functions length, -- take and drop. We need definitions for them to do some -- proofs about them. -- Count the length of a list. our_length :: [a] -> Int our_length [] = 0 our_length (x : xs) = our_length xs + 1 -- Take at most n elements of a list. our_take :: Int -> [a] -> [a] our_take n [] = [] our_take n (x : xs) | n == 0 = [] | otherwise = x : our_take (n - 1) xs -- Drop n elements, or all of them, from a list. our_drop :: Int -> [a] -> [a] our_drop n [] = [] our_drop n (x : xs) | n == 0 = x : xs | otherwise = our_drop (n - 1) xs -- A simple binary tree type. data Tree a = Leaf | Branch a (Tree a) (Tree a) -- Count the number of Leaf constructors in the tree. leaves :: Tree a -> Int leaves Leaf = 1 leaves (Branch v l r) = leaves l + leaves r -- Compute the height of the tree, the longest chain of -- Branch constructors from the tree to a Leaf. height :: Tree a -> Int height Leaf = 0 height (Branch v l r) = max (height l) (height r) + 1
1. Exercise 1.
We want to show sumTo n = (n * (n + 1)) / 2. Define P(n) = (sumTo n == (n * (n + 1)) / 2). P(0): sumTo 0 = ... LHS equals 0 by definition. RHS equals 0. Assume P(k), and think about P(k + 1). P(k + 1): (sumTo (k + 1) == ((k + 1) * ((k + 1) + 1) / 2). The LHS is equal to (if (k + 1 <= 0) then 0 else sumTo (k + 1 - 1) + k + 1) == sumTo k + k + 1 (from definition of sumTo, simplification) == ((k * (k + 1)) / 2) + k + 1 (using IH P(k)) == .... We leave sorting out the arithmetic as an exercise to the reader.
2. Exercise 2.
Prove P(n): add n Z = n. Proof by induction. P(0): add Z Z = Z. True from definition of add. Assume P(k) (add k Z = k), show P(S k). P(S k): add (S k) Z = S k. LHS == S (add k Z) (by definition of add) == S k (from IH P(k)) == RHS.
3. Exercise 3.
Prove that P(xs): take (length xs) xs == xs.
Note that P is roughly a function from [a] to bools, or proofs, or
truth, or something like that.
Base case: P([]):
take (length []) [] == [].
LHS == [] (from definition of take)
== RHS.
Inductive case: Assume P(xs), prove P(x : xs):
That is, show: take (length (x : xs)) (x : xs) == (x : xs).
LHS == take (length xs + 1) (x : xs) (using definition of length)
== x : take ((length xs + 1) - 1) xs
(using definition of take, and the argument that length xs + 1 /= 0)
== x : take (length xs) xs (by simplification)
== x : xs (using IH P(xs))
== RHS.
Aside: length xs + 1 is not 0, because length xs is always
non-negative. We could show that by induction as well. Skipped in
interest of time. Exercise to the interested reader.
4. Exercise 4.
Show that take 5 xs ++ drop 5 xs == xs
First we will show P(xs): ∀n. take n xs ++ drop n xs == xs.
Proof of P by induction.
Base case: P([]): ∀n. take n [] ++ drop n [] == [].
Let's skip the details of this case.
Inductive case: Assume P(xs), show P(x : xs):
∀n. take n (x : xs) ++ drop n (x : xs) == x : xs.
Fix n.
Case split. Is n == 0?
True case:
LHS == [] ++ (x : xs) (by definition of take & drop)
== x : xs (by definition of append)
== RHS.
False case:
LHS == (x : take (n - 1) xs) ++ drop (n - 1) xs
== x : (take (n - 1) xs ++ drop (n - 1) xs)
(either by the definition of append
-- or by sub-proof, skipped for brevity)
== x : xs (by IH P(xs), specialised to n - 1)
== RHS.
We have now proven ∀xs. P(xs). We conclude our original
property by specialising n to 5.
5. Exercise 5.
Prove that ∀t. height t < leaves t. Let us first prove P(t): height t + 1 <= leaves t. We proceed by induction on the tree type and P. Base case P(Leaf): height Leaf + 1 <= leaves Leaf This reduces to 1 <= 1 (from the definitions), which is true. Inductive case: Assume P(l) and P(r), show P(Branch v l r): height (Branch v l r) + 1 <= leaves (Branch v l r) This reduces (using the definitions) to: max (height l) (height r) + 1 + 1 <= leaves l + leaves r We have these IHs: P(l): height l + 1 <= leaves l P(r): height r + 1 <= leaves r If we add both sides of those inequalities, we derive: height l + 1 + height r + 1 <= leaves l + leaves r The above step is correct. It works because of a "monotonicity" rule about + and <= that we omit here. The inequality we need and the inequality we have shown above have the same RHS. We can prove what we need if we also show: max (height l) (height r) + 1 + 1 <= height l + 1 + height r + 1 This simplifies to: max (height l) (height r) <= height l + height r We're close! We can use this fact about max: ∀x y z. max x y <= z if x <= z and y <= z. Again, this fact is left as an exercise to the reader if you want to check every last part of the proof. To use that fact to prove our goal, we need these two facts: height l <= height l + height r height r <= height l + height r And now we have reduced the problem to a simple consequence of the fact that heights are non-negative, which is fairly obvious, and which can easily be proven by induction. That completes our proof by induction of ∀t. P(t). Finally, we can use that fact to prove our original goal.