Revert "perf: inline decidable instances (#10934)"

This reverts commit 12750d2.

Author: hargoniX

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'
-
-@[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
+@[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 {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

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)

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} :

tests/lean/run/10934.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