In lean, why is it possible to prove zero_ne_succ (without adding it as an axiom) by using pattern matching?

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

(A supplement to @It'sNotALie's answer.) My understanding is that 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

protected eliminator mynat.rec : Π {motive : mynat → Sort l},
  motive mynat.zero → (Π (ᾰ : mynat), motive ᾰ → motive ᾰ.succ) → Π (n : mynat), motive n

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 defintion. The elimination principle 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.

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.binduction_on
#print mynat.brec_on
#print mynat.cases_on
#print mynat.has_sizeof_inst
#print mynat.ibelow
#print mynat.no_confusion
#print mynat.no_confusion_type
#print mynat.rec_on
#print mynat.sizeof
#print mynat.succ.inj
#print mynat.succ.inj_arrow
#print mynat.succ.inj_eq
#print mynat.succ.sizeof_spec
#print mynat.zero.inj
#print mynat.zero.inj_arrow
#print mynat.zero.inj_eq
#print mynat.zero.sizeof_spec

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

def mynat.succ.inj : ∀ {ᾰ ᾰ_1 : mynat}, ᾰ.succ = ᾰ_1.succ → ᾰ = ᾰ_1 :=
λ {ᾰ ᾰ_1 : mynat} (a : ᾰ.succ = ᾰ_1.succ), mynat.no_confusion a (λ (ᾰ_eq : ᾰ = ᾰ_1), ᾰ_eq)

Second, 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.

And as @It'sNotALie implied, you can see this by printing out any proof to see what it becomes underneath (and use set option pp.all true to remove any syntactic sugar if needed).

Answer 2

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).