Question on Natural Number Game Tutorial World

Stream: new members

[Kaixin Wang]

I'm stuck on the last part, which asks us to prove 2+2=4. I reduced it to showing 1+1+(1+1) = 1+1+1+1. How do I proceed?

[Kaixin Wang]

image.png what is wrong with line 3?

[Kevin Buzzard]

try space after 2 before [?

[Rémy Degenne]

nth is not a tactic (hence the error "unknown tactic"). You should write nth_rewrite instead of nth rewrite.

[Kevin Buzzard]

oh! no space between nth and rewrite -- it's a _

[Kaixin Wang]

image.png
What's wrong with line 4

[Kaixin Wang]

I want to convert 2+succ 1 = 3+1 -> succ (2+1) = 3+1

[Kaixin Wang]

thanks for your help. I appreciate it

[Richard Copley]

The error says unknown tactic, because add_succ isn't the name of a tactic, and the grammar is expecting a tactic name next.
Try exact add_succ 2 1?

[Kevin Buzzard]

I didn't teach exact yet so that probably won't work. You need to be rwing everything.

rw is a tactic, add_succ is a lemma, they're different types of thing.

[Kaixin Wang]

Thanks for your help! I got it!

[Kaixin Wang]

For this quest, am I supposed to use the induction tactic or not?
image.png

[Kaixin Wang]

image.png

[Kaixin Wang]

image.png

[Kevin Buzzard]

You're definitely supposed to be using induction there! What mode are you playing in?

[Kaixin Wang]

I used both typewriter and editor mode and got the same error.

[Kaixin Wang]

image.png
I'm not sure, there is still an induction error, but I seem to be on the right track. I'm not sure if I can do something like hd to immediately finish.

[Kaixin Wang]

image.png

[Kaixin Wang]

Now it looks like this
all goals seem to be solved

[Kevin Buzzard]

Sorry about all this! It should be fixed now. Can you confirm?

[Kaixin Wang]

Yes this is fixed. Thank you very much!

[Kaixin Wang]

I have a question about using nth_rewrite.
image.png

[Kaixin Wang]

By doing rw[succ_eq_add_one] twice I get this
image.png

[Kaixin Wang]

But when I initially do nth_rewrite 2[succ_eq_add_one] I get an error

[Kaixin Wang]

I'm fairly confident this is not a typo, since nth_rewrite 1[succ_eq_add_one] does not give me an error.

[Kevin Buzzard]

This seems to be an old Lean or mathlib bug, present in v4.4 (the version the game is using) and gone in v4.6 (the version modern mathlib is using). @Jon Eugster am I right in thinking that I can't just follow the instructions here to bump mathlib in NNG4, because I need to make sure that the version of Lean is compatible with the game maker?

[Kaixin Wang]

Is there a way to use add_comm to swap b and c here
image.png
?

[Kevin Buzzard]

Sure -- add_comm takes inputs. add_comm b c is a proof of b + c = c + b. add_comm is a proof of ? + ? = ? + ?. rw will match the first thing it sees, so rw [add_comm] will just rewrite the first addition it runs into, but rw [add_comm b c] will only ever change b + c to c + b.

[Kevin Buzzard]

Click on rw in the list of tactics to find extensive documentation and examples for how to use rw.

[Kaixin Wang]

Thank you!

[Jon Eugster]

Kevin Buzzard said:

This seems to be an old Lean or mathlib bug, present in v4.4 (the version the game is using) and gone in v4.6 (the version modern mathlib is using). Jon Eugster am I right in thinking that I can't just follow the instructions here to bump mathlib in NNG4, because I need to make sure that the version of Lean is compatible with the game maker?

The nng is using v4.5.0, isnt it? or did you really mean v4.4?

But no, that would be tricky to do because if you use a newer mathlib you would need to make sure std is on the version mathlib uses and not the version the GameServer uses, while hoping that the GameServer still compiles with the wrong std version. lake isn't designed to deal with package versioning in a robust way, so its up to the developer to fiddle around make sure all dependencies are compatible. That's why I decided to just stick to the v4.X.0 tags (which are comparible across all repos) and just live with the bugs until mathlib releases a new such tag... But that should be any day now :)

[Kevin Buzzard]

Oh, I just hadn't git pulled for a while. Yes, it seems that we're on v4.5.0 (I was on v4.4.0). I'm not pushing you to update, I was just wondering how this actually worked. So basically I do nothing until someone updates GameServer, and then we can bump NNG and I fix any issues which happen at that point?

[Jon Eugster]

Yes the workflow at the moment is:

• wait until GameServer has the new version tag
• change your lean-toolchain to that new version
• call lake update -R and lake build
• potentially fix any errors

[Kaixin Wang]

So is this why currently there is a 502 bad gateway error?

[Kevin Buzzard]

No, updating main is independent of deploying main.

[Kevin Buzzard]

@Jon Eugster any idea?

[Jon Eugster]

no, absolutely none. but I'll try to fix that tomorrow morning.