From 2497cf0b4072e9250b5f32fa1974ab2a2e9830ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 29 Oct 2025 09:06:51 +0100 Subject: [PATCH] fix: Revert "perf: inline decidable instances" (#11007) This PR reverts leanprover/lean4#10934 --- src/Init/Core.lean | 21 ++------ src/Init/Prelude.lean | 1 - src/Init/PropLemmas.lean | 12 +++++ tests/lean/run/10934.lean | 74 -------------------------- tests/lean/run/grind_cutsat_tests.lean | 3 -- 5 files changed, 17 insertions(+), 94 deletions(-) delete mode 100644 tests/lean/run/10934.lean diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 0b3e395456..44f9d1d745 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1140,21 +1140,12 @@ variable {p q : Prop} decidable_of_decidable_of_iff (p := p) (h ▸ Iff.rfl) end -@[inline] -instance exists_prop_decidable {p} (P : p → Prop) - [Decidable p] [∀ h, Decidable (P h)] : Decidable (Exists P) := - if h : p then - decidable_of_decidable_of_iff ⟨fun h2 => ⟨h, h2⟩, fun ⟨_, h2⟩ => h2⟩ - else isFalse fun ⟨h', _⟩ => h h' +@[macro_inline] instance {p q} [Decidable p] [Decidable q] : Decidable (p → q) := + if hp : p then + if hq : q then isTrue (fun _ => hq) + else isFalse (fun h => absurd (h hp) hq) + else isTrue (fun h => absurd h hp) -@[inline] -instance forall_prop_decidable {p} (P : p → Prop) - [Decidable p] [∀ h, Decidable (P h)] : Decidable (∀ h, P h) := - if h : p then - decidable_of_decidable_of_iff ⟨fun h2 _ => h2, fun al => al h⟩ - else isTrue fun h2 => absurd h2 h - -@[inline] instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) := if hp : p then if hq : q then @@ -1202,13 +1193,11 @@ theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : | isTrue _ => rfl | isFalse _ => rfl -@[macro_inline] instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) := match dC with | isTrue _ => dT | isFalse _ => dE -@[inline] instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h) := match dC with | isTrue hc => dT hc diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 7412c35d34..d1dab605bf 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1099,7 +1099,6 @@ until `c` is known. | Or.inl h => hp h | Or.inr h => hq h -@[inline] instance [dp : Decidable p] : Decidable (Not p) := match dp with | isTrue hp => isFalse (absurd hp) diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index 2c0228e17a..088b74433a 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -447,6 +447,18 @@ theorem Decidable.by_contra [Decidable p] : (¬p → False) → p := of_not_not @[expose] protected def Or.by_cases' [Decidable q] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α := if hq : q then h₂ hq else h₁ (h.resolve_right hq) +instance exists_prop_decidable {p} (P : p → Prop) + [Decidable p] [∀ h, Decidable (P h)] : Decidable (∃ h, P h) := +if h : p then + decidable_of_decidable_of_iff ⟨fun h2 => ⟨h, h2⟩, fun ⟨_, h2⟩ => h2⟩ +else isFalse fun ⟨h', _⟩ => h h' + +instance forall_prop_decidable {p} (P : p → Prop) + [Decidable p] [∀ h, Decidable (P h)] : Decidable (∀ h, P h) := +if h : p then + decidable_of_decidable_of_iff ⟨fun h2 _ => h2, fun al => al h⟩ +else isTrue fun h2 => absurd h2 h + @[bool_to_prop] theorem decide_eq_true_iff {p : Prop} [Decidable p] : (decide p = true) ↔ p := by simp @[simp, bool_to_prop] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} : diff --git a/tests/lean/run/10934.lean b/tests/lean/run/10934.lean deleted file mode 100644 index d07885f091..0000000000 --- a/tests/lean/run/10934.lean +++ /dev/null @@ -1,74 +0,0 @@ -set_option trace.compiler.ir.result true - -/-- -trace: [Compiler.IR] [result] - def _example (x_1 : u8) (x_2 : u8) : u8 := - case x_1 : u8 of - Bool.false → - case x_2 : u8 of - Bool.false → - let x_3 : u8 := 1; - ret x_3 - Bool.true → - ret x_1 - Bool.true → - ret x_2 - def _example._boxed (x_1 : tagged) (x_2 : tagged) : tagged := - let x_3 : u8 := unbox x_1; - let x_4 : u8 := unbox x_2; - let x_5 : u8 := _example x_3 x_4; - let x_6 : tobj := box x_5; - ret x_6 --/ -#guard_msgs in -example (a b : Bool) : Bool := decide (a ↔ b) - -/-- -trace: [Compiler.IR] [result] - def _example (x_1 : u8) (x_2 : u8) : u8 := - case x_1 : u8 of - Bool.false → - let x_3 : u8 := 1; - ret x_3 - Bool.true → - ret x_2 - def _example._boxed (x_1 : tagged) (x_2 : tagged) : tagged := - let x_3 : u8 := unbox x_1; - let x_4 : u8 := unbox x_2; - let x_5 : u8 := _example x_3 x_4; - let x_6 : tobj := box x_5; - ret x_6 --/ -#guard_msgs in -example (a b : Bool) : Bool := decide (a → b) - -/-- -trace: [Compiler.IR] [result] - def _example (x_1 : u8) (x_2 : u8) : u8 := - case x_1 : u8 of - Bool.false → - ret x_1 - Bool.true → - ret x_2 - def _example._boxed (x_1 : tagged) (x_2 : tagged) : tagged := - let x_3 : u8 := unbox x_1; - let x_4 : u8 := unbox x_2; - let x_5 : u8 := _example x_3 x_4; - let x_6 : tobj := box x_5; - ret x_6 --/ -#guard_msgs in -example (a b : Bool) : Bool := decide (∃ _ : a, b) - -/-- -trace: [Compiler.IR] [result] - def _example (x_1 : u8) : u8 := - ret x_1 - def _example._boxed (x_1 : tagged) : tagged := - let x_2 : u8 := unbox x_1; - let x_3 : u8 := _example x_2; - let x_4 : tobj := box x_3; - ret x_4 --/ -#guard_msgs in -example (a : Bool) : Bool := decide (if _h : a then True else False) diff --git a/tests/lean/run/grind_cutsat_tests.lean b/tests/lean/run/grind_cutsat_tests.lean index 97d68e9c65..812411955d 100644 --- a/tests/lean/run/grind_cutsat_tests.lean +++ b/tests/lean/run/grind_cutsat_tests.lean @@ -28,9 +28,6 @@ set_option trace.grind.lia.model true in example (a b c d e : Int) : test1 a b c d e := by (fail_if_success cutsat); sorry --- TODO: this should not be necessary (compare to 20 before) -set_option synthInstance.maxSize 400 in - /-- info: false -/ #guard_msgs (info) in #eval test1 101 0 5335 0 0