feat: add grind.unusedLemmaThreshold option to report unused E-matching activations (#12805)

This PR adds a `set_option grind.unusedLemmaThreshold` that, when set to
N > 0
and `grind` succeeds, reports E-matching lemmas that were activated at
least N
times but do not appear in the final proof term. This helps identify
`@[grind]`
annotations that fire frequently without contributing to proofs.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Init/Grind/Config.lean

@@ -15,6 +15,9 @@ Passed to `grind` using, for example, the `grind (config := { matchEqs := true }
 structure Config where
   /-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
   trace : Bool := false
+  /-- If `markInstances` is `true`, E-matching proofs are marked with instance IDs
+  for precise tracking of which theorems appear in the final proof. -/
+  markInstances : Bool := false
   /-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
   or for which no patterns can be generated. -/
   lax : Bool := false

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -253,6 +253,9 @@ def grind
     return ()
   mvarId.withContext do
     let params ← mkGrindParams config only ps mvarId
+    let params := if Grind.grind.unusedLemmaThreshold.get (← getOptions) > 0 then
+      { params with config.markInstances := true }
+    else params
     Grind.withProtectedMCtx config mvarId fun mvarId' => do
       let finalize (result : Grind.Result) : TacticM Unit := do
         if result.hasFailed then
@@ -263,7 +266,10 @@ def grind
           Grind.evalGrindTactic seq
           -- **Note**: We are returning only the first goal that could not be solved.
           let goal? := if let goal :: _ := (← get).goals then some goal else none
-          Grind.liftGrindM <| Grind.mkResult params goal?
+          let result ← Grind.liftGrindM <| Grind.mkResult params goal?
+          if goal?.isNone then
+            Grind.liftGrindM <| Grind.checkUnusedActivations mvarId' result.counters
+          return result
         finalize result
       else
         let result ← Grind.main mvarId' params

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

@@ -481,7 +481,7 @@ where
   go (proof prop : Expr) : M Unit := do
     let mut proof := proof
     let mut prop := prop
-    if (← getConfig).trace then
+    if (← getConfig).trace || (← getConfig).markInstances then
       /-
       **Note**: It is incorrect to use `mkFreshId` here because we use `withFreshNGen` at
       `instantiateTheorem`. So, we generate an unique id by using the number of instances generated so far.
@@ -927,7 +927,7 @@ private def ematchCore (extraThms : Array EMatchTheorem) : GoalM InstanceMap :=
 
 /--
 Performs one round of E-matching, and returns `true` if new instances were generated.
-Recall that the mapping is nonempty only if tracing is enabled.
+Recall that the mapping is nonempty only if tracing or instance marking is enabled.
 -/
 def ematch' (extraThms : Array EMatchTheorem := #[]) : GoalM (Bool × InstanceMap) := do
   let numInstances := (← get).ematch.numInstances
@@ -943,6 +943,8 @@ def ematch' (extraThms : Array EMatchTheorem := #[]) : GoalM (Bool × InstanceMa
     and we may have pending facts to process.
     -/
     processNewFacts
+  if (← getConfig).markInstances then
+    modifyThe Grind.State fun s => { s with instanceMap := s.instanceMap.insertMany map.toArray }
   return (progress, map)
 
 /--
@@ -954,7 +956,9 @@ def ematch (extraThms : Array EMatchTheorem := #[]) : GoalM Bool :=
 /-- Performs one round of E-matching using the giving theorems, and returns `true` if new instances were generated. -/
 def ematchOnly (thms : Array EMatchTheorem) : GoalM Bool := do
   let numInstances := (← get).ematch.numInstances
-  go |>.run'
+  let (_, s) ← go |>.run
+  if (← getConfig).markInstances then
+    modifyThe Grind.State fun st => { st with instanceMap := st.instanceMap.insertMany s.instanceMap.toArray }
   return (← get).ematch.numInstances != numInstances
 where
   go : EMatch.M Unit := do profileitM Exception "grind ematch" (← getOptions) do

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

@@ -18,6 +18,8 @@ import Lean.Meta.Tactic.Grind.ForallProp
 import Lean.Meta.Tactic.Grind.CtorIdx
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.Solve
+import Lean.Meta.Tactic.Grind.EMatch
+import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.LawfulEqCmp
@@ -236,6 +238,55 @@ def Result.toMessageData (result : Result) : MetaM MessageData := do
       msgs := msgs ++ [msg]
   return MessageData.joinSep msgs m!"\n"
 
+/--
+Walks the proof term collecting `Origin`s of E-matching instances that appear,
+using the `mdata` markers placed by `markTheoremInstanceProof`.
+-/
+private partial def collectUsedOrigins (e : Expr) (map : EMatch.InstanceMap) : Std.HashSet Origin :=
+  let (_, s) := go e |>.run ({}, {})
+  s.2
+where
+  go (e : Expr) : StateM (Std.HashSet ExprPtr × Std.HashSet Origin) Unit := do
+    if isMarkedSubsingletonApp e then return ()
+    if (← get).1.contains { expr := e } then return ()
+    modify fun (v, o) => (v.insert { expr := e }, o)
+    if let some uniqueId := EMatch.isTheoremInstanceProof? e then
+      if let some thm := map[uniqueId]? then
+        modify fun (v, o) => (v, o.insert thm.origin)
+    match e with
+    | .lam _ d b _
+    | .forallE _ d b _ => go d; go b
+    | .proj _ _ b
+    | .mdata _ b       => go b
+    | .letE _ t v b _  => go t; go v; go b
+    | .app f a         => go f; go a
+    | _ => return ()
+
+/--
+Checks whether any E-matching lemmas were activated but do not appear in the final proof term.
+Controlled by `set_option grind.unusedLemmaThreshold`.
+Uses grind's instance-marking infrastructure for precise tracking.
+-/
+def checkUnusedActivations (mvarId : MVarId) (counters : Counters) : GrindM Unit := do
+  let threshold := grind.unusedLemmaThreshold.get (← getOptions)
+  if threshold == 0 then return ()
+  let proof ← instantiateMVars (mkMVar mvarId)
+  let map := (← get).instanceMap
+  let usedOrigins := collectUsedOrigins proof map
+  let mut unused : Array (Name × Nat) := #[]
+  for (origin, count) in counters.thm do
+    if count < threshold then continue
+    match origin with
+    | .decl declName =>
+      unless usedOrigins.contains origin do
+        unused := unused.push (declName, count)
+    | _ => pure ()
+  unless unused.isEmpty do
+    let sorted := unused.qsort fun (_, c₁) (_, c₂) => c₁ > c₂
+    let data ← sorted.mapM fun (declName, counter) =>
+      return .trace { cls := `thm } m!"{declName} ↦ {counter}" #[]
+    logWarning <| .trace { cls := `grind } "grind: activated but unused E-matching lemmas" data
+
 /--
 When `Config.revert := false`, we preprocess the hypotheses, and add them to the `grind` state.
 It starts at `goal.nextDeclIdx`. If `num?` is `some num`, then at most `num` local declarations are processed.
@@ -300,9 +351,15 @@ def GrindM.runAtGoal (mvarId : MVarId) (params : Params) (k : Goal → GrindM α
   go.run params (evalTactic? := evalTactic?)
 
 def main (mvarId : MVarId) (params : Params) : MetaM Result := do profileitM Exception "grind" (← getOptions) do
+  let params := if grind.unusedLemmaThreshold.get (← getOptions) > 0 then
+    { params with config.markInstances := true }
+  else params
   GrindM.runAtGoal mvarId params fun goal => do
     let failure? ← solve goal
-    mkResult params failure?
+    let result ← mkResult params failure?
+    if failure?.isNone then
+      checkUnusedActivations mvarId result.counters
+    return result
 
 /--
 Resolves delayed metavariable assignments created inside the current `withNewMCtxDepth` block.

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

@@ -78,6 +78,11 @@ register_builtin_option grind.warning : Bool := {
   descr    := "generate a warning whenever `grind` is used"
 }
 
+register_builtin_option grind.unusedLemmaThreshold : Nat := {
+  defValue := 0
+  descr    := "report E-matching lemmas activated at least this many times but not used in the proof (0 = disabled)"
+}
+
 /--
 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
@@ -232,6 +237,9 @@ structure State where
   Cached anchors (aka stable hash codes) for terms in the `grind` state.
   -/
   anchors : PHashMap ExprPtr UInt64 := {}
+  /-- Accumulated E-matching instance map for precise unused lemma tracking.
+  Only populated when `config.markInstances` is `true`. -/
+  instanceMap : Std.HashMap Name EMatchTheorem := {}
 
 instance : Nonempty State :=
   .intro {}

tests/elab/grind_unused_lemmas.lean

@@ -0,0 +1,24 @@
+-- Test that grind.unusedLemmaThreshold reports activated but unused E-matching lemmas
+
+def foo : Nat → Nat
+  | 0 => 1
+  | n + 1 => foo n + 1
+
+@[grind =] theorem foo_zero : foo 0 = 1 := rfl
+@[grind =] theorem foo_succ (n : Nat) : foo (n + 1) = foo n + 1 := rfl
+@[grind =] theorem bar (n : Nat) : foo n + 0 = foo n := Nat.add_zero _
+
+-- `bar` is activated but not used in the proof. With threshold=1, we get a warning.
+/--
+trace: [grind] grind: activated but unused E-matching lemmas
+  [thm] bar ↦ 1
+-/
+#guard_msgs in
+set_option grind.unusedLemmaThreshold 1 in
+example (n : Nat) (h : n = 0) : foo n = 1 := by
+  grind
+
+-- Without the option (threshold=0), no warning.
+#guard_msgs in
+example (n : Nat) (h : n = 0) : foo n = 1 := by
+  grind