fix: Revert "perf: inline decidable instances" (#11007)
This PR reverts leanprover/lean4#10934
This commit is contained in:
Henrik Böving
GitHub
parent
167429501b
commit
2497cf0b40
5 changed files with 17 additions and 94 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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} :
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue