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

@@ -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
 

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