NN Game Inequality World Level 9 Help

Stream: general

[Andrew Helwer]

The goal: theorem le_total (a b : mynat) : a ≤ b ∨ b ≤ a :=

I try to use induction on a or b but always get to something like this state:

a d : mynat,
q : ∃ (c : mynat), a = d + c
⊢ ∃ (c : mynat), a = succ d + c

Which... I don't think is provable, because you need the assumption that c is nonzero I think. Help? Here's my proof so far:

rw le_iff_exists_add,
rw le_iff_exists_add,
induction b with d hd,
right,
use a,
rwa zero_add,
cases hd with p q,
cases p with e he,
left,
use succ e,
rw add_succ,
rw succ_eq_succ_iff,
exact he,
right,

Any help would be appreciated!

[Jalex Stark]

This might help:

rw le_iff_exists_add,
rw le_iff_exists_add,
induction b with d hd,
right,
use a,
rwa zero_add,
cases hd with p q,
cases p with e he,
cases e,
left,
use 1,

[Andrew Helwer]

I'm actually not sure that does help, as it solves a case I was already able to solve. I still end up with the same state with:

rw le_iff_exists_add,
rw le_iff_exists_add,
induction b with d hd,
right,
use a,
rwa zero_add,
cases hd with p q,
cases p with e he,
cases e,
left,
use 1,
rw add_one_eq_succ,
rw add_zero at he,
apply succ_eq_succ_of_eq,
exact he,
left,
use succ (succ e),
rw add_succ,
apply succ_eq_succ_of_eq,
exact he,
right,

[Kevin Buzzard]

Do you know a maths proof @Andrew Helwer ? It's getting to the point of the game where you can't just jump in, you need to have a plan.

[Andrew Helwer]

I actually don't know the proof off the top of my head... looking at the solution to this it seems as though this is another case of using revert on a variable before using induction: https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world10/level9.lean

[Kevin Buzzard]

Right. You can't just fix a and induct on b because you end up with an inductive hypothesis you can't use. You have to think about precisely which statement you're going to prove by induction

[Andrew Helwer]

It's difficult for me to wrap my head around when we'd want to revert a variable before inducting on it. Would be helpful to have a level or two focusing on it!

[Kevin Buzzard]

Induction, at its heart, is infinitely many statements $P(0),P(1),P(2)\,dots$, plus a proof of $P(0)$, plus a proof that $P(n)\implies P(n+1)$. Mathematicians often say "now done by induction" without making absolutely precise what $P(n)$ is. If you have some statement $Q(m,n)$ involving variables $m$ and $n$, and a mathematicians says "prove it by induction on $n$", it's not entirely clear what they mean. One possibility is that we fix an integer $m$, regard it as a constant, and define $P(n)$ to be $Q(m,n)$. Another possibility is that we define $P(n)$ to be $\forall m, Q(m,n)$. You can see that this is a different $P(n)$. These choices might looks "sort of the same" but they're not, because when you're trying to deduce $P(n+1)$ from $P(n)$, in one situation $m$ is fixed but in another situation you're allowed to change it -- you have a stronger hypothesis but you're trying to prove a stronger conclusion. I'm in a bit of a rush right now and unfortunately do not have some crystal clear example which I can give you off the top of my head, but this is the heart of it I think. An example would probably make things clearer -- but on the other hand, you're looking at an example right now in this Lean level.

[Chris Hughes]

There's never a downside to using $\forall m, Q(m,n)$ instead of $Q(m,n)$ as your induction hypothesis.

[Andrew Helwer]

Thanks for the explanation! I will think on this and try to break down exactly how it makes a difference in the two levels I've found so far where it's important.

[Kevin Buzzard]

The difference is that q is useless here

q : ∃ (c : mynat), a = d + c
⊢ ∃ (c : mynat), a = succ d + c

because, using the language of my earlier post, $P(m,n)$ does not actually imply $P(m,n+1)$. But maybe $\forall m, P(m,n)$ might imply $\forall m, P(m,n+1)$.

I am hoping that over Easter I will be able to make all the changes which people have been suggesting for the game; until then I need to concentrate on UG teaching etc.

[Scott Morrison]

It might simply suffice in this level to add a link to an extra "spoiler" page, which just includes Kevin's "Induction, at its heart ..." paragraph above, and perhaps says something about revert and induction ... generalizing ....

[Andrew Helwer]

it's tricky because it's quite a subtle difference I think. Even in the cases where fix m as some arbitrary value, that implicitly says it would work for any m in the natural numbers right?