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:
h₃, a proof of
P (S m) (S n), we can easily prove the result
m = n.
- We can easily construct
h₁, a proof of
S(m) = S(m) → P (S m) (S m).
Why does this help? Substituting equation
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₃