Mon afternoon: natural number game

Stream: Lean for the curious mathematician 2020

[Kevin Buzzard]

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!

[Johan Commelin]

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

[Dima Pasechnik]

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

[Dima Pasechnik]

in vscode, thatis

[Mario Carneiro]

you have a not compiled mathlib

[Johan Commelin]

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

[Kevin Buzzard]

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!

[Dima Pasechnik]

not compiled mathlib? hmm...

[Mario Carneiro]

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

[Mario Carneiro]

try leanproject up

[Dima Pasechnik]

That's what I see

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

[Mario Carneiro]

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

[Dima Pasechnik]

$ 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

[Amos Turchet]

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

[Amos Turchet]

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

[Amos Turchet]

but rw le_zero at h1 does not work

[Jalex Stark]

le_zero h1 is a term of type a=0

[Mario Carneiro]

have h2 : a = 0 := le_zero h1

[Amos Turchet]

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

[Rob Lewis]

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

[Amos Turchet]

does rw only apply to equalities and iff's?

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Amos Turchet]

rw le_zero h1 does not work btw

[Mario Carneiro]

in what context?

[Amos Turchet]

ok I think I needed le_zero a to apply the rw

[Patrick Massot]

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

[Patrick Massot]

That's why we have breakout rooms

[Amos Turchet]

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

[Patrick Massot]

ring

[Patrick Massot]

But using it in the game is cheating

[Patrick Massot]

At least in the early worlds

[Amos Turchet]

thanks!

[Amos Turchet]

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?

[Mario Carneiro]

yes, or abel or simp [add_assoc]

[Alex J. Best]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

my other suggestions would work after that

[Mario Carneiro]

simpa [add_assoc] using h1 should also work

[Amos Turchet]

last one worked perfectly!

[Rob Lewis]

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

[Peter Bruin]

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

[Peter Bruin]

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?

[Peter Bruin]

(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...)

[Alex J. Best]

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

[Alex J. Best]

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

[Peter Bruin]

Great, thanks!

[Alex J. Best]

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

[Peter Bruin]

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

[Patrick Massot]

To rw inside repeat

[Peter Bruin]

OK, thanks!

[Andrew Sutherland]

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.

[Johan Commelin]

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

[Kevin Buzzard]

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 :-)

[Amos Turchet]

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

[Johan Commelin]

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

[Kevin Buzzard]

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