Prerequisites

• 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.
  • Reduced the issue to a self-contained, reproducible test case.

Description

When using rw or kabstract with the occs parameter, metavariables in the lemma that we are rewriting by (or the expression we are abstracting) are instantiated by the first match found, even if this match is disallowed by occurrences.

Steps to Reproduce

variable (f : Nat → Nat) (w : ∀ n, f n = 0)

example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by
  rw (config := {occs := .pos [2]}) [w]
  -- Oh no! This currently rewrites the second `f 1`, rather than the first `f 2`,
  -- because the argument of `w` has already be fixed to `1` when we visit `f 1`.

Note this behaviour makes it impossible to achieve some rewrites. (Of course there are usually workarounds with conv, or by specifying arguments, but it is more difficult if automation wants to know about all possible rewrites.)

Expected behavior:

variable (f : Nat → Nat) (w : ∀ n, f n = 0)

example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by
  rw (config := {occs := .pos [2]}) [w]
  trace_state -- ⊢ [f 1, 0, f 1, f 2] = [0, 0, 0, 0]
  rw [w, w]

Actual behavior:

variable (f : Nat → Nat) (w : ∀ n, f n = 0)

example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by
  rw (config := {occs := .pos [2]}) [w]
  trace_state -- ⊢ [f 1, f 2, 0, f 2] = [0, 0, 0, 0]
  rw [w, w]

Versions

The config := {occs := ...} option has only just landed in Lean, so you will need to either test this on master or on nightly-2023-09-14 when it arrives or later.