Zulip Chat Archive

Stream: new members

Topic: Goals which are disjunctions


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Dec 18 2020 at 20:16):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Dec 18 2020 at 20:19):

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

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Dec 18 2020 at 21:07):

How long have you been assuming it? ;-)

view this post on Zulip Kevin Buzzard (Dec 18 2020 at 21:07):

You're beginning to discover the ugly truth

view this post on Zulip 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 :-(.

view this post on Zulip 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