Induction Exercises

I've put these exercises together so that you could get practice with doing induction yourself. Try and do each of them, and when you think you've got a good proof, see a member of the course staff in office hours or consulting to check your answer.

For each proof, you should follow this format and fill in the details:
Look at the Induction Examples page to see some well constructed proofs.

P(n):
Claim:
Proof by Induction (What type of induction? What set are you inducting over?)
	Base Case: Demonstration that P(Base Case) is true Repeat this step for each base case in the set you're inducting over
	Inductive Step
	Induction Hypothesis:
	What are you proving:
	Left to Right Proof (or Right to Left Proof): (Make sure to use your Induction Hypothesis) Repeat this step for each rule in the inductive case of the set you're inducting over
Statement that you've proven your claim:
QED

The following function definitions will be useful:
NOTE: This are not necessarily how the ML language implements these function. Also note that most of these functions should be defined in terms of foldl and foldr, but we'll consider more explicit definitions to make it easier to show the steps in the substitution model.

fun power(x:int,y:int):int =
  if y=0 then 1 else x*power(x, y-1)

fun copy(l:'a list):'a list =
  case l of
    []    => []
   |x::xs => x::copy(xs)

fun compose(f:'a->'b, g:'c->'a):'c->'b =
  fn x => f(g(x))

fun reverse(l:'a list):'a list =
  case l of
    []    => []
   |x::xs => reverse(xs)@[x]

fun filter(p:'a->bool, l:'a list):'a list) =
  case l of
    []    => []
   |x::xs => if p(x) then x::filter(p, xs) else filter(p, xs)

fun append(x:'a list, y:'a list):'a list =
  case x of
    []    => y
   |x::xs => x::append(xs, y)

fun revapp(x:'a list, y:'a list):'a list =
  case x of
    []    => y
   |x::xs => revapp(xs, x::y)

fun length(l:'a list):int =
  case l of
    []    => 0
   |_::xs => 1+length(xs)

fun map(f:'a->'b, l:'a list):'b list =
  case l of
    []    => []
   |x::xs => f(x)::map(f, xs)

fun mem(x:int, l:int list):bool =
  case l of
    []    => false
   |y::ys => if x=y then true else mem(x, ys)

This first section asks you to write definitions for inductively defined sets:

Inductively define the set of positive odd integers.

Inductively define the set of well-formed formulas in predicate calculus.

Inductively define the set of positive integers not divisible by 5.

Inductively define the set of strings.

Prove the following with induction. Clearly state the set you're inducting over, and clearly state what type of induction you are using. When applicable, use structural induction in preference to mathematical induction.

1 + nh <= (1 + h)ⁿ for all non-negative values of n. h is greater than -1. This is called Bernoulli's inequality.

Use mathematical induction to show that n²-1 is divisible by 8 whenever n is an odd positive integer.

Which amounts of money can be formed using just dimes and quarters? Prove your answer using a form of mathematical induction (either weak or strong).

n! < nⁿ whenever n is a positive integer greater than 1

power(x,y) = x^y

map(f, map(g,x)) = map(compose(f,g), x)

reverse(reverse(x)) = x

append(x,y) = revapp(revapp(x, []) y)
Challenge: Why would we want to use the later expression instead of (append x y)? What is the running time of both expressions?

append(x, []) = x

length(x)+length(y) = length(append(x,y))

append(map(f,x), map(f,y)) = map(f, append(x,y))

reverse(x) = revapp(x, [])

length(filter(p, x)) <= length(x)

Handout written by Brandon Bray