Rewriting specific term

Stream: new members

[Nico Beck]

I am doing the natural number game. I have a hypothesis h : a + b = a. I would like to use a rewrite rule

add_zero (a : mynat) a + 0 = a

to change the second instance of a in h, but I can't figure out how to apply the rewrite tactic rw to spefic a terms, and not to all occurrences of a in h.

rw \l add_zero at h,

gives me h: (a + 0) + b = a + 0, which is not what I want.

rw \l add_zero at h {1},

is a syntax error. (I thought it might work, because of this page: https://leanprover.github.io/tutorial/A1_Quick_Reference.html)
The documantation about rw is just TODO, and the lean theorem book does not help me either. Does somebody know how to do it?

[Kevin Buzzard]

There are a few ways to do a targetted rewrite in Lean but I can't remember how many of them work in NNG. How about instead writing something like

have h2 : a + b = a + 0,
{ rw add_zero,
  exact h },

? That's an easy enough fix.

[Notification Bot]

This topic was moved here from #lean4 > Rewriting specific term by Bryan Gin-ge Chen

[Nico Beck]

It's a bit dissatisfying, but it works. Thanks! I did not know that I could introduce new goals this way.

[Kyle Miller]

Nico Beck said:

(I thought it might work, because of this page: https://leanprover.github.io/tutorial/A1_Quick_Reference.html)

I remember being very confused why I couldn't get any of that to work when I was first learning -- turns out that's a reference for Lean 2, not Lean 3!

[Kevin Buzzard]

There are other ways, I just don't remember how many work in NNG, which is using quite an old version of Lean 3 and mathlib (and which doesn't always have the right things imported, so the below may only work on some levels). Here's two more ways:

import tactic

example (a b : ℕ) (h : a + b = a) : a + b = a + 0 :=
begin
  nth_rewrite 1 ← add_zero a at h, -- h : a + b = a + 0
  rw add_zero at h, -- back to h : a + b = a
  conv_rhs at h {rw ← add_zero a}, -- h : a + b = a + 0
  exact h,
end