perf: inline decidable instances (#10934)

This PR adds inline annotations to several `Decidable` instances.
Additionally, it removes the `Decidable` instance for `p → q` which is
made redundant by `forall_prop_decidable`.

Author: Rob23oba

src/Init/Core.lean

@@ -1140,12 +1140,21 @@ variable {p q : Prop}
   decidable_of_decidable_of_iff (p := p) (h ▸ Iff.rfl)
 end
 
-@[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 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
 
+@[inline]
 instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
   if hp : p then
     if hq : q then
@@ -1193,11 +1202,13 @@ 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,6 +1099,7 @@ 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,18 +447,6 @@ 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

@@ -0,0 +1,74 @@
+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)

tests/lean/run/grind_cutsat_tests.lean

@@ -28,6 +28,9 @@ set_option trace.grind.cutsat.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