From 82d90b4cdcd3e5c9a57e0764e6b0ff57fe505e73 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Tue, 10 Feb 2026 10:49:19 +0000
Subject: [PATCH] fix: force unfolding of the Decidable instace in
 Decidable.rec (#12399)

This PR adds a custom simproc to handle `Decidable.rec`, where we force
the rewrite in the argument of the `Decidable` type, that normally is
not rewritten due to being a subsingleton.

Closes #12386
---
 src/Lean/Meta/Tactic/Cbv/ControlFlow.lean |  3 +++
 tests/lean/run/12386.lean                 | 29 +++++++++++++++++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 tests/lean/run/12386.lean

diff --git a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
index f1f7d29b2f..be62f67ce7 100644
--- a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
+++ b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
@@ -183,6 +183,9 @@ public def simpControlCbv : Simproc := fun e => do
     simpCond e
   else if declName == ``dite then
     simpDIteCbv e
+  else if declName == ``Decidable.rec then
+    -- We force the rewrite in the last argument, so that we can unfold the `Decidable` instance.
+    (simpInterlaced · #[false,false,true,true,true]) >> reduceRecMatcher <| e
   else
     tryMatcher e
 
diff --git a/tests/lean/run/12386.lean b/tests/lean/run/12386.lean
new file mode 100644
index 0000000000..7e5258e8ef
--- /dev/null
+++ b/tests/lean/run/12386.lean
@@ -0,0 +1,29 @@
+set_option cbv.warning false
+
+def minFacAux (n : Nat) : Nat → Nat
+  | k =>
+    if h : n < k * k then n
+    else
+      if h' : k ∣ n then k
+      else
+        have : k ≤ n := by have := Nat.le_mul_self k; omega
+        minFacAux n (k + 2)
+termination_by k => n + 2 - k
+
+def Nat.minFac (n : Nat) : Nat :=
+  if 2 ∣ n then 2 else minFacAux n 3
+
+def Nat.log (b n : Nat) : Nat :=
+  if b ≤ 1 then 0 else (go b n).2 where
+  go : Nat → Nat → Nat × Nat
+  | _, 0 => (n, 0)
+  | b, fuel + 1 =>
+    if n < b then
+      (n, 0)
+    else
+      let (q, e) := go (b * b) fuel
+      if q < b then (q, 2 * e) else (q / b, 2 * e + 1)
+
+theorem test : ¬∃ k, k ≤ Nat.log 2 15 ∧ 0 < k ∧ 15 = Nat.minFac 15 ^ k := by
+  apply of_decide_eq_true
+  conv => lhs; cbv