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
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
+ 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
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
(fun n0 : nat => n0 = n0 + 0): this is the proposition we want to prove inductively.
eq_refl: this is the base case.
0 + 0is 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
n0and want to prove it for
IHnis the induction hypothesis.
n: the final argument tells that we apply the inductive proof to
plus_n_Ois 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.