7

In Lean I occasionally want to apply a rw tactic to exactly one of multiple identical terms. For example I have the goal

⊢ 0 = 0

and I want to rw it to

⊢ a * 0 = 0

I also have

mul_zero (a : mynat) :
  a * 0 = 0

Now I should be able to just rewrite the 0 to a * 0. However trying

rw ← zero_mul a,

gives me

⊢ a * 0 = a * 0

Which is not what I want!

Is there a reason lean does this and is there some way to apply a rewrite to only one term?

Wheat Wizard
  • 3,982
  • 14
  • 34

2 Answers2

4

rw rewrites all identical terms simultaneously. There is a different tactic nth_rewrite which only rewrites a specific occurrence of a term. You need mathlib for nth_rewrite, and I'm not sure if it is available in the Natural Number Game.

import tactic
example : 0 = 0 :=
begin
  nth_rewrite 0 [← nat.mul_zero 2],
  -- ⊢ 2 * 0 = 0
end
Floris van Doorn
  • 391
  • 1
  • 6
3

You can use the conv tactics for this

lemma a : 0 = 0 :=
begin
  conv {
    to_lhs, 
    rw ← nat.mul_zero 2,
  },
end

see: https://leanprover-community.github.io/extras/conv.html

Alex J Best
  • 306
  • 1
  • 6