Zulip Chat Archive

Stream: new members

Topic: rewrite specific term


Liang Zhang (Dec 23 2021 at 06:40):

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 (Dec 23 2021 at 06:43):

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

Kevin Buzzard (Dec 23 2021 at 06:45):

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 (Dec 23 2021 at 06:51):

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 (Dec 23 2021 at 06:52):

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

Liang Zhang (Dec 23 2021 at 06:52):

Got it

Kevin Buzzard (Dec 23 2021 at 06:53):

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 (Dec 23 2021 at 06:54):

Maybe search this Zulip for occs?

Kevin Buzzard (Dec 23 2021 at 06:56):

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 (Dec 23 2021 at 07:02):

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


Last updated: Dec 20 2023 at 11:08 UTC