natural number game

Stream: Berkeley Lean Seminar

[Kyle Miller]

In the advanced multiplication world, I was trying to prove something by cases, and one of the goals was 0 = succ b. Is there a way to tell it that this is a contradiction? I thought 0 and succ were constructors.

[Kevin Buzzard]

If your goal is 0 = succ b then you can't make any further progress -- you'll have to get a contradiction from your hypotheses.

[Kyle Miller]

Oh right, thanks. Not sure why I thought that should have been possible. (In any case, I passed this pons asinorum -- somehow even after carefully thinking through the induction argument, it took 100x longer than all the exercises to that point. Inequality world has been fine so far, but a \le b \or b \le a gave me pause since it didn't seem constructive at first.)

[Jalex Stark]

you don't need things to be constructive

[Kyle Miller]

How do you set up "assume not(a \le b)"? With everything I tried, Lean complained about how the existential wasn't decidable.

[Jalex Stark]

(also what does "i pass this pons asinorum means?)

[Jalex Stark]

by_cases a \le b?

[Jalex Stark]

should apply the law of excluded middle to split your proof in two, in on branch you have a ≤ b and in the other you have ¬ a ≤ b

[Kyle Miller]

"pons asinorum" referred to an early theorem in Euclid's elements that many had a difficult time getting through. (I think it's the one about the base angles of an isosceles triangle being the same.)

[Jalex Stark]

hah okay, i was confused because google told me exactly what it was, but i still didn't understand your meaning

[Jalex Stark]

is by_cases what you want? or by_contradiction?

[Jalex Stark]

tactic#by_contradiction ?

[Jalex Stark]

ugh the linkifier doesn't work because the title of the relevant section is "by_contra / by_contradiction"

[Kyle Miller]

by_cases a \le b gives by_cases tactic failed, type of given expression is not decidable state

[Patrick Lutz]

what is "the linkifier" btw?

[Kyle Miller]

I think the issue is that a \le b is actually an existential statement, but I don't appreciate why it's not decidable yet

[Jalex Stark]

try typing tactic#simp

[Patrick Lutz]

@Kyle Miller I think it should be something like by_cases h : a \leq b

[Patrick Lutz]

tactic#have

[Patrick Lutz]

oh cool

[Jalex Stark]

can you give me the URL of the level you're playing?

[Jalex Stark]

it shouldn't matter that it's not decidable, because we're mathematicians

[Kyle Miller]

I think I used it without the h : in earlier exercises, but it gives the same error.

[Kyle Miller]

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=10&level=9

[Jalex Stark]

maybe you can tell it to not worry by using the classical tactic

[Kyle Miller]

Indeed you can

[Jalex Stark]

when i write a lean file locally, i start with the following after my imports

noncomputable theory
open_locale classical

[Jalex Stark]

and I haven't had to worry about declaring classical

[Jalex Stark]

but i guess for the NNG this is required

[Jalex Stark]

for anyone following along at home, we came up with this proof script as a way to start off this level

classical,
by_cases a ≤ b,

[Kevin Buzzard]

If you open an issue I will fix this so that you don't have to put classical

[Kyle Miller]

How do you convert a not-exists into a for-all-not?

[Patrick Lutz]

tactic#push_neg

[Kyle Miller]

The next question would be how you import tactic.push_neg from within the body of a proof.

[Kevin Buzzard]

aargh

[Kevin Buzzard]

You should just clone the repo and fill in the sorrys in VS Code, adding imports which you need :D

[Kyle Miller]

Anyway, I'm just trying the classical version as an exercise. I got a perfectly good induction argument.

[Kyle Miller]

I probably should have followed Kevin Buzzard's advice, but I pushed through and did push_neg by hand, so now I have

a b : mynat,
_inst : Π (a : Prop), decidable a,
h : ¬a ≤ b,
f : ∀ (c : mynat), a + c ≠ b
⊢ b ≤ a

I'm not seeing how I would prove this from f.

[Patrick Lutz]

well, at some point you'll probably have to use induction

[Kevin Buzzard]

Do you have le_total yet?

[Kyle Miller]

This would be for le_total itself. (Just finished the natural number game. It was a nice way to get acquainted with Lean! I knew a bit of Agda coming into it, which was likely helpful.)