From d66aaebca69ce116712f549fbeb310ce091fd48a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Mon, 2 Mar 2026 17:11:48 +0000 Subject: [PATCH] perf: simplify `cbv` `ite`/`dite` simprocs by reducing `Decidable` instance directly (#12677) This PR changes the approach in `simpIteCbv` and `simpDIteCbv`, by replacing call to `Decidable.decide` with reducing and direct pattern matching on the `Decidable` instance for `isTrue`/`isFalse`. This produces simpler proof terms. --------- Co-authored-by: Claude Opus 4.6 --- src/Init/Sym/Lemmas.lean | 12 ++ src/Lean/Meta/Tactic/Cbv/ControlFlow.lean | 127 +++++++++------------- tests/lean/run/cbv4.lean | 2 - 3 files changed, 62 insertions(+), 79 deletions(-) diff --git a/src/Init/Sym/Lemmas.lean b/src/Init/Sym/Lemmas.lean index eb98fbf976..0ac5d82d66 100644 --- a/src/Init/Sym/Lemmas.lean +++ b/src/Init/Sym/Lemmas.lean @@ -30,6 +30,18 @@ theorem ite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) (c' : Prop) {inst' : Decidable c'} (h : c = c') : @ite α c inst a b = @ite α c' inst' a b := by simp [*] +theorem ite_true {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) {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 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_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_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 diff --git a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean index 412c765abb..d39f4e4f2c 100644 --- a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean +++ b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean @@ -35,6 +35,21 @@ corresponding branch. namespace Lean.Meta.Sym.Simp open Internal +/-- 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 + | 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 + +/-- Simplify the `Decidable` instance, then try `simpIteDecidable`. -/ +def simpIteDecidableWithFallback (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 + /-- Like `simpIte` but also evaluates `Decidable.decide` when the condition does not reduce to `True`/`False` directly. -/ public def simpIteCbv : Simproc := fun e => do @@ -46,48 +61,39 @@ public def simpIteCbv : Simproc := fun e => do | .rfl _ => if (← isTrueExpr c) then return .step a <| mkApp3 (mkConst ``ite_true f.constLevels!) α a b - else if (← isFalseExpr c) then + else if (← isFalseExpr c) then return .step b <| mkApp3 (mkConst ``ite_false f.constLevels!) α a b else - let toEval ← mkAppS₂ (mkConst ``Decidable.decide) c inst - let evalRes ← simp toEval - match evalRes with - | .rfl _ => - return .rfl (done := true) - | .step v hv _ => - if (← isBoolTrueExpr v) then - let h' := mkApp3 (mkConst ``eq_true_of_decide) c inst hv - let inst' := mkConst ``instDecidableTrue - let c' ← getTrueExpr - 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' - let ha := mkApp3 (mkConst ``ite_true f.constLevels!) α a b - let ha ← mkEqTrans e e' h' a ha - return .step a ha (done := false) - else if (← isBoolFalseExpr v) then - let h' := mkApp3 (mkConst ``eq_false_of_decide) c inst hv - let inst' := mkConst ``instDecidableFalse - let c' ← getFalseExpr - 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' - let hb := mkApp3 (mkConst ``ite_false f.constLevels!) α a b - let hb ← mkEqTrans e e' h' b hb - return .step b hb (done := false) - else - return .rfl (done := true) + simpIteDecidableWithFallback f α c inst a b <| 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 - 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' + simpIteDecidableWithFallback f α c inst a b <| do + 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) + +/-- 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 + | Decidable.isTrue _ hp => + let a' ← share <| a.betaRev #[hp] + return .step a' <| mkApp6 (mkConst ``Sym.dite_true f.constLevels!) α c inst a b hp + | Decidable.isFalse _ hnp => + let b' ← share <| b.betaRev #[hnp] + return .step b' <| mkApp6 (mkConst ``Sym.dite_false f.constLevels!) α c inst a b hnp + | _ => fallback + +/-- Simplify the `Decidable` instance, then try `simpDIteDecidable`. -/ +def simpDIteDecidableWithFallback (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 /-- Like `simpDIte` but also evaluates `Decidable.decide` when the condition does not reduce to `True`/`False` directly. -/ @@ -105,41 +111,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 - let toEval ← mkAppS₂ (mkConst ``Decidable.decide) c inst - let evalRes ← simp toEval - match evalRes with - | .rfl _ => return .rfl (done := true) - | .step v hv _ => - if (← isBoolTrueExpr v) then - let h' := mkApp3 (mkConst ``eq_true_of_decide) c inst hv - let inst' := mkConst ``instDecidableTrue - let e' := e.getBoundedAppFn 4 - let h ← shareCommon h' - let c' ← getTrueExpr - 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 - let a' ← share <| a.betaRev #[mkConst ``True.intro] - let ha := mkApp3 (mkConst ``dite_true f.constLevels!) α a b - let ha ← mkEqTrans e e' h' a' ha - return .step a' ha - else if (← isBoolFalseExpr v) then - let h' := mkApp3 (mkConst ``eq_false_of_decide) c inst hv - let inst' := mkConst ``instDecidableFalse - let e' := e.getBoundedAppFn 4 - let h ← shareCommon h' - let c' ← getFalseExpr - 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 - let b' ← share <| b.betaRev #[mkConst ``not_false] - let hb := mkApp3 (mkConst ``dite_false f.constLevels!) α a b - let hb ← mkEqTrans e e' h' b' hb - return .step b' hb - else - return .rfl (done := true) + simpDIteDecidableWithFallback f α c inst a b <| return .rfl (done := true) | .step c' h _ => if (← isTrueExpr c') then let h' ← shareCommon <| mkOfEqTrueCore c h @@ -150,14 +122,15 @@ 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 - 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' + simpDIteDecidableWithFallback f α c inst a b <| do + 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) /-- Short-circuit evaluation of `Or`. Simplifies only the left argument; if it reduces to `True`, returns `True` immediately without evaluating the right side. -/ diff --git a/tests/lean/run/cbv4.lean b/tests/lean/run/cbv4.lean index 2145354aaa..3e644d777d 100644 --- a/tests/lean/run/cbv4.lean +++ b/tests/lean/run/cbv4.lean @@ -11,6 +11,4 @@ def checkAll (gas : Nat) : Nat → Bool | 0 => true | n + 1 => bif manyStep (n + 2) (n + 2) gas then checkAll gas n else false -set_option maxRecDepth 5000 -set_option trace.Meta.Tactic true example : checkAll 70 100 = true := by cbv