Zulip Chat Archive

Stream: new members

Topic: Natural numbers game

alex van tilburg (Jan 27 2021 at 10:14):

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 (Jan 27 2021 at 10:15):

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 (Jan 27 2021 at 10:18):

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 (Jan 27 2021 at 10:21):

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 (Jan 27 2021 at 10:22):

Okay thx I'll try it

alex van tilburg (Jan 27 2021 at 10:30):

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 (Jan 27 2021 at 10:35):

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 (Jan 27 2021 at 10:38):

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 (May 08 2021 at 13:38):

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

Patrick Massot (May 08 2021 at 13:44):

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 (May 08 2021 at 13:44):

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

Mario Carneiro (May 08 2021 at 13:45):

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

Patrick Massot (May 08 2021 at 13:47):

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 (May 08 2021 at 13:48):

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

Patrick Massot (May 08 2021 at 13:48):

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

Mario Carneiro (May 08 2021 at 13:50):

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

Mario Carneiro (May 08 2021 at 13:52):

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

Mario Carneiro (May 08 2021 at 13:52):

although probably not the way you intended

JIM (May 08 2021 at 13:55):

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

Patrick Massot (May 08 2021 at 13:56):

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

Hunter Monroe (Jun 23 2021 at 16:29):

@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 (Jun 23 2021 at 16:29):

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

Hunter Monroe (Jun 23 2021 at 16:48):

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

Hunter Monroe (Jun 25 2021 at 04:08):

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 (Jun 25 2021 at 06:11):

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 (Jun 25 2021 at 07:39):

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

Kevin Buzzard (Jun 25 2021 at 20:26):

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 (Jun 28 2021 at 10:47):

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 (Jun 28 2021 at 10:49):

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 (Jun 28 2021 at 10:51):

Ok no worries, thanks! :)

Kevin Buzzard (Jun 28 2021 at 10:53):

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 (Jun 28 2021 at 15:28):

@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 (Jun 28 2021 at 15:32):

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 (Jun 28 2021 at 15:42):

Yes. I was thinking something like:

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

Stephen Butler (Jun 28 2021 at 15:46):

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.

Last updated: Dec 20 2023 at 11:08 UTC