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.