Understanding the use of `injection` in Ch2.1

Stream: Analysis I

[intarga]

Hello, I'm new to both lean and analysis. I'm struggling to understand theorem Nat.succ_ne, specifically this line:

  injection h

Going in, we have tactic state:

n : Nat
h : n++ = 0
⊢ False

My understanding of injection is that it requires both sides of the equality to be expressible as the same constructor, and it will transform the equality into equalities between each of the arguments of the constructor. I don't understand how this can apply here, as n++ and 0 do not use the same constructor.

The book introduces this as an axiom, so it doesn't give any insight into the reasoning here either. The rest of the theorems in the section make sense to me (including succ_cancel which also uses injection), it's only this one I'm stumped on.

[Aaron Liu]

it works when both sides of the equality have the same constructor, and it will use constructor injectivity to break it into equality of the parts

it also works when the equality is between two different constructors, and it will use constructor injectivity to derive a contradiction

[intarga]

Ahh I see!

But then the book discusses a similar number system that "wraps around", so this theorem shouldn't apply there, does that mean that that number system could not be defined with two constructors like Nat?

[Aaron Liu]

the property of Nat which allows you to prove this is that Nat is initial

[Aaron Liu]

that means you can do recursive pattern matching on it and the resulting function satisfies some definitional reductions

[intarga]

Initial meaning it has an initial value 0 that others can be constructed from? What determines that Nat is initial? The fact that it has one and only one constructor which doesn't take an argument?

[Aaron Liu]

intarga said:

Initial meaning it has an initial value 0 that others can be constructed from? What determines that Nat is initial? The fact that it has one and only one constructor which doesn't take an argument?

initial in the category-theory sense, that for any other type X with functions zero : X and succ : X → X, there exists a unique map f : Nat → X := Nat.rec zero (fun _ => succ) such that f 0 = zero and f n++ = succ (f n)

[Aaron Liu]

here's a proof using the raw recursors

example : ∀ (n : Nat), Nat.succ n = Nat.zero → False :=
  fun (n : Nat) (hn : Nat.succ n = 0) =>
    @Eq.rec Nat (Nat.succ n)
      (fun (a : Nat) (ha : Nat.succ n = a) =>
        @Nat.rec (fun (u : Nat) => Prop) False
          (fun (s : Nat) (ih : Prop) => False → False) a)
      (fun (f : False) => f) Nat.zero hn

[Aaron Liu]

intarga said:

What determines that Nat is initial? The fact that it has one and only one constructor which doesn't take an argument?

All inductive types are initial

[Aaron Liu]

it's like the definition of inductive type or something

[Ruben Van de Velde]

Looking it from the lean side, no, a function where succ succ succ ... zero would be equal to zero can't be implemented in lean as an inductive type that looks like Nat

[intarga]

Aaron Liu said:

intarga said:

What determines that Nat is initial? The fact that it has one and only one constructor which doesn't take an argument?

All inductive types are initial

Ok, this makes sense to me. So it would be correct to say that a "wrapping" number system as described in the book would not be definable as an inductive type?

[Aaron Liu]

you can't define such a wrapping number system in Lean as an inductive type with succ as a constructor

[intarga]

Excellent, thanks a bunch for the help!

[Kevin Buzzard]

It is an (in my mind) pretty amazing fact that Lean manages to shrink Peano's original bunch of axioms down to three:

1) zero is a natural
2) the successor of a natural is a natural
3) That's it.

What (3) means formally is "the only way you can make naturals is via (1) and (2)", a.k.a. "if you want to do something for all naturals, it suffices to (a) do it for zero and, (b) assuming you've done it for n, do it for the successor of n" a.k.a. the principle of mathematical recursion (which contains induction as a special case, where the thing you're doing for n is proving the statement P(n)). Using only this, you can actually prove things like the successor function being injective, 0 not being a successor and so on. I do this in the natural number game.