Rewrite subterm in expression

Stream: new members

[Severen Redwood]

Hi, I've proved the associativity of addition in the natural number game, but for the base case I had to resort to letting refl skip some steps for me because I couldn't figure out how to rewrite a subterm in an expression.

Here's my proof with a comment that should hopefully explain the dilemma.

induction c with k hk,
-- Base case
rw add_zero,
refl, -- skips steps for me!
-- for the above, I want to reason in Lean that:
-- (a + b) + 0 = (a + b) = (a + (b + 0)) = a + (b + 0)
-- rw add_zero gets me to the second from the left, but then I can't figure out
-- how to rewrite b using add_zero again.
-- Inductive step
rw add_succ,
rw hk,
rw <- add_succ,
rw <- add_succ,
refl,

[Severen Redwood]

What refl automated for me is admittedly incredibly trivial, but I would like to know how I could get the goal to "a + (b + c) = a + (b + c)" manually.

[Reid Barton]

Rather than thinking about rewriting

(a + b) + 0  ->  a + b  ->  a + (b + 0)

it would be easier in this case to think about

(a + b) + 0  ->  a + b  <-  a + (b + 0)

[Severen Redwood]

Do you mean as a mental model for how refl closes the goal?

[Reid Barton]

Well, you could think about it that way too but what I meant was: I think your goal is

|- (a + b) + 0 = a + (b + 0)

Rather than trying to rewrite the left-hand side until it turns into the right-hand side, you can rewrite both sides until they turn into the same other thing (namely a + b).

[Severen Redwood]

Ah right. I wasn't sure if you meant that or not because I don't (yet) know how to use rw to rewrite the RHS. That of course makes sense.

[Kevin Buzzard]

rw h rewrites the left hand side of h into the right hand side, but anywhere in the goal.

[Severen Redwood]

oh my god!

[Severen Redwood]

Ok thanks, that works then. Sorry if my question was a bit strange in light of that haha

[Reid Barton]

No worries, the answer to your original implied question is rw <- add_zero b, btw.

[Kevin Buzzard]

But seeing as you ask, probably something like rw ←add_zero b might work and do what you wanted to do?

[Severen Redwood]

I seem to end up in this state with that image.png

[Severen Redwood]

rather than |- a + b = a + b from applying rw add_zero twice

[Severen Redwood]

Also, I've seen in a couple places that there's a Discord server with other undergraduates and such. Would that be a better place for these kinds of questions? (I also have to admit I'm just more familiar and present on Discord)

[Reid Barton]

Oh right, because rw wants to replace all occurrences of the thing it's rewriting. It's possible to avoid that using another tactic but I don't think it exists in the NNG.

[Severen Redwood]

Ah oh well, now that I know that rw applies anywhere in the goal, it works swimmingly to use that.

[Severen Redwood]

thanks for the help!

[Huỳnh Trần Khanh]

Severen Redwood said:

Also, I've seen in a couple places that there's a Discord server with other undergraduates and such. Would that be a better place for these kinds of questions? (I also have to admit I'm just more familiar and present on Discord)

oh yes there's a Discord but I prefer Zulip now :joy: questions get answered very quickly on Zulip and the threaded structure makes things more organized :joy: anyway if you want to join the Discord server you should make a new thread here and say you want an invite, then someone will PM you... but you need to complete NNG first I guess, if you haven't completed NNG yet then you won't be allowed into the server

[Severen Redwood]

Huỳnh Trần Khanh said:

Severen Redwood said:

Also, I've seen in a couple places that there's a Discord server with other undergraduates and such. Would that be a better place for these kinds of questions? (I also have to admit I'm just more familiar and present on Discord)

oh yes there's a Discord but I prefer Zulip now :joy: questions get answered very quickly on Zulip and the threaded structure makes things more organized :joy: anyway if you want to join the Discord server you should make a new thread here and say you want an invite, then someone will PM you... but you need to complete NNG first I guess, if you haven't completed NNG yet then you won't be allowed into the server

But don't I get a free pass as a maths undergraduate?! At least according to this archived message it's enough...image.png

Although I'm making steady progress on NNG and am enjoying it, so I don't mind completing that first at all :wink: