perf: inline Decidable instances (#11008)

This PR inlines several Decidable instances for performance reasons.

Unlike the previous #10934 it does not attempt to also simplify the
Decidable instance system as
that has proven to have non trivial performance impact.

Co-authored-by: Rob23oba <[email protected]>

Author: hargoniX

src/Init/Core.lean

@@ -1146,6 +1146,7 @@ end
     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
@@ -1193,11 +1194,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,12 +447,14 @@ 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)
 
+@[inline]
 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'
 
+@[inline]
 instance forall_prop_decidable {p} (P : p → Prop)
   [Decidable p] [∀ h, Decidable (P h)] : Decidable (∀ h, P h) :=
 if h : p then

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)