Induction Principles

Induction, sometimes called mathematical induction, is a tool for reasoning about countably infinite structures. Commonly, we can use something called a "proof by induction" to verify facts which reside in infinity.

Let's review. Pretend you're majoring in computer science at a college and you're in your first year: You are asked to show that a + b = b + a. We both hope that you proceed as follows--

You: Professor, what are a and b?
Professor: a and b are arbitrary natural numbers
You: and the + sign, it's ordinary natural number addition?
Professor: yes
You: and what does arbitrary mean?

The professor updates the question. "Please show forall (a b : nat), a + b = b + a"

We hope you do not commence with the following list

+ 1 = 1 + 0
+ 2 = 2 + 1
+ 2 = 2 + 0
...

Even if you were aware that a systematic listing procedure exists, you would be foiled by lack of paper, because you're asked to operate on all of an infinite set (or, in short time, a type).

We instead hope you commence the following proof

You: let a and b be arbitrary nats. By induction on a, there are two cases to prove. In the first case, a = Z. The goal we need to verify is Z + b = b + Z. Since Z is the neutral nat with respect to +, this simplifies to b = b, which we know by reflexivity. In the second case, let n be some arbitrary nat and assume that n + b = b + n. The goal we need to verify is (Suc n) + b = b + (Suc n). By the definition of +, we can simplify this to Suc (n + b) = b + (Suc n) then apply our assumption, transforming our goal to Suc (b + n) = b + (Suc n). If we're equipped with a lemma that Suc can get pulled out from the right argument rather than the left, we can apply it to obtain Suc (b + n) = Suc (b + n), which we can see is true by reflexivity.
Professor: Very good. Let's take a closer look at some of the details for the rest of the class. nat is precisely a data type which consists of one nullary constructor (or constant) and one unary constructor. The former is the famous number Z while the latter is the successor function Suc, known as Suc n = n + 1. Now please enlighten us with the definition of + you referenced.
You:

Fixpoint plus (n m : nat) : mynat :=
  match n with
  | Z => m
  | S n' => S (plus n' m)
  end.

Professor: Marvelous! As I have a class full of programmers, I expect one of them can explain what's going on?
Simplicio: Your pattern match has two branches because your type has two constructors like the professor said. When the left argument n is Z, you return the right argument m, otherwise you destruct n into S n' where n' is also a nat, and return the expression S (plus n' m).
Professor: Indeed. In other words, the nonzero case looks like n + m = 1 + (n-1) + m, so the term is decreasing to Z. Now someone needs to write nat on the board. Simplicio, are you up for it?
Simplicio: Sure.

Inductive nat : Type :=
| Z : nat
| S (n : nat) : nat.

Professor: Thank you. Now who would like to prove that the twice reverse of a list l is equal to l?
You: No.
Professor: Excuse me?
Simplicio: What I think they mean, professor, is that we don't know how to work with lists just yet, nor to take their reverse.
Professor: Very well. Allow me a moment.

Inductive listnat : Type :=
  | empt : listnat
  | cons (h : nat) (t : listnat) : listnat.

Fixpoint append (l1 l2 : listnat) : listnat :=
  match l1 with
  | empt => l2
  | cons h t => cons h (append t l2)
  end.

Fixpoint rev (l : listnat) : listnat :=
  match l with
  | empt => empt
  | cons h t => append (reverse t) (cons h empt)
  end.

Professor: Now, if you'd be so kind.
You:

Theorem reverse_involutive : forall (l : listnat),
    reverse (reverse l) = l.
Proof.
  intros l.
  induction l as [| head tail IHtail].
  - simpl; reflexivity.
  - simpl.
    rewrite reverse_append_distributive.
    rewrite IHtail.
    simpl.
    reflexivity.
Qed.

Professor: Splendid! Our construction of lists also supports induction, as you demonstrated.

In Coq, every inductive data type (that is, a type defined with the Inductive keyword) comes equipped with an induction principle. Let's observe the following definition

Inductive coin :=
  | heads : coin
  | tails : coin.

This is saying that heads is a coin and tails is a coin, and if you observe the Coq system's output when you run this block of code it says

coin is defined
coin_rect is defined
coin_ind is defined
coin_rec is defined

coin_ind is the induction principle for the coin data type. Let's run Check coin_ind to print it out

coin_ind
     : forall P : coin -> Prop, P heads -> P tails -> forall c : coin, P c

This is just a function type. In english, it says "for every predicate over coins, if it holds of heads and of tails, then it holds for all coins."

To see it in action, define a predicate (a function coin -> Prop, where Prop stands for Propositions)

Definition is_heads : coin -> Prop :=
  fun c => c = heads.

and apply coin_ind to is_heads

Check coin_ind is_heads
(* coin_ind is_heads
     : is_heads heads -> is_heads tails -> forall c : coin, is_heads c *)

We have specialized the induction principle which is defined over all predicates to a particular predicate is_heads. To further specialize it, we would need to supply a proof of is_heads heads, and to specialize it all the way to the end we would need a proof of is_heads tails. is_heads tails is not a provable proposition, so the example is silly.

I wanted to show you that function application happens at the type level and that specializing a forall behaves like supplying an argument to a function.

Professor: The tactic induction that you used to generate goals and an induction hypothesis in the list example was precisely empowered by the induction principle for listnat. Observe.

The Professor writes Check listnat on the board, and just beneath it begins to materialize the following type

listnat_ind
     : forall P : listnat -> Prop,
       P empt ->
       (forall (h : nat) (t : listnat), P t -> P (cons h t)) ->
       forall l : listnat, P l

Professor: In english, the type is saying that if I have an arbitrary predicate about listnats, if I have a proof that it holds of the empty list, and a proof that if it holds of some list then it holds of that list prepended with some h, then I've effectively proved that it holds for all natlists. This is in fact the very type that tells the induction keyword how to generate goals and hypotheses for you.
Simplicio: Sure, I believe that. It reminds me of ordinary induction over nat.
You: That's because the types are similar. Both have one constant constructor and another constructor with one point of self-reference.
Simplicio: Professor, could you please print out the induction principle for nat?
Professor: Check nat_ind

nat_ind
     : forall P : nat -> Prop,
       P Z -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

You: See, the term h in listnat_ind matters, but it doesn't impact the shape of the type, since the only things impacting the shape are points of self reference.
Professor: Very good.

The english translation for the preceding type is literally the definition of ordinary, vanilla "mathematical induction". The type nat_ind is nothing but an algorithmic description of how to prove stuff about nat, and you'll find the same for any other inductive type (including bool (which we saw by another name, coin), various types of trees, and even whole programming languages).

Professor: One last example before we conclude our discussion of induction. You, please write on the board the type of trees with data in the leaves.
You:

Inductive tree : Type :=
  | leaf (n : nat) : tree
  | node (l r : tree) : tree.

The board shimmers as it announces: tree is defined. tree_ind is defined.

Professor: Simplicio. Please talk us through how you'd calculate the induction principle for tree, without letting the system just print it out for you.
Simplicio: gulp. well. You have to start by quantifying over predicates, so i'd start forall P : tree -> Prop, .... We have two constructors, so there will be two proofs enabling the conclusion that forall (t : tree), P t. Then, I notice that the first constructor doesn't have any self-reference, so the first proof needed would be forall (n : nat), P (leaf n). Now we come to the self-referential constructor, that of node. There are two trees in a node construction, so there should be two premises for this proof, it'll look like _ -> _ -> _, which I know will be _ -> _ -> P (node l r). We need to establish l and r, so there will be quantifiers, and finally we need to assume the predicate of the decreased arguments, so the proof corresponding to the second constructor is forall (l : tree), P l -> forall (r : tree), P r -> P (node l r). Now I can wrap it all together, and say

tree_ind 
     : forall P : tree -> Prop, 
     (forall (n : nat), P (leaf n)) -> 
     (forall (l : tree), P l -> forall (r : tree), P r -> P (node l r)) -> 
     forall (t : tree), P t

Professor: Excellent! Very well done!

To learn more, read Software Foundations.