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

Pingback: Injectivity of succ – exlean