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
bare 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
0 + 1 = 1 + 0 1 + 2 = 2 + 1 0 + 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
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
Zis the neutral
natwith respect to
+, this simplifies to
b = b, which we know by reflexivity. In the second case, let
nbe some arbitrary
natand 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
Succan 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.
natis precisely a data type which consists of one nullary constructor (or constant) and one unary constructor. The former is the famous number
Zwhile the latter is the successor function
Suc, known as
Suc n = n + 1. Now please enlighten us with the definition of
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
Z, you return the right argument
m, otherwise you destruct
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
naton 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
lis equal to
- 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.
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.
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 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
inductionthat you used to generate goals and an induction hypothesis in the list example was precisely empowered by the induction principle for
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
inductionkeyword how to generate goals and hypotheses for you.
- Simplicio: Sure, I believe that. It reminds me of ordinary induction over
- 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_ind : forall P : nat -> Prop, P Z -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
- You: See, the term
listnat_indmatters, 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.
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
nodeconstruction, 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
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.