In Lean, why is it possible to prove $\text{succ}\; x \neq 0$ without adding it as an axiom?

Question

If I define a custom set of natural numbers:

inductive mynat : Type
| zero : mynat
| succ : mynat → mynat

I can prove no successor is equal to 0 by defining a function using pattern matching:

def is_zero : mynat -> Prop
| mynat.zero := true
| (mynat.succ _) := false

theorem mynat_zero_ne_succ (a : mynat) : mynat.succ a ≠ mynat.zero :=
begin
    have r : is_zero (mynat.succ a) = is_zero (mynat.succ a),
    refl,
    conv at r {
        to_lhs,
        rw is_zero,
    },
    apply not.intro,
    intro h,
    rw h at r,
    rw is_zero at r,
    rw r,
    exact true.intro
end

Normally "no successor equals zero" is one of the Peano axioms. It has to be stated to get the natural numbers. But here it's apparently a theorem that you get as soon as you define the successor function.

I can see that what's going in here is something very fundamental in Lean about how inductive types or pattern matching work (and therefore how equality must work). The definition of the function, and the way it's used when rewriting, presupposes that zero is never of the form "succ _". I was wondering what that something actually is, and what it's called.

Answer 1

Update: Since this is the accepted answer and since it was originally written for Lean 3, let me update it to Lean 4 with a bit more information.

First, the proof is simply

theorem mynat_zero_ne_succ (a : mynat) : mynat.succ a ≠ mynat.zero := by
  simp

(In Lean 3 you could just put a period at the end to get a proof as in @It'sNotALie.'s answer, but that doesn't work in Lean 4.)

---

Here is how this works. When you do

inductive mynat : Type
| zero : mynat
| succ : mynat → mynat

then Lean is adding four new "things" to the context:

inductive mynat : Type

constructor mynat.zero : mynat
constructor mynat.succ : mynat → mynat

recursor mynat.rec.{u} : {motive : mynat → Sort u} →
  motive mynat.zero → ((a : mynat) → motive a → motive (mynat.succ a)) → (t : mynat) → motive t

These "things" could be thought of as axioms, but unlike typical axioms there is no danger of these being inconsistent with whatever axioms and theorems are already in the environment (assuming Lean's theory and implementation are consistent, and the axioms in the context are as well). So it is more normal to think of them more like automatic definitions and theorems that Lean adds for you.

The inductive type mynat and the two constructors mynat.zero and mynat.succ are clear and just come from the inductive definition. The elimination principle (or recursor as Lean 4 calls it) mynat.rec is the workhorse of inductive definitions. It is what is used to do anything we want with mynat including:

• Prove the basic structural facts about zero and succ, including the first three Peano axioms.
• Define any recursive functions on mynat, including the usual + and * along with their four definitional (Peano axiom) equalities.
• Prove the induction principle.

The elimination principle rec is discussed in Theorem Proving in Lean, 7. Inductive Types. And if you want more detail, the first chapter of The HoTT Book is a great introduction to dependent type theory. Also, see @Andrej Bauer's answer for a direct proof using mynat.rec.

But also note, you will almost never need to use the elimination principle rec directly. First, Lean automatically defines a number of definitions and theorems based on rec. (Unlike rec these are not "axioms". They have proofs/definitions.) For mynat, here are a list of all the automatically generated theorems and definitions that Lean creates for mynat.

#print mynat.below
#print mynat.binductionOn
#print mynat.brecOn
#print mynat.casesOn
#print mynat.ibelow
#print mynat.noConfusion
#print mynat.noConfusionType
#print mynat.recOn
#print mynat.succ.inj
#print mynat.succ.injEq

For example, mynat.succ.inj is the usual Peano axiom saying that successor is injective:

theorem mynat.succ.inj : ∀ {a a_1 : mynat}, mynat.succ a = mynat.succ a_1 → a = a_1 :=
fun {a a_1} x => mynat.noConfusion x fun a_eq => a_eq

In Lean 3 these were all created automatically and easy to find via autocomplete. In Lean 4, they are more hidden and I don't believe they are intended to be called directly by a typical user.

Instead one can access them via the simp tactic. Hence the by simp proof above. Notice how simp fills in a proof using myNat.noConfusion:

theorem mynat_zero_ne_succ : ∀ (a : mynat), mynat.succ a ≠ mynat.zero :=
fun a => of_eq_true (Eq.trans (congrArg Not (eq_false' fun h => mynat.noConfusion h)) not_false_eq_true)

See the Lean 3 blog post No confusion over no_confusion for a deeper explanation of what is going on here.

Other tactics like contradiction also do something similar.

theorem mynat_zero_ne_succ (a : mynat) : mynat.succ a ≠ mynat.zero := by
  intro h
  contradiction

and gives a cleaner proof underneath:

theorem mynat_zero_ne_succ : ∀ (a : mynat), mynat.succ a ≠ mynat.zero :=
fun a h => mynat.noConfusion h

Moreover, the tools in Lean for working with inductive definitions such as the induction and cases tactics, as well as match statements all use (or de-sugar in the case of match) to using these built-in theorems and definitions. (Note, that is on the theorem-proving side. When it comes to generating executable code in the compiler or virtual machine, I think Lean avoids mynat.rec entirely and directly converts, say, match to executable code.)

Answer 2

In Lean type theory $\mathrm{succ}\,n \neq 0$ may be simply proved using recursion, as follows.

Theorem: For all $n : \mathbb{N}$, $\mathrm{succ}\,n \neq 0$.

Proof. Define $f : \mathbb{N} \to \mathrm{Prop}$ by $$f = \mathrm{rec}_\mathbb{N} \, (\lambda x . \mathrm{Prop}) \, \bot \, (\lambda x y . \top),$$ where $\mathrm{rec}_\mathbb{N}$ is the induction principle for the inductive type $\mathbb{N}$. Consider any $n : \mathbb{N}$. By the definition of $f$: \begin{align*} f(0) &\equiv \bot, \\ f(\mathrm{succ}\,n) &\equiv \top. \end{align*} If it were the case that $\mathrm{succ}\, n = 0$ then it would follow that $\top = f(\mathrm{succ}\,n) = f(0) = \bot$, therefore $\bot$ would be true. $\Box$

Here is the Lean proof of the theorem, without any tactics:

inductive N : Type
| zero : N
| succ : N → N

def f : N → Prop :=
  @N.rec (fun _ => Prop) False (fun _ _ => True)

example (n : N) : N.succ n ≠ N.zero :=
  fun e => @Eq.subst _ f (N.succ n) N.zero e True.intro

What is going on? Peano arithmetic is a single-sorted theory in which we can speak only about numbers, so there we must postulate that not all numbers are equal, or else the theory could be trivial. In constrast, type theory contains natural numbers as just one inductive type, and we can use the recursion principle to define maps out of it, just like we did above.

We should mention that the use of Prop (or a universe) is essential here, as it is well-known that Martin-Löf type theory without univeres does not prove $0 \neq 1$.

Answer 3

Some good resources on topics like this are Theorem Proving in Lean and no confusion over no_confusion. Essentially, injective types are designed in this way; I think TPIL puts it most succintly:

By design, the elements of an inductive type are freely generated, which is to say, the constructors are injective and have disjoint ranges.

Fun fact: a valid proof of this statement is actually theorem mynat_zero_ne_succ (a : mynat) : mynat.succ a ≠ mynat.zero. (you can #print mynat_zero_ne_succ to see the term mode, and you'll also see why I linked the no_confusion article).

Answer 4

I recently asked this question and got linked to here. Between the comments on my question and the answers on this one I found out how to witness the proof of "zero is not one" and that "succ is injective". However, the proofs I found seem different enough to the others above that I thought it worth posting what I did - I can't post on my original question because that got closed. Also there might be some changes between LEAN3 and the proofs below I wrote in LEAN4.

As @It'sNotALie said, it's because the inductive type constructors are all injective. But how can we actually write the proof? TPIL4 Chapter 7: Inductive Types (CTRL + F: "injective") does explain how to do this. There is a tactic injective that witnesses the difference between terms constructed by distinct constructors. Using this tactic you can write the following:

inductive Peano where
  | zero : Peano
  | succ : Peano → Peano
  deriving Repr

open Peano

def pred (m : Peano) : Peano :=
  match m with
    | zero   => zero
    | succ n => n

theorem succ_injective (m n : Peano) : (succ m) = (succ n) → m = n :=
  by
    intro t
    injection t

theorem zero_neq_one : zero ≠ (succ zero) :=
  λ e : zero = (succ zero) => by injection e

theorem zero_not_succ (m : Peano) : zero ≠ succ m :=
  by
    intro t
    injection t

As suggested in TPIL4 one can write the proofs in more than one way.

theorem zero_not_succ (m : Peano) : zero ≠ succ m :=
  by
    intro t
    contradiction

One of the articles linked on this question suggests that injectivity of the successor constructor can be witnessed by constructing an inverse pred. This can be done as follows:

def pred (m : Peano) : Peano :=
  match m with
    | zero   => zero
    | succ n => n

theorem succ_injective (m n : Peano) : (succ m) = (succ n) → m = n :=
  by
    intro t
    exact congrArg pred t