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:
- From
h₃
, a proof ofP (S m) (S n)
, we can easily prove the resultm = n
. - We can easily construct
h₁
, a proof ofS(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₃