From a4b5eecb8eba89f5e94d33647b7ef770d3467f6c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 14 Jul 2025 15:05:02 -0700
Subject: [PATCH] perf: skip unnecessary preprocessing steps  in `grind` when
 possible (#9369)

This PR optimizes the `grind` preprocessor by skipping unnecessary steps
when possible.
---
 .../Meta/Tactic/Grind/MarkNestedSubsingletons.lean |  2 +-
 src/Lean/Meta/Tactic/Grind/Simp.lean               |  1 +
 src/Lean/Meta/Tactic/Grind/Util.lean               | 14 +++++++++++++-
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean b/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean
index 2c3d40c009..3c9844bf44 100644
--- a/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean
+++ b/src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean
@@ -36,7 +36,7 @@ Recall that the congruence closure module has special support for them.
 -/
 -- TODO: consider other subsingletons in the future? We decided to not support them to avoid the overhead of
 -- synthesizing `Subsingleton` instances.
-partial def markNestedSubsingletons (e : Expr) : GrindM Expr := do
+partial def markNestedSubsingletons (e : Expr) : GrindM Expr := do profileitM Exception "grind mark subsingleton" (← getOptions) do
   visit e |>.run' {}
 where
   visit (e : Expr) : M Expr := do
diff --git a/src/Lean/Meta/Tactic/Grind/Simp.lean b/src/Lean/Meta/Tactic/Grind/Simp.lean
index a4690ba256..08fdd2a093 100644
--- a/src/Lean/Meta/Tactic/Grind/Simp.lean
+++ b/src/Lean/Meta/Tactic/Grind/Simp.lean
@@ -40,6 +40,7 @@ Unfolds all `reducible` declarations occurring in `e`.
 Similar to `unfoldReducible`, but uses `inShareCommon` as an extra filter
 -/
 def unfoldReducible' (e : Expr) : GrindM Expr := do
+  if !(← isUnfoldReducibleTarget e) then return e
   let pre (e : Expr) : GrindM TransformStep := do
     if (← inShareCommon e) then return .done e
     let .const declName _ := e.getAppFn | return .continue
diff --git a/src/Lean/Meta/Tactic/Grind/Util.lean b/src/Lean/Meta/Tactic/Grind/Util.lean
index 43934d71a6..fc038be73e 100644
--- a/src/Lean/Meta/Tactic/Grind/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Util.lean
@@ -50,10 +50,20 @@ should not be unfolded by `unfoldReducible`.
 def isGrindGadget (declName : Name) : Bool :=
   declName == ``Grind.EqMatch
 
+def isUnfoldReducibleTarget (e : Expr) : CoreM Bool := do
+  let env ← getEnv
+  return Option.isSome <| e.find? fun e => Id.run do
+    let .const declName _ := e | return false
+    if getReducibilityStatusCore env declName matches .reducible then
+      return !isGrindGadget declName
+    else
+      return false
+
 /--
 Unfolds all `reducible` declarations occurring in `e`.
 -/
-def unfoldReducible (e : Expr) : MetaM Expr :=
+def unfoldReducible (e : Expr) : MetaM Expr := do
+  if !(← isUnfoldReducibleTarget e) then return e
   let pre (e : Expr) : MetaM TransformStep := do
     let .const declName _ := e.getAppFn | return .continue
     unless (← isReducible declName) do return .continue
@@ -116,6 +126,7 @@ Recall that we still have to process `Expr.forallE` because of `ForallProp.lean`
 Moreover, we may not want to reduce `p → q` to `¬p ∨ q` when `(p q : Prop)`.
 -/
 def eraseIrrelevantMData (e : Expr) : CoreM Expr := do
+  if Option.isNone <| e.find? fun e => e.isMData then return e
   let pre (e : Expr) := do
     match e with
     | .letE .. | .lam .. => return .done e
@@ -127,6 +138,7 @@ def eraseIrrelevantMData (e : Expr) : CoreM Expr := do
 Converts nested `Expr.proj`s into projection applications if possible.
 -/
 def foldProjs (e : Expr) : MetaM Expr := do
+  if Option.isNone <| e.find? fun e => e.isProj then return e
   let post (e : Expr) := do
     let .proj structName idx s := e | return .done e
     let some info := getStructureInfo? (← getEnv) structName |