From 9bfd16ef5ec2d6dda537063b85f886d7ad279fe2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Wed, 11 Feb 2026 11:47:18 +0000
Subject: [PATCH] refactor: main loop of the `cbv` tactic (#12417)

This PR refactors the main loop of the `cbv` tactic. Rather than using
multiple simprocs, a central pre simproc is introduced. Moreover, let
expressions are no longer immediately zeta-reduced due to performance on
one of the benchmarks (`leroy.lean`).

Stacked on top of #12416
---
 src/Lean/Meta/Tactic/Cbv/ControlFlow.lean |  4 +-
 src/Lean/Meta/Tactic/Cbv/Main.lean        | 70 +++++++++++------------
 tests/bench/cbv/leroy.lean                |  3 +-
 3 files changed, 38 insertions(+), 39 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
index be62f67ce7..716215e301 100644
--- a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
+++ b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
@@ -174,8 +174,10 @@ def tryMatcher : Simproc := fun e => do
       <|> reduceRecMatcher
         <| e
 
+/-
+  Precondition: `e` is an application
+-/
 public def simpControlCbv : Simproc := fun e => do
-  if !e.isApp then return .rfl
   let .const declName _ := e.getAppFn | return .rfl
   if declName == ``ite then
     simpIteCbv e
diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index 56d538ba69..e80da0abe9 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@@ -24,9 +24,6 @@ public register_builtin_option cbv.warning : Bool := {
   descr    := "disable `cbv` usage warning"
 }
 
-def skipBinders : Simproc := fun e => do
-  return .rfl (e.isLambda || e.isForall)
-
 def tryMatchEquations (appFn : Name) : Simproc := fun e => do
   let thms ← getMatchTheorems appFn
   thms.rewrite (d := dischargeNone) e
@@ -57,8 +54,11 @@ def tryMatcher : Simproc := fun e => do
       <|> reduceRecMatcher
         <| e
 
-def handleConstApp : Simproc :=
-  tryEquations <|> tryUnfold
+def handleConstApp : Simproc := fun e => do
+  if (← isCbvOpaque e.getAppFn.constName!) then
+    return .rfl (done := true)
+  else
+    tryEquations <|> tryUnfold <| e
 
 def betaReduce : Simproc := fun e => do
   -- TODO: Improve term sharing
@@ -81,17 +81,6 @@ def handleApp : Simproc := fun e => do
   | .lam .. => betaReduce e
   | _ => return .rfl
 
-def isOpaqueApp : Simproc := fun e => do
-  let some fnName := e.getAppFn.constName? | return .rfl
-  let hasTheorems := (← getCbvEvalLemmas fnName).isSome
-  if hasTheorems then
-    let res ← (simpAppArgs >> tryCbvTheorems) e
-    match res with
-    | .rfl false => return .rfl
-    | _ => return res
-  else
-    return .rfl (← isCbvOpaque fnName)
-
 def isOpaqueConst : Simproc := fun e => do
   let .const constName _ := e | return .rfl
   let hasTheorems := (← getCbvEvalLemmas constName).isSome
@@ -139,17 +128,18 @@ def handleProj : Simproc := fun e => do
 def simplifyAppFn : Simproc := fun e => do
     unless e.isApp do return .rfl
     let fn := e.getAppFn
-    unless fn.isLambda || fn.isConst do
-      let res ← simp fn
-      match res with
-      | .rfl _ => return res
-      | .step e' proof _ =>
-        let newType ← Sym.inferType e'
-        let congrArgFun := Lean.mkLambda `x .default newType (mkAppN (.bvar 0) e.getAppArgs)
-        let newValue ← mkAppNS e' e.getAppArgs
-        let newProof ← mkCongrArg congrArgFun proof
-        return .step newValue newProof
-    return .rfl
+    if fn.isLambda || fn.isConst then
+      return .rfl
+    else
+    let res ← simp fn
+    match (← simp fn) with
+    | .rfl _ => return res
+    | .step e' proof _ =>
+      let newType ← Sym.inferType e'
+      let congrArgFun := Lean.mkLambda `x .default newType (mkAppN (.bvar 0) e.getAppArgs)
+      let newValue ← mkAppNS e' e.getAppArgs
+      let newProof ← mkCongrArg congrArgFun proof
+      return .step newValue newProof
 
 def handleConst : Simproc := fun e => do
   let .const n _ := e | return .rfl
@@ -163,16 +153,24 @@ def handleConst : Simproc := fun e => do
   let some thm ← getUnfoldTheorem n | return .rfl
   Theorem.rewrite thm e
 
-def cbvPre : Simproc :=
-      isBuiltinValue <|> isProofTerm <|> skipBinders
-  >>  isOpaqueApp
-  >>  simpControlCbv
-    <|> ((isOpaqueConst >> handleConst) <|> simplifyAppFn <|> handleProj) <|> zetaReduce
+def cbvPreStep : Simproc := fun e => do
+  match e with
+  | .lit .. => foldLit e
+  | .proj .. => handleProj e
+  | .const .. => isOpaqueConst >> handleConst <| e
+  | .app .. => simpControlCbv <|> simplifyAppFn <| e
+  | .letE .. =>
+    if e.letNondep! then
+      let betaAppResult ← toBetaApp e
+      return .step (betaAppResult.e) (betaAppResult.h)
+    else
+      zetaReduce e
+  | .forallE .. | .lam .. | .fvar .. | .mvar .. | .bvar .. | .sort .. => return .rfl (done := true)
+  | _ => return .rfl
 
-def cbvPost : Simproc :=
-      evalGround
-  >>  (handleApp <|> zetaReduce)
-  >>  foldLit
+def cbvPre : Simproc := isBuiltinValue <|> isProofTerm <|> cbvPreStep
+
+def cbvPost : Simproc := evalGround <|> handleApp
 
 public def cbvEntry (e : Expr) : MetaM Result := do
   trace[Meta.Tactic.cbv] "Called cbv tactic to simplify {e}"
diff --git a/tests/bench/cbv/leroy.lean b/tests/bench/cbv/leroy.lean
index 06999ec3a5..4470bf1c40 100644
--- a/tests/bench/cbv/leroy.lean
+++ b/tests/bench/cbv/leroy.lean
@@ -176,7 +176,7 @@ def runSingleDecideTest (n : Nat) : MetaM Unit := do
   Meta.checkWithKernel goalMVar
   let endTime ← IO.monoNanosNow
   let kernelMs := (endTime - startTime).toFloat / 1000000.0
-  IO.println s!"native_decide: goal_{n}: {ms} ms, kernel: {kernelMs} ms"
+  IO.println s!"decide: goal_{n}: {ms} ms, kernel: {kernelMs} ms"
 
 set_option maxRecDepth 400000
 set_option maxHeartbeats 400000
@@ -192,5 +192,4 @@ def runDecideTests : MetaM Unit := do
   for n in [10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 150, 200, 250, 300, 350, 400, 450, 500, 600, 700, 800, 900, 1000] do
     runSingleDecideTest n
 
-
 #eval runCbvTests