feat: restrinct local theorem instantiation using anchors.

Author: leodemoura

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 := #[]

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -1896,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.

tests/lean/run/grind_finish_trace.lean

@@ -219,3 +219,35 @@ example (f g : Int → Int) (x y z w : Int)
   fail_if_success grind [#23ad] -- not possible to solve using this set of anchors.
   set_option trace.grind.split true in
   grind [#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 [#99cb]