From 6bebf9c529374bdb0736c3e1545dc563fafc3421 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Mon, 2 Mar 2026 13:47:04 +0000 Subject: [PATCH] feat: add short-circuit evaluation for `Or` and `And` in cbv (#12763) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds pre-pass simprocs `simpOr` and `simpAnd` to the `cbv` tactic that evaluate only the left argument of `Or`/`And` first, short-circuiting when the result is determined without evaluating the right side. Previously, `cbv` processed `Or`/`And` via congruence, which always evaluated both arguments. For expressions like `decide (m < n ∨ expensive)`, when `m < n` is true, the expensive right side is now skipped entirely. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 --- src/Init/Sym/Lemmas.lean | 6 ++ src/Lean/Meta/Tactic/Cbv/ControlFlow.lean | 44 +++++++++++++ tests/elab/cbv1.lean | 78 +++++++++++++++++++++++ 3 files changed, 128 insertions(+) diff --git a/src/Init/Sym/Lemmas.lean b/src/Init/Sym/Lemmas.lean index 7eb0aefefe..eb98fbf976 100644 --- a/src/Init/Sym/Lemmas.lean +++ b/src/Init/Sym/Lemmas.lean @@ -20,6 +20,12 @@ theorem ne_self (a : α) : (a ≠ a) = False := by simp theorem not_true_eq : (¬ True) = False := by simp theorem not_false_eq : (¬ False) = True := by simp +theorem or_eq_true_left (a b : Prop) (h : a = True) : (a ∨ b) = True := by simp [h] +theorem or_eq_right (a b : Prop) (h : a = False) : (a ∨ b) = b := by simp [h] + +theorem and_eq_false_left (a b : Prop) (h : a = False) : (a ∧ b) = False := by simp [h] +theorem and_eq_left (a b : Prop) (h : a = True) : (a ∧ b) = b := by simp [h] + 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 [*] diff --git a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean index be3c54e859..412c765abb 100644 --- a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean +++ b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean @@ -159,6 +159,46 @@ public def simpDIteCbv : Simproc := fun e => do let h' := mkApp3 (e.replaceFn ``Sym.dite_cond_congr) c' inst' h return .step e' h' +/-- Short-circuit evaluation of `Or`. Simplifies only the left argument; +if it reduces to `True`, returns `True` immediately without evaluating the right side. -/ +public def simpOr : Simproc := fun e => do + let_expr Or a b := e | return .rfl + match (← simp a) with + | .rfl _ => + if (← isTrueExpr a) then + return .step (← getTrueExpr) (mkApp (mkConst ``true_or) b) (done := true) + else if (← isFalseExpr a) then + return .step b (mkApp (mkConst ``false_or) b) + else + return .rfl + | .step a' ha _ => + if (← isTrueExpr a') then + return .step (← getTrueExpr) (mkApp (e.replaceFn ``Sym.or_eq_true_left) ha) (done := true) + else if (← isFalseExpr a') then + return .step b (mkApp (e.replaceFn ``Sym.or_eq_right) ha) + else + return .rfl + +/-- Short-circuit evaluation of `And`. Simplifies only the left argument; +if it reduces to `False`, returns `False` immediately without evaluating the right side. -/ +public def simpAnd : Simproc := fun e => do + let_expr And a b := e | return .rfl + match (← simp a) with + | .rfl _ => + if (← isFalseExpr a) then + return .step (← getFalseExpr) (mkApp (mkConst ``false_and) b) (done := true) + else if (← isTrueExpr a) then + return .step b (mkApp (mkConst ``true_and) b) + else + return .rfl + | .step a' ha _ => + if (← isFalseExpr a') then + return .step (← getFalseExpr) (mkApp (e.replaceFn ``Sym.and_eq_false_left) ha) (done := true) + else if (← isTrueExpr a') then + return .step b (mkApp (e.replaceFn ``Sym.and_eq_left) ha) + else + return .rfl + end Lean.Meta.Sym.Simp namespace Lean.Meta.Tactic.Cbv @@ -223,6 +263,10 @@ public def simpControlCbv : Simproc := fun e => do 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 if declName == ``Or then + simpOr e + else if declName == ``And then + simpAnd e else tryMatcher e diff --git a/tests/elab/cbv1.lean b/tests/elab/cbv1.lean index af76b3cab6..375c4e421a 100644 --- a/tests/elab/cbv1.lean +++ b/tests/elab/cbv1.lean @@ -223,3 +223,81 @@ Eq.mpr -/ #guard_msgs in #print slow_path + +/-! ## Or/And short-circuit evaluation -/ + +theorem or_test_1 : (1 < 2 ∨ (10000).factorial = 0) = True := by cbv + +/-- +info: theorem or_test_1 : (1 < 2 ∨ 10000! = 0) = True := +Lean.Sym.or_eq_true_left (1 < 2) (10000! = 0) (Lean.Sym.Nat.lt_eq_true 1 2 (eagerReduce (Eq.refl true))) +-/ +#guard_msgs in +#print or_test_1 + +theorem or_test_2 : (3 < 2 ∨ 1 < 2) = True := by cbv + +/-- +info: theorem or_test_2 : (3 < 2 ∨ 1 < 2) = True := +Eq.trans (Lean.Sym.or_eq_right (3 < 2) (1 < 2) (Lean.Sym.Nat.lt_eq_false 3 2 (eagerReduce (Eq.refl false)))) + (Lean.Sym.Nat.lt_eq_true 1 2 (eagerReduce (Eq.refl true))) +-/ +#guard_msgs in +#print or_test_2 + +theorem or_test_3 : (3 < 2 ∨ 5 < 4) = False := by cbv + +/-- +info: theorem or_test_3 : (3 < 2 ∨ 5 < 4) = False := +Eq.trans (Lean.Sym.or_eq_right (3 < 2) (5 < 4) (Lean.Sym.Nat.lt_eq_false 3 2 (eagerReduce (Eq.refl false)))) + (Lean.Sym.Nat.lt_eq_false 5 4 (eagerReduce (Eq.refl false))) +-/ +#guard_msgs in +#print or_test_3 + +theorem and_test_1 : (3 < 2 ∧ (10000).factorial = 0) = False := by cbv + +/-- +info: theorem and_test_1 : (3 < 2 ∧ 10000! = 0) = False := +Lean.Sym.and_eq_false_left (3 < 2) (10000! = 0) (Lean.Sym.Nat.lt_eq_false 3 2 (eagerReduce (Eq.refl false))) +-/ +#guard_msgs in +#print and_test_1 + +theorem and_test_2 : (1 < 2 ∧ 3 < 4) = True := by cbv + +/-- +info: theorem and_test_2 : (1 < 2 ∧ 3 < 4) = True := +Eq.trans (Lean.Sym.and_eq_left (1 < 2) (3 < 4) (Lean.Sym.Nat.lt_eq_true 1 2 (eagerReduce (Eq.refl true)))) + (Lean.Sym.Nat.lt_eq_true 3 4 (eagerReduce (Eq.refl true))) +-/ +#guard_msgs in +#print and_test_2 + +theorem and_test_3 : (1 < 2 ∧ 5 < 4) = False := by cbv + +/-- +info: theorem and_test_3 : (1 < 2 ∧ 5 < 4) = False := +Eq.trans (Lean.Sym.and_eq_left (1 < 2) (5 < 4) (Lean.Sym.Nat.lt_eq_true 1 2 (eagerReduce (Eq.refl true)))) + (Lean.Sym.Nat.lt_eq_false 5 4 (eagerReduce (Eq.refl false))) +-/ +#guard_msgs in +#print and_test_3 + +theorem or_and : (1 < 2 ∨ (3 < 2 ∧ (10000).factorial = 0)) = True := by cbv + +/-- +info: theorem or_and : (1 < 2 ∨ 3 < 2 ∧ 10000! = 0) = True := +Lean.Sym.or_eq_true_left (1 < 2) (3 < 2 ∧ 10000! = 0) (Lean.Sym.Nat.lt_eq_true 1 2 (eagerReduce (Eq.refl true))) +-/ +#guard_msgs in +#print or_and + +theorem and_or : (3 < 2 ∧ (1 < 2 ∨ (10000).factorial = 0)) = False := by cbv + +/-- +info: theorem and_or : (3 < 2 ∧ (1 < 2 ∨ 10000! = 0)) = False := +Lean.Sym.and_eq_false_left (3 < 2) (1 < 2 ∨ 10000! = 0) (Lean.Sym.Nat.lt_eq_false 3 2 (eagerReduce (Eq.refl false))) +-/ +#guard_msgs in +#print and_or