feat: allow configuring occs in rw

src/Init/Meta.lean

@@ -1280,11 +1280,27 @@ def neutralConfig : Simp.Config := {
 
 end Simp
 
+inductive Occurrences where
+  | all
+  | pos (idxs : List Nat)
+  | neg (idxs : List Nat)
+  deriving Inhabited, BEq
+
+def Occurrences.contains : Occurrences → Nat → Bool
+  | all,      _   => true
+  | pos idxs, idx => idxs.contains idx
+  | neg idxs, idx => !idxs.contains idx
+
+def Occurrences.isAll : Occurrences → Bool
+  | all => true
+  | _   => false
+
 namespace Rewrite
 
 structure Config where
   transparency : TransparencyMode := TransparencyMode.reducible
   offsetCnstrs : Bool := true
+  occs : Occurrences := Occurrences.all
 
 end Rewrite
 

src/Init/Tactics.lean

@@ -350,6 +350,15 @@ This provides a convenient way to unfold `e`.
 - `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a
   list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`
   can also be used, to signify the target of the goal.
+
+Using `rw (config := {occs := .pos L}) [e]`,
+where `L : List Nat`, you can control which "occurrences" are rewritten.
+(This option applies to each rule, so usually this will only be used with a single rule.)
+Occurrences count from `1`.
+At the first occurrence, whether allowed or not,
+arguments of the rewrite rule `e` may be instantiated,
+restricting which later rewrites can be found.
+`{occs := .neg L}` allows skipping specified occurrences.
 -/
 syntax (name := rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic
 

src/Lean/Data.lean

@@ -15,7 +15,6 @@ import Lean.Data.LOption
 import Lean.Data.Lsp
 import Lean.Data.Name
 import Lean.Data.NameMap
-import Lean.Data.Occurrences
 import Lean.Data.OpenDecl
 import Lean.Data.Options
 import Lean.Data.Parsec

src/Lean/Data/Occurrences.lean

@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-namespace Lean
-
-inductive Occurrences where
-  | all
-  | pos (idxs : List Nat)
-  | neg (idxs : List Nat)
-  deriving Inhabited, BEq
-
-def Occurrences.contains : Occurrences → Nat → Bool
-  | all,      _   => true
-  | pos idxs, idx => idxs.contains idx
-  | neg idxs, idx => !idxs.contains idx
-
-def Occurrences.isAll : Occurrences → Bool
-  | all => true
-  | _   => false
-
-end Lean

src/Lean/Elab/Tactic/Rewrite.lean

@@ -11,14 +11,15 @@ import Lean.Elab.Tactic.Config
 namespace Lean.Elab.Tactic
 open Meta
 
-def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config) : TacticM Unit := do
+def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config := {}) : TacticM Unit := do
   Term.withSynthesize <| withMainContext do
     let e ← elabTerm stx none true
     let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
     let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
     replaceMainGoal (mvarId' :: r.mvarIds)
 
-def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config) : TacticM Unit := do
+def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config := {}) :
+    TacticM Unit := do
   Term.withSynthesize <| withMainContext do
     let e ← elabTerm stx none true
     let localDecl ← fvarId.getDecl

src/Lean/Meta/KAbstract.lean

@@ -3,7 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-import Lean.Data.Occurrences
 import Lean.HeadIndex
 import Lean.Meta.Basic
 
@@ -12,7 +11,14 @@ namespace Lean.Meta
 /--
 Abstract occurrences of `p` in `e`. We detect subterms equivalent to `p` using key-matching.
 That is, only perform `isDefEq` tests when the head symbol of substerm is equivalent to head symbol of `p`.
-By default, all occurrences are abstracted, but this behavior can be controlled using the `occs` parameter.
+
+By default, all occurrences are abstracted,
+but this behavior can be controlled using the `occs` parameter.
+
+All matches of `p` in `e` are considered for occurrences,
+but at the first match (whether included in the occurrences or not)
+metavariables appearing in `p` (or `e`) may become instantiated,
+affecting the possibility of subsequent matches.
 -/
 def kabstract (e : Expr) (p : Expr) (occs : Occurrences := .all) : MetaM Expr := do
   let e ← instantiateMVars e

src/Lean/Meta/Tactic/Rewrite.lean

@@ -20,7 +20,7 @@ structure RewriteResult where
 Rewrite goal `mvarId`
 -/
 def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
-    (symm : Bool := false) (occs : Occurrences := Occurrences.all) (config := { : Rewrite.Config }) : MetaM RewriteResult :=
+    (symm : Bool := false) (config := { : Rewrite.Config }) : MetaM RewriteResult :=
   mvarId.withContext do
     mvarId.checkNotAssigned `rewrite
     let heqType ← instantiateMVars (← inferType heq)
@@ -34,7 +34,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           if lhs.getAppFn.isMVar then
             throwTacticEx `rewrite mvarId m!"pattern is a metavariable{indentExpr lhs}\nfrom equation{indentExpr heqType}"
           let e ← instantiateMVars e
-          let eAbst ← withConfig (fun oldConfig => { config, oldConfig with }) <| kabstract e lhs occs
+          let eAbst ← withConfig (fun oldConfig => { config, oldConfig with }) <| kabstract e lhs config.occs
           unless eAbst.hasLooseBVars do
             throwTacticEx `rewrite mvarId m!"did not find instance of the pattern in the target expression{indentExpr lhs}"
           -- construct rewrite proof
@@ -69,7 +69,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
 
 @[deprecated MVarId.rewrite]
 def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
-    (symm : Bool := false) (occs : Occurrences := Occurrences.all) (config := { : Rewrite.Config }) : MetaM RewriteResult :=
-  mvarId.rewrite e heq symm occs config
+    (symm : Bool := false) (config := { : Rewrite.Config }) : MetaM RewriteResult :=
+  mvarId.rewrite e heq symm config
 
 end Lean.Meta

tests/lean/interactive/1403.lean.expected.out

@@ -4,5 +4,5 @@
  {"start": {"line": 1, "character": 2}, "end": {"line": 1, "character": 12}},
  "contents":
  {"value":
-  "`rewrite [e]` applies identity `e` as a rewrite rule to the target of the main goal.\nIf `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction.\nIf `e` is a defined constant, then the equational theorems associated with `e` are used.\nThis provides a convenient way to unfold `e`.\n- `rewrite [e₁, ..., eₙ]` applies the given rules sequentially.\n- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a\n  list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`\n  can also be used, to signify the target of the goal.\n",
+  "`rewrite [e]` applies identity `e` as a rewrite rule to the target of the main goal.\nIf `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction.\nIf `e` is a defined constant, then the equational theorems associated with `e` are used.\nThis provides a convenient way to unfold `e`.\n- `rewrite [e₁, ..., eₙ]` applies the given rules sequentially.\n- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a\n  list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`\n  can also be used, to signify the target of the goal.\n\nUsing `rw (config := {occs := .pos L}) [e]`,\nwhere `L : List Nat`, you can control which \"occurrences\" are rewritten.\n(This option applies to each rule, so usually this will only be used with a single rule.)\nOccurrences count from `1`.\nAt the first occurrence, whether allowed or not,\narguments of the rewrite rule `e` may be instantiated,\nrestricting which later rewrites can be found.\n`{occs := .neg L}` allows skipping specified occurrences.\n",
   "kind": "markdown"}}

tests/lean/rewrite.lean

@@ -54,3 +54,53 @@ exact h₁ h₃
 
 example (α : Type) (p : Prop) (a b c : α) (h : p → a = b) : a = c := by
   rw [h _]  -- should manifest goal `⊢ p`, like `rw [h]` would
+
+/-!
+Testing the `occs` configuration argument.
+-/
+
+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]
+  -- Because the metavariables are instantiated after finding the first occurrence,
+  -- even though this is rejected, with the current behaviour this rewrites the second `f 1`,
+  -- rather than the first `f 2`.
+  -- Arguably this behaviour should be changed.
+  trace_state
+  rw [w, w]
+
+example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by
+  rw (config := {occs := .all}) [w]
+  trace_state -- expecting [0, f 2, 0, f 2] = [0, 0, 0, 0]
+  rw [w]
+
+example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by
+  rw (config := {occs := .pos [1, 2]}) [w]
+  trace_state -- expecting [0, f 2, 0, f 2] = [0, 0, 0, 0]
+  -- After the first rewrite, the argument of `w` have been instantiated as `1`,
+  -- so the second eligible rewrite is the second `f 1`.
+  rw [w]
+
+example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by
+  rw (config := {occs := .neg [1]}) [w]
+  -- Again, the rejected first occurrence nevertheless instantiates the metavariables.
+  -- Argubly the state here should be `[f 1, 0, f 1, 0] = [0, 0, 0, 0]`,
+  -- but for now if `[f 1, f 2, 0, f 2] = [0, 0, 0, 0]`
+  trace_state
+  rw [w, w]
+
+example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by
+  -- Arguably should succeed giving `[f 1, f 2, 0, f 2] = [0, 0, 0, 0]`
+  -- but currently fails.
+  fail_if_success rw (config := {occs := .neg [1, 2]}) [w]
+  trace_state
+  rw [w, w]
+
+example : [f 1, f 2, f 1, f 2] = [0, 0, 0, 0] := by
+  rw (config := {occs := .neg [1, 3]}) [w]
+  -- Arguably should give `[f 1, 0, f 1, f 2] = [0, 0, 0, 0]`
+  -- but currently gives `[f 1, f 2, 0, f 2] = [0, 0, 0, 0]`
+  trace_state
+  rw [w, w]
+

tests/lean/rewrite.lean.expected.out

@@ -31,3 +31,21 @@ p : Prop
 a b c : α
 h : p → a = b
 ⊢ p
+f : Nat → Nat
+w : ∀ (n : Nat), f n = 0
+⊢ [f 1, f 2, 0, f 2] = [0, 0, 0, 0]
+f : Nat → Nat
+w : ∀ (n : Nat), f n = 0
+⊢ [0, f 2, 0, f 2] = [0, 0, 0, 0]
+f : Nat → Nat
+w : ∀ (n : Nat), f n = 0
+⊢ [0, f 2, 0, f 2] = [0, 0, 0, 0]
+f : Nat → Nat
+w : ∀ (n : Nat), f n = 0
+⊢ [f 1, f 2, 0, f 2] = [0, 0, 0, 0]
+f : Nat → Nat
+w : ∀ (n : Nat), f n = 0
+⊢ [f 1, f 2, f 1, f 2] = [0, 0, 0, 0]
+f : Nat → Nat
+w : ∀ (n : Nat), f n = 0
+⊢ [f 1, f 2, 0, f 2] = [0, 0, 0, 0]