rewrite specific term

Stream: new members

[Liang Zhang]

I'm working through https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=8&level=8

in the goal I have

22:9: goal
a b : mynat,
h : a + b = a
⊢ b = 0

I would like to rewrite only the second a in h into a + 0 with add_zero. However, rw ← (add_zero a) at h, rewrites both as. How can I do that?

[Kevin Buzzard]

One painless way would be by introducing a new hypothesis. have h2, a+b=a+0, then rw add_zero, exact h

[Kevin Buzzard]

There are other ways to do it (you can do the rewrite, either using conv mode or some extra inputs into the rw tactic) but I don't teach these in NNG

[Liang Zhang]

Kevin Buzzard said:

There are other ways to do it (you can do the rewrite, either using conv mode or some extra inputs into the rw tactic) but I don't teach these in NNG

Thanks! How can I find the extra possible inputs? BTW, what is NNG?

[Kevin Buzzard]

NNG=natural number game. I think on the leanprover-community website there is information about conv mode

[Liang Zhang]

Got it

[Kevin Buzzard]

There doesn't seem to be a mention of the occs parameter for rw but that's the other approach. My way is easiest though :-)

[Kevin Buzzard]

Maybe search this Zulip for occs?

[Kevin Buzzard]

Oh apparently it might not do the job and you might have to use nth_rewrite but that might not be in NNG Lean which is quite old

[Liang Zhang]

I think you are right. nth_rewrite is not available in NNG. Will go with your suggestion. Thanks!