Natural numbers game

Stream: new members

[alex van tilburg]

I am new to Lean. I was doing the Natural numbers game. I don't know if you all heard of it but I am stuck in the advanced multiplication world. Can someone give me a hint how to prove theorem mul_pos (a b : mynat) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=.

[Kevin Buzzard]

My instinct would be to show that a=succ(something), and then b=succ(something) and then deduce that a * b = succ(something) and hence not 0

[Callum Hobbis]

I am also very new to Lean, but I found that when I was going through the Natural Numbers Game and I got to the Advanced Multiplication World, my thinking had to shift from 'follow your nose and just do the most obvious thing at each step' to 'think about it mathematically, how you would prove it with a pen and paper, and then formalise it' - I got stuck on this level too when just trying to do the most obvious thing at each step!

[Kevin Buzzard]

Looking at the answers in the github repo, my sketch proof above seems to be the one in the repo and it comes out relatively painlessly, you finish with succ_ne_zero. I agree that at some point you have to stop following your nose! We get a fair few questions about level 4 of advanced multiplication world here. Hopefully the comments in the level now make it easier, but it's still a toughie.

[alex van tilburg]

Okay thx I'll try it

[alex van tilburg]

Okay @Kevin Buzzard thank you so much for the hint to end with succ_ne_zero. It helped me to see how to finish the prove so where to work to. I got to finish the prove after a day struggling with it.

[alex van tilburg]

This question is about the next one where I also struggled. theorem eq_zero_or_eq_zero_of_mul_eq_zero (a b : mynat) (h : a * b = 0) : a = 0 ∨ b = 0 := I want to prove it with exfalso since I have h: succ c * succ d = 0 and I want to prove succ c \ne 0 and succ d \ne 0 and use this fact to apply mul_pos, but how should I write that down in Lean?

[alex van tilburg]

Okay I just tried to apply mul_pos to the false goal and the goals are managable now so I got it thx anyways.

[JIM]

Hi everyone,
I'm stuck when solving the Natural number game level 10.
could anybody teach me how to do next?
image.png
at the same time, however, when i'm trying to solve the problem, i happen to type like this:
image.png
it says that the goal is completed
i'm comfused about what's happening

[Patrick Massot]

The first tip is to post urls to the level you are talking about, especially since you didn't mention a world name. https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=8&level=10 Then you can copy-paste text instead of screenshots so that people can read them easily and copy-paste them into the game.

[Mario Carneiro]

cases b with a,
refl,
rw add_succ at H,
exfalso,
by cases h:H,

[Mario Carneiro]

This is a complete proof, there isn't anything wrong

[Patrick Massot]

Mario, this assumes too much understanding of what Lean is actually doing. I'm sure Kevin meant exact succ_ne_zero (a+d) H, as the last line.

[Mario Carneiro]

Oh, is cases on equality not taught at this point?

[Patrick Massot]

I would be surprised if this were taught at all in the NNG

[Mario Carneiro]

there are other things wrong here: by is superfluous, and cases h:H is more simply written cases H

[Mario Carneiro]

but from a technical standpoint that text does make lean produce a valid proof

[Mario Carneiro]

although probably not the way you intended

[JIM]

thank you, I'm new with this but I will follow the tip mext time

[Patrick Massot]

There is no problem at all. Everyone needs to learn those kind of things when arriving here.

[Hunter Monroe]

@Kevin Buzzard The pro tip "Did you spot the import? What do you think it does?" in the natural numbers game in world 7 level 8 is on a page with no (visible) import. Should this have been in level 9? I did not make a PR.

[Kevin Buzzard]

lol, please make a PR and I'll deal with it when I'm at a computer. Thanks

[Hunter Monroe]

OK see https://github.com/ImperialCollegeLondon/natural_number_game/pull/113

[Hunter Monroe]

Some of the theorem names in the game do not match mathlib, eg succ_inj vs succ.inj--perhaps they should be aligned to smooth the transition from one to the other?

[Huỳnh Trần Khanh]

I would say that this doesn't really matter. There are a lot of differences between the natural number game and mathlib. There are even theorems that are equivalent to refl.

[Eric Wieser]

Note that even the rw tactic is different to the one in regular lean

[Kevin Buzzard]

It is what it is, it seems to work, I know I should explain {} better, I am reluctant to mess with what seems to be a winning strategy.

[Gemma Crowe]

Hi! Does anyone know if I can install the Natural numbers game on my computer with blank copies of the exercises? At the moment each task has the solution filled in already, and I'd like to work through these myself before looking at the solutions. For some reason it's not saving my progress when I try this online :( thanks!

[Kevin Buzzard]

Hmm. I would be tempted to just rewrite the game yourself :-)

Unfortunately the framework we used to make NNG meant that we had to also supply all solutions. If you would like to work on basic Lean stuff on your own computer then maybe you'd prefer the complex number game which you can just download and install and fill in the sorrys yourself. This game assumes that we have a fully working copy of the real numbers to hand, and then makes the complex numbers from scratch.

[Gemma Crowe]

Ok no worries, thanks! :)

[Kevin Buzzard]

I guess the full nerd thing to do would be to download the NNG repo with leanproject and then write a regex which matches the begin [natnumgame] ... end blocks and sorries them out.

[Stephen Butler]

@Gemma Crowe @Kevin Buzzard I wonder if some cunning search and replace can take all of the begin < stuff> end blocks from the completed files with solutions and replace them with begin sorry end ?

[Patrick Massot]

As usual with grep/sed/awk, as soon as you need to spend more than ten seconds thinking about how to do it, you'll have an easier time writing a python script doing it. See for instance how this problem is handled in https://github.com/leanprover-community/lftcm2020/blob/master/mk_exercises.py

[Stephen Butler]

Yes. I was thinking something like:

read line
is it a begin?
   write  to output file:
        begin
        sorry
        end
else
    write line to output file

[Stephen Butler]

I've not really looked at Python. C and C++ were more my thing. Plus a whole load of shell and other scripting. Although I never really got deeply into sed and awk.