feat: add anchor support for restricting search space in grind only (#11003)

This PR adds support for specifying anchors to restrict the search space in `grind` when using `grind only`. Anchors can limit which case splits are performed and which local lemmas are instantiated.
2025-10-28 21:16:10 -04:00 · 2025-10-28 21:16:10 -04:00 · d436619c6d
commit d436619c6d
parent 19533ab1d4
11 changed files with 393 additions and 204 deletions
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@ -9,6 +9,8 @@ public import Init.Grind.Attr
 public section
 namespace Lean.Parser.Tactic

+syntax anchor := "#" noWs hexnum
+
 syntax grindLemma    := ppGroup((Attr.grindMod ppSpace)? ident)
 /--
 The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
@ -16,15 +18,12 @@ when selecting patterns.
 -/
 syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)

-/-!
-`grind` tactic and related tactics.
-/
 syntax grindErase    := "-" ident
 /--
 The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
 when selecting patterns.
 -/
-syntax grindParam    := grindErase <|> grindLemma <|> grindLemmaMin
+syntax grindParam    := grindErase <|> grindLemma <|> grindLemmaMin <|> anchor

 namespace Grind
 declare_syntax_cat grind_filter (behavior := both)
@ -73,7 +72,6 @@ syntax (name := linarith) "linarith" : grind
 /-- The `sorry` tactic is a temporary placeholder for an incomplete tactic proof. -/
 syntax (name := «sorry») "sorry" : grind

-syntax anchor := "#" noWs hexnum
 syntax thm := anchor <|> grindLemma <|> grindLemmaMin

 /--
--- a/src/Lean/Elab/Tactic/Grind/Anchor.lean
+++ b/src/Lean/Elab/Tactic/Grind/Anchor.lean
@ -0,0 +1,20 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+namespace Lean.Elab.Tactic.Grind
+open Meta Grind
+
+public def elabAnchorRef (anchor : TSyntax `hexnum) : CoreM AnchorRef := do
+  let numDigits := anchor.getHexNumSize
+  let val := anchor.getHexNumVal
+  if val >= UInt64.size then
+    throwError "invalid anchor, value is too big"
+  let anchorPrefix := val.toUInt64
+  return { numDigits, anchorPrefix }
+
+end Lean.Elab.Tactic.Grind
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@ -24,6 +24,7 @@ import Lean.Meta.Tactic.ExposeNames
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.RenameInaccessibles
 import Lean.Elab.Tactic.Grind.Filter
+import Lean.Elab.Tactic.Grind.Anchor
 import Lean.Elab.Tactic.Grind.ShowState
 import Lean.Elab.Tactic.Grind.Config
 import Lean.Elab.SetOption
@ -139,14 +140,6 @@ def ematchThms (only : Bool) (thms : Array EMatchTheorem) : GrindTacticM Unit :=
    getGoal
  replaceMainGoal [goal]

-def elabAnchor (anchor : TSyntax `hexnum) : CoreM (Nat × UInt64) := do
-  let numDigits := anchor.getHexNumSize
-  let val := anchor.getHexNumVal
-  if val >= UInt64.size then
-    throwError "invalid anchor, value is too big"
-  let val := val.toUInt64
-  return (numDigits, val)
-
@[builtin_grind_tactic instantiate] def evalInstantiate : GrindTactic := fun stx => withMainContext do
  let `(grind| instantiate $[ only%$only ]? $[ approx ]? $[ [ $[$thmRefs?:thm],* ] ]?) := stx | throwUnsupportedSyntax
  let goal ← getMainGoal
@ -162,14 +155,14 @@ def elabAnchor (anchor : TSyntax `hexnum) : CoreM (Nat × UInt64) := do
      | _ => throwErrorAt thmRef "unexpected theorem reference"
  ematchThms only thms
 where
-  collectThms (numDigits : Nat) (anchorPrefix : UInt64) (thms : PArray EMatchTheorem) : StateT (Array EMatchTheorem) GrindTacticM Unit := do
+  collectThms (anchorRef : AnchorRef) (thms : PArray EMatchTheorem) : StateT (Array EMatchTheorem) GrindTacticM Unit := do
    let mut found : Std.HashSet Expr := {}
    for thm in thms do
      -- **Note**: `anchors` are cached using pointer addresses, if this is a performance issue, we should
      -- cache the theorem types.
      let type ← inferType thm.proof
      let anchor ← liftGrindM <| getAnchor type
-      if isAnchorPrefix numDigits anchorPrefix anchor then
+      if anchorRef.matches anchor then
        -- **Note**: We display the anchor term at most once.
        unless found.contains type do
          logTheoremAnchor thm.proof
@ -177,11 +170,11 @@ where
        modify (·.push thm)

  elabLocalEMatchTheorem (anchor : TSyntax `hexnum) : GrindTacticM (Array EMatchTheorem) := withRef anchor do
-    let (numDigits, anchorPrefix) ← elabAnchor anchor
+    let anchorRef ← elabAnchorRef anchor
    let goal ← getMainGoal
    let thms ← StateT.run' (s := #[]) do
-      collectThms numDigits anchorPrefix goal.ematch.thms
-      collectThms numDigits anchorPrefix goal.ematch.newThms
+      collectThms anchorRef goal.ematch.thms
+      collectThms anchorRef goal.ematch.newThms
      get
    if thms.isEmpty then
      throwError "no local theorems"
@ -246,7 +239,8 @@ where
    | .cases _ | .intro | .inj | .ext | .symbol _ =>
      throwError "invalid modifier"

-def logAnchor (e : Expr) : TermElabM Unit := do
+def logAnchor (c : SplitInfo) : TermElabM Unit := do
+  let e := c.getExpr
  let stx ← getRef
  if e.isFVar || e.isConst then
    /-
@ -270,19 +264,18 @@ def logAnchor (e : Expr) : TermElabM Unit := do

@[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => do
  let `(grind| cases #$anchor:hexnum) := stx | throwUnsupportedSyntax
-  let (numDigits, val) ← elabAnchor anchor
+  let anchorRef ← elabAnchorRef anchor
  let goal ← getMainGoal
  let candidates := goal.split.candidates
-  let (e, goals, genNew) ← liftSearchM do
+  let (c, goals, genNew) ← liftSearchM do
    for c in candidates do
-      let e := c.getExpr
-      let anchor ← getAnchor c.getExpr
-      if isAnchorPrefix numDigits val anchor then
+      let anchor ← c.getAnchor
+      if anchorRef.matches anchor then
        let some result ← split? c
          | throwError "`cases` tactic failed, case-split is not ready{indentExpr c.getExpr}"
-        return (e, result)
+        return (c, result)
    throwError "`cases` tactic failed, invalid anchor"
-  goal.withContext <| withRef anchor <| logAnchor e
+  goal.withContext <| withRef anchor <| logAnchor c
  let goals ← goals.filterMapM fun goal => do
    let goal := { goal with ematch.num := 0 }
    let (goal, _) ← liftGrindM <| SearchM.run goal do
--- a/src/Lean/Elab/Tactic/Grind/Main.lean
+++ b/src/Lean/Elab/Tactic/Grind/Main.lean
@ -13,9 +13,9 @@ public import Lean.PremiseSelection.Basic
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.EMatchTheoremParam
 import Lean.Elab.Tactic.Grind.Basic
+import Lean.Elab.Tactic.Grind.Param
 import Lean.Elab.MutualDef
 meta import Lean.Meta.Tactic.Grind.Parser
-
 public section
 namespace Lean.Elab.Tactic
 open Meta
@ -71,18 +71,6 @@ def elabInitGrindNorm : CommandElab := fun stx =>
        Grind.registerNormTheorems pre post
  | _ => throwUnsupportedSyntax

-private def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name) : MetaM Unit := do
-  let minIndexable := false -- TODO: infer it
-  let kinds ← match s.getKindsFor (.decl declName) with
-    | [] => return ()
-    | [k] => pure m!"@{k.toAttribute minIndexable}"
-    | [.eqLhs gen, .eqRhs _]
-    | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute minIndexable}"
-    | ks =>
-      let ks := ks.map fun k => m!"@{k.toAttribute minIndexable}"
-      pure m!"{ks}"
-  logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`"
-
 private def parseModifier (s : String) : CoreM Grind.AttrKind := do
  let stx := Parser.runParserCategory (← getEnv) `Lean.Parser.Attr.grindMod s
  match stx with
@ -90,30 +78,9 @@ private def parseModifier (s : String) : CoreM Grind.AttrKind := do
  | _ => throwError "unexpected modifier {s}"

 open PremiseSelection in
-def elabGrindParams
-    (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool)
-    (premises : Array Suggestion := #[]) (lax : Bool := false) :
-    MetaM Grind.Params := do
+def elabGrindPremises
+    (params : Grind.Params) (premises : Array Suggestion := #[]) : MetaM Grind.Params := do
  let mut params := params
-  for p in ps do
-    try
-      match p with
-      | `(Parser.Tactic.grindParam| - $id:ident) =>
-        let declName ← realizeGlobalConstNoOverloadWithInfo id
-        if let some declName ← Grind.isCasesAttrCandidate? declName false then
-          Grind.ensureNotBuiltinCases declName
-          params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) }
-        else if (← Grind.isInjectiveTheorem declName) then
-          params := { params with inj := params.inj.erase (.decl declName) }
-        else
-          params := { params with ematch := (← params.ematch.eraseDecl declName) }
-      | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) =>
-        params ← processParam params p mod? id (minIndexable := false)
-      | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $id:ident) =>
-        params ← processParam params p mod? id (minIndexable := true)
-      | _ => throwError "unexpected `grind` parameter{indentD p}"
-    catch ex =>
-      if !lax then throw ex
  for p in premises do
    let attr ← match p.flag with
    | some flag => parseModifier flag
@ -130,108 +97,15 @@ def elabGrindParams
      -- Let's only do this if there is a prospect of a premise selector supprting this.
      throwError "unexpected modifier {p.flag}"
  return params
-where
-  ensureNoMinIndexable (minIndexable : Bool) : MetaM Unit := do
-    if minIndexable then
-      throwError "redundant modifier `!` in `grind` parameter"

-  processParam (params : Grind.Params)
-      (p : TSyntax `Lean.Parser.Tactic.grindParam)
-      (mod? : Option (TSyntax `Lean.Parser.Attr.grindMod))
-      (id : TSyntax `ident)
-      (minIndexable : Bool)
-      : MetaM Grind.Params := do
-    let mut params := params
-    let declName ← try
-      realizeGlobalConstNoOverloadWithInfo id
-    catch err =>
-      if (← resolveLocalName id.getId).isSome then
-        throwErrorAt id "redundant parameter `{id}`, `grind` uses local hypotheses automatically"
-      else
-        throw err
-    let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer
-    match kind with
-    | .ematch .user =>
-      unless only do
-        withRef p <| Grind.throwInvalidUsrModifier
-      ensureNoMinIndexable minIndexable
-      let s ← Grind.getEMatchTheorems
-      let thms := s.find (.decl declName)
-      let thms := thms.filter fun thm => thm.kind == .user
-      if thms.isEmpty then
-        throwErrorAt p "invalid use of `usr` modifier, `{.ofConstName declName}` does not have patterns specified with the command `grind_pattern`"
-      for thm in thms do
-        params := { params with extra := params.extra.push thm }
-    | .ematch kind =>
-      params ← withRef p <| addEMatchTheorem params id declName kind minIndexable
-    | .cases eager =>
-      ensureNoMinIndexable minIndexable
-      withRef p <| Grind.validateCasesAttr declName eager
-      params := { params with casesTypes := params.casesTypes.insert declName eager }
-    | .intro =>
-      if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
-        for ctor in info.ctors do
-          params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
-      else
-        throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
-    | .inj =>
-      let thm ← Grind.mkInjectiveTheorem declName
-      params := { params with inj := params.inj.insert thm }
-    | .ext =>
-      throwError "`[grind ext]` cannot be set using parameters"
-    | .infer =>
-      if let some declName ← Grind.isCasesAttrCandidate? declName false then
-        params := { params with casesTypes := params.casesTypes.insert declName false }
-        if let some info ← isInductivePredicate? declName then
-          -- If it is an inductive predicate,
-          -- we also add the constructors (intro rules) as E-matching rules
-          for ctor in info.ctors do
-            -- **Note**: We should not warn if `declName` is an inductive
-            params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False)
-      else
-        params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
-    | .symbol prio =>
-      ensureNoMinIndexable minIndexable
-      params := { params with symPrios := params.symPrios.insert declName prio }
-    return params
-
-  addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name)
-      (kind : Grind.EMatchTheoremKind)
-      (minIndexable : Bool) (suggest : Bool := false) (warn := true) : MetaM Grind.Params := do
-    let info ← getAsyncConstInfo declName
-    match info.kind with
-    | .thm | .axiom | .ctor =>
-      match kind with
-      | .eqBoth gen =>
-        ensureNoMinIndexable minIndexable
-        let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios
-        let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios
-        if warn &&
-           params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
-           params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then
-          warnRedundantEMatchArg params.ematch declName
-        return { params with extra := params.extra.push thm₁ |>.push thm₂ }
-      | _ =>
-        if kind matches .eqLhs _ | .eqRhs _ then
-          ensureNoMinIndexable minIndexable
-        let thm ← if suggest && !Grind.backward.grind.inferPattern.get (← getOptions) then
-          Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true)
-        else
-          Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
-        if warn && params.ematch.containsWithSamePatterns thm.origin thm.patterns then
-          warnRedundantEMatchArg params.ematch declName
-        return { params with extra := params.extra.push thm }
-    | .defn =>
-      if (← isReducible declName) then
-        throwError "`{.ofConstName declName}` is a reducible definition, `grind` automatically unfolds them"
-      if !kind.isEqLhs && !kind.isDefault then
-        throwError "invalid `grind` parameter, `{.ofConstName declName}` is a definition, the only acceptable (and redundant) modifier is '='"
-      ensureNoMinIndexable minIndexable
-      let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
-        | throwError "failed to generate equation theorems for `{.ofConstName declName}`"
-      return { params with extra := params.extra ++ thms.toPArray' }
-    | _ =>
-      throwError "invalid `grind` parameter, `{.ofConstName declName}` is not a theorem, definition, or inductive type"
+open PremiseSelection in
+def elabGrindParamsAndPremises
+    (params : Grind.Params)
+    (ps : TSyntaxArray ``Parser.Tactic.grindParam)
+    (premises : Array Suggestion := #[])
+    (only : Bool) (lax : Bool := false) : MetaM Grind.Params := do
+  let params ← elabGrindParams params ps (lax := lax) (only := only)
+  elabGrindPremises params premises

 def mkGrindParams
    (config : Grind.Config) (only : Bool) (ps : TSyntaxArray ``Parser.Tactic.grindParam) (mvarId : MVarId) :
@ -246,7 +120,7 @@ def mkGrindParams
    pure suggestions
  else
    pure #[]
-  let params ← elabGrindParams params ps only premises (lax := config.lax)
+  let params ← elabGrindParamsAndPremises params ps premises (only := only) (lax := config.lax)
  trace[grind.debug.inj] "{params.inj.getOrigins.map (·.pp)}"
  return params

--- a/src/Lean/Elab/Tactic/Grind/Param.lean
+++ b/src/Lean/Elab/Tactic/Grind/Param.lean
@ -0,0 +1,172 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Main
+import Lean.Elab.Tactic.Grind.Basic
+import Lean.Elab.Tactic.Grind.Anchor
+namespace Lean.Elab.Tactic
+open Meta
+
+/-!
+`grind` parameter elaboration
+-/
+
+def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name) : MetaM Unit := do
+  let minIndexable := false -- TODO: infer it
+  let kinds ← match s.getKindsFor (.decl declName) with
+    | [] => return ()
+    | [k] => pure m!"@{k.toAttribute minIndexable}"
+    | [.eqLhs gen, .eqRhs _]
+    | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute minIndexable}"
+    | ks =>
+      let ks := ks.map fun k => m!"@{k.toAttribute minIndexable}"
+      pure m!"{ks}"
+  logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`"
+
+def parseModifier (s : String) : CoreM Grind.AttrKind := do
+  let stx := Parser.runParserCategory (← getEnv) `Lean.Parser.Attr.grindMod s
+  match stx with
+  | .ok stx => Grind.getAttrKindCore stx
+  | _ => throwError "unexpected modifier {s}"
+
+def ensureNoMinIndexable (minIndexable : Bool) : MetaM Unit := do
+  if minIndexable then
+    throwError "redundant modifier `!` in `grind` parameter"
+
+public def addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name)
+    (kind : Grind.EMatchTheoremKind)
+    (minIndexable : Bool) (suggest : Bool := false) (warn := true) : MetaM Grind.Params := do
+  let info ← getAsyncConstInfo declName
+  match info.kind with
+  | .thm | .axiom | .ctor =>
+    match kind with
+    | .eqBoth gen =>
+      ensureNoMinIndexable minIndexable
+      let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios
+      let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios
+      if warn &&
+          params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
+          params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then
+        warnRedundantEMatchArg params.ematch declName
+      return { params with extra := params.extra.push thm₁ |>.push thm₂ }
+    | _ =>
+      if kind matches .eqLhs _ | .eqRhs _ then
+        ensureNoMinIndexable minIndexable
+      let thm ← if suggest && !Grind.backward.grind.inferPattern.get (← getOptions) then
+        Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true)
+      else
+        Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
+      if warn && params.ematch.containsWithSamePatterns thm.origin thm.patterns then
+        warnRedundantEMatchArg params.ematch declName
+      return { params with extra := params.extra.push thm }
+  | .defn =>
+    if (← isReducible declName) then
+      throwError "`{.ofConstName declName}` is a reducible definition, `grind` automatically unfolds them"
+    if !kind.isEqLhs && !kind.isDefault then
+      throwError "invalid `grind` parameter, `{.ofConstName declName}` is a definition, the only acceptable (and redundant) modifier is '='"
+    ensureNoMinIndexable minIndexable
+    let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
+      | throwError "failed to generate equation theorems for `{.ofConstName declName}`"
+    return { params with extra := params.extra ++ thms.toPArray' }
+  | _ =>
+    throwError "invalid `grind` parameter, `{.ofConstName declName}` is not a theorem, definition, or inductive type"
+
+def processParam (params : Grind.Params)
+    (p : TSyntax `Lean.Parser.Tactic.grindParam)
+    (mod? : Option (TSyntax `Lean.Parser.Attr.grindMod))
+    (id : TSyntax `ident)
+    (minIndexable : Bool)
+    (only : Bool)
+    : MetaM Grind.Params := do
+  let mut params := params
+  let declName ← try
+    realizeGlobalConstNoOverloadWithInfo id
+  catch err =>
+    if (← resolveLocalName id.getId).isSome then
+      throwErrorAt id "redundant parameter `{id}`, `grind` uses local hypotheses automatically"
+    else
+      throw err
+  let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer
+  match kind with
+  | .ematch .user =>
+    unless only do
+      withRef p <| Grind.throwInvalidUsrModifier
+    ensureNoMinIndexable minIndexable
+    let s ← Grind.getEMatchTheorems
+    let thms := s.find (.decl declName)
+    let thms := thms.filter fun thm => thm.kind == .user
+    if thms.isEmpty then
+      throwErrorAt p "invalid use of `usr` modifier, `{.ofConstName declName}` does not have patterns specified with the command `grind_pattern`"
+    for thm in thms do
+      params := { params with extra := params.extra.push thm }
+  | .ematch kind =>
+    params ← withRef p <| addEMatchTheorem params id declName kind minIndexable
+  | .cases eager =>
+    ensureNoMinIndexable minIndexable
+    withRef p <| Grind.validateCasesAttr declName eager
+    params := { params with casesTypes := params.casesTypes.insert declName eager }
+  | .intro =>
+    if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
+      for ctor in info.ctors do
+        params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
+    else
+      throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
+  | .inj =>
+    let thm ← Grind.mkInjectiveTheorem declName
+    params := { params with inj := params.inj.insert thm }
+  | .ext =>
+    throwError "`[grind ext]` cannot be set using parameters"
+  | .infer =>
+    if let some declName ← Grind.isCasesAttrCandidate? declName false then
+      params := { params with casesTypes := params.casesTypes.insert declName false }
+      if let some info ← isInductivePredicate? declName then
+        -- If it is an inductive predicate,
+        -- we also add the constructors (intro rules) as E-matching rules
+        for ctor in info.ctors do
+          -- **Note**: We should not warn if `declName` is an inductive
+          params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable (warn := False)
+    else
+      params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
+  | .symbol prio =>
+    ensureNoMinIndexable minIndexable
+    params := { params with symPrios := params.symPrios.insert declName prio }
+  return params
+
+def processAnchor (params : Grind.Params) (val : TSyntax `hexnum) : CoreM Grind.Params := do
+  let anchorRefs := params.anchorRefs?.getD #[]
+  let anchorRef ← Grind.elabAnchorRef val
+  return { params with anchorRefs? := some <| anchorRefs.push anchorRef }
+
+public def elabGrindParams (params : Grind.Params) (ps : TSyntaxArray ``Parser.Tactic.grindParam)
+    (only : Bool) (lax : Bool := false) : MetaM Grind.Params := do
+  let mut params := params
+  for p in ps do
+    try
+      match p with
+      | `(Parser.Tactic.grindParam| - $id:ident) =>
+        let declName ← realizeGlobalConstNoOverloadWithInfo id
+        if let some declName ← Grind.isCasesAttrCandidate? declName false then
+          Grind.ensureNotBuiltinCases declName
+          params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) }
+        else if (← Grind.isInjectiveTheorem declName) then
+          params := { params with inj := params.inj.erase (.decl declName) }
+        else
+          params := { params with ematch := (← params.ematch.eraseDecl declName) }
+      | `(Parser.Tactic.grindParam| $[$mod?:grindMod]? $id:ident) =>
+        params ← processParam params p mod? id (minIndexable := false) (only := only)
+      | `(Parser.Tactic.grindParam| ! $[$mod?:grindMod]? $id:ident) =>
+        params ← processParam params p mod? id (minIndexable := true) (only := only)
+      | `(Parser.Tactic.grindParam| #$anchor:hexnum) =>
+        unless only do
+          throwErrorAt anchor "invalid anchor, `only` modifier expected"
+        params ← processAnchor params anchor
+      | _ => throwError "unexpected `grind` parameter{indentD p}"
+    catch ex =>
+      if !lax then throw ex
+  return params
+
+end Lean.Elab.Tactic
--- a/src/Lean/Meta/Tactic/Grind/Anchor.lean
+++ b/src/Lean/Meta/Tactic/Grind/Anchor.lean
@ -86,11 +86,11 @@ public partial def getAnchor (e : Expr) : GrindM UInt64 := do
  return a

 /--
-Example: `isAnchorPrefix 4 0x0c88 0x0c88ab10ef20206a` returns `true`
+Example: `{ numDigits := 4, anchorPrefix := 0x0c88 }.matches 0x0c88ab10ef20206a` returns `true`
 -/
-public def isAnchorPrefix (numHexDigits : Nat) (anchorPrefix : UInt64) (anchor : UInt64) : Bool :=
-  let shift := 64 - numHexDigits.toUInt64*4
-  anchorPrefix == anchor >>> shift
+public def AnchorRef.matches (anchorRef : AnchorRef) (anchor : UInt64) : Bool :=
+  let shift := 64 - anchorRef.numDigits.toUInt64*4
+  anchorRef.anchorPrefix == anchor >>> shift

 public class HasAnchor (α : Type u) where
  getAnchor : α → UInt64
@ -124,12 +124,15 @@ public structure ExprWithAnchor where
 public instance : HasAnchor ExprWithAnchor where
  getAnchor e := e.anchor

-public def mkAnchorSyntaxFromPrefix (numDigits : Nat) (anchorPrefix : UInt64) : CoreM (TSyntax ``Parser.Tactic.Grind.anchor) := do
+public def mkAnchorSyntaxFromPrefix (numDigits : Nat) (anchorPrefix : UInt64) : CoreM (TSyntax ``Parser.Tactic.anchor) := do
  let hexnum := mkNode `hexnum #[mkAtom (anchorPrefixToString numDigits anchorPrefix)]
-  `(Parser.Tactic.Grind.anchor| #$hexnum)
+  `(Parser.Tactic.anchor| #$hexnum)

-public def mkAnchorSyntax (numDigits : Nat) (anchor : UInt64) : CoreM (TSyntax ``Parser.Tactic.Grind.anchor) := do
+public def mkAnchorSyntax (numDigits : Nat) (anchor : UInt64) : CoreM (TSyntax ``Parser.Tactic.anchor) := do
  let anchorPrefix := anchor >>> (64 - 4*numDigits.toUInt64)
  mkAnchorSyntaxFromPrefix numDigits anchorPrefix

+public def SplitInfo.getAnchor (s : SplitInfo) : GrindM UInt64 := do
+  Grind.getAnchor s.getExpr
+
 end Lean.Meta.Grind
--- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean
+++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Propagate
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Anchor
 import Lean.Meta.Tactic.Grind.EqResolution
 import Lean.Meta.Tactic.Grind.SynthInstance
 public section
@ -74,6 +75,15 @@ private def mkEMatchTheoremWithKind'? (origin : Origin) (proof : Expr) (kind : E
 private def isNewPat (patternsFoundSoFar : Array (List Expr)) (thm' : EMatchTheorem) : Bool :=
  patternsFoundSoFar.all fun ps => thm'.patterns != ps

+/--
+Returns `true`, if there are no anchor references restricting the search,
+or there is an anchor references `ref` s.t. `ref` matches `proof`.
+-/
+private def checkAnchorRefs (proof : Expr) : GrindM Bool := do
+  let some anchorRefs ← getAnchorRefs | return true
+  let anchor ← getAnchor (← inferType proof)
+  return anchorRefs.any (·.matches anchor)
+
 private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
  let proof ← mkEqTrueProof e
  let origin ← if let some fvarId := isEqTrueHyp? proof then
@ -82,6 +92,9 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
    let idx ← modifyGet fun s => (s.ematch.nextThmIdx, { s with ematch.nextThmIdx := s.ematch.nextThmIdx + 1 })
    pure <| .local ((`local).appendIndexAfter idx)
  let proof := mkOfEqTrueCore e proof
+  -- **Note**: Do we really need to restrict the instantiation of local theorems?
+  -- **Note**: Should we distinguish anchors restricting case-splits and local theorems?
+  unless (← checkAnchorRefs proof) do return ()
  let size := (← get).ematch.newThms.size
  let gen ← getGeneration e
  let mut patternsFoundSoFar := #[]
--- a/src/Lean/Meta/Tactic/Grind/Main.lean
+++ b/src/Lean/Meta/Tactic/Grind/Main.lean
@ -29,14 +29,15 @@ public section
 namespace Lean.Meta.Grind

 structure Params where
-  config     : Grind.Config
-  ematch     : EMatchTheorems := default
-  inj        : InjectiveTheorems := default
-  symPrios   : SymbolPriorities := {}
-  casesTypes : CasesTypes := {}
-  extra      : PArray EMatchTheorem := {}
-  norm       : Simp.Context
-  normProcs  : Array Simprocs
+  config      : Grind.Config
+  ematch      : EMatchTheorems := default
+  inj         : InjectiveTheorems := default
+  symPrios    : SymbolPriorities := {}
+  casesTypes  : CasesTypes := {}
+  extra       : PArray EMatchTheorem := {}
+  norm        : Simp.Context
+  normProcs   : Array Simprocs
+  anchorRefs? : Option (Array AnchorRef) := none
  -- TODO: inductives to split

 def mkParams (config : Grind.Config) : MetaM Params := do
@ -90,7 +91,8 @@ def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTacti
  let simp := params.norm
  let config := params.config
  let symPrios := params.symPrios
-  x (← mkMethods evalTactic?).toMethodsRef { config, simpMethods, simp, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr, symPrios }
+  let anchorRefs? := params.anchorRefs?
+  x (← mkMethods evalTactic?).toMethodsRef { config, anchorRefs?, simpMethods, simp, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr, symPrios }
    |>.run' { scState }

 private def mkCleanState (mvarId : MVarId) (params : Params) : MetaM Clean.State := mvarId.withContext do
--- a/src/Lean/Meta/Tactic/Grind/Split.lean
+++ b/src/Lean/Meta/Tactic/Grind/Split.lean
@ -167,6 +167,15 @@ private inductive SplitCandidate where
  | none
  | some (c : SplitInfo) (numCases : Nat) (isRec : Bool) (tryPostpone : Bool)

+/--
+Returns `true`, if there are no anchor references restricting the search,
+or there is an anchor references `ref` s.t. `ref` matches `c`.
+-/
+private def checkAnchorRefs (c : SplitInfo) : GrindM Bool := do
+  let some anchorRefs ← getAnchorRefs | return true
+  let anchor ← c.getAnchor
+  return anchorRefs.any (·.matches anchor)
+
 /-- Returns the next case-split to be performed. It uses a very simple heuristic. -/
 private def selectNextSplit? : GoalM SplitCandidate := do
  if (← isInconsistent) then return .none
@ -186,30 +195,38 @@ where
        modify fun s => { s with split.num := numSplits, ematch.num := 0 }
      return c?
    | c::cs =>
-    trace_goal[grind.debug.split] "checking: {c.getExpr}"
-    match (← checkSplitStatus c) with
-    | .notReady => go cs c? (c::cs')
-    | .resolved => go cs c? cs'
-    | .ready numCases isRec tryPostpone =>
-    if (← cheapCasesOnly) && numCases > 1 then
-      go cs c? (c::cs')
-    else match c? with
-    | .none => go cs (.some c numCases isRec tryPostpone) cs'
-    | .some c' numCases' _ tryPostpone' =>
-     let isBetter : GoalM Bool := do
-       if tryPostpone' && !tryPostpone then
-         return true
-       else if tryPostpone && !tryPostpone' then
-         return false
-       else if numCases == 1 && !isRec && numCases' > 1 then
-         return true
-       if (← getGeneration c.getExpr) < (← getGeneration c'.getExpr) then
-         return true
-       return numCases < numCases'
-     if (← isBetter) then
-        go cs (.some c numCases isRec tryPostpone) (c'::cs')
-      else
+    if !(← checkAnchorRefs c) then
+      /-
+      **Note**: `grind`s context contains anchor references restricting the
+      case-splits that can be performed, and `c` does not matches any of
+      the references provided.
+      -/
+      go cs c? cs'
+    else
+      trace_goal[grind.debug.split] "checking: {c.getExpr}"
+      match (← checkSplitStatus c) with
+      | .notReady => go cs c? (c::cs')
+      | .resolved => go cs c? cs'
+      | .ready numCases isRec tryPostpone =>
+      if (← cheapCasesOnly) && numCases > 1 then
        go cs c? (c::cs')
+      else match c? with
+      | .none => go cs (.some c numCases isRec tryPostpone) cs'
+      | .some c' numCases' _ tryPostpone' =>
+      let isBetter : GoalM Bool := do
+        if tryPostpone' && !tryPostpone then
+          return true
+        else if tryPostpone && !tryPostpone' then
+          return false
+        else if numCases == 1 && !isRec && numCases' > 1 then
+          return true
+        if (← getGeneration c.getExpr) < (← getGeneration c'.getExpr) then
+          return true
+        return numCases < numCases'
+      if (← isBetter) then
+          go cs (.some c numCases isRec tryPostpone) (c'::cs')
+        else
+          go cs c? (c::cs')

 private def mkGrindEM (c : Expr) :=
  mkApp (mkConst ``Lean.Grind.em) c
@ -266,7 +283,7 @@ def getSplitCandidateAnchors (filter : Expr → GoalM Bool := fun _ => return tr
  let candidates := (← get).split.candidates
  let candidates ← candidates.toArray.filterMapM fun c => do
    let e := c.getExpr
-    let anchor ← getAnchor e
+    let anchor ← c.getAnchor
    let status ← checkSplitStatus c
    -- **Note**: we ignore case-splits that are not ready or have already been resolved.
    -- We may consider adding an option for including "not-ready" splits in the future.
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@ -57,6 +57,15 @@ register_builtin_option grind.warning : Bool := {
  descr    := "generate a warning whenever `grind` is used"
 }

+/--
+Anchors are used to reference terms, local theorems, and case-splits in the `grind` state.
+We also use anchors to prune the search space when they are provided as `grind` parameters
+and the `finish` tactic.
+-/
+structure AnchorRef where
+  numDigits : Nat
+  anchorPrefix : UInt64
+
 /-- Opaque solver extension state. -/
 opaque SolverExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩
@[expose] def SolverExtensionState : Type := SolverExtensionStateSpec.fst
@ -101,6 +110,11 @@ structure Context where
  simpMethods  : Simp.Methods
  config       : Grind.Config
  /--
+  If `anchorRefs? := some anchorRefs`, then only local instances and case-splits in `anchorRefs`
+  are considered.
+  -/
+  anchorRefs?  : Option (Array AnchorRef)
+  /--
  If `cheapCases` is `true`, `grind` only applies `cases` to types that contain
  at most one minor premise.
  Recall that `grind` applies `cases` when introducing types tagged with `[grind cases eager]`,
@ -298,6 +312,10 @@ def getOrderingEqExpr : GrindM Expr := do
 def getIntExpr : GrindM Expr := do
  return (← readThe Context).intExpr

+/-- Returns the anchor references (if any) being used to restrict the search. -/
+def getAnchorRefs : GrindM (Option (Array AnchorRef)) := do
+  return (← readThe Context).anchorRefs?
+
 def resetAnchors : GrindM Unit := do
  modify fun s => { s with anchors := {} }

@ -1878,6 +1896,12 @@ def anchorPrefixToString (numDigits : Nat) (anchorPrefix : UInt64) : String :=
 def anchorToString (numDigits : Nat) (anchor : UInt64) : String :=
  anchorPrefixToString numDigits (anchor >>> (64 - 4*numDigits.toUInt64))

+def AnchorRef.toString (anchorRef : AnchorRef) : String :=
+  anchorPrefixToString anchorRef.numDigits anchorRef.anchorPrefix
+
+instance : ToString AnchorRef where
+  toString := AnchorRef.toString
+
 /--
 Returns activated `match`-declaration equations.
 Recall that in tactics such as `instantiate only [...]`, `match`-declarations are always instantiated.
--- a/tests/lean/run/grind_finish_trace.lean
+++ b/tests/lean/run/grind_finish_trace.lean
@ -178,3 +178,76 @@ example (f : Int → Int) (x y : Int)
    have : x ≠ 0
    have : x ≠ 1
    have : x ≠ 2
+
+example (f g : Int → Int) (x y z w : Int)
+    : 0 ≤ x → x ≤ 1 → 0 ≤ w →
+      g 0 = z → g 1 = z → g 2 = z →
+      f 0 = y → f 1 = y →
+      g w ≠ z → f x = y := by
+  set_option trace.grind.split true in
+  grind =>
+    mbtc
+    cases #23ad
+    mbtc
+    cases #beb4
+
+/--
+trace: [grind.split] w = 0, generation: 0
+[grind.split] x = 0, generation: 0
+[grind.split] w = 1, generation: 0
+[grind.split] x = 1, generation: 0
+-/
+#guard_msgs in
+example (f g : Int → Int) (x y z w : Int)
+    : 0 ≤ x → x ≤ 1 → 0 ≤ w →
+      g 0 = z → g 1 = z → g 2 = z →
+      f 0 = y → f 1 = y →
+      g w ≠ z → f x = y := by
+  set_option trace.grind.split true in
+  grind
+
+/--
+trace: [grind.split] x = 0, generation: 0
+[grind.split] x = 1, generation: 0
+-/
+#guard_msgs in
+example (f g : Int → Int) (x y z w : Int)
+    : 0 ≤ x → x ≤ 1 → 0 ≤ w →
+      g 0 = z → g 1 = z → g 2 = z →
+      f 0 = y → f 1 = y →
+      g w ≠ z → f x = y := by
+  fail_if_success grind [#23ad] -- not possible to solve using this set of anchors.
+  set_option trace.grind.split true in
+  grind only [#23ad, #beb4] -- Only these two splits were performed.
+
+/--
+trace: [grind.ematch.instance] h: f (f a) = f a
+[grind.ematch.instance] h: f (f (f a)) = f (f a)
+[grind.ematch.instance] h: f (f (f (f a))) = f (f (f a))
+[grind.ematch.instance] h_1: g (g (g b)) = g (g b)
+[grind.ematch.instance] h_1: g (g b) = g b
+-/
+#guard_msgs in
+example (f g : Int → Int)
+    (_ : ∀ x, f (f x) = f x)
+    (_ : ∀ x, g (g x) = g x)
+    (a b : Int)
+    (_ : g (g b) = b)
+    : f (f (f a)) = f a := by
+  set_option trace.grind.ematch.instance true in
+  grind
+
+/--
+trace: [grind.ematch.instance] h: f (f a) = f a
+[grind.ematch.instance] h: f (f (f a)) = f (f a)
+[grind.ematch.instance] h: f (f (f (f a))) = f (f (f a))
+-/
+#guard_msgs in
+example (f g : Int → Int)
+    (_ : ∀ x, f (f x) = f x)
+    (_ : ∀ x, g (g x) = g x)
+    (a b : Int)
+    (_ : g (g b) = b)
+    : f (f (f a)) = f a := by
+  set_option trace.grind.ematch.instance true in
+  grind only [#99cb]