Templates for informal proofs by induction

In the real world of mathematical communication, written proofs range from extremely longwinded and pedantic to extremely brief and telegraphic. The ideal is somewhere in between, of course, but while you are getting used to the style it is better to start out at the pedantic end. Also, during the learning phase, it is probably helpful to have a clear standard to compare against. So... For the rest of the course, all your inductive proofs should match one of the two following templates.

Proof by induction over an inductively defined set

Template:

• Theorem: <Universally quantified proposition of the form "For all n:S, P(n)," where S is some inductively defined set.>
  Proof: By induction on n.
  <one case for each constructor c of S...>
  • Suppose n = c a1 ... ak, where <...and here we state the IH for each of the a's that has type S, if any>. We must show <...and here we restate P(c a1 ... ak)>.
    <go on and prove P(n) to finish the case...>
  • <other cases similarly...> ☐

Example:

• Theorem: For all sets X, lists l : list X, and numbers n, if length l = n then index (S n) l = None.
  Proof: By induction on l.
  • Suppose l = []. We must show, for all numbers n, that, if length [] = n, then index (S n) [] = None.
    This follows immediately from the definition of index.
  • Suppose l = x :: l' for some x and l', where length l' = n' implies index (S n') l' = None, for any number n'. We must show, for all n, that, if length (x::l') = n then index (S n) (x::l') = None.
    Let n be a number with length l = n. Since
                length l = length (x::l') = S (length l'),
    it suffices to show that
                index (S (length l')) l' = None.
    But this follows directly from the induction hypothesis, picking n' to be length l'. ☐

Induction over an inductively defined proposition

Since inductively defined proof objects are often called "derivation trees," this form of proof is also known as induction on derivations. Template:

• Theorem: <Proposition of the form "Q -> P," where Q is some inductively defined proposition (more generally, "For all x y z, Q x y z -> P x y z")>
  Proof: By induction on a derivation of Q. <Or, more generally, "Suppose we are given x, y, and z. We show that Q x y z implies P x y z, by induction on a derivation of Q x y z"...>
  <one case for each constructor c of Q...>
  • Suppose the final rule used to show Q is c. Then <...and here we state the types of all of the a's together with any equalities that follow from the definition of the constructor and the IH for each of the a's that has type Q, if there are any>. We must show <...and here we restate P>.
    <go on and prove P to finish the case...>
  • <other cases similarly...> ☐

Example

• Theorem: The <= relation is transitive -- i.e., for all numbers n, m, and o, if n <= m and m <= o, then n <= o.
  Proof: By induction on a derivation of m <= o.
  • Suppose the final rule used to show m <= o is le_n. Then m = o and the result is immediate.
  • Suppose the final rule used to show m <= o is le_S. Then o = S o' for some o' with m <= o'. By induction hypothesis, n <= o'.
    But then, by le_S, n <= o. ☐