The simplest type type with a recursive constructor is the type of natural numbers. Here’s our own implementation. Note
O is the capital letter
O, not the numeral
inductive mynat : Type | O : mynat | succ : mynat → mynat
The most transparent parts of this definition are the constructors. We know
O : mynat and we know
succ n : mynat, given
n : mynat.
In particular, we have both
O : mynat and
O.succ : mynat.
open mynat example : mynat := O -- 0 is a natural number example : mynat := O.succ -- so is 1
What isn’t evident is that
O.succ are distinct.
In this blog post, we’ll show an elementary method for proving this result, but we are duty-bound to mention the standard, albeit more mystical, Lean approach. For each inductive type
T, Lean automatically generates a function
T.no_confusion that can be used to prove distinctness. The internals of this function will be the subject of a later post.
example : O ≠ O.succ := λ h, mynat.no_confusion h
Rather that using the
no_confusion sledgehammer, we’ll adopt a more straightforward approach. As above, we’ll use a proof by negation. Assume
h : O = O.succ and try to derive
What data do we have? We have an equation
O = O.succ. Thus, anything true for
O is also true for
The clever idea is to construct a predicate
mynat such that
Q(O) is something we can easily prove but for which
Q(O.succ) is the statement
O ≠ succ(O). Thus, by substituting the assumption
h : O = O.succ into the proof of
Q(O), we would have a proof of
Q(O.succ), equally a proof of
O ≠ succ(O). But this contradicts
One point to note about the proof above is that when we derive
O ≠ succ(O)), we haven’t immediately finished the proof. That’s because we only proved
Q(O.succ) on the assumption
h : O = O.succ.
One approach is to define
O = y → P(y), where
P is the predicate defined so that
O and is
def P : mynat → Prop | O := true | (succ k) := false def Q (y : mynat) : Prop := O = y → P y
O = O → P(O), which is
O = O → true. This, clearly, is something we can prove.
lemma QO : Q(O) := λ h, trivial
On the other hand,
O = O.succ → P(O.succ), equally
O = O.succ → false.
example : Q(O.succ) = (O ≠ O.succ) := rfl
It merely remains to finish the argument by substitution.
example : O ≠ succ(O) := assume h : O = succ(O), have h₂ : O ≠ succ(O), from @eq.subst _ Q _ _ h QO, show false, from h₂ h
We can easily generalise this argument.
lemma succ_ne_zero (m : mynat) : O ≠ succ(m) := assume h : O = succ(m), have h₂ : O ≠ succ(m), from @eq.subst _ Q _ _ h QO, show false, from h₂ h
Pingback: Injectivity of succ – exlean