What's in a proof?

Let’s work through this very simple theorem in Coq:

Theorem plus_n_O :
  forall (n : nat), n = n + 0.
Proof.
  intros n.
  induction n; simpl.
  - reflexivity.
  - rewrite <- IHn. reflexivity.
Qed.

The theorem, called plus_n_O, states that n + 0 equals to n for all natural numbers n (represented by the inductive datatype nat).

The first two lines are the theorem statement and below them is the proof script. If you look at the script, you notice that it’s similar to what you’d do in a pen-and-paper proof: use induction on n, evaluate + in both cases, use induction hypothesis in the inductive step.

Another way of viewing this code snippet is that we define a function plus_n_O that, given natural number n, returns a value of type n + 0 = n. Both of these interpretations are valid - this idea is known as propositions as types.

The proof script does not look much like a function, but it does generate one. With the command Print plus_n_O, we can look at the proof object it generates:

plus_n_O = 
fun n : nat =>
nat_ind
  (fun n0 : nat => n0 = n0 + 0)
  eq_refl
  (fun (n0 : nat) (IHn : n0 = n0 + 0) =>
   eq_ind n0 (fun n1 : nat => S n0 = S n1) eq_refl (n0 + 0) IHn)
  n
     : forall n : nat, n = n + 0

What’s going on here? nat_ind is the induction principle for nat, eq_refl is the constructor for the equality type ? = ? and eq_ind is the induction principle for the equality type.

Coq < Check nat_ind.
nat_ind
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

Coq < Check eq_ind.
eq_ind
     : forall (A : Type) (x : A) (P : A -> Prop),
       P x -> forall y : A, x = y -> P y

Let’s go through the arguments of nat_ind in plus_n_O:

(fun n0 : nat => n0 = n0 + 0): this is the proposition we want to prove inductively.
eq_refl: this is the base case. 0 + 0 is convertible to 0, so nothing else is needed.
(fun (n0 : nat) (IHn : n0 = n0 + 0) => eq_ind n0 (fun n1 : nat => S n0 = S n1) eq_refl (n0 + 0) IHn): this is the inductive case. We’ve proven the proposition for n0 and want to prove it for S n0. IHn is the induction hypothesis.
n: the final argument tells that we apply the inductive proof to n that plus_n_O is quantified over.

In the inductive case, eq_ind is used to rewrite S n0 = S n0 into S n0 = S (n0 + 0), which is convertible into S n0 = S n0 + 0, which is what we want.

I’m not sure if this write-up helps anyone else, but it was helpful for me to work through this example to better understand the relationship between a proof script and a proof term. I recommend the exercise.