## Stream: new members

### Topic: Goals which are disjunctions

#### Victor Miller (Dec 18 2020 at 20:14):

I'm working my way through the natural number game and have gotten everything except for inequality world 9:
theorem le_total (a b : mynat) : a ≤ b ∨ b ≤ a :=. The problem here is that the goal is a disjunction. Normally, I know that
 P \or Q  is equivalent to  \not P \-> Q, and so I would start with an intro to get \not P in as a hypothesis, but I can't do that. I've fiddled around with trying to introduce \not a \le b as a hypothesis, or do a by_cases on that, but lean says that it isn't decidable. I'm stuck -- what am I missing here? Remember that the natural number game rules are (or should be) restricted to the tactics that are given there.

#### Mario Carneiro (Dec 18 2020 at 20:16):

I believe NNG teaches that you can prove a disjunction using left or right

#### Kevin Buzzard (Dec 18 2020 at 20:16):

Let P(a) be "for all b, a<=b or b<=a" and prove by induction on a?

#### Mario Carneiro (Dec 18 2020 at 20:16):

Of course, you can't start the proof like that because you will get an unsolvable goal, but if you use induction that's how you can finish

#### Victor Miller (Dec 18 2020 at 20:17):

That's what I was afraid of. Is it not safe to consider P or Q as equivalent to not P -> Q?

#### Kevin Buzzard (Dec 18 2020 at 20:18):

Yes that's the same, probably you can do that in NNG as well, but what is "not a<=b" going to buy you?

#### Kevin Buzzard (Dec 18 2020 at 20:19):

it's "for all c, b isn't a + c"

#### Victor Miller (Dec 18 2020 at 20:52):

Thanks all. I did finally do it by induction and many cases. The proof was really long!

#### Kevin Buzzard (Dec 18 2020 at 21:07):

How long have you been assuming it? ;-)

#### Kevin Buzzard (Dec 18 2020 at 21:07):

You're beginning to discover the ugly truth

#### Victor Miller (Dec 18 2020 at 21:25):

I remember looking at Russell and Whitehead's Principia a number of years ago and wondering why it was so long. Now I have an idea :-(.

#### Kevin Buzzard (Dec 18 2020 at 21:54):

Of course the idea is not that we all recreate the basic interface for the natural numbers -- the idea is that we take the maths that interests us and makes it in the way that mathematicians make it, because all this basic stuff is in the library already.

Last updated: May 09 2021 at 19:11 UTC