NNG world 9 level 4

Stream: new members

[Matt Yan]

world 9 level 4 shows an example where a stronger (more general) version of the theorem is provable but (supposedly) a weaker version can't be proved. This is very counter-intuitive. Is this a limitation of Lean? And honestly I can't tell the differences between the "stronger" theorem $a \, c: \N, ha: a \ne 0 \vdash \forall b, ab = ac \Rightarrow b = c$ and the "weaker" theorem $a\, b\, c : \N, ha: a \ne 0 \vdash ab = ac \Rightarrow b = c$. It feels a bit weird to have $\forall$ in the game for the first time (a mix of set-theoretic language and type-theoretic language)?

[Yaël Dillies]

That's very common with induction, isn't it? You sometimes have to strengthen the induction hypothesis for the induction to carry through.

[Kevin Buzzard]

Ha no it's not a limitation of Lean! It's the way mathematics works.

[Matt Yan]

Guess I'll just have to step up my induction game. Personally, I think there is a more intuitive proof without modifying the theorem, which can't be used somehow? If you just do a basic induction c with n hn, you'll end up with hn: ab = an -> b=n. In a classical proof, I would immediately discuss by cases:
Case 1. ab = an is true
this can then nicely substituted into the goal to show it's vacuously true (the antecedent becomes a = 0 and is false)
Case 2. ab = an is false
this means the induction hypothesis is vacously true and anything follows.

I remember doing similar stuff with by_cases to a term of Proposition type...but somehow this can't be done for a = b types?

[Daniel Roca González]

Wait what is your goal in that context?

[Kevin Buzzard]

Probably the way to think about this is to step back and actually ask yourself "what is induction?" . Here's what it is. You have some context (some variables, or whatever, which are fixed and which you can use to make mathematical statements) and then infinitely many true-false statements P(0), P(1), P(2), ... . You want to prove them all. The principle of induction says that if you prove P(0) and "forall n, P(n) - P(n+1)" then you can deduce them all. The subtlety in this level is that if you have some stuff in your context, like a variable b, then that variable is fixed. If the P(n) all depend on b then b can't change as you start manipulating the P(n). However if your context doesn't contain the variable b but P(n) is of the form "for all b, (something to do with b and n)" then this is different, because if you know P(n) then you know a statement about all b, and you might want to prove P(n+1) for a specific b by using P(n) for b+1 or something like that. You can't do this if b is in your context, you can only do it if it's being universally quantified over as part of P.

In short, when you're doing induction to prove a statement P, in a language like Lean, you have to really think hard about precisely what P says, and in particular which variables are free and which are bound.