Notes on Induction on Natural Numbers and on Lists

Induction on Natural Numbers (Mathematical Induction)

The classical rule, mentioned on page 454 of LPL, can in Fitch format be written
   | Q(0)
   | | Nat(n)
   | | Q(n)
   | | -
   | | ...
   | | Q(n+1)
   | ...
 * | An(Nat(n) -> Q(n))
Here Nat(n) holds for n=0,1,2,3,4...

Alternatively, we could choose another starting point:

   | Q(1)
   | | Nat(n) /\ n >=1
   | | Q(n)
   | | -
   | | ...
   | | Q(n+1)
   | ...
 * | An((Nat(n) /\ n >=1) -> Q(n))

Example (cf. page 454): We want to prove that for n >= 1 we have Q(n) where

   Q(n): 1 + ... + n = n(n+1)/2
The proof is as follows:
Base case
We must establish Q(1), that is
   1 = 1(1+1)/2
which is trivial.
Inductive step
We must establish the subproof
   | Nat(n) /\ n >=1
   | Q(n)
   | -
   | Q(n+1)
To do so, note that the conclusion follows from the calculation
     1 + ... + n+1 
   = (1 + ... + n) + n+1
   = n(n+1)/2 + n+1     
   = (n(n+1) + 2(n+1))/2
   = (n+1)(n+2)/2        
where the second equality is due to the fact that by our induction hypothesis, Q(n) holds.

Course-of-values induction

Alternatively, we may use the following rule
   | | Nat(n) /\ n >=1
   | | Am((1 <= m < n) -> Q(m))
   | | -
   | | ...
   | | Q(n)
   | ...
 * | An((Nat(n) /\ n >=1) -> Q(n))
To justify the validity of this rule, assume (in order to arrive at a contradiction) that the conclusion does not hold. That is, there exists natural numbers not satisfying Q. Let k be the least such number. That is, for all m < k we have Q(m). But then our premise tells us that also Q(k), yielding the desired contradiction.

Example: Consider the Fibonacci numbers given by

  fib(1) = 1
  fib(2) = 1
  fib(n) = fib(n-1) + fib(n-2)    for n >= 3
Theorem: If n is divisible by 3, then fib(n) is even, otherwise fib(n) is odd.

Proof: We shall employ course-of-values induction; there is thus no base step but "only" the inductive step where we have to establish

   | Nat(n) /\ n >=1
   | Am((1 <= m < n) -> Q(m))
   | - 
   | Q(n)
with Q the property mentioned in the theorem.

We have to do a case analysis; in all cases, we can assume that the result holds for all m < n.

n = 1 or n = 2
These are not divisible by 3, and accordingly fib(n) = 1 which is odd.
n is divisible by 3
Then neither n-1 nor n-2 is divisible by 3. Our induction hypothesis thus tells us that fib(n-1) and fib(n-2) are both odd. As fib(n) = fib(n-1) + fib(n-2), this implies that fib(n) is even, as desired.
n > 3 but n is not divisible by 3
Then exactly one of n-1 and n-2 is divisible by 3. Our induction hypothesis then tells us that exactly one of fib(n-1) and fib(n-2) is even. As fib(n) = fib(n-1) + fib(n-2), this implies that fib(n) is odd, as desired.
Note that the last two steps couldn't have been carried out using the original principle of induction, where we in order to establish Q(n) can assume only Q(n-1) but not Q(n-2).

Induction on Lists

This very important data structure is inductively defined as follows
   1. nil    is a list

   2. if  x  is a list and c is a value
      then (c :: x) is a list
That is, a list is either empty (nil) or a value c in front of a list.

Example: Consider a list with the elements 5,7,4 (note that the order matters). This list is in our syntax written as

   (5 :: (7 :: (4 :: nil)))
or graphically
      ::
     /  \
    5    ::
        /  \
       7    ::
           /  \
          4   nil
The induction principle for lists is (using Fitch format)
   | Q(nil)
   | | List(x)
   | | Q(x)
   | | -
   | | ...
   | | Q((c::x))
   | ...
 * | Ax(List(x) -> Q(x))
So in order to show that a property holds for all lists, you must show that it holds for the empty list, and that the property holds for a non-empty list provided it holds for its "tail".

Example: Consider the append function, taking two lists as arguments and returning their concatenation (also a list), and given by the following recursive definition

  append    nil   y = y

  append (c :: x) y = (c :: (append x y))
For example, we have
    append (5 :: (7 :: nil))  (8 :: (4 :: nil))
  = (5 :: (append (7 :: nil)  (8 :: (4 :: nil))))
  = (5 :: (7 :: (append  nil  (8 :: (4 :: nil)))))
  = (5 :: (7 :: (8 :: (4 :: nil))))
Theorem: For all x, we have Q(x) where
  Q(x): append x nil = x
Proof: Structural induction.
The base case
We must establish Q(nil), that is
  append nil nil = nil
which is trivial from the definition of append.
The inductive step
We must establish the subproof
   | List(x)
   | Q(x)
   | -
   | Q((c::x))
where the conclusion follows from the calculation
     append (c :: x) nil
   = (c :: (append x nil))    definition of append
   = (c :: x)                 the induction hypothesis
We can also prove that the append function is associative:

Theorem: For all x,y,z, we have Q(x) where

  Q(x): append (append x y) z = append x (append y z)
Proof: Structural induction.
The base case
We must establish Q(nil), that is
  append (append nil y) z = append nil (append y z)
which is trivial since both left hand side and right hand side reduces to
  append y z.
The inductive step
We can assume Q(x), and must establish Q((c :: x)) which follows from the calculation
     append (append (c :: x) y) z
  =  append (c :: (append x y)) z    definition of append
  =  (c :: (append (append x y) z))  definition of append
  =  (c :: (append x (append y z)))  induction hypothesis
  =  append (c :: x) (append y z)    definition of append

Other kinds of Structural Induction

We saw that for natural numbers, "course-of-values induction" is often more applicable than the standard induction principle. Similarly, for other inductively defined data structures (like binary trees), it is often more convenient to apply the following induction principle
    | | Ay("y smaller than x" -> Q(y))
    | | -
    | | Q(x)
    | ...
  * | Ax Q(x)
The unspecific "smaller than" can be defined in a numerous ways. For binary trees, one could for instance say that "y is smaller than x" iff y has fewer nodes than x.


Torben Amtoft