Why can IHn' (n' = n' + 0) from induction be used to prove n = n + 0 in Coq?

Question

In Software Foundations's Logical Foundations, they use the idea of induction to prove things. From stepping through the following proof, it is difficult to see why you can rewrite what you're trying to prove with your original hypothesis. Why can IHn' (n' = n' + 0) from induction be used to prove n = n + 0?

Are they not essentially the same statement?

Theorem plus_n_O : ∀ n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity. Qed.

Answer 1

They are the same statement, but about different numbers: one is about n', the other one is about n, which corresponds to S n' in the goal. Induction is precisely about showing that something is valid for S n' just by knowing that it holds for n'. The fact that they are different numbers is what makes this non-trivial. For example, it is not possible to show that S n' is odd assuming that n' is odd, even though both statements are "the same".

You asked about the mechanics of rewriting. After simplification, your goal looks like this:

n' : nat
IHn' : n' = n' + O
---------------------------------------
S n' = S (n' + O)

When you call rewrite, you are telling Coq to replace n' + O by n' in the goal. This leads to the statement S n' = S n', which is a simple equality that can be discharged by the axiom of reflexivity.

Edit

Here is another way to think about induction. Let's forget about the induction tactic for a second. It is possible to prove that 0 = 0 + 0:

Lemma plus_0_0 : 0 = 0 + 0.
Proof. reflexivity. Qed.

We can prove similar statements about any concrete natural number:

Lemma plus_1_0 : 1 = 1 + 0.
Proof. reflexivity. Qed.

Lemma plus_2_0 : 2 = 2 + 0.
Proof. reflexivity. Qed.

However, we can obtain these proofs differently, making fewer assumptions about the shape of the number we are talking about. First, we prove the following conditional statement.

Lemma plus_Sn_0 : forall n', n' = n' + 0 -> S n' = S n' + 0.
Proof. intros n' Hn'. simpl. rewrite <- Hn'. reflexivity. Qed.

This lemma states the inductive step of a proof by induction. Note that it does not say that n = n + 0 holds for all natural numbers n, but that it holds only for numbers of the form n = S n' provided that n' = n' + 0. We know that this works for n' = 0, because we proved it above. Combined with plus_Sn_0, we have another proof of 1 = 1 + 0.

Lemma plus_1_0' : 1 = 1 + 0.
Proof. apply plus_Sn_0. apply plus_0_0. Qed.

Now, we know that the statement holds for n' = 1, we can play the same trick for n = 2:

Lemma plus_2_0' : 2 = 2 + 0.
Proof. apply plus_Sn_0. apply plus_1_0'. Qed.

This proof does not use directly the fact that 0 = 0 + 0. This is why the fact that we proved the base case is irrelevant for proving the inductive step: all we need to know about is the predecessor of the number we are interested in -- in this case, this predecessor being 1.

Naturally, we could have expanded out the proof of plus_1_0' inside the proof of plus_2_0':

Lemma plus_2_0'' : 2 = 2 + 0.
Proof. apply plus_Sn_0. apply plus_Sn_0. apply plus_0_0. Qed.

More generally, given any natural number constant n, we can prove that n = n + 0 without induction by applying plus_Sn_0 n times followed by plus_0_0. The principle of mathematical induction extrapolates this intuitive observation for any expression n denoting a natural number, and not just constants.