## Stream: Lean for the curious mathematician 2020

### Topic: Mon afternoon: natural number game

#### Kevin Buzzard (Jul 13 2020 at 11:27):

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!

#### 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?

#### Dima Pasechnik (Jul 13 2020 at 12:11):

in vscode, thatis

#### Mario Carneiro (Jul 13 2020 at 12:11):

you have a not compiled mathlib

#### Johan Commelin (Jul 13 2020 at 12:11):

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

#### 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!

#### Dima Pasechnik (Jul 13 2020 at 12:12):

not compiled mathlib? hmm...

#### Mario Carneiro (Jul 13 2020 at 12:13):

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

#### Mario Carneiro (Jul 13 2020 at 12:13):

try leanproject up

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


#### Mario Carneiro (Jul 13 2020 at 12:14):

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

#### 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


#### 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: $a \leq 0$

#### Amos Turchet (Jul 13 2020 at 12:16):

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

#### Amos Turchet (Jul 13 2020 at 12:16):

but rw le_zero at h1 does not work

#### Jalex Stark (Jul 13 2020 at 12:16):

le_zero h1 is a term of type a=0

#### Mario Carneiro (Jul 13 2020 at 12:17):

have h2 : a = 0 := le_zero h1

#### Amos Turchet (Jul 13 2020 at 12:17):

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

#### Rob Lewis (Jul 13 2020 at 12:17):

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

#### Amos Turchet (Jul 13 2020 at 12:17):

does rw only apply to equalities and iff's?

yes

#### Mario Carneiro (Jul 13 2020 at 12:17):

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

#### Amos Turchet (Jul 13 2020 at 12:19):

rw le_zero h1 does not work btw

in what context?

#### Amos Turchet (Jul 13 2020 at 12:20):

ok I think I needed le_zero a to apply the rw

#### Patrick Massot (Jul 13 2020 at 12:20):

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

#### Patrick Massot (Jul 13 2020 at 12:21):

That's why we have breakout rooms

#### 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 *?

#### Patrick Massot (Jul 13 2020 at 12:47):

ring

#### Patrick Massot (Jul 13 2020 at 12:47):

But using it in the game is cheating

#### Patrick Massot (Jul 13 2020 at 12:47):

At least in the early worlds

thanks!

#### 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?

#### Mario Carneiro (Jul 13 2020 at 12:53):

yes, or abel or simp [add_assoc]

#### Alex J. Best (Jul 13 2020 at 12:53):

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

#### Scott Morrison (Jul 13 2020 at 12:54):

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

#### 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

#### Mario Carneiro (Jul 13 2020 at 12:54):

my other suggestions would work after that

#### Mario Carneiro (Jul 13 2020 at 12:55):

simpa [add_assoc] using h1 should also work

#### Amos Turchet (Jul 13 2020 at 12:55):

last one worked perfectly!

#### 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.

#### Peter Bruin (Jul 13 2020 at 14:09):

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

#### 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},
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 (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...)

#### Alex J. Best (Jul 13 2020 at 14:17):

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

#### Alex J. Best (Jul 13 2020 at 14:17):

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

Great, thanks!

#### 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

#### 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?

#### Patrick Massot (Jul 13 2020 at 14:18):

To rw inside repeat

OK, thanks!

#### 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.

#### 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?

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

#### 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

#### Johan Commelin (Jul 13 2020 at 18:32):

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

#### 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