rw tactic in NNG4 behaving unexpectedly

Stream: new members

[Nikolai Morin]

I am doing the Lean Natural Number game and having difficulty understanding the behavior of rw and nth_rewrite.

According to the game itself (in tutorial level 8), rw is supposed to replace all occurrences of a term, but when I write

theorem add_assoc (a b c : ℕ) : a + b + c = a + (b + c) := by
  induction a with x hx
  rw [zero_add, zero_add]

then the last step needs two applications of the rewrite rule to also rewrite the right side of the goal equation. Also, if I replace the rw with nth_rewrite 2 [zero_add] (which is not a useful step here, I know) to only remove the 0 + on the right side, I get

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  0 + b

Is that a bug in the game? How can I apply a rewrite only to the right side of the goal?

[Mauricio Collares]

If you click on the "rw" tactic (in the list of tactics on the right-hand side), it will tell you more precisely what it means by "all occurrences" in the "Targetted usage" section. Not sure if it's useful for your particular question, but the documentation there is quite detailed and it's worth a read.

[Mauricio Collares]

But basically, rw and nth_rewrite first try to locate some part of the expression that matches the lemma you passed. Then it infers the arguments to the relevant lemma, and those parameters will be "fixed" for some purposes; it won't "reinfer" them to match other instances of the desired expression.

[Nikolai Morin]

Thanks, that's helpful. So, are you saying thet when I do nth_rewrite 2 [zero_add] to the goal 0 + b + c = 0 + (b + c), then it finds the first match of 0 + ? at the very beginning and infers ? to be b, then searches for another instance of 0 + b only, instead of 0 + ??

[Kevin Buzzard]

I have no idea why nth_rewrite 2 [zero_add] doesn't change only the second 0 + ?, I am surprised by this. You can write rw [zero_add (b + c)] to change only the RHS.

[Kevin Buzzard]

I've asked in #mathlib4 -- see here.