# One of these things is not like the other

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 `0`.

``````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` and `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 `false`.

What data do we have? We have an equation `O = O.succ`. Thus, anything true for `O` is also true for `O.succ`.

The clever idea is to construct a predicate `Q` on `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 `h`.

One point to note about the proof above is that when we derive `Q(O.succ)` (i.e. `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 `Q(y)` by `O = y → P(y)`, where `P` is the predicate defined so that `P(y)` is `true` when `y` is `O` and is `false` otherwise.

``````def P : mynat → Prop
| O         := true
| (succ k)  := false

def Q (y : mynat) : Prop := O = y → P y``````

Then `Q(O)` is `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, `Q(O.succ)` is `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``````