connection b/w induction proofs and recursive def of ℕ

Stream: new members

[rzeta0]

I'm trying to understand the connection between the template for simple induction and the recursive definition of natural numbers.

Here's the template for simple induction:

  induction n with
  | zero =>
    sorry
  | succ n ih =>
    sorry

and here is Lean's definition of Nat

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

I think I understand the connection intuitively but if I try to write it down or explain it to someone else - I can't, and that means I don't really understand it.

I apologise if this question is a bit vague - it is because I can't grasp precisely what I don't understand, other than to say "I can't explain the connection".

---

Here is my (failed) attempt at explaining the connection:

• The definition of Nat defines zero. Proving a proposition P is true for zero,, P(0) is nothing special.

• The definition of Nat defines the successor of a natural number as an another natural number. It doesn't define it as unique as per Peano axioms, but I assume that is encoded elsewhere. Proving P(n)→ P(n+1)` is not on it's down sufficient to say the proposition holds for all natural numbers.

• Both together, P(0) ∧ ( P(n)→P(n+1) ) is sufficient to say the proposition is true for all natural numbers n but only if we have some way of generating all the natural numbers, that is showing n+1 exists if n exists, and that is done by the second part of the definition of Nat - `| succ (n : Nat) : Nat.

[rzeta0]

---

Update - I asked on stackexchange and as expected, the outcome was not fruitful.

https://math.stackexchange.com/questions/5017564/connection-between-induction-proofs-and-recursive-definition-of-natural-numbers

[Eric Wieser]

When you write inductive like that, Lean effectively axiomatizes:

• The type Nat
• The constructors Nat.zero and Nat.succ
• The recursion principle Nat.rec
• The reduction rules which characterize this recursion principle

The induction keyword is just sugar for Nat.rec in your example

[rzeta0]

So is the following not actually the definition of Nat but simply defining extra properties of an already defined Nat ?

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

I found this by right-clicking and "Go to definition".

(I realise we've moved away from the original question to explain why induction proofs look like the definition of Nat)

[Matt Diamond]

I asked on stackexchange and as expected, the outcome was not fruitful.

I'm sorry this was the case. Some users on that site can be intolerant towards questions that they feel are insufficiently rigorous, forgetting that rigor requires understanding in the first place.

[rzeta0]

That site used to be better 10 years ago, something has changed. Thanks for your comment, I appreciate it.

[Edward van de Meent]

rzeta0 said:

So is the following not actually the definition of Nat but simply defining extra properties of an already defined Nat ?

no, that is where it is defined. What i think eric is talking about is that lean figures out what induction should look like by itself: whenever you define an inductive, lean automatically gives you a .rec function which allows you to do induction.

[rzeta0]

Thanks Edward, that is helpful. Reading about "inductive types" is on my to-do list.

So back to the original question, I'm trying to understand why an induction proof looks like the definition of Nat.

I recently learned the word "constructor" in the context of the recursive definitions. So I guess my question becomes "why do we match each constructor" in an induction proof.

[Edward van de Meent]

because constructors denote "primitive"/"atomic" ways to create a value of an inductive type: these constructors are considered to be injective "by definition", and only finite uses of constructors can ever occur. Matching each constructor happens because these are exactly all ways to create a new value of the type

[Zhang Qinchuan]

This is more than mathematical induciton, it is structural induction.

Every object of some inductive type is constructed by just one of its constructor, hence you can prove proposition about it by checking all its constructor.

Every natural number in Lean is generated by the rules Nat.zero and Nat.succ freely.

[Yakov Pechersky]

Just like there's an xkcd for many topics, so there is a Xena blog post: https://xenaproject.wordpress.com/2021/04/03/induction-and-inductive-types/

[rzeta0]

Thanks Edward, Yakov and Zhang- I will think about your reply, xenaproject blog (which looks like it might do the trick) and the wikipedia page over the next day or so.

All this is outside my comfort zone so thanks for your patience.

[rzeta0]

So I read the blog and the wiki article and I think they are just beyond my level of expertise.

However I did manage to understand what I think is the key point, also made by Edward above, that the constructors for Nat are all the ways to generate any and all natural numbers, and therefore an induction proof which proves a proposition is true for all these constructors must therefore be true for all natural numbers.

Thanks again for trying to help.