rw at * using hypothesis

[jldodds]

Prerequisites

• [x ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

rw H at * tactic where H is a hypothesis also rewrites in that hypothesis, making it useless, sometimes in the middle of tactic execution

Steps to Reproduce

Observe the rewrite in the following proof

lemma test {A B : Type} (f : A -> B) a b c (h1 : f a = b) (h2 : f a = c) : false :=
begin
rw h1 at *,
admit
end

Expected behavior: [What you expect to happen]
Behavior equivalent to rw h1 at h2

at worst rewriting both of them, but it's preferable to leave h1 alone for possible future use

Actual behavior: [What actually happens]
rewrite occurs in h1, making it trivial before h2 can be rewritten

Reproduces how often: [What percentage of the time does it reproduce?]
always

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Lean (version 3.2.1, commit f1ec117, RelWithDebInfo)

Any additional information, configuration or data that might be necessary to reproduce the issue.

[leodemoura]

We can change the behavior of rw h at * to skip the hypothesis h if h is a hypothesis. I think this is a good compromise.
However, the following will still produce an useless hypothesis.

lemma test {A B : Type} (f : A -> B) a b c (h1 : f a = b) (h2 : f a = c) : false :=
begin
rw [id h1] at *,
admit
end

This is just an example, we can create much more convoluted examples that produce the undesirable behavior.

[jldodds]

I was using it in a context addressed by this PR. So the fix mentioned would address that.

For what it's worth, Coq doesn't do the rewrite in the case you mentioned, but I have no insight into how that is achieved. Perhaps no rewrites in any hypothesis that is used to construct the term to rewrite by? This is likely a good idea using the current implementation, as otherwise the result of the rewrite might depend on the order of hypotheses in the goal, which doesn't seem desirable.

[leodemoura]

Perhaps no rewrites in any hypothesis that is used to construct the term to rewrite by?

We can also do this. I don't see an example where this would be undesired.

otherwise the result of the rewrite might depend on the order of hypotheses in the goal, which doesn't seem desirable.

This is not an issue. The rewrite tactic actually creates a new hypothesis with the same name, and (tries to) clear the old one.

[jldodds]

What I mean is that if the rewrite proceeds on a hypothesis that is being rewritten by, the remaining rewrites will use the rewritten term. As an example, change the order of h1 and h2 in the statement of the example