Injectivity of succ

In the last post, I showed how to prove, using only elementary tools, that zero is not the successor of any natural number, that O = succ(m) leads to a contradiction.

In this post, we’ll see that the successor function is injective. Writing S in place of succ, we’ll show that if S(m) = S(n), then m = n.

As before, we start with our own version of the natural numbers.

inductive mynat : Type
  | O : mynat
  | S : mynat → mynat

The strategy for our proof will be to find a predicate P on pairs of natural numbers such that on the assumption h : S(m) = S(n), the following criteria are satisfied:

1. From h₃, a proof of P (S m) (S n), we can easily prove the result m = n.
2. We can easily construct h₁, a proof of S(m) = S(m) → P (S m) (S m).

Why does this help? Substituting equation h into h₁ gives

h₂ : S(m) = S(n) → P (S m) (S n). But we know h, a proof of the antecedent of this implication, and hence we derive h₃ := h₂ h, the desired proof of P (S m) (S n). From this, we prove our initial target m = n.

I’m sure you will agree that the first condition above is satisfied if P is chosen so that P (S m) (S n) = m = n.

Since this is a good candidate for P, we’ll give it a Lean definition.

def P : mynat → mynat → Prop
| (S a) (S b) := a = b
| _     _     := true

The second pattern in the definition isn’t used on our proof, but Lean functions are total, so we must define P in all cases.

What remains is to prove the second criterion. By definition, P (S m) (S m) is simply m = m. This is true by reflexivity.

Those are all the ingredients. Time to assemble them up into a Lean proof.

lemma succ_inj (m n : mynat) (h : S m = S n) : m = n :=
have h₁ : S(m) = S(m) → P (S m) (S m),  from λ _, rfl,
have h₂ : S(m) = S(n) → P (S m) (S n),  from h ▸ h₁,
have h₃ : P (S m) (S n),                from h₂ h,
show m = n,                             from h₃