| 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)/2The proof is as follows:
1 = 1(1+1)/2which is trivial.
| 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)/2where the second equality is due to the fact that by our induction hypothesis, Q(n) holds.
| | Nat(n) | | Am(m < n -> Q(m)) | |-- | | ... | | Q(n) | ... * | An(Nat(n) -> 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(0) = 1 fib(1) = 1 fib(n) = fib(n-1) + fib(n-2) for n >= 2Theorem: If
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) | Am(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.
1. nil is a list 2. if x is a list and c is a value then (c :: x) is a listThat 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 nilThe 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". We call that induction principle structural induction.
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 = xProof: Structural induction.
append nil nil = nilwhich is trivial from the definition of append.
| 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
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.
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.
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
| | 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.