rw [h] uses h from the environment in preference to h from the local context

[joneugster]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

rw seems to priorities other statements over variables in context. I would expect the reverse.

Context

Zulip discussion and (non-minimised) question in New Members stream

Steps to Reproduce

See the following MWE:

import Lean

open List

example (A B : Prop) (all : A ↔ B) (b : B) : A := by
  rw[all] -- error: failed to rewrite using equation theorems for 'List.all'
  assumption

Expected behavior: The above MWE should succeed.

Actual behavior: rw fails.

Note that all other tactics - simp, apply, exact, ... do correctly use the local all instead of List.all, so it seems to be a rw-specific issue.

Moreover, the same behaviour shows it open List is replaced with def all := 3.

Versions

(lean4web)
4.2.0-rc3

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[semorrison]

Thanks. If anyone would like to identify the cause of this difference in behaviour that would be very helpful. I'd be happy to review a fix PR if there is an easy solution.

[thorimur]

@semorrison I think this is because rewrite (or more specifically withRWRulesSeq) matches on each rule syntax and specifically processes identifiers differently (i.e. as global constants). This happens in TacticM, so we can probably just check if the id is an fvar before doing so! I can PR tomorrow. :)

EDIT: Actually, I wanted to PR tonight; see #2738 . :) Still technically in progress, though—I'm fairly confident this is the right way to do this, but not 100% sure. (I'm also not sure that it won't break anything!) (Just as a stylistic matter, is there a single combinator succeeds x somewhere which lands in m Bool, and is pure true if x : m a succeeds, and pure false if it fails?) Feel free to review, though!