With the Curry-Howard correspondence and its realization in Coq in mind, we can now take a deeper look at induction principles.

Proof by Recursion

In the previous chapter we saw most of our favorite tactics explained as simple programs:

• destruct is just case analysis (match)
• apply is function application
• rewrite is an application of eq_eqL
• split, left, right, and reflexivity are just applying constructors

But what about induction? Let's start by writing out a suitable inductive predicate. A nice option is the Coq standard library's definition of even and odd.

We just wrote a "mutually inductive" definition. In short, it says that O is Even, the successor of an Odd number is Even and then successor of an Even number is Odd. Here's the lemma we'd like to prove.

The proof of even_or_odd is actually quite easy to program!

Unfortunately, writing entire proofs in the programming language can be quite hard. Fortunately, there is a simple program that makes these proofs easy.

nat_ind takes four arguments:

    1) A proposition P over natural numbers
    2) A proof of P O 
    3) A proof that P m -> P (S m). 
    4) An arbitrary n

and it constructs a recursive proof that P n. Let's try to prove nat_ind ourselves.

We can now use nat_ind to prove even_or_odd in the proof environment

Aside: Proving False

Now that we know how to write recursive proofs, let's do something fun. Let's prove False.

Induction in Depth

Every time we declare a new Inductive datatype, Coq automatically generates an induction principle for this type. This induction principle is a theorem like any other: If t is defined inductively, the corresponding induction principle is called t_ind. Here is the one for lists:

The induction tactic is a straightforward wrapper that, at its core, simply performs apply t_ind. To see this more clearly, let's experiment with directly using apply nat_ind, instead of the induction tactic, to carry out some proofs. Here, for example, is an alternate proof of a theorem that we saw in the Induction chapter.

This proof is basically the same as the earlier one, but a few minor differences are worth noting. First, in the induction step of the proof (the "x :: l" case), we have to do a little bookkeeping manually (the intros) that induction does automatically. Second, we do not introduce l into the context before applying list_ind -- the conclusion of list_ind is a quantified formula, and apply needs this conclusion to exactly match the shape of the goal state, including the quantifier. (However, we can specify l using with.) By contrast, the induction tactic works either with a variable in the context or a quantified variable in the goal. Third, we had to manually supply the name of the induction principle with apply, but induction figures that out itself. These conveniences make induction nicer to use in practice than applying induction principles like nat_ind directly. But it is important to realize that, modulo these bits of bookkeeping, applying list_ind is what we are really doing.

Exercise: 2 stars, standard, optional (plus_one_r')

Complete this proof without using the induction tactic.

Coq generates induction principles for every datatype defined with Inductive, including those that aren't recursive. Although of course we don't need induction to prove properties of non-recursive datatypes, the idea of an induction principle still makes sense for them: it gives a way to prove that a property holds for all values of the type. These generated principles follow a similar pattern. If we define a type t with constructors c₁ ... cn, Coq generates a theorem with this shape:
    t_ind : ∀ P : t → Prop,
              ... case for c₁ ... →
              ... case for c₂ ... → ...
              ... case for cn ... →
              ∀ n : t, P n

The specific shape of each case depends on the arguments to the corresponding constructor. Before trying to write down a general rule, let's look at some more examples. First, an example where the constructors take no arguments:

Exercise: 1 star, standard, optional (rgb)

Write out the induction principle that Coq will generate for the following datatype. Write down your answer on paper or type it into a comment, and then compare it with what Coq prints.

In general, the automatically generated induction principle for inductive type t is formed as follows:

• Each constructor c generates one case of the principle.
• If c takes no arguments, that case is:
        "P holds of c"
• If c takes arguments x₁:a₁ ... xn:an, that case is:
        "For all x₁:a₁ ... xn:an, if [P] holds of each of the arguments of type [t], then [P] holds of [c x₁ ... xn]"

Exercise: 1 star, standard, optional (booltree_ind)

Write out the induction principle that Coq will generate for the following datatype. (Again, write down your answer on paper or type it into a comment, and then compare it with what Coq prints.)

Exercise: 1 star, standard, optional (ex_set)

Here is an induction principle for an inductively defined set.
      ExSet_ind :
         ∀ P : ExSet → Prop,
             (∀ b : bool, P (con1 b)) →
             (∀ (n : nat) (e : ExSet), P e → P (con2 n e)) →
             ∀ e : ExSet, P e

Give an Inductive definition of ExSet:

Induction Principles in Prop

Earlier, we looked in detail at the induction principles that Coq generates for inductively defined sets. The induction principles for inductively defined propositions like even are a tiny bit more complicated. As with all induction principles, we want to use the induction principle on even to prove things by inductively considering the possible shapes that something in even can have. Intuitively speaking, however, what we want to prove are not statements about evidence but statements about numbers: accordingly, we want an induction principle that lets us prove properties of numbers by induction on evidence. For example: From what we've said so far, you might expect the inductive definition of ev...
      Inductive ev : nat → Prop :=
      | ev_0 : even 0
      | ev_SS : ∀ n : nat, even n → even (S (S n)).

...to give rise to an induction principle that looks like this...
    ev_ind_max : ∀ P : (∀ n : nat, even n → Prop),
         P O ev_0 →
         (∀ (m : nat) (E : ev m),
            P m E →
            P (S (S m)) (ev_SS m E)) →
         ∀ (n : nat) (E : ev n),
         P n E

... because:

• Since ev is indexed by a number n (every ev object E is a piece of evidence that some particular number n is even), the proposition P is parameterized by both n and E -- that is, the induction principle can be used to prove assertions involving both an even number and the evidence that it is even.
• Since there are two ways of giving evidence of evenness (even has two constructors), applying the induction principle generates two subgoals:
  • We must prove that P holds for O and ev_0.
  • We must prove that, whenever m is an even number and E is an evidence of its evenness, if P holds of m and E, then it also holds of S (S m) and ev_SS m E.
• If these subgoals can be proved, then the induction principle tells us that P is true for all even numbers n and evidence E of their evenness.

This is more flexibility than we normally need or want: it is giving us a way to prove logical assertions where the assertion involves properties of some piece of evidence of evenness, while all we really care about is proving properties of numbers that are even -- we are interested in assertions about numbers, not about evidence. It would therefore be more convenient to have an induction principle for proving propositions P that are parameterized just by n and whose conclusion establishes P for all even numbers n:
       ∀ P : nat → Prop,
         ... →
       ∀ n : nat,
         even n → P n

For this reason, Coq actually generates the following simplified induction principle for ev:

In particular, Coq has dropped the evidence term E as a parameter of the the proposition P. In English, ev_ind says: Suppose P is a property of natural numbers (that is, P n is a Prop for every n). To show that P n holds whenever n is even, it suffices to show:

• P holds for 0,
• for any n, if n is even and P holds for n, then P holds for S (S n).

As expected, we can apply ev_ind directly instead of using induction. For example, we can use it to show that ev' (the slightly awkward alternate definition of evenness that we saw in an exercise in the \chap{IndProp} chapter) is equivalent to the cleaner inductive definition ev:

Strengthening Induction Principles

Sometimes the default kind of induction that Coq gives you isn't sufficient for a given task. Let's try to prove a simple theorem about our definition of even from the beginning of this chapter.

Maybe we can do induction on the even n predicate?

We're going to need a better induction principle.

Exercise: 3 stars, standard, recommended (odd_decomposition)

Write a corresponding induction principle for odd and use it to prove the corresponding lemma about odd numbers.

Let's look at a more interesting example: an arbitrarily branching tree:

Let's see if we can use this to prove the correctness of a tree mapping function: