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