From 78c9a01bb265cdddb5d187a02ba2200479b3f97c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 3 Jan 2026 20:27:46 -0800
Subject: [PATCH] feat: check `Sym.simp` thresholds (#11890)

This PR ensures that `Sym.simp` checks thresholds for maximum recursion
depth and maximum number of steps. It also invokes `checkSystem`.
Additionally, this PR simplifies the main loop. Assigned metavariables
and `zetaDelta` reduction are now handled by installing `pre`/`post`
methods.
---
 src/Lean/Meta/Sym/Simp/DiscrTree.lean |  2 +-
 src/Lean/Meta/Sym/Simp/Main.lean      | 21 ++++++++-------------
 src/Lean/Meta/Sym/Simp/SimpM.lean     |  2 --
 tests/bench/sym/simp_1.lean           |  2 ++
 4 files changed, 11 insertions(+), 16 deletions(-)

diff --git a/src/Lean/Meta/Sym/Simp/DiscrTree.lean b/src/Lean/Meta/Sym/Simp/DiscrTree.lean
index 5ca55fbc10..2c162285af 100644
--- a/src/Lean/Meta/Sym/Simp/DiscrTree.lean
+++ b/src/Lean/Meta/Sym/Simp/DiscrTree.lean
@@ -130,7 +130,7 @@ def getKey (e : Expr) : Key :=
   | .lit v            => .lit v
   | .const declName _ => .const declName e.getAppNumArgs
   | .fvar fvarId      => .fvar fvarId e.getAppNumArgs
-  | .forallE _ _ _ _  => .arrow
+  | .forallE ..       => .arrow
   | _ => .other
 
 /-- Push `e` arguments/children into the `todo` stack.  -/
diff --git a/src/Lean/Meta/Sym/Simp/Main.lean b/src/Lean/Meta/Sym/Simp/Main.lean
index 60f1788e83..11ed515129 100644
--- a/src/Lean/Meta/Sym/Simp/Main.lean
+++ b/src/Lean/Meta/Sym/Simp/Main.lean
@@ -25,20 +25,12 @@ def simpLet (_ : Expr) : SimpM Result := do
   -- **TODO**
   return .rfl
 
-def simpFVar (_ : Expr) : SimpM Result := do
-  -- **TODO**
-  return .rfl
-
-def simpMVar (_ : Expr) : SimpM Result := do
-  -- **TODO**
-  return .rfl
-
 def simpApp (e : Expr) : SimpM Result := do
   congrArgs e
 
 def simpStep : Simproc := fun e => do
   match e with
-  | .lit _ | .sort _ | .bvar _ | .const .. => return .rfl
+  | .lit _ | .sort _ | .bvar _ | .const .. | .fvar _  | .mvar _ => return .rfl
   | .proj .. =>
     reportIssue! "unexpected kernel projection term during simplification{indentExpr e}\npre-process and fold them as projection applications"
     return .rfl
@@ -50,8 +42,6 @@ def simpStep : Simproc := fun e => do
   | .lam .. => simpLambda e
   | .forallE .. => simpForall e
   | .letE .. => simpLet e
-  | .fvar .. => simpFVar e
-  | .mvar .. => simpMVar e
   | .app .. => simpApp e
 
 abbrev cacheResult (e : Expr) (r : Result) : SimpM Result := do
@@ -59,11 +49,16 @@ abbrev cacheResult (e : Expr) (r : Result) : SimpM Result := do
   return r
 
 @[export lean_sym_simp]
-def simpImpl (e₁ : Expr) : SimpM Result := do
-  if (← get).numSteps >= (← getConfig).maxSteps then
+def simpImpl (e₁ : Expr) : SimpM Result := withIncRecDepth do
+  let numSteps := (← get).numSteps
+  if numSteps >= (← getConfig).maxSteps then
     throwError "`simp` failed: maximum number of steps exceeded"
   if let some result := (← getCache).find? { expr := e₁ } then
     return result
+  let numSteps := numSteps + 1
+  if numSteps % 1000 == 0 then
+    checkSystem "simp"
+  modify fun s => { s with numSteps }
   match (← pre e₁) with
   | .step e₂ h₁ => cacheResult e₁ (← mkEqTransResult e₁ e₂ h₁ (← simp e₂))
   | .rfl =>
diff --git a/src/Lean/Meta/Sym/Simp/SimpM.lean b/src/Lean/Meta/Sym/Simp/SimpM.lean
index 76911557ab..cca7d355b8 100644
--- a/src/Lean/Meta/Sym/Simp/SimpM.lean
+++ b/src/Lean/Meta/Sym/Simp/SimpM.lean
@@ -100,8 +100,6 @@ invalidating the cache and causing O(2^n) behavior on conditional trees.
 
 /-- Configuration options for the structural simplifier. -/
 structure Config where
-  /-- If `true`, unfold let-bindings (zeta reduction) during simplification. -/
-  zetaDelta : Bool := true
   /-- Maximum number of steps that can be performed by the simplifier. -/
   maxSteps : Nat := 0
   -- **TODO**: many are still missing
diff --git a/tests/bench/sym/simp_1.lean b/tests/bench/sym/simp_1.lean
index b803e6fcc0..8293c148e6 100644
--- a/tests/bench/sym/simp_1.lean
+++ b/tests/bench/sym/simp_1.lean
@@ -101,6 +101,8 @@ def benchManyRewrites (n : Nat) : MetaM Unit := do
   let proofSize ← getProofSize r
   IO.println s!"many_rewrites_{n}: {timeMs}ms, proof_size={proofSize}"
 
+set_option maxRecDepth 100000
+
 /-! ## Run all benchmarks -/
 def runAllBenchmarks : MetaM Unit := do
   IO.println "=== Simplifier Stress Tests ==="