Explain induction in baby-steps.

Stream: new members

[Jay]

I am new to Lean (just started today).

The first thing I am struggling with is the induction tactic from the "Addition world" tutorials in the Natural Number Game. It asks me to use it but I don't understand what it is doing.

Here is where its use is introduced:

https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Addition/level/1

If I use

induction n with d hd

It splits into two goals. The manual page on this even use the same example to explain induction but I still don't understand what happened when I applied it.

Will you please explain?

[llllvvuu]

Are you familiar with Algebraic Data Types (e.g. Rust, Haskell, etc)? If so, this syntax may be more familiar to you:

theorem zero_add₁ (n : Nat) : 0 + n = n :=
  match n with
  | .zero => sorry
  | .succ n => sorry

This is ~the same:

theorem zero_add₂ (n : Nat) : 0 + n = n := by
  induction n with
  | zero => sorry
  | succ n hn => sorry

It is like "if-else" but it has support from the type theory via a rule in the type theory known as the "recursor" or "eliminator", which basically postulates that if a type as defined as one of N things, then we can define a function on that type by defining it on each of those N things.

[llllvvuu]

Note that induction in the Natural Number Game is overridden to use Lean 3 syntax which is different from Lean 4 syntax. I think this is confusing, but much ink has already been spilled on this topic (search "nng induction'").

[Mario Carneiro]

The idea behind induction is that every element of an inductive type is built up by applying constructors finitely many times, so if we can establish a property by reducing it to the same property on smaller pieces then we will have shown that every value has the property.

As it applies to Nat, we have two constructors, zero : Nat and succ : Nat -> Nat. So if zero has property P, and successors of things with property P also have property P, then everything built up from zero and successor (which is everything in the type) has property P.

This is all then wrapped up in a convenient tactic called induction. When you write induction n, lean takes your goal to be the property P n here, and then applies the rule of proof by induction, meaning that we have to show that P 0 holds, and that P (succ n) holds given that P n holds. These are the two subgoals that lean will give back to you.

[Jay]

Thanks. I am going to take these responses and go back to the tutorial and try to work through the idea for a while. I will come back when I have learned something new or got stuck.

[Jay]

Ok. That was a partial success. I will need to go through the intro to induction again. I made it through the tutorial and finished all the games. Unfortunately, I think I cheated. I merely reused induction in the same way I'd seen it used in previous examples so I knew what tactics and theorems to use to complete the game but I don't believe I really understood why it worked. I really just repeated a process without understanding its function.

That's probably enough for me for one night. Thank you all for you help so far. I am likely to come back for more tomorrow.

[Mark Fischer]

Here's how I understand it (I'm new too so take it this with the appropriate grain of salt :P).

Lean is based on the Calculus of Inductive Constructions which I think comes with the idea of induction sort of built in. Which is to say you need to be convinced that a proof by induction is a valid line of reasoning a priori.

---

Here's a sort of loose-weave example. Say I want to convince somebody that I'll never be older than my brother.

• When I was born, my brother was older than me.
• If my brother is older than me for a given year, he will still be older than me the next year (This is because each year we both age the same amount).
• Therefore, for any year after my birth, my brother is older than me.

Without any concrete information about how old we are today or how old we'll end up being is this a valid argument? It seems like it, right?

Ok maybe the argument isn't sound in this case - if my brother stops aging when he dies, or if we may need to account for time dilation due to space travel, then one of the premises is suspect (Which would mean you wouldn't find a proof for the inductive step).

Though assuming the premises are true, then conclusion seems to follow.

---

How does this work in lean? I'm actually not sure. I think it's just a rule in the foundational system. If you have an inductive proof that is run-able as a program, then I think the runtime semantics would be that you could feed it a specific age (say 13) and the proof would loop through my ages from 0 to 13, at each step is applies the proof of the inductive step to show that it's true for the next year, and then it can return a proof that when I'm 13, my brother is older than me. Because this can be done for any age, the type system sees this as a proof for every age.

[Mr Proof]

I would also like to know if "proof by induction" is an additional axiom that has to added to the other logical axioms, or whether it follows from other axioms. I seem to recall that somewhere it said that proof by induction is it's own axiom, but I'm not sure.

[Henrik Böving]

Proof by induction is a consequence of the recursors and their computation rules that are axiomatically generated for each inductive type.