`rw [foo] at *` rewrites `foo` itself

[madvorak]

Description

In Lean 4, if you use rw [foo] at * then it rewrites everything including foo. If you had foo : x = y then you obtain foo : y = y afterwards. It might happen that foo would be useful again later. After rw [foo] at * it is useless and foo only clutters the infoview.

Steps to Reproduce

example (α : Type) (a b c d : α) (hab : a = b) (hac : a = c) :
  a = d  :=
by
  rw [hab] at *
  sorry

Expected behavior:

I think that rw [hab] at * should rewrite a only in hac and the goal. This is how it worked in Lean 3.

Actual behavior:

α : Type
a b c d : α
hab : b = b
hac : b = c
⊢ b = d

After rw [hab] at * you can see that hab : b = b is in the infoview.

Reproduces how often:

100 %

Additional Information

Lean 3 code

example (α : Type) (a b c d : α) (hab : a = b) (hac : a = c) :
  a = d  :=
begin
  rw [hab] at *,
  sorry
end

gives:

α : Type,
a b c d : α,
hab : a = b,
hac : b = c
⊢ b = d

[alexkeizer]

The relevant (top-level) code is in src/lean/Lean/Elab/Tactic/Rewrite.lean and src/lean/Lean/Elab/Tactic/Location.lean

In the following, if loc (the location) turns out to be Location.Wildcard, then we want to somehow change that "actually, all locations, except these specific local hypotheses"

@[builtin_tactic Lean.Parser.Tactic.rewriteSeq] def evalRewriteSeq : Tactic := fun stx => do
  let cfg ← elabRewriteConfig stx[1]
  let loc   := expandOptLocation stx[3]
  withRWRulesSeq stx[0] stx[2] fun symm term => do
    withLocation loc
      (rewriteLocalDecl term symm · cfg)
      (rewriteTarget term symm cfg)
      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")

[semorrison]

Perhaps rewriteLocalDecl could gain a flag allowSelf := true that, if set to false, stops if term is the local hypothesis. Then in evalRewriteSeq quoted above we could set that flag according to whether loc \ne *.

(It may be worth checking how Lean 3 handled this special case.)