fix: cbv handling of ite/dite/decide (#12816)

This PR solves three distinct issues with the handling of `ite`/`dite`,`decide`. 1) We prevent the simprocs from picking up `noncomputable`, `Classical` instances, such as `Classical.propDecidable`, when simplifying the proposition in `ite`/`dite`/`decide`. 2) We fix a type mismatch occurring when the condition/proposition is unchanged but the `Decidable` instance is simplified. 3) If we rewrite the proposition from `c` to `c'` and the evaluation of the original instance `Decidable c` gets stuck we try fallback path of of obtaining `Decidable c'` instance and evaluating it. This matters when the instance is evaluated via `cbv_eval` lemmas. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-17 10:24:07 +00:00 · 2026-03-06 16:18:39 +00:00
parent 68ea28c24f
commit 54f188160c
4 changed files with 180 additions and 40 deletions
--- a/src/Init/Sym/Lemmas.lean
+++ b/src/Init/Sym/Lemmas.lean
@@ -33,15 +33,27 @@ theorem ite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α)
 theorem ite_true {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) {ht : c} : @ite α c inst a b = a := by
  simp [*]

+theorem ite_true_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) (c' : Prop) (h : c = c') {ht : c'} : @ite α c inst a b = a := by
+  simp [*]
+
 theorem ite_false {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) {ht : ¬ c} : @ite α c inst a b = b := by
  simp [*]

+theorem ite_false_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) (c' : Prop) (h : c = c') {ht : ¬ c'} : @ite α c inst a b = b := by
+  simp [*]
+
 theorem dite_true {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α) {ht : c} : @dite α c inst a b = a ht := by
  simp [*]

+theorem dite_true_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α) (c' : Prop) (h : c = c') {ht : c'} : @dite α c inst a b = a (h.mpr_prop ht) := by
+  subst h; simp [*]
+
 theorem dite_false {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α) {ht : ¬ c} : @dite α c inst a b = b ht := by
  simp [*]

+theorem dite_false_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α) (c' : Prop) (h : c = c') {ht : ¬ c'} : @dite α c inst a b = b (h.mpr_not ht) := by
+  subst h; simp [*]
+
 theorem dite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α)
    (c' : Prop) {inst' : Decidable c'} (h : c = c')
    : @dite α c inst a b = @dite α c' inst' (fun h' => a (h.mpr_prop h')) (fun h' => b (h.mpr_not h')) := by
--- a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
+++ b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
@@ -19,6 +19,8 @@ import Lean.Meta.AppBuilder
 import Init.Sym.Lemmas
 import Lean.Meta.Tactic.Cbv.TheoremsLookup
 import Lean.Meta.Tactic.Cbv.Opaque
+import Lean.Meta.Tactic.Cbv.CbvEvalExt
+import Lean.Compiler.NoncomputableAttr

 /-!
 # Control Flow Handling for Cbv
@@ -35,20 +37,47 @@ corresponding branch.
 namespace Lean.Meta.Sym.Simp
 open Internal

+def isCbvNoncomputable (p : Name) : CoreM Bool := do
+  let evalLemmas ← Tactic.Cbv.getCbvEvalLemmas p
+  return evalLemmas.isNone && Lean.isNoncomputable (← getEnv) p
+
+/--
+Attemps to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance
+-/
+def trySynthComputableInstance (p : Expr) : SymM <| Option Expr := do
+  let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) p) | return .none
+  if (← inst'.getUsedConstants.anyM (isCbvNoncomputable ·)) then return .none
+  shareCommon inst'
+
 /-- Reduce `ite` by matching the `Decidable` instance for `isTrue`/`isFalse`. -/
-def simpIteDecidable (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
-  match_expr inst with
+def matchIteDecidable (f α c inst a b instToMatch : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match_expr instToMatch with
  | Decidable.isTrue _ hp =>
    return .step a <| mkApp6 (mkConst ``Sym.ite_true f.constLevels!) α c inst a b hp
  | Decidable.isFalse _ hnp =>
    return .step b <| mkApp6 (mkConst ``Sym.ite_false f.constLevels!) α c inst a b hnp
  | _ => fallback

+/-- Like `matchIteDecidable`, but for the congruence case where `c` was simplified to `c'` with proof `h`. -/
+def matchIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match_expr inst' with
+  | Decidable.isTrue _ hp =>
+    return .step a <| mkApp8 (mkConst ``Sym.ite_true_congr f.constLevels!) α c inst a b c' h hp
+  | Decidable.isFalse _ hnp =>
+    return .step b <| mkApp8 (mkConst ``Sym.ite_false_congr f.constLevels!) α c inst a b c' h hnp
+  | _ => fallback
+
 /-- Simplify the `Decidable` instance, then try `simpIteDecidable`. -/
-def simpIteDecidableWithFallback (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
+def simpAndMatchIteDecidable (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
  match (← simp inst) with
-  | .rfl _ => simpIteDecidable f α c inst a b fallback
-  | .step inst' _ _ => simpIteDecidable f α c inst' a b fallback
+  | .rfl _ => matchIteDecidable f α c inst a b inst fallback
+  | .step inst' _ _ => matchIteDecidable f α c inst a b inst' fallback
+
+/-- Like `simpAndMatchIteDecidable`, but for the congruence case where `c` was simplified to `c'`. -/
+def simpAndMatchIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match (← simp inst') with
+  | .rfl _ => matchIteDecidableCongr f α c inst a b c' h inst' fallback
+  | .step inst'' _ _ => matchIteDecidableCongr f α c inst a b c' h inst'' fallback

 /-- Like `simpIte` but also evaluates `Decidable.decide` when the condition does not
 reduce to `True`/`False` directly. -/
@@ -64,23 +93,27 @@ public def simpIteCbv : Simproc := fun e => do
      else if (← isFalseExpr c) then
        return .step b <| mkApp3 (mkConst ``ite_false f.constLevels!) α a b
      else
-        simpIteDecidableWithFallback f α c inst a b <| return .rfl (done := true)
+        simpAndMatchIteDecidable f α c inst a b do return .rfl (done := true)
    | .step c' h _ =>
      if (← isTrueExpr c') then
        return .step a <| mkApp (e.replaceFn ``ite_cond_eq_true) h
      else if (← isFalseExpr c') then
        return .step b <| mkApp (e.replaceFn ``ite_cond_eq_false) h
      else
-        simpIteDecidableWithFallback f α c inst a b <| do
+        -- If we got stuck with simplifying `p` then let's try evaluating the original isntance
+        simpAndMatchIteDecidable f α c inst a b do
+          -- If we get stuck here, maybe the problem is that we need to look at `Decidable c'`
          let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h
-          let e' := e.getBoundedAppFn 4
-          let e' ← mkAppS₄ e' c' inst' a b
-          let h' := mkApp3 (e.replaceFn ``Sym.ite_cond_congr) c' inst' h
-          return .step e' h' (done := true)
+          simpAndMatchIteDecidableCongr f α c inst a b c' h inst' do
+            -- If we fail, then we just rewrite `c` to `c'`
+            let e' := e.getBoundedAppFn 4
+            let e' ← mkAppS₄ e' c' inst' a b
+            let h' := mkApp3 (e.replaceFn ``Sym.ite_cond_congr) c' inst' h
+            return .step e' h' (done := true)

 /-- Reduce `dite` by matching the `Decidable` instance for `isTrue`/`isFalse`. -/
-def simpDIteDecidable (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
-  match_expr inst with
+def matchDIteDecidable (f α c inst a b instToMatch : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match_expr instToMatch with
  | Decidable.isTrue _ hp =>
    let a' ← share <| a.betaRev #[hp]
    return .step a' <| mkApp6 (mkConst ``Sym.dite_true f.constLevels!) α c inst a b hp
@@ -89,11 +122,30 @@ def simpDIteDecidable (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM
    return .step b' <| mkApp6 (mkConst ``Sym.dite_false f.constLevels!) α c inst a b hnp
  | _ => fallback

+/-- Like `matchDIteDecidable`, but for the congruence case where `c` was simplified to `c'` with proof `h`. -/
+def matchDIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match_expr inst' with
+  | Decidable.isTrue _ hp =>
+    let hp' := mkApp4 (mkConst ``Eq.mpr_prop) c c' h hp
+    let a' ← share <| a.betaRev #[hp']
+    return .step a' <| mkApp8 (mkConst ``Sym.dite_true_congr f.constLevels!) α c inst a b c' h hp
+  | Decidable.isFalse _ hnp =>
+    let hnp' := mkApp4 (mkConst ``Eq.mpr_not) c c' h hnp
+    let b' ← share <| b.betaRev #[hnp']
+    return .step b' <| mkApp8 (mkConst ``Sym.dite_false_congr f.constLevels!) α c inst a b c' h hnp
+  | _ => fallback
+
 /-- Simplify the `Decidable` instance, then try `simpDIteDecidable`. -/
-def simpDIteDecidableWithFallback (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
+def simpAndMatchDIteDecidable (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
  match (← simp inst) with
-  | .rfl _ => simpDIteDecidable f α c inst a b fallback
-  | .step inst' _ _ => simpDIteDecidable f α c inst' a b fallback
+  | .rfl _ => matchDIteDecidable f α c inst a b inst fallback
+  | .step inst' _ _ => matchDIteDecidable f α c inst a b inst' fallback
+
+/-- Like `simpAndMatchDIteDecidable`, but for the congruence case where `c` was simplified to `c'`. -/
+def simpAndMatchDIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match (← simp inst') with
+  | .rfl _ => matchDIteDecidableCongr f α c inst a b c' h inst' fallback
+  | .step inst'' _ _ => matchDIteDecidableCongr f α c inst a b c' h inst'' fallback

 /-- Like `simpDIte` but also evaluates `Decidable.decide` when the condition does not
 reduce to `True`/`False` directly. -/
@@ -111,7 +163,7 @@ public def simpDIteCbv : Simproc := fun e => do
        let b' ← share <| b.betaRev #[mkConst ``not_false]
        return .step b' <| mkApp3 (mkConst ``dite_false f.constLevels!) α a b
      else
-        simpDIteDecidableWithFallback f α c inst a b <| return .rfl (done := true)
+        simpAndMatchDIteDecidable f α c inst a b do return .rfl (done := true)
    | .step c' h _ =>
      if (← isTrueExpr c') then
        let h' ← shareCommon <| mkOfEqTrueCore c h
@@ -122,15 +174,18 @@ public def simpDIteCbv : Simproc := fun e => do
        let b ← share <| b.betaRev #[h']
        return .step b <| mkApp (e.replaceFn ``dite_cond_eq_false) h
      else
-        simpDIteDecidableWithFallback f α c inst a b <| do
+        -- If we get stuck after simplifying `p` to `p'`, then we try to evaluate the original instance 
+        simpAndMatchDIteDecidable f α c inst a b do
+          -- Otherwise, we make `Decidable c'` instance and try to evaluate it instead
          let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h
-          let e' := e.getBoundedAppFn 4
-          let h ← shareCommon h
-          let a ← share <| mkLambda `h .default c' (a.betaRev #[mkApp4 (mkConst ``Eq.mpr_prop) c c' h (mkBVar 0)])
-          let b ← share <| mkLambda `h .default (mkNot c') (b.betaRev #[mkApp4 (mkConst ``Eq.mpr_not) c c' h (mkBVar 0)])
-          let e' ← mkAppS₄ e' c' inst' a b
-          let h' := mkApp3 (e.replaceFn ``Sym.dite_cond_congr) c' inst' h
-          return .step e' h' (done := true)
+          simpAndMatchDIteDecidableCongr f α c inst a b c' h inst' do
+            let e' := e.getBoundedAppFn 4
+            let h ← shareCommon h
+            let a ← share <| mkLambda `h .default c' (a.betaRev #[mkApp4 (mkConst ``Eq.mpr_prop) c c' h (mkBVar 0)])
+            let b ← share <| mkLambda `h .default (mkNot c') (b.betaRev #[mkApp4 (mkConst ``Eq.mpr_not) c c' h (mkBVar 0)])
+            let e' ← mkAppS₄ e' c' inst' a b
+            let h' := mkApp3 (e.replaceFn ``Sym.dite_cond_congr) c' inst' h
+            return .step e' h' (done := true)

 /-- Short-circuit evaluation of `Or`. Simplifies only the left argument;
 if it reduces to `True`, returns `True` immediately without evaluating the right side. -/
@@ -173,16 +228,16 @@ public def simpAnd : Simproc := fun e => do
      return .rfl

 /-- Reduce `decide` by matching the `Decidable` instance for `isTrue`/`isFalse`. -/
-def simpDecideByInst (p inst : Expr) : SimpM Result := do
-  match_expr inst with
+def matchDecideDecidable (p inst instToMatch : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match_expr instToMatch with
  | Decidable.isTrue _ hp =>
    return .step (← getBoolTrueExpr) <| mkApp3 (mkConst ``Sym.decide_isTrue) p inst hp
  | Decidable.isFalse _ hnp =>
    return .step (← getBoolFalseExpr) <| mkApp3 (mkConst ``Sym.decide_isFalse) p inst hnp
-  | _ => return .rfl (done := true)
+  | _ => fallback

 /-- Like `simpDecideByInst`, but for the case where `p` was simplified to `p'` with proof `h`. -/
-def simpDecideByInstCongr (p p' h inst inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+def matchDecideDecidableCongr (p p' h inst inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
  match_expr inst' with
  | Decidable.isTrue _ hp =>
    return .step (← getBoolTrueExpr) <| mkApp5 (mkConst ``Sym.decide_isTrue_congr) p p' h inst hp
@@ -191,16 +246,16 @@ def simpDecideByInstCongr (p p' h inst inst' : Expr) (fallback : SimpM Result) :
  | _ => fallback

 /-- Simplify the `Decidable` instance, then try `simpDecideByInst`. -/
-def simpDecideByInstWithFallback (p inst : Expr) : SimpM Result := do
+def simpAndMatchDecideDecidable (p inst : Expr) (fallback : SimpM Result) : SimpM Result := do
  match (← simp inst) with
-  | .rfl _ => simpDecideByInst p inst
-  | .step inst' _ _ => simpDecideByInst p inst'
+  | .rfl _ => matchDecideDecidable p inst inst fallback
+  | .step inst' _ _ => matchDecideDecidable p inst inst' fallback

 /-- Like `simpDecideByInstWithFallback`, but for the case where `p` was simplified to `p'`. -/
-def simpDecideByInstWithFallbackCongr (p p' h inst inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+def simpAndMatchDecideDecidableCongr (p p' h inst inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
  match (← simp inst') with
-  | .rfl _ => simpDecideByInstCongr p p' h inst inst' fallback
-  | .step inst'' _ _ => simpDecideByInstCongr p p' h inst inst'' fallback
+  | .rfl _ => matchDecideDecidableCongr p p' h inst inst' fallback
+  | .step inst'' _ _ => matchDecideDecidableCongr p p' h inst inst'' fallback

 /-- Simplify `Decidable.decide` by simplifying the proposition and reducing the instance.

@@ -221,20 +276,20 @@ public def simpDecideCbv : Simproc := fun e => do
      else if (← isFalseExpr p) then
        return .step (← getBoolFalseExpr) (mkApp (mkConst ``decide_false) inst)
      else
-        simpDecideByInstWithFallback p inst
+        simpAndMatchDecideDecidable p inst do return .rfl (done := true)
    | .step p' hp _ =>
      if (← isTrueExpr p') then
        return .step (← getBoolTrueExpr) <| mkApp3 (mkConst ``Sym.decide_prop_eq_true) p inst hp
      else if (← isFalseExpr p') then
        return .step (← getBoolFalseExpr) <| mkApp3 (mkConst ``Sym.decide_prop_eq_false) p inst hp
      else
-        let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) p') | return .rfl
-        let inst' ← shareCommon inst'
-        simpDecideByInstWithFallbackCongr p p' hp inst inst' (do
+        let inst' ← trySynthComputableInstance p'
+        let inst' := inst'.getD <| mkApp4 (mkConst ``decidable_of_decidable_of_eq) p p' inst hp
+        simpAndMatchDecideDecidableCongr p p' hp inst inst' do
          let res := (mkConst ``Decidable.decide)
          let res ← shareCommon res
          let res ← mkAppS₂ res p' inst'
-          return .step res (mkApp5 (mkConst ``Decidable.decide.congr_simp) p p' hp inst inst') (done := true))
+          return .step res (mkApp5 (mkConst ``Decidable.decide.congr_simp) p p' hp inst inst') (done := true)

 end Lean.Meta.Sym.Simp

--- a/tests/elab/cbv_classical.lean
+++ b/tests/elab/cbv_classical.lean
@@ -0,0 +1,38 @@
+set_option cbv.warning false
+
+/-!
+# A regression test against `cbv` picking up `Classical.propDecidable`,
+when re-synthesizing instances.
+
+When `cbv` encounters `decide P`, it simplifies the proposition `P`. If `P`
+unfolds (e.g. `IsEven 2` → `∃ k, 2 * k = 2`), `simpDecideCbv` tries to
+synthetize `Decidable` instance for the *unfolded* form. With `open Classical`,
+this was picking up `Classical.propDecidable` (which uses `choice`), replacing
+the original computable instance with one that cannot be evaluated.
+
+The code now contains a guard ensuring that the instance is not made of constants
+marked as `noncomputable`.
+-/
+
+-- A predicate wrapping an existential — has a computable `DecidablePred` instance,
+-- but the unfolded existential has none (except the classical one).
+def IsEven (n : Nat) : Prop := ∃ k, n = 2 * k
+
+instance : DecidablePred IsEven := fun n =>
+  if h : n % 2 = 0 then
+    .isTrue ⟨n / 2, by omega⟩
+  else
+    .isFalse (by intro ⟨k, hk⟩; omega)
+
+
+-- Works, using the provided `DecidablePred` instance.
+example : decide (IsEven 2) = true := by cbv
+
+example : decide (IsEven 3) = false := by cbv
+
+-- Should not fail, when `Classical.propDecidable` becomes available.
+open Classical in
+example : decide (IsEven 2) = true := by cbv
+
+open Classical in
+example : decide (IsEven 3) = false := by cbv
--- a/tests/elab/cbv_decidable_congr.lean
+++ b/tests/elab/cbv_decidable_congr.lean
@@ -0,0 +1,35 @@
+set_option cbv.warning false
+set_option trace.Meta.Tactic true
+axiom P : Prop
+axiom instDecidableP : Decidable P
+axiom Q : Prop
+
+axiom P_eval : P = Q
+attribute [cbv_eval] P_eval
+example : P = Q := by cbv
+
+axiom hQ : Q
+
+axiom instDecidableQ : Decidable Q
+noncomputable instance : Decidable P := instDecidableP
+noncomputable instance : Decidable Q := instDecidableQ
+axiom dQ_eval : instDecidableQ = Decidable.isTrue hQ
+attribute [cbv_eval] dQ_eval
+
+example : (if P then true else false) = true := by cbv
+
+example : (if P then true else false) = true := by conv => lhs; cbv
+
+example : (if _ : P then true else false) = true := by cbv
+
+example : P := by decide_cbv
+
+example : decide P = true := by conv => lhs; cbv
+
+example : Q := by decide_cbv
+
+example : decide Q = true := by conv => lhs; cbv
+
+example : (if Q then true else false) = true := by cbv
+
+example : (if _ : Q then true else false) = true := by cbv