perf: speed up reflection of if in bv_decide (#6162)

This PR adds a slight performance improvement to reflection of `if`
statements that I noticed by profiling Leanwuzla against SMTCOMP's
`non-incremental/QF_BV/fft/Sz256_6616.smt2`.

In particular:
1. The profile showed about 4 percent of the total run time were spent
constructing these decidable instances in reflection of `if` statements.
We can construct them much quicker by hand as they always have the same
structure
2. This delays construction of these statements until we actually
generate the reflection proof that we wish to submit to the kernel. Thus
if we encounter a SAT instad of an UNSAT problem we will not spend time
generating these expressions anymore.

```
baseline
  Time (mean ± σ):     31.236 s ±  0.258 s
  Range (min … max):   30.899 s … 31.661 s    10 runs

after
  Time (mean ± σ):     30.671 s ±  0.288 s
  Range (min … max):   30.350 s … 31.156 s    10 runs
```

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean

@@ -58,15 +58,28 @@ where
     let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
     let eqBV ← ReifiedBVLogical.ofPred eqBVPred
 
-    let trueExpr := mkConst ``Bool.true
-    let impExpr ← mkArrow (← mkEq eqDiscrExpr trueExpr) (← mkEq eqBVExpr trueExpr)
-    let decideImpExpr ← mkAppOptM ``Decidable.decide #[some impExpr, none]
     let imp ← ReifiedBVLogical.mkGate eqDiscr eqBV eqDiscrExpr eqBVExpr .imp
 
     let proof := do
       let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
       let congrProof ← imp.evalsAtAtoms
       let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr lhs.width) discrExpr lhsExpr rhsExpr
+
+      let trueExpr := mkConst ``Bool.true
+      let eqDiscrTrueExpr ← mkEq eqDiscrExpr trueExpr
+      let eqBVExprTrueExpr ← mkEq eqBVExpr trueExpr
+      let impExpr ← mkArrow eqDiscrTrueExpr eqBVExprTrueExpr
+      -- construct a `Decidable` instance for the implication using forall_prop_decidable
+      let decEqDiscrTrue := mkApp2 (mkConst ``instDecidableEqBool) eqDiscrExpr trueExpr
+      let decEqBVExprTrue := mkApp2 (mkConst ``instDecidableEqBool) eqBVExpr trueExpr
+      let impDecidable := mkApp4 (mkConst ``forall_prop_decidable)
+        eqDiscrTrueExpr
+        (.lam .anonymous eqDiscrTrueExpr eqBVExprTrueExpr .default)
+        decEqDiscrTrue
+        (.lam .anonymous eqDiscrTrueExpr decEqBVExprTrue .default)
+
+      let decideImpExpr := mkApp2 (mkConst ``Decidable.decide) impExpr impDecidable
+
       return mkApp4
         (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
         decideImpExpr