Indutive Proofs

1. Introduction

We want to prove assertions involving many different entities:

Since all of these are inductively defined, they give rise to inductive principles.

(!) Example Proofs

For example, we may want to prove the following assertions:

We could prove each of these by induction over the term (i.e. ), the value (i.e. ), the first relation (i.e. ), or the second relation (i.e. ). We need to choose.

Induction allows us to work with infinite collections of objects which are:

(*) Reminder

Remember the set , where , or in Haskell:

data Nat = Zero | Succ Nat

This gives rise to the following inductive principle for any :

We can also perform induction over trees, , or in Haskell:

data Tree a = Leaf a | Node (Tree a) a (Tree a)

This gives rise to the following inductive principle for any :

2. Induction

We can use the syntax for simple expressions, where to define an inductive principle:

We can use this inductive principle to prove the determinacy and totality of simple expressions.

(?) Proof of Determinacy of

We want to show . We can prove this by induction over the structure of .

1. BASE CASE

To Show .

  1. Take arbitrary and .
  2. Assume .
  3. The derivations and must have been constructed using the rule , by the operational semantics of .
  4. by (3) and the rule .
  5. by (4) and properties of .

Hence, .

2. INDUCTIVE STEP (ADDITION)

The inductive hypothesis is, for arbitrary :

To Show .

  1. Take arbitrary and .
  2. Assume that .
  3. The derivations and must have been constructed using the rule , by the operational semantics of .
  4. by (3) and the rule .
  5. by (4) and the inductive hypothesis.
  6. by (4) and (5).

Hence, .

3. INDUCTIVE STEP (MULTIPLICATION)

The inductive hypothesis is, for arbitrary :

To Show .

  1. Take arbitrary and .
  2. Assume that .
  3. The derivations and must have been constructed using the rule , by the operational semantics of .
  4. by (3) and the rule .
  5. by (4) and the inductive hypothesis.
  6. by (4) and (5).

Hence, .

4. CONCLUSION

By the principle of induction, we have shown that . Hence, the operational semantics of is deterministic. $

To prove by inductions, we need to:

  1. State over which identity is the induction performed.
  2. Base case - state what is to be shown.
  3. Prove the base case. State what is taken arbitrary and justify each step.
  4. Inductive step - state what is taken arbitrary, the inductive state, and what is to be shown.
  5. Prove the inductive step. State what is taken arbitrary and justify each step.
  6. Not all lemmas require a proof by induction.
Back to Home