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₃``````

2 thoughts on “Injectivity of succ”

1. Tom

This is very nice, but is there a simpler way? I was assuming that injectivity of the constructors of an inductive type would be a foundational assumption of the system. Does it even make sense to have recursors defined on a type if it weren’t injective?

I looked into this more and now understand that constructors are not always injective: the exception is when the inductive type is a Prop type. Since we have proof-irrelevance, all values of a Prop type are equal, and so you can’t possibly extract the different elements from them. See Exists for a concrete use of that: you can’t pull out the particular element that exists from it.

So if mynat here were instead a Prop, what goes wrong? I couldn’t see it until I tried, but the problem is that rec_on for a Prop can only produce a Prop type. But the definition of P here is producing not a Prop type but Prop itself, which is of course a Type. That’s not allowed: we can only yield a Prop.

Thanks for the blog posts – they’re very enjoyable and helpful for beginners like myself at this.