rw duplicates a hypothesis

Stream: lean4

[Heather Macbeth]

It seems that rw sometimes duplicates a hypothesis rather than replacing it. Is this intended, or -- if it's a bug -- has it been reported? Example:

theorem foo [OfNat α 0] {a b : α} : a = b ↔ a = 0 := sorry

example (a b : Nat) (h : a = b) : False := by
  rw [foo] at h

The goal state is now

a b : Nat
h✝ : a = b
h : a = 0
⊢ False

I'm on nightly-2023-02-24 (edit: also happens on nightly-2023-03-15).

[Alex Keizer]

IIRC, it has to do with the fact that you changed the type of h to something which is not defeq with the old type, so any uses of h in other expressions have to refer to the old h.

[Heather Macbeth]

Aha, that makes sense!

It would be nice if there were some extra logic which noticed that in this goal state there are no uses of h in other expressions, and then went ahead and deleted h✝. (This is surely the more typical situation!). Is that possible?

[Heather Macbeth]

For what it's worth, Lean 3 (on the web editor's current version of the community fork) apparently does do this, keeping two different h in the goal state after rw only if the original h is referenced somewhere. Reference code:

variable {α : Type*}

lemma foo [has_zero α] {a b : α} : a = b ↔ a = 0 := sorry

example (a b : nat) (h : a = b)  : false :=
begin
  rw [foo] at h,

end

example (a b : nat) (h : a = b) {x : {k : nat // k = b}} (hx : x = ⟨a, h⟩) : false :=
begin
  rw [foo] at h,

end

[Mario Carneiro]

that logic already exists. There must be something hidden in the context which is referring to the old h

[Mario Carneiro]

Note that it works as expected if foo is not generic, i.e. theorem foo {a b : Nat} : a = b ↔ a = 0 := sorry

[Mario Carneiro]

so probably the thing that is referring to the old h is a metavariable which is not yet solved (e.g. the variable α in foo)

[Mario Carneiro]

You can clear the variable after the fact:

theorem foo [OfNat α 0] {a b : α} : a = b ↔ a = 0 := sorry

example (a b : Nat) (h : a = b) : False := by
  rw [foo] at h
  rename_i h2
  clear h2

[Mario Carneiro]

Now this is unexpected:

theorem foo {α} [OfNat α 0] (a b : α) : (a = b) = (a = 0) := sorry
theorem bar (α) [OfNat α 0] (a b : α) : (a = b) = (a = 0) := sorry

variable (a b : Nat) (h : a = b)
example : False := by rw [foo] at h; rename_i h2; sorry -- does not replace h
example : False := by rw [bar] at h; rename_i h2; sorry -- replaces h

[Heather Macbeth]

Mario Carneiro said:

so probably the thing that is referring to the old h is a metavariable which is not yet solved (e.g. the variable α in foo)

Interesting. Is that a bug? It seems like the variable α should be identifiable here as Nat?

[Eric Wieser]

rw [bar _] vs rw [bar] shows the same behavior as above

[Heather Macbeth]

I opened lean4#2158 for this.