# Zulip Chat Archive

## Stream: general

### Topic: NN Game Inequality World Level 9 Help

#### Andrew Helwer (Mar 03 2020 at 03:22):

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 (Mar 03 2020 at 03:31):

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 (Mar 03 2020 at 20:50):

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 (Mar 03 2020 at 21:47):

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 (Mar 03 2020 at 22:22):

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 (Mar 03 2020 at 23:20):

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 (Mar 04 2020 at 20:46):

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 (Mar 04 2020 at 21:21):

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 (Mar 04 2020 at 21:23):

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

#### Andrew Helwer (Mar 04 2020 at 21:30):

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 (Mar 04 2020 at 21:46):

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 (Mar 05 2020 at 00:43):

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 (Mar 05 2020 at 21:44):

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?

Last updated: Aug 03 2023 at 10:10 UTC