Zulip Chat Archive

Stream: Lean for the curious mathematician 2020

Topic: Mon afternoon: natural number game


view this post on Zulip Kevin Buzzard (Jul 13 2020 at 11:27):

Links:
1) pdf slides: https://wwwf.imperial.ac.uk/~buzzard/xena/monday_NNG.pdf
2) Natural number game: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/
3) A tactic cheat sheet: https://github.com/kbuzzard/xena/blob/master/tactics.md

Installing the natural number game on your own computer: leanproject get ImperialCollegeLondon/natural_number_game should work, and if it doesn't then ask. If it does work, then open the project (e.g. with code . in the natural_number_game directory, or with "Open Folder" in VS Code and opening the natural_number_game directory). Then open the file src/game/world10/level18q.leanand fill in the sorrys!

view this post on Zulip Johan Commelin (Jul 13 2020 at 12:01):

@LFTCM If you have any questions about NNG, please ask here.

view this post on Zulip Dima Pasechnik (Jul 13 2020 at 12:11):

is it normal that clicking on import data.real.basic just says Loading... on the RHS, and nothing more?

view this post on Zulip Dima Pasechnik (Jul 13 2020 at 12:11):

in vscode, thatis

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:11):

you have a not compiled mathlib

view this post on Zulip Johan Commelin (Jul 13 2020 at 12:11):

Yes... I think it is. If you don't have anything else in the file.

view this post on Zulip Kevin Buzzard (Jul 13 2020 at 12:11):

Ha John Cremona just ran into the

[Errno 2] No such file or directory: '/home/john/.mathlib/886b15b5ea473ae51ed90de31b05f23de00be10d.tar.bz2'

problem with

leanproject get ImperialCollegeLondon/natural_number_game

The easiest fix: delete the natural_number_game directory and type

leanproject get ImperialCollegeLondon/natural_number_game

again!

view this post on Zulip Dima Pasechnik (Jul 13 2020 at 12:12):

not compiled mathlib? hmm...

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:13):

well, if it takes more than a few seconds to stop loading, that is

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:13):

try leanproject up

view this post on Zulip Dima Pasechnik (Jul 13 2020 at 12:14):

That's what I see

invalid import: data.option.defs
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)
...

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:14):

Lean ran out of memory. Use Ctrl-Shift-P > "Lean: Restart"

view this post on Zulip Dima Pasechnik (Jul 13 2020 at 12:15):

$ leanproject up
configuring _user_local_packages 1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
configuring _user_local_packages 1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
This project does not depend on mathlib

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:15):

here's a question: I'm trying the "lost level". At one point I have an hypothesis of the form h1: a0a \leq 0

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:16):

and I want to apply the lemma already proven that says le_zero (i.e. a0a=0 a \leq 0 \Rightarrow a = 0)

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:16):

but rw le_zero at h1 does not work

view this post on Zulip Jalex Stark (Jul 13 2020 at 12:16):

le_zero h1 is a term of type a=0

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:17):

have h2 : a = 0 := le_zero h1

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:17):

yeah I got around the issue but I was wonderin "why it does not work"

view this post on Zulip Rob Lewis (Jul 13 2020 at 12:17):

I'm going to move Dima's posts to the "install session" thread.

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:17):

does rw only apply to equalities and iff's?

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:17):

yes

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:17):

You can rw with le_zero h1 though to replace a with 0

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:19):

rw le_zero h1 does not work btw

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:19):

in what context?

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:20):

ok I think I needed le_zero a to apply the rw

view this post on Zulip Patrick Massot (Jul 13 2020 at 12:20):

Remember you can share your screen on Zoom so that some experienced user can see it

view this post on Zulip Patrick Massot (Jul 13 2020 at 12:21):

That's why we have breakout rooms

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:46):

what's the name of the tactic that simplifies expressions involving only associativity and commutativity of + and *?

view this post on Zulip Patrick Massot (Jul 13 2020 at 12:47):

ring

view this post on Zulip Patrick Massot (Jul 13 2020 at 12:47):

But using it in the game is cheating

view this post on Zulip Patrick Massot (Jul 13 2020 at 12:47):

At least in the early worlds

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:47):

thanks!

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:52):

I guess to prove a = a + (e + d + f) when I have an assumption h1: a = a + e + d + f can be resolved with ring?

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:53):

yes, or abel or simp [add_assoc]

view this post on Zulip Alex J. Best (Jul 13 2020 at 12:53):

You could try rw h1, ac_refl which is more low-level than ring.

view this post on Zulip Scott Morrison (Jul 13 2020 at 12:54):

Hmm... neither of Mario's suggestions will actually use your hypothesis h1.

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:54):

ring actually can't handle proofs using hypotheses, you would have to use transitivity, apply h1 first

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:54):

my other suggestions would work after that

view this post on Zulip Mario Carneiro (Jul 13 2020 at 12:55):

simpa [add_assoc] using h1 should also work

view this post on Zulip Amos Turchet (Jul 13 2020 at 12:55):

last one worked perfectly!

view this post on Zulip Rob Lewis (Jul 13 2020 at 12:56):

And to pile on, linarith will also solve this kind of thing, as long as you aren't subtracting natural numbers.

view this post on Zulip Peter Bruin (Jul 13 2020 at 14:09):

In level 5 of the multiplication world in the natural number game, my solution looks like

view this post on Zulip Peter Bruin (Jul 13 2020 at 14:12):

lemma mul_assoc (a b c : mynat) : (a * b) * c = a * (b * c) :=
begin
induction c with d hd,
rw mul_zero,
rw mul_zero,
rw mul_zero,
by refl,
repeat {rw mul_succ},
rwa [hd, mul_add],
end

In the second part of the induction the repeat tactic works, but if I try to replace the three rw mul_zero lines in the first part by repeat {rw mul_zero} I get invalid apply tactic, failed to unify a * b * succ d = a * (b * succ d) with [...]. Does this mean you can only use repeat when there is a single goal?

view this post on Zulip Peter Bruin (Jul 13 2020 at 14:17):

(In the meantime I found out that the three rw mul_zero lines can be removed completely, but that doesn't really answer my question...)

view this post on Zulip Alex J. Best (Jul 13 2020 at 14:17):

What's happened is that you no longer need the refl.

view this post on Zulip Alex J. Best (Jul 13 2020 at 14:17):

This is a slight quirk of the way the natural number game is set up

view this post on Zulip Peter Bruin (Jul 13 2020 at 14:17):

Great, thanks!

view this post on Zulip Alex J. Best (Jul 13 2020 at 14:18):

The rw inside the repeat is actually doing more than the rw outside, for pedagogical reasons rw in the game was made to do less so its clearer which step is doing what, but the repeat negates this

view this post on Zulip Peter Bruin (Jul 13 2020 at 14:18):

In other words, the remark that rwa will check if the goal can be proved by refl also applies to repeat?

view this post on Zulip Patrick Massot (Jul 13 2020 at 14:18):

To rw inside repeat

view this post on Zulip Peter Bruin (Jul 13 2020 at 14:19):

OK, thanks!

view this post on Zulip Andrew Sutherland (Jul 13 2020 at 17:51):

I have to say the NNG is totally addictive. Every time I take down one boss I can't wait to fight the next one! If video arcades were still a thing I could definitely see people lining up with quarters in hand to play this.

view this post on Zulip Johan Commelin (Jul 13 2020 at 17:57):

@Andrew Sutherland Wait till you get to the modular forms level!
@Kevin Buzzard Did you write it already?

view this post on Zulip Kevin Buzzard (Jul 13 2020 at 18:01):

ring doesn't work in NNG for a long time because we're rolling our own nat and half of the game is spent proving they're a commutative semiring; before this ring isn't going to work :-)

view this post on Zulip Amos Turchet (Jul 13 2020 at 18:30):

I'm curious whether the elliptic curve quest went much further after I had to leave the super interesting discussion

view this post on Zulip Johan Commelin (Jul 13 2020 at 18:32):

https://github.com/ImperialCollegeLondon/Example-Lean-Projects/tree/master/src/elliptic_curves

view this post on Zulip Kevin Buzzard (Jul 13 2020 at 18:41):

We are embarrassingly stuck right now. I'll get back to it later :-)


Last updated: May 06 2021 at 01:57 UTC