Natural Number Game

Stream: new members

[Olonbayar Temuulen]

image.png
What is the best way to solve this, without relying on simp?

[Kevin Buzzard]

Is an acceptable reply "you shouldn't be in this state in the first place"? Are you trying to prove $(x+y)^2=x^2+2xy+y^2$ by induction instead of just multiplying it out?

[Kevin Buzzard]

The Pow.pow is a bit miserable in the hypotheses, how did that end up there? The user is supposed to never see that.

[Jon Eugster]

Kevin Buzzard said:

The Pow.pow is a bit miserable in the hypotheses, how did that end up there? The user is supposed to never see that.

That's been a "fix" in the new mathlib version turning a ^ b into Pow.pow a b. I pushed a fix for this a couple days ago, but haven't updated the live version yet. I'll do that now.

[Olonbayar Temuulen]

Via "being a bit overly adventurous with induction and trying to pin down exactly how add_assoc , add_mul, mul_assoc, mul_comm and to slightly lesser extent add_mul" worked, since the documentation felt a big vague. The notes on the left mention the user to check the targeting function comments of "rw", but i felt that the explanation there was lacking too.

[Etienne dg]

I'm in 5/6 of advanced addition in NNG. I applied the cases and solved the first Goal. Now, I would like to use the succ_ne_zero theorem, but I get the error You have not unlocked the lemma/definition 'MyNat.succ_ne_zero' yet!. The same error message is displayed for every peano theorem, despite these not being grayed out. Is it a bug or is it expected?

[Ruben Van de Velde]

That sounds unexpected

[Kevin Buzzard]

Screenshot-from-2024-02-23-20-54-36.png

This works for me on none rules. Do you know which rules you're using? (go to the home screen and check?)

[Etienne dg]

Yes, it works for me with none, by why not on regular?

[Kevin Buzzard]

Bug?

[Kevin Buzzard]

Wait -- have you definitely unlocked succ_ne_zero? I've just played through on regular mode and by the time I'm at advanced addition world 5/6 I have only unlocked zero_ne_succ. You can use symm to switch the sides of an equality/inequality.

[Kevin Buzzard]

Hmm, OK, I went and proved succ_ne_zero and indeed it doesn't solve the problem on "regular" rules:

bug.png

[Kevin Buzzard]

@Jon Eugster can you explain (again) how I am supposed to set up imports so that this works with regular rules? My game state is this

cafe.png

and Algorithm 6 (which I've just done) does unlock succ_ne_zero in Advanced Addition 5, but I don't seem to be able to use the lemma in the level.

[Jon Eugster]

It should be enough that the algorithm level imports import Game.Level.AdvAddition. You can check with #check succ_ne_zero in that level's lean file if you have the imports correctly.

I can look through the nng repo (and fix if necessary) next time on my computer, but that could be Tuesday, dep. on how fast I'm done marking 300 exams🤦🏻‍♂️

Should probably rethink if one could use the final Env. which has everythibg imported instead of the level's env:thinking: otherwise we'll always get "unlocked but not imported" problems. But that poses other problems...

[Jon Eugster]

Etienne dg said:

I'm in 5/6 of advanced addition in NNG. I applied the cases and solved the first Goal. Now, I would like to use the succ_ne_zero theorem, but I get the error You have not unlocked the lemma/definition 'MyNat.succ_ne_zero' yet!. The same error message is displayed for every peano theorem, despite these not being grayed out. Is it a bug or is it expected?

reading this, that sounds like a bug indeed. let me look at that more closely on Tuesday!

[Kevin Buzzard]

#check succ_ne_zero works fine in the source code (at least on main -- I don't know if main is the version which is currently deployed)

[Jon Eugster]

Etienne dg said:

I'm in 5/6 of advanced addition in NNG. I applied the cases and solved the first Goal. Now, I would like to use the succ_ne_zero theorem, but I get the error You have not unlocked the lemma/definition 'MyNat.succ_ne_zero' yet!. The same error message is displayed for every peano theorem, despite these not being grayed out. Is it a bug or is it expected?

Indeed, that's a bug and there is a fix in the pipeline : 780514. I think v4.6.0 should be coming up in a few days, so I'll be included in that bump.

[Etienne dg]

Kevin Buzzard said:

Wait -- have you definitely unlocked succ_ne_zero? I've just played through on regular mode and by the time I'm at advanced addition world 5/6 I have only unlocked zero_ne_succ. You can use symm to switch the sides of an equality/inequality.

When I try to symm an inequality, it doesn't work, I get :
symmetry lemmas only apply to binary relations

Indeed, the succ_ne_zero is unlocked in Algorithm world, which is not the main branch. Is Advanced Addition doable without Algorithm ? Otherwise, I think it should depend on Algorithm World

[Kevin Buzzard]

Yes it's definitely doable -- it was doable before algorithm world even existed! I'm surprised symm doesn't work on inequalities! You can intro to turn it into an equality and then symm at hyp for a workaround if it's really true that it doesn't work on inequalities.

[Etienne dg]

Ok, it was just me not using symm correctly

[Emily Riehl]

I'm giving a talk tomorrow evening and was planning to introduce a group of students to the new natural numbers game in lean4. I had thought I'd use the "regular" mode with most tactics locked away but ran into trouble when I got to the start of addition word because I don't see the "induction" tactic listed anywhere on the upper right hand side. Indeed, when I try to use induction to prove that 0 + n = n I get the error message:

The tactic 'induction' is not available in this game!

When I switch from the regular mode to the mode with no rules, I can use induction, but I still don't see it listed on the upper right. Have I missed something or is there a bug?

[Kevin Buzzard]

This is most definitely a bug and you're the second person to report it in the last 24 hours.

[Kevin Buzzard]

Will try and fix within the next hour or two

[Kevin Buzzard]

If I build mainlocally I get the following warnings

[1921/1922] Building Game
stdout:
./././Game.lean:113:0: warning: No world introducing induction, but required by LessOrEqual
./././Game.lean:113:0: warning: No world introducing induction, but required by AdvMultiplication
./././Game.lean:113:0: warning: No world introducing generalizing, but required by AdvMultiplication
./././Game.lean:113:0: warning: No world introducing induction, but required by Multiplication
./././Game.lean:113:0: warning: No world introducing induction, but required by AdvAddition
./././Game.lean:113:0: warning: No world introducing induction, but required by Addition
./././Game.lean:113:0: warning: No world introducing induction, but required by Power

which might well be somehing to do with it.

[Kevin Buzzard]

I've got it

[Kevin Buzzard]

Fingers crossed it will be fixed in an hour or so. Thanks for reporting!

[Kevin Buzzard]

Should be fixed now :fingers_crossed: .

[Etienne dg]

In the set theory game, Level 6 / 6 : Union is associative, the following input validates the goal, but also prints an error, what happens?

Objects:
U: Type
ABC: Set U
x: U
Assumptions:
h_1: x ∈ B
Goal:
x ∈ A ∪ (B ∪ C)

Input :
 exact Or.inr.inl h_1

Result:
intermediate goal solved 🎉

Error:
invalid field notation, type is not of the form (C ...) where C is a constant
  Or.inr
has type
  ?m.198 → ?m.197 ∨ ?m.198

[Kevin Buzzard]

I think that if Lean ever generates an error then you can't trust anything else that it says (after an error it typically solves what it's thinking about with sorry so you might get spurious claims about goals being solved, when they are not).

[Kevin Buzzard]

The error is a very obscure way of saying "Or.inr makes sense, and Or.inl makes sense, but Or.inr.inl makes no sense", by the way.

[Jon Eugster]

I'll adjust the logic for this "intermediate goal solved" message! I have a hunch that currently it only checks "no. new goals < no. previous goals" and forgets to look at the errors.

And as Kevin said, after a fatal error there are zero goals left.

[Emily Riehl]

Kevin Buzzard said:

This is most definitely a bug and you're the second person to report it in the last 24 hours.

Thanks @Kevin Buzzard.

I wonder whether some of the games (like natural numbers game, or perhaps a different one), could have a "reading comprehension" mode, where we can see more of the source code. Like at the start of the addition world, I would have liked to see the definition of the natural numbers type and of addition. These definitions are described in the text on the left but for those who want to jump from the games to writing their own Lean code it might be help to be able to pair these descriptions with the actual implementation, at least in code snippets. Though perhaps the code is so complicated that this isn't such a good idea...

[Kevin Buzzard]

For what it's worth, the source code is on github so you can see the definition of the naturals here and it is what you think. However just after that is a load of gobble-de-gook (setting up a bijection between the game's MyNat and Lean's real Nats, enabling us to be able to use numerals for MyNat. In general the code in the repository is a mix of straightforward stuff (for example the multiplication file is relatively self-explanatory) and hacks which we'd never want the user to see (e.g. modifying the rw tactic so that it doesn't close goals if they become x = x after the rewrite, because tests showed that users found this confusing).

There are a few times when I do belch out some code for the user to see, but it's not clear to me that this is helpful; I might have made a poor choice in what to belch out though. I think the genesis of NNG was the idea that proving basic theorems was fun and everything else was complicated so let's hide all the other stuff completely. I can quite believe that other games could take a different approach!

[Dan Velleman]

@Etienne dg : The problem is that you can't say Or.inr.inl. I think what you mean is: exact Or.inr (Or.inl h_1). The point is that Or.inl h_1 is a proof of x ∈ B ∪ C, and therefore Or.inr (Or.inl h_1) is a proof of the goal.

[Mark Fischer]

@Emily Riehl A bit of an side, but your comment made me think about it. I assume there's an interesting historical perspective on the definition of numbers. Really multiple such perspectives. You can imagine, for example, that Church invented lambda calculus and, knowing the properties of ℕ ahead of time, sought a definition for the Naturals in his new system. We tend to think definitions come first, but sometimes the motivation is the other way around.

I imagine you might be able to make a game of that sort of a thing. "Define an object then prove it has the following properties." In NNG4, the algorithms world would likely benefit (Def an algorithm/tactic that closes these 4 theorems or some-such). Certainly a great Intro to Formal Software Verification game would do well with such a premise.

I imagine that in the coming years, lean4game develop support for a lot more interaction with Lean's other core ideas in a hopefully targeted game-friend way. We'll see, I suppose!

[Yagub Aliyev]

Anyone know why https://adam.math.hhu.de/ is down? I didn't know there were two versions of NNG one in the above link and one in https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game

They are very different, aren't they?

[Jon Eugster]

I'm trying to fix the server asap, no idea what happened.

The linked nng is the old Lean3-version which hasn't been maintained in a while, as far as I know.

[Jon Eugster]

and it's all online again. Sorry for that.

[Yagub Aliyev]

Spanish game is gone forever?

[Jon Eugster]

Gone until the author updates it. But I just implemented the key element for translation of games, so you can expect to have the STG incorporate it's Spanish translation in the nearer future :blush:

[Daniel Massart]

I get "Oops, sorry, an unexpected error occurred / Cannot read properties of undefined (reading 'steps')" messages, is that what Yagub means by the server being down ? if not, what does it mean ?

[Kevin Buzzard]

The server being down was a temporary problem where nothing worked at all for a few hours. This has now been fixed.

[Daniel Massart]

Kevin Buzzard said:

The server being down was a temporary problem where nothing worked at all for a few hours. This has now been fixed.

then it has to be something else because I keep getting those messages before I even do "execute". It used (meaning, yesterday) to only occur at stage 8 of the multiplication world but now it is also occurring at stage 2 of the advanced addition world and stage 5 of the algorithm world, completely blocking me. Does anyone have an idea what's happening ? thanks in advance !

[Kevin Buzzard]

I'm a bit confused about what we're talking about. I'm at a conference today but I just went to https://adam.math.hhu.de/#/g/leanprover-community/NNG4/world/Algorithm/level/5 and it's working fine for me. Are we talking about some Spanish translation or about the main game? If the main game, can you give me some more clues, e.g. a screenshot of the error, an explanation of which "rule mode" you're playing the game with (regular/relaxed/none) etc?

[Daniel Massart]

I'm talking about the main game, regular rules.
here is a screenshot :
Capture-décran-du-2024-03-02-06-35-59.png
thanks a lot for your time, it's nothing life-threatening !

[Kevin Buzzard]

Annoyingly, I cannot reproduce yet. I might have to play through everything again (I'm quite good at this now...)

[Daniel Massart]

Kevin Buzzard said:

Annoyingly, I cannot reproduce yet. I might have to play through everything again (I'm quite good at this now...)

It's extremely embarassing to be putting you through this. It also occurs at level 8 of advanced multiplication, if that may save you some time

[Kevin Buzzard]

I can't reproduce :-( I just cleared my save state, started at the beginning of the game, and played through up to advanced addition level 2 and it worked fine for me.

stuck.png

I don't know enough about the game engine to suggest a diagnosis of your error (I just wrote the Lean code for the levels, I know nothing about the infrastructure of the game). If you can face it, can you download and delete your save state and see if this fixes the problem? Or maybe upload your save state and compare with mine? Mine is here.

[Kevin Buzzard]

Occasionally I edit or move levels which have already been deployed, and I can imagine that this really messes up people who have got saved game states from before I do this but I have no idea whether this cavalier attitude on my part can cause the error you're seeing.

[Daniel Massart]

I sent you my saved state (all 572 lines of it as a comment to your gist, can you see it ? I''m not sure I'm ready to delete all my progress at this stage

[Kevin Buzzard]

Oh nice -- I can indeed reproduce now. I get

Oops!

Sorry, an unexpected error has occurred.

v is undefined

for advanced addition level 2.

[Kevin Buzzard]

I really don't know what I'm doing here, but looking at your upload I see

    "AdvAddition": {
      "1": {
        "code": "induction n with n hn\nrepeat rw[add_zero]\nintro h\napply h\nrepeat rw[add_succ]\nintro\napply succ_inj at a_1\napply hn at a_1\nexact a_1\n",
        "completed": true,
        "selections": [
          {
            "selectionStartLineNumber": 10,
            "selectionStartColumn": 1,
            "positionLineNumber": 10,
            "positionColumn": 1
          }
        ],
        "help": [
          0
        ]
      },
      "2": {
        "code": "repeat rw[add_comm]\n",
        "completed": false,
        "selections": [
          {
            "selectionStartLineNumber": 2,
            "selectionStartColumn": 1,
            "positionLineNumber": 2,
            "positionColumn": 1
          }
        ],
        "help": []
      }
    },

which looks to me like you tried repeat rw[add_comm] on advanced addition world level 2; I guess this is not a particularly wise idea (it sends Lean into an infinite loop) but I would not expect this to take down the server.

OK so if I edit your saved state, carefully deleting the comma on the line just before the "2", and all the stuff following the "2" up until but not including the }, which I quoted, then I can play advanced addition world level 2 using your save state. This is a bit of a hack but it's worked for me. Does it work for you?

The gist which is working for me is here.

[Daniel Massart]

I did enter the infinite loop but then I did "retry" and only then did things go sideways

[Kevin Buzzard]

Interesting! I'll see if I can reproduce. Obviously we don't want users to be able to break things even if they write code which loops.

[Daniel Massart]

I had the feeling that Lean recognized the infinite loop and aborted it on its own initiative, allowing me to retry

[Daniel Massart]

It did work, but only for the advanced addition world ! so I guess what I have to do now is to do as you did for the multiplication and algorithm worlds. What exactly is the magic you performed ?

[Kevin Buzzard]

I am suggesting you (a) download your save file (b) save a copy! (c) edit it manually with a text editor (remove the bad proofs) (d) upload.

@Jon Eugster I can reproduce this now.
1) Start a new game with rules none (or any other choice for rules, and play through up to solving add_comm, addition world level 3)
2) Go to addition world level 4, and for your first move try repeat rw [add_comm]
3) You now broke the game: you can never solve addition world level 4, you get the error

Oops!

Sorry, an unexpected error has occurred.

v is undefined

You can fix it by downloading the save state and manually removing the bad proof.

[Kevin Buzzard]

On the other hand, I've played this game loads recently and the major problem I was constantly having a couple of months ago (the game not updating after you entered a tactic) has never occurred, so this is a major win.

[Daniel Massart]

for instance in
"8": {
"code": "repeat rw[mul_comm]\n",
"completed": false,
"selections": [
{
"selectionStartLineNumber": 2,
"selectionStartColumn": 1,
"positionLineNumber": 2,
"positionColumn": 1
}
],
"help": []
}
what should I delete exactly ? should I just delete it all ? I'm afraid there might be some hidden nuclear key somewhere.

[Kevin Buzzard]

Well you've not quoted the code in #backticks so zulip has mangled all the spacing, but if you could see the spacing then you can see that this is somehow a dictionary of size 8, and you want to change it into a dictionary of size 7, so you need to delete ,"8" : {stuff}

[Kevin Buzzard]

I should say that I don' t know the first thing about these files, but looking carefully at the spacing enabled me to figure things out. The structure of the file seems to be this:

{
  "inventory": [ <stuff>
  ],
  "openedIntro": true,
  "data": {
    "Tutorial": {
      "1": { <stuff>
      },
      "2": { <stuff>
      },
      ...
      },
      "8": { <stuff>
      }
    },
    "Addition": {
      "1": { <stuff>
      },
      "2": {
      (etc)

and it seems that you can just edit the file in the obvious way. Keep a backup in case you mess up! You won't lose your progress that way.

[Daniel Massart]

Kevin Buzzard said:

Well you've not quoted the code in #backticks so zulip has mangled all the spacing, but if you could see the spacing then you can see that this is somehow a dictionary of size 8, and you want to change it into a dictionary of size 7, so you need to delete ,"8" : {stuff}

ok thanks, I was a bit confused in your previous message by "comma before the 2, then all the stuff up to (but not including) }", ","8" : {stuff}" makes more sense to me.

By the way, huge thanks to the author(s) of the game, it's a lot of fun !

[Kevin Buzzard]

The comma thing is that you want to change "7":{stuff},"8":{stuff}} to "7":{stuff}}, i.e. you need to remove the comma just before the 8 as well as all the 8 data.

[Dan Velleman]

@Jon Eugster It might be nice if the game offered more options for deleting information. Right now your only option is to delete everything. Perhaps there could be a dialog box in which you select what levels or worlds you want to delete information from (with delete all as one option)?

[Jon Eugster]

That should certainly not happen:grimacing:

Unfortunately I might not be able to fix anything during the next week if it's not preventing people completely from playing, as Im in the mountains with very poor internet.

@Daniel Massart do I understand correctly that you are now able to continue now? Could you (and @Kevin Buzzard) send me a DM with the downloaded game state wihich was broken? I'll try investigate as soon as Im back.

[Jon Eugster]

Dan Velleman said:

Jon Eugster It might be nice if the game offered more options for deleting information. Right now your only option is to delete everything. Perhaps there could be a dialog box in which you select what levels or worlds you want to delete information from (with delete all as one option)?

Feature requests like this are best put as an issue at the lean4game githib repo:+1: Sometimes it takes a while, but I do try to address all issues that are submitted there.

[Dan Velleman]

OK, I submitted an issue.

[Kevin Buzzard]

Jon Eugster said:

That should certainly not happen:grimacing:

Unfortunately I might not be able to fix anything during the next week if it's not preventing people completely from playing, as Im in the mountains with very poor internet.

Daniel Massart do I understand correctly that you are now able to continue now? Could you (and Kevin Buzzard) send me a DM with the downloaded game state wihich was broken? I'll try investigate as soon as Im back.

Yes Jon I think at least we know how to get around the problem. I posted a repro above so it could happen to others. In NNG3 if anyone tried repeat rw [add_comm] then it hung NNG3 but you could just delete the line to recover. Here the issue is that repeat rw [add_comm] really is deadly because you can't ever get back to the input box to remove it.

[Kevin Buzzard]

@Daniel Massart let me know if you need more help getting back on track; I'm confident that I can edit your savefile to reset any given level, as long as you tell me which levels you want reset.

[Daniel Massart]

Kevin Buzzard said:

Daniel Massart let me know if you need more help getting back on track; I'm confident that I can edit your savefile to reset any given level, as long as you tell me which levels you want reset.

so far it works perfectly fine, exactly as you said, by deleting the content of an exercise, plus the comma right before it

[Daniel Massart]

I thought this one might be interesting as well :
Capture-décran-du-2024-03-03-13-54-07.png

[Kevin Buzzard]

That looks like expected behaviour to me. What interests you about it?

[Daniel Massart]

Kevin Buzzard said:

That looks like expected behaviour to me. What interests you about it?

I found funny that it (rightly) claimed not to know what succ_zero_eq_one means, and at the same time it considered it solved the intermediate goal, as if it knew that I actually meant one_eq_succ_zero. In any case it seemed to mess with its brain and I had to delete the level as you showed me yesterday

[Kevin Buzzard]

After an error Lean goes totally haywire and you can't believe anything it says other than the error.

[Jon Eugster]

Daniel Massart said:

I thought this one might be interesting as well :
Capture-décran-du-2024-03-03-13-54-07.png

Thanks for noticing. After the next update the message "intermediate goal solved" will not be displayed anymore if there are zero goals present due to errors

[T D]

The game seems to break if I try to use the repeat tactic
eg; "repeat rw [xyz]"
Anyone know anything about this?

[Ruben Van de Velde]

I've seen some discussion about a bug that happens when you cause an infinite loop

[Jon Eugster]

T D said:

The game seems to break if I try to use the repeat tactic
eg; "repeat rw [xyz]"
Anyone know anything about this?

literally in this same topic about 5 messages up ;)

I'll hope to fix this today, sorry for the troubles🤞🏼

[Isak Colboubrani]

T D said:

The game seems to break if I try to use the repeat tactic
eg; "repeat rw [xyz]"
Anyone know anything about this?

See this thread for some additional context.

[Jon Eugster]

Isak Colboubrani said:

T D said:

The game seems to break if I try to use the repeat tactic
eg; "repeat rw [xyz]"
Anyone know anything about this?

See this thread for some additional context.

Does it still crash for you?

The current fix unfortunately requires you to go into "Editor mode" (top right) and delete the last line manually, but that should be usable for the time being. Or at least I hoped it would.

[Daniel Massart]

something I don't get about the tactic "cases' " in the set theory game : at some point I have a hypothesis

ht: (t = A ∨ t = B) ∧ x ∈ t

and if I do cases' ht with htA htB, it answers

htA: t = A ∨ t = B
htB: x ∈ t

when it should reply with
htA : t =A \and x \in t
htAB: t =B \and x \in t

am I missing something ?

[Dan Velleman]

If ht were (t = A ∧ x ∈ t) ∨ (t = B ∧ x ∈ t), then you would get the behavior you seem to be expecting. But that's not what ht is. Of course, ht is equivalent to that statement, but you'd have to prove that equivalence to make use of it.

I think a better approach would be to say have htleft : t = A ∨ t = B := ht.left. Now you can do cases' htleft with htA htB. Or you could just say cases' ht.left with htA htB.

[Dan Velleman]

The point is, the behavior of cases' h with hA hB that is described in the set theory game is only for situations in which h is an "or" statement. It's not enough for it to be logically equivalent to an "or" statement, it has to literally be an "or" statement. (You can experiment with cases' in situations in which h is not an "or" statement and see what it does, as you accidentally did in your situation, but that's not how the tactic is used in the set theory game.)

[Matt Diamond]

Yeah, it's important to understand that cases' doesn't have any special knowledge of boolean logic. What it knows is that And is a type with two parameters, so it simply destructures ht into those two parameters.

[Daniel Massart]

Matt Diamond said:

Yeah, it's important to understand that cases' doesn't have any special knowledge of boolean logic. What it knows is that And is a type with two parameters, so it simply destructures ht into those two parameters.

thanks to both of you for your answers ! still, wouldn't it be better if it answered with an error message like "sorry, I expect a litteral "or" statement here", rather than proposing something absurd like a desperate student ?

[Matt Diamond]

I don't understand what's absurd about the behavior of cases' here... if I have a statement P ∧ Q, then it can be helpful to destructure that into two separate propositions

[Matt Diamond]

cases' has many applications beyond just dealing with Or

[Daniel Massart]

Matt Diamond said:

cases' has many applications beyond just dealing with Or

ok, this is the information I missed, in the game the definition just says "if you have a p \or q hypothesis..."
thanks for your time !

[Matt Diamond]

Ah, I can see why that might lead you to believe it was a specialized function. Happy to help!

[Dan Velleman]

Perhaps I should addI have added a comment in the game saying that the cases' tactic has other uses, but in the game we only use it for breaking a proof into cases based on an "or" assumption.

The game is only intended to teach a limited amount about Lean--it's not trying to cover all uses of all tactics.

[Meek Msaki]

Hi ya'll. I'm not a mathematician but want to learn formal verification. Currently stuck on Addition Level 2/5: succ_add

How do think about reducing this problem?

Screenshot-2024-04-05-at-12.27.53-AM.png

[Mario Carneiro]

try using add_succ

[Meek Msaki]

on the right side of left side or both?

[Meek Msaki]

Mario Carneiro said:

try using add_succ

on the right side, left side or both?

[Mario Carneiro]

both

[Meek Msaki]

succ (succ a + d) = succ (succ (a + d))
How to reduce this running out of ideas, not sure in what way I should apply the induction tactic.

Should I apply induction on both a and d and solve their specific branches? Will induction reduce this problem further?

[Meek Msaki]

Seems like i am getting into some kind of infinite loop when i do that Screenshot-2024-04-05-at-1.07.35-AM.png @Mario Carneiro

[Mario Carneiro]

Meek Msaki said:

succ (succ a + d) = succ (succ (a + d))
How to reduce this running out of ideas,

This is very close to the hypothesis hd you have... maybe you should try rewriting with it

[Mario Carneiro]

Should I apply induction on both a and d and solve their specific branches? Will induction reduce this problem further?

No, another induction will make a big mess and probably not help

[Meek Msaki]

Mario Carneiro said:

Meek Msaki said:

succ (succ a + d) = succ (succ (a + d))
How to reduce this running out of ideas,

This is very close to the hypothesis hd you have... maybe you should try rewriting with it

thanks that worked

[Meek Msaki]

How do I rewrite h? I am assuming it's rw [zero_add h] but that doesn't seen to work

Screenshot-2024-04-05-at-2.03.53-AM.png

[Yaël Dillies]

No, you want to use rw [lemma] at hypothesis

[Meek Msaki]

Yaël Dillies said:

No, you want to use rw [lemma] at hypothesis

worked thanks!

[Meek Msaki]

I'm stuck on this one not sure how to approach this problem any ideas that could be of help?

Screenshot-2024-04-05-at-2.55.07-AM.png

[Kevin Buzzard]

Don't do what you did, go back to the beginning and induct on n instead

[Kevin Buzzard]

By the way, multiplication world then power world is the recommended route for beginners, before going down this path.

[Meek Msaki]

Kevin Buzzard said:

By the way, multiplication world then power world is the recommended route for beginners, before going down this path.

Got it! But your tip helped, was able to complete level!

[Kevin Buzzard]

If you want to forge ahead then go ahead and feel free to ask more questions!

[Meek Msaki]

Not sure what direction I should take this, have been stuck for a while and need some suggestions

Screenshot-2024-04-05-at-4.02.07-AM.png

[Kevin Buzzard]

My guess is induction on the variable on the right ie b. That usually makes progress for these early levels. The point of the variable on the right is that multiplication is defined by recursion on the variable on the right so basic proofs should use induction on the variable on the right. By the time you've proved $a\times b=b\times a$ this distinction is irrelevant but it looks like you're not there yet.

[Meek Msaki]

I got to

Assumptions: hd: succ a * d = a * d + d

Goal: succ (succ a * d + a) = succ (a * d + a + d)

I don't have access to succ_mul yet
I was thinking about doing a add_comm on a and d on the right side but that's about it currently

[Meek Msaki]

This is after add_right_comm, I see hd has a*d + d on the right hand side which can be useful but forgot what tactic to use

Screenshot-2024-04-05-at-4.22.05-AM.png

So close to solving it:
Assumptions: hd: succ a * d = a * d + d

Goal: succ (a + (a * d + d)) = succ (a + succ a * d)

[Richard Copley]

Now look at the assumption.

[Richard Copley]

Assumptions: hd: succ a * d = a * d + d
Goal: succ (a + (a * d + d)) = succ (a + succ a * d)

[Meek Msaki]

Richard Copley said:

Assumptions: hd: succ a * d = a * d + d
Goal: succ (a + (a * d + d)) = succ (a + succ a * d)

solved!

[Meek Msaki]

Stuck here, i've been writing on pen and paper but the invisible brackets are really hard to work with when applying my mul_comm tactics, any tips?

Screenshot-2024-04-05-at-3.48.37-PM.png

Assumptions:hd: b ^ d * a ^ d = (a * b) ^ d
Goal: b * (b ^ d * (a ^ d * a)) = b * (b ^ d * a ^ d * a)

[Richard Copley]

It's hard to guess how you got into exactly that state (not that there's anything wrong with it). For concreteness, if you had started like this instead :

-- expand stuff out
rw [pow_succ, pow_succ, pow_succ, hd]
-- remove all brackets
rw [← mul_assoc, ← mul_assoc]

so that your context is

Assumptions:
hd: (a * b) ^ d = a ^ d * b ^ d
Goal:
a ^ d * b ^ d * a * b = a ^ d * a * b ^ d * b

then the next thing to do is to use mul_assoc carefully* to put brackets around "b ^ d * a" so that you can use mul_comm.

(*Here "carefully" means that you'll need to supply arguments for one or more of mul_assoc's parameters -- and why not all three of them?!)

[Notification Bot]

A message was moved here from #new members > graph theory project by Richard Copley.

[Meek Msaki]

Richard Copley said:

It's hard to guess how you got into exactly that state (not that there's anything wrong with it). For concreteness, if you had started like this instead :

-- expand stuff out
rw [pow_succ, pow_succ, pow_succ, hd]
-- remove all brackets
rw [← mul_assoc, ← mul_assoc]

so that your context is

Assumptions:
hd: (a * b) ^ d = a ^ d * b ^ d
Goal:
a ^ d * b ^ d * a * b = a ^ d * a * b ^ d * b

then the next thing to do is to use mul_assoc carefully* to put brackets around "b ^ d * a" so that you can use mul_comm.

(*Here "carefully" means that you'll need to supply arguments for one or more of mul_assoc's parameters -- and why not all three of them?!)

was helpful thanks, completed level!

[Meek Msaki]

Any tips on this. I want to at least get at zero_ne_one. Any ideas on how to get it to 0 on left and 1 on right? It seems that I am not able to use zero_ne_succ yet

Screenshot-2024-04-06-at-11.46.58-AM.png

Goal : 1≠1+1

I can get it to succ 0 ≠ succ (succ 0)

But not sure how to proceed

[Kevin Buzzard]

you can intro h, because the definition of $A\not=B$ is $(A=B)\implies False$. Then apply succ_inj at h.

[Meek Msaki]

Kevin Buzzard said:

you can intro h, because the definition of $A\not=B$ is $(A=B)\implies False$. Then apply succ_inj at h.

Screenshot-2024-04-06-at-3.21.10-PM.png

How come I don't get an implication as you are suggesting? and weird how it's saying succ_inj is an unknown tactic

[Kevin Buzzard]

Indeed it's not a tactic. But apply is. And you did get an implication, that's why intro worked.

[Meek Msaki]

I'm on Level 5 / 6 : add_right_eq_zero

The question introduces that we will be solving Goal:

a + b = 0 → a = 0

Does not include the case for b though

I seem to getting stuck finding a solution, any help would do. This is how far I have gotten

Screenshot-2024-04-06-at-9.48.17-PM.png

[Mitchell Lee]

Try to get a contradiction by rewriting the a + succ d that appears in the hypothesis h as succ (a + d)

[Kevin Buzzard]

This looks doable -- h is provably false so you can get a contradiction from it, proving the goal. Manipulate h until it's of the form succ x = 0 and then apply succ_ne_zero to it. (oh sorry, for some reason I didn't see Mitchell's comment until after I'd posted mine)

[Meek Msaki]

add_left_cancel is not working as I expect. I though goal 2 will become b = x but it is not doing that.

Can someone confirm that I am using the tactic the right way, maybe I am doing it wrong.

Screenshot-2024-04-11-at-12.23.19-AM.png

[Ruben Van de Velde]

That's because add_left_cancel goes the other way: if you already know that a+b=a+c, it proves b=c. But you need to prove that a+b=a+c.

[Ruben Van de Velde]

You took a wrong turn before this, though.

[Ruben Van de Velde]

Think about the mathematics: if z=y+b and y=x+a, then z=x+___

[Stu B22]

Hello folks. In the online NNG4, I am stuck in how to target rewrite tactic (rw) arguments at a subexpression (not just a single named term). For example, to prove the goal below, we merely need to rearrange terms using rw[mul_comm] and rw[mul_assoc], but how do we tell the tactic which subexpressions we want to group as arguments to mul_comm and mul_assoc?
a ^ prevN * b ^ prevN * (a * b) = a ^ prevN * a * (b ^ prevN * b)

Not important, but this is the exercise where I have that goal:
https://adam.math.hhu.de/#/g/leanprover-community/NNG4/world/Power/level/7

I know we can target individual terms, for example we could do rw[mul_comm a b]
but I can't see how to do rw[mul_comm (b ^ prevN) a] or the like, which is what we need.
(I can't find this topic mentioned in the docs, can't find an online example of anyone doing it, and when I try it I get errors).

Maybe rw tactic (in the Natural Number Game impl) cannot do this kind of targeting, although I see it is willing to grab subexpressions positionally, if we do say nth_rewrite 3 [mul_comm]

[Kevin Buzzard]

There is no b^prevN * a in the term so you can't do what you want to do, if I've understood correctly what you want to do.

[Mark Fischer]

--deleted--

[Stu B22]

Thanks. To be more precise, let's say the first move I want to make is to exchange the order of these 2 sub-expressions on the LHS:
b ^ prevN and (a * b)
I want to swap their order using rw[mul_comm ?1 ?2], but I don't know what to put for ?1 and ?2.
When I try rw[mul_comm (b ^ prevN) (a * b)]
I get tactic 'rewrite' failed, did not find instance of the pattern in the target expression b ^ prevN * (a * b)

[Kevin Buzzard]

Right, there is no b ^ prevN * (a * b) in the goal either. You can only change x * y to y * x if x * y is actually present in the goal. The left hand side of your goal is (a ^ prevN * b ^ prevN) * (a * b) and if you draw that as a little tree with *s with two legs coming out of it like the computer scientists like to do, you can see that the thing you want to be there isn't there.

[Stu B22]

Thank you Kevin. I see that I am able to use rw[mul_comm (a ^ prevN * b ^ prevN) (a * b)] so that answers my question about syntax, and I am ready to work on the proof again. I think it would be useful to show an example like that one (requiring parentheses in the tactic input) in the docs/lessons. I don't recall seeing one, but maybe I missed it. Grateful for your help. :smiley:

[VayusElytra]

Hi! I just started learning Lean today and am slightly confused about Algorithm World 5. If one has an equality as an assumption, such as, in this case,

h: succ a = succ b

how does one just apply a function to both sides of this equation? (in this case, pred). Apologies, this feels like something I should really be able to figure out on my own...

[Ruben Van de Velde]

Either apply pred at h or apply_fun pred at h might work

[Ruben Van de Velde]

But there might also be a theorem that gets you there directly

[VayusElytra]

yeah seems like apply_fun is not available in the NNG :(
edit: it's ok now! it was, indeed, something i should not have needed to ask about haha

[Jon Eugster]

It's fine to ask anything here, really!

As you probably figured from the hint the game gives you, the intended solution is not to do work on h but use the new lemma pred_succ you received at the goal a = b instead.

Another way to do what you asked (besides apply_fun) would be apply congr_arg pred at h but that's not in the game, either. One could probably ask for one of these alternative options to be included in the game. Afaik Kevin's design is to keep it as minimalistic as possible, so I don't know if it would be added, but it might be worth suggesting nevertheless.

[VayusElytra]

Thank you very much! Yes, that's what I figured. I feel like it makes sense to restrict possible tactics this early on as you say.

Hopping onto this, another question; I frequently find myself in situations such as this one:
image.png
It is very simple to conclude from here of course, one just needs to apply add_left_comm for instance, which gives A + (B + C) = B + (A + C) for any A, B, C naturals. However, I've found that it frequently doesn't find that pattern in the expression; I suppose because Lean is looking for natural numbers and finding e x c and e x b instead. Is there a way to still be able to apply add_left_comm here in spite of this?

I'll add another closely related question: in this instance
image.png
this input successfully swaps a^d and a. However, trying nth_rewrite 6 [mul_comm] does not swap a and b ^ succ d. Why is that?

[Jon Eugster]

It's generally useful if you provide some example that people can use to play with, either a code block that runs as-is on live.lean-lang.org or in the game context a link to the level together with some code how to get to your state. Lean's sometimes quite hard to read from a screenshot as a öot is goi g on behind the scenes.

Second question: I only count 5 *, so I'm not surprised the command fails when you tell it it should rewrite the 6th occurance. (note for some reason nth_rw starts counting at 1)

First question: I'm not sure, that's where a #mwe would help to see if it's something with the modified rw, or if it just generally wants some underscores _ after the lamme name as rw seems to do that sometimes

[Jon Eugster]

(second question: also note that you don't count them left-to-right as you see them. Instead you also have to take the invisible parenthesis into account to know how nth_rw counts.)

[VayusElytra]

Thanks! I'll make sure to provide that next time (because to be frank, one day after, I also have trouble remembering how exactly I got there...)

[Ruben Van de Velde]

One disadvantage of the lean4 NNG is that it's harder to copy/paste everything you've done in a level. I wonder if that could be improved

[Kevin Buzzard]

Do you know about editor mode @Ruben Van de Velde ?

editor_mode.png

[Ruben Van de Velde]

I did not!

[Kevin Buzzard]

Maybe it should be better advertised!

[Jon Eugster]

I think it could make sense to have a button in each level that creates a preformatted question in the "new members"stream: https://github.com/leanprover-community/lean4game/issues/227 for collecting ideas on that. (I don't have plans to do it rn, but might eventually)

[Bernardo Borges]

Hello Everyone! Firstly I must say, NNG4 is a great game and learning experience! Congrats to everyone involved!
Now to the question. This may be evident to some, but as english is not my mother language I may not be getting the meaning... In the last level of the power world we have:
image.png
I am now intrigued between two possibilities:

1. This is Fermat's Last Theorem. It is HARD, and will take millions of lines of code, and it's work in progress by Kevin etc. Go do something else.
2. This is a CLUNKY VERSION of Fermat's Last Theorem. Even if the full theorem is hard, you should be able to prove this version with what we have. Go about it.
   Which one of these should I take? Thanks! :)

[Yaël Dillies]

Your point 2 is wrong. The statement as presented really is Fermat's last theorem, so it is hard.

[Yaël Dillies]

What's clunky about it is that it uses m + 3, instead of m with m ≥ 3.

[Bernardo Borges]

Ah phew, I wasn't really sure about it and started working on the problem... then I realized this might be a silly effort :grinning_face_with_smiling_eyes: The game let's you give it a try tho

[Bernardo Borges]

image.png
This means this blue guy won't turn green so soon...

[Kevin Buzzard]

#FLT

[awefhio]

Hi, I'm working through the game and I'm at level 11/11 of the <= world.

In this step, I'm looking at succ a = succ 0, and I naturally want to use "apply succ_inj" to get a = 0
However, the next step actually adds another succ to the expression. Am I doing something wrong here?

image.png

[awefhio]

full code for reference:

cases x
left
rfl
right
rw [two_eq_succ_one] at hx
apply succ_le_succ at hx
rw [one_eq_succ_zero, two_eq_succ_one]
apply le_one at hx
cases hx
left
apply succ_inj

[Bernardo Borges]

You can use ```lean to create a code block

[Bernardo Borges]

Indeed, in Mathlib Nat.succ_inj is a.succ = b.succ ↔ a = b but in NNG you only have succ_inj (a b : ℕ) (h : MyNat.succ a = MyNat.succ b) : a = b, and even so, it's behaving like the oposite direction here

[awefhio]

is this a bug then?

a related question: after

rw [one_eq_succ_zero, two_eq_succ_one]

the goal is
image.png

I would actually like to use

repeat apply succ_inj

but that does nothing in the interface. Is this not a valid operation? I was hoping it would turn

succ a = succ 0 ∨ succ a = succ 1

into

a = 0 ∨ a = 1

such that I can use

apply le_one at hx

and complete the proof immediately

[Mitchell Lee]

This is not a bug. I recommend reading the description of the apply tactic to understand what is going on.

[Bernardo Borges]

awefhio said:

full code for reference:

cases x
left
rfl
right
rw [two_eq_succ_one] at hx
apply succ_le_succ at hx
rw [one_eq_succ_zero, two_eq_succ_one]
apply le_one at hx
cases hx
left
apply succ_inj

Funny enough,

rw [succ_inj (succ a) (succ 0)]
rfl

Will close this goal

[awefhio]

Mitchell Lee said:

This is not a bug. I recommend reading the description of the apply tactic to understand what is going on.

ah I think I understand, applying a proof goes backwards if it is a goal and forwards if it is a hypothesis?

[Paul Rowe]

Bernardo Borges said:

image.png
This means this blue guy won't turn green so soon...

Has anybody yet played the prank of saying, "I loved the NNG. Found it quite easy in the end," followed by a (doctored) screenshot will all green circles?

[Ruben Van de Velde]

"oh, I thought that was our homework"

[Kevin Buzzard]

I'm working on it!

[Paul Rowe]

But that will be the real thing, not just a prank! Plus, I guess I secretly thought of you as being the main audience for the joke/prank.

[Jon Eugster]

There are actually two rather simple ways to solve the game ;)

Screenshot_20240523_200705.png

One requires magic, the other out-of-the-box thinking (but both can be achieved with the provided game framework, i.e. without post-editing of screenshots or modifying CSS in the browser dev-tools :upside_down: )

[Bernardo Borges]

Nice how you warped into the Power World without passing the last World (the edge is gray)

[Jon Eugster]

(I set the rules to "none"/"relaxed" in order to skip everything before that, as it's only about Power level 10)