From f3b8f76ec4515495cda311a619e231a70ea36c08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Fri, 13 Feb 2026 13:25:35 +0000
Subject: [PATCH] test: add `cbv` benchmark for evaluating `Decidable.decide`
 (#12467)

This PR adds a benchmark for `cbv` tactic for evaluating
`Decidable.decide` for a `Decidable` instance for a problem of checking
if a number is not a prime power.

The test has been inspired by a recent discussion on the [leanprover
zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Can't.20decide.20if.2015.20is.20a.20prime.20power/with/572513330).
---
 tests/bench/cbv/decide.lean              | 41 ++++++++++++++++++++++++
 tests/bench/speedcenter.exec.velcom.yaml |  6 ++++
 2 files changed, 47 insertions(+)
 create mode 100644 tests/bench/cbv/decide.lean

diff --git a/tests/bench/cbv/decide.lean b/tests/bench/cbv/decide.lean
new file mode 100644
index 0000000000..89efa7675b
--- /dev/null
+++ b/tests/bench/cbv/decide.lean
@@ -0,0 +1,41 @@
+import Lean
+open Lean
+
+abbrev Nat.Prime (p : Nat) : Prop :=
+  2 ≤ p ∧ ∀ (m : Nat), m < p → 2 ≤ m → ¬m ∣ p
+
+abbrev IsPrimePow (n : Nat) : Prop :=
+  ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
+
+def mkProblemInst (n : Nat) : Expr :=
+  let n := mkNatLit n
+  let f := mkApp (mkConst ``IsPrimePow) n
+  mkApp (mkConst ``Not) f
+
+def runSingleTest (n : Nat) : MetaM Unit := do
+  let toFeed := mkProblemInst n
+  let startTime ← IO.monoNanosNow
+  let mvar ← Meta.mkFreshExprMVar toFeed
+  let mvar := mvar.mvarId!
+  let [mvar] ← mvar.applyConst ``of_decide_eq_true | throwError "Could not apply `of_decide_eq_true`"
+  let executed ← Lean.Meta.Tactic.Cbv.cbvGoal mvar
+  if (executed.isSome) then
+    throwError "Did not fully reduce"
+  let endTime ← IO.monoNanosNow
+  let ms := (endTime - startTime).toFloat / 1000000.0
+  let executed ← instantiateMVars (.mvar mvar)
+  let startTime ← IO.monoNanosNow
+  Meta.checkWithKernel executed
+  let endTime ← IO.monoNanosNow
+  let kernelMs := (endTime - startTime).toFloat / 1000000.0
+  IO.println s!"cbv: goal_{n}: {ms} ms, kernel: {kernelMs} ms"
+
+set_option maxHeartbeats 400000
+
+def runCbvTests : MetaM Unit := do
+  IO.println "=== Call-By-Value Tactic Tests ==="
+  IO.println ""
+  for n in [6,10,12,14,15,18,20] do
+    runSingleTest n
+
+#eval runCbvTests
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 197b1eadcc..734f3de270 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -683,3 +683,9 @@
   run_config:
     <<: *time
     cmd: lean ./cbv/dedup.lean
+- attributes:
+    description: cbv tactic (evaluating Decidable.decide)
+    tags: [other]
+  run_config:
+    <<: *time
+    cmd: lean ./cbv/decide.lean