experiment: whnf optimization in cbv for Decidable.decide

src/Lean/Meta/Tactic/Cbv/ControlFlow.lean

@@ -174,6 +174,32 @@ def tryMatcher : Simproc := fun e => do
       <|> reduceRecMatcher
         <| e
 
+def whnfSimproc : Simproc := fun e => do
+  let r ← withAtLeastTransparency .default <| whnf e
+  let r ← Sym.share r
+  return .step r (← Sym.mkEqRefl r)
+
+def simpDecideProp : Simproc := fun e => do
+  let numArgs := e.getAppNumArgs
+  if numArgs < 2 then return .rfl (done := true)
+  propagateOverApplied e (numArgs - 2) fun e => do
+    let_expr Decidable.decide p h := e | return .rfl
+    match (← (whnfSimproc >> simp) h) with
+    | .rfl _ =>
+      return .rfl
+    | .step e' _ _ =>
+      let args := e'.getAppArgs
+      if (e'.isAppOf ``isTrue) then
+        let hp := args[1]!
+        let proof := mkApp3 (mkConst ``decide_eq_true) p h hp
+        return .step (← Sym.getBoolTrueExpr) proof
+      else if (e'.isAppOf ``isFalse) then
+        let hnp := args[1]!
+        let proof := mkApp3 (mkConst ``decide_eq_false) p h hnp
+        return .step (← Sym.getBoolFalseExpr) proof
+      else
+        return .rfl
+
 /-
   Precondition: `e` is an application
 -/
@@ -185,6 +211,8 @@ public def simpControlCbv : Simproc := fun e => do
     simpCond e
   else if declName == ``dite then
     simpDIteCbv e
+  else if declName == ``Decidable.decide then
+    simpDecideProp <| e
   else if declName == ``Decidable.rec then
     -- We force the rewrite in the last argument, so that we can unfold the `Decidable` instance.
     (simpInterlaced · #[false,false,true,true,true]) >> reduceRecMatcher <| e