Simple questions about the Natural Number Game

Stream: new members

[Victor Miller]

I've successfully completed the Natural Number Game using the web interface. Is there some simple way of saving my solutions? I realize that I can probably go through each one and copy and paste, but is there some less tedious way?

Also in level 2 of Addition World one is asked to prove

lemma add_assoc (a b c : mynat) : (a + b) + c = a + (b + c) :=

I did the following. Can someone explain why after I did repeat {rw add_zero} I didn't need to do refl? Under what circumstances does lean figure that out automatically?

induction c with d hd,
repeat {rw add_zero},
repeat {rw add_succ},
rw hd,
refl,

[Kevin Buzzard]

Modern Lean is beefed up from old natural number Lean. After extensive playing of the natural number game, people realised that they were often ending proofs with rw mul_assoc, refl or rw h, refl etc so they beefed up rw so that every time the user used it, it tried refl afterwards just to see if it worked.

[Victor Miller]

That's good. So how come it didn't work after I said rw hd ?

[Kevin Buzzard]

it didn't try hard enough. It only tries on some level of reducibility.

[Victor Miller]

Ok.

[Kevin Buzzard]

refl is a tactic whose job it is to solve an undecidable problem.

[Kevin Buzzard]

so you mustn't let it try too hard because it can get pretty lost sometimes.

[Kevin Buzzard]

After rw, it tries refl but only a bit.

[Kevin Buzzard]

I'm not making this up.

[Victor Miller]

I just changed the rw hd to repeat {rw hd} and the need for refl went away.

[Shing Tak Lam]

(Kevin has a point but I think he's talking about something else)

In NNG rw has been modified, so it doesn't try refl after the rw. That is why you need the refl at the end of your proof as it uses NNG rw. I think within repeat { ... }, it uses the standard Lean rw, so it does call refl after performing the rewrite.

[Bryan Gin-ge Chen]

It's possible to get your solutions (encoded in a JSON object) from your browser's local storage.

First, open the NNG site and then open your browser's dev tools. If you're using Firefox, then navigate to the "Storage" tab and open the "Local storage" dropdown on the left and click on "imperial.ac.uk". If you're using Chrome, navigate to the "Application" tab and do the same thing.

You should see an entry with key Natural number game-1-savedGameData. The corresponding value is a JSON-encoded string containing all of your solutions.

[Victor Miller]

Thanks. That worked. I was using Safari on my mac. I had do Develop->Show Page Resources, and then click on storage. Very similar to what you suggested.