perf: avoid expensive instance re-synthesis in cbv

src/Init/Sym/Lemmas.lean

@@ -179,4 +179,14 @@ theorem decide_isFalse_congr (p p' : Prop) (heq : p = p') {inst : Decidable p} {
 theorem decide_prop_eq_true (p : Prop) {inst : Decidable p} (h : p = True) : decide p = true := by simp [*]
 theorem decide_prop_eq_false (p : Prop) {inst : Decidable p} (h : p = False) : decide p = false := by simp [*]
 
+theorem decidable_eq_isTrue (p : Prop) (inst : Decidable p) (h : p) : inst = .isTrue h :=
+  Subsingleton.elim _ _
+theorem decidable_eq_isFalse (p : Prop) (inst : Decidable p) (h : ¬p) : inst = .isFalse h :=
+  Subsingleton.elim _ _
+
+theorem eq_mp_prop {p q : Prop} (h : p = q) (hp : p) : q := h ▸ hp
+theorem eq_mp_not {p q : Prop} (h : p = q) (hnp : ¬p) : ¬q := h ▸ hnp
+theorem iff_mp_not {p q : Prop} (h : p ↔ q) (hnp : ¬p) : ¬q := fun hq => hnp (h.mpr hq)
+theorem iff_mpr_not {p q : Prop} (h : p ↔ q) (hnq : ¬q) : ¬p := fun hp => hnq (h.mp hp)
+
 end Lean.Sym

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

@@ -116,12 +116,17 @@ builtin_cbv_simproc ↓ simpIteCbv (@ite _ _ _ _ _) := fun e => do
         simpAndMatchIteDecidable f α c inst a b do
           -- If we get stuck here, maybe the problem is that we need to look at `Decidable c'`
           let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h
-          simpAndMatchIteDecidableCongr f α c inst a b c' h inst' do
-            -- If we fail, then we just rewrite `c` to `c'`
+          -- If we fail, then we just rewrite `c` to `c'`
+          let rewriteCond : SimpM Result := do
             let e' := e.getBoundedAppFn 4
             let e' ← mkAppS₄ e' c' inst' a b
             let h' := mkApp3 (e.replaceFn ``Sym.ite_cond_congr) c' inst' h
             return .step e' h' (done := true) (contextDependent := cd)
+          simpAndMatchIteDecidableCongr f α c inst a b c' h inst' do
+            -- The original instance is stuck; try a synthesized instance for `c'`
+            let .some instS ← trySynthInstance (mkApp (mkConst ``Decidable) c') | rewriteCond
+            let instS ← shareCommon instS
+            simpAndMatchIteDecidableCongr f α c inst a b c' h instS rewriteCond
 
 /-- Reduce `dite` by matching the `Decidable` instance for `isTrue`/`isFalse`. -/
 def matchDIteDecidable (f α c inst a b instToMatch : Expr) (fallback : SimpM Result) : SimpM Result := do
@@ -198,14 +203,19 @@ builtin_cbv_simproc ↓ simpDIteCbv (@dite _ _ _ _ _) := fun e => do
         simpAndMatchDIteDecidable f α c inst a b do
           -- Otherwise, we make `Decidable c'` instance and try to evaluate it instead
           let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h
-          simpAndMatchDIteDecidableCongr f α c inst a b c' h inst' do
+          let rewriteCond : SimpM Result := do
             let e' := e.getBoundedAppFn 4
             let h ← shareCommon h
             let a ← share <| mkLambda `h .default c' (a.betaRev #[mkApp4 (mkConst ``Eq.mpr_prop) c c' h (mkBVar 0)])
             let b ← share <| mkLambda `h .default (mkNot c') (b.betaRev #[mkApp4 (mkConst ``Eq.mpr_not) c c' h (mkBVar 0)])
             let e' ← mkAppS₄ e' c' inst' a b
             let h' := mkApp3 (e.replaceFn ``Sym.dite_cond_congr) c' inst' h
             return .step e' h' (done := true) (contextDependent := cd)
+          simpAndMatchDIteDecidableCongr f α c inst a b c' h inst' do
+            -- The original instance is stuck; try a synthesized instance for `c'`
+            let .some instS ← trySynthInstance (mkApp (mkConst ``Decidable) c') | rewriteCond
+            let instS ← shareCommon instS
+            simpAndMatchDIteDecidableCongr f α c inst a b c' h instS rewriteCond
 
 /-- Reduce `decide` by matching the `Decidable` instance for `isTrue`/`isFalse`. -/
 def matchDecideDecidable (p inst instToMatch : Expr) (fallback : SimpM Result) : SimpM Result := do
@@ -273,11 +283,97 @@ builtin_cbv_simproc ↓ simpDecideCbv (@Decidable.decide _ _) := fun e => do
       else
         let inst' ← trySynthComputableInstance p'
         let inst' := inst'.getD <| mkApp4 (mkConst ``decidable_of_decidable_of_eq) p p' inst hp
-        simpAndMatchDecideDecidableCongr p p' hp inst inst' do
+        let rebuild : SimpM Result := do
           let res := (mkConst ``Decidable.decide)
           let res ← shareCommon res
           let res ← mkAppS₂ res p' inst'
           return .step res (mkApp5 (mkConst ``Decidable.decide.congr_simp) p p' hp inst inst') (done := true) (contextDependent := cd)
+        simpAndMatchDecideDecidableCongr p p' hp inst inst' do
+          -- The instance is stuck; try a synthesized instance for `p'` (the synthesized
+          -- instance may be evaluable even when the original is opaque)
+          let .some instS ← trySynthInstance (mkApp (mkConst ``Decidable) p') | rebuild
+          let instS ← shareCommon instS
+          simpAndMatchDecideDecidableCongr p p' hp inst instS rebuild
+
+/-- Rewrites `e : Decidable q` to `isTrue hq`/`isFalse hq`. Since any two `Decidable q`
+instances are equal by `Subsingleton`, the proof only needs `hq`, a proof or refutation
+of `q`. -/
+def mkDecidableCtorStep (q e hq : Expr) (isTrue : Bool) (cd : Bool) : SimpM Result := do
+  let hq ← shareCommon hq
+  let ctor := if isTrue then ``Decidable.isTrue else ``Decidable.isFalse
+  let thm := if isTrue then ``Sym.decidable_eq_isTrue else ``Sym.decidable_eq_isFalse
+  let e' ← share <| mkApp2 (mkConst ctor) q hq
+  return .step e' (mkApp3 (mkConst thm) q e hq) (contextDependent := cd)
+
+/--
+Rewrites a stuck instance `e : Decidable q` to constructor form by deciding the
+proposition `q` directly. This handles instances that cannot be evaluated structurally,
+e.g. `Nat.decEq 15 (Nat.minFac 15 ^ 1)` unfolds to a *dependent* match on
+`Nat.beq 15 (Nat.minFac 15 ^ 1)`, which congruence cannot rewrite and kernel reduction
+cannot evaluate when the argument is defined by well-founded recursion. The proposition
+route evaluates `q` with the full evaluator; if it reaches `True`/`False`, the rewrite to
+`isTrue`/`isFalse` is justified by `Sym.decidable_eq_isTrue`/`Sym.decidable_eq_isFalse`
+(any two `Decidable q` instances are equal by `Subsingleton`).
+-/
+public def decideStuckInstance (q : Expr) (stuck : Bool → SimpM Result) : Simproc := fun e => do
+  match (← simp q) with
+  | .rfl _ cd =>
+    if (← isTrueExpr q) then mkDecidableCtorStep q e (mkConst ``True.intro) true cd
+    else if (← isFalseExpr q) then mkDecidableCtorStep q e (mkConst ``not_false) false cd
+    else stuck cd
+  | .step q' hq _ cd =>
+    if (← isTrueExpr q') then mkDecidableCtorStep q e (mkOfEqTrueCore q hq) true cd
+    else if (← isFalseExpr q') then mkDecidableCtorStep q e (mkOfEqFalseCore q hq) false cd
+    else stuck cd
+
+/--
+Evaluates a `Decidable`-transport wrapper `e : Decidable q` (e.g.
+`decidable_of_decidable_of_eq`) by evaluating the wrapped instance `inst : Decidable p`.
+
+If `inst` reduces to `isTrue`/`isFalse`, rewrites `e` to constructor form directly: the
+proof carried by the constructor is transported from `p` to `q` via `mkTrue`/`mkFalse`,
+and the rewrite itself is justified by `Subsingleton` (see `mkDecidableCtorStep`). If the
+inner instance is stuck, falls back to deciding the proposition `q` itself. If that fails
+as well, the wrapper is marked done: unfolding it would expose `dite p`, whose fallback
+paths re-create the wrapper around the same stuck instance and loop forever.
+-/
+def evalDecidableTransport (q inst : Expr) (mkTrue mkFalse : Expr → Expr) : Simproc := fun e => do
+  let matchInst (instVal : Expr) (cd : Bool) (fallback : SimpM Result) : SimpM Result := do
+    match_expr instVal with
+    | Decidable.isTrue _ hp => mkDecidableCtorStep q e (mkTrue hp) true cd
+    | Decidable.isFalse _ hnp => mkDecidableCtorStep q e (mkFalse hnp) false cd
+    | _ => fallback
+  -- The instance route is stuck: try to decide the proposition `q` directly.
+  let propFallback (cdInst : Bool) : SimpM Result := do
+    let r ← decideStuckInstance q (fun cd => return mkRflResult (done := true) (contextDependent := cd)) e
+    return if cdInst && !r.isContextDependent then r.withContextDependent else r
+  match (← simp inst) with
+  | .rfl _ cd => matchInst inst cd (propFallback cd)
+  | .step inst' _ _ cd => matchInst inst' cd (propFallback cd)
+
+builtin_cbv_simproc ↓ simpDecidableOfDecidableOfEq (@decidable_of_decidable_of_eq _ _ _ _) := fun e => do
+  let_expr decidable_of_decidable_of_eq p q inst h := e | return .rfl
+  evalDecidableTransport q inst
+    (fun hp => mkApp4 (mkConst ``Sym.eq_mp_prop) p q h hp)
+    (fun hnp => mkApp4 (mkConst ``Sym.eq_mp_not) p q h hnp) e
+
+builtin_cbv_simproc ↓ simpDecidableOfDecidableOfIff (@decidable_of_decidable_of_iff _ _ _ _) := fun e => do
+  let_expr decidable_of_decidable_of_iff p q inst h := e | return .rfl
+  evalDecidableTransport q inst
+    (fun hp => mkApp4 (mkConst ``Iff.mp) p q h hp)
+    (fun hnp => mkApp4 (mkConst ``Sym.iff_mp_not) p q h hnp) e
+
+builtin_cbv_simproc ↓ simpDecidableOfIff (@decidable_of_iff _ _ _ _) := fun e => do
+  let_expr decidable_of_iff b a h inst := e | return .rfl
+  evalDecidableTransport b inst
+    (fun hp => mkApp4 (mkConst ``Iff.mp) a b h hp)
+    (fun hnp => mkApp4 (mkConst ``Sym.iff_mp_not) a b h hnp) e
+
+builtin_cbv_simproc ↓ simpDecidableOfIff' (@decidable_of_iff' _ _ _ _) := fun e => do
+  let_expr decidable_of_iff' a b h inst := e | return .rfl
+  evalDecidableTransport a inst
+    (fun hq => mkApp4 (mkConst ``Iff.mpr) a b h hq)
+    (fun hnq => mkApp4 (mkConst ``Sym.iff_mpr_not) a b h hnq) e
 
 end Lean.Meta.Sym.Simp
 

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

@@ -167,6 +167,25 @@ def handleApp : Simproc := fun e => do
   | .lam .. => betaReduce e
   | _ => return .rfl
 
+/--
+Post-pass fallback for stuck `Decidable`-valued applications: decides the underlying
+proposition instead (see `decideStuckInstance`). Runs after `handleApp` has failed to
+make progress with equations, unfolding, and matcher reduction.
+-/
+def handleStuckDecidable : Simproc := fun e => do
+  let .const declName _ := e.getAppFn | return .rfl
+  if declName == ``Decidable.isTrue || declName == ``Decidable.isFalse then return .rfl
+  let info ← getConstInfo declName
+  -- Cheap pre-filter: the head's result type must be `Decidable`, or dependent (a bound
+  -- variable head, e.g. the motive application of a stuck matcher); otherwise the
+  -- application cannot be `Decidable`-valued and we skip the `inferType`.
+  match info.type.getForallBody.getAppFn with
+  | .const clsName _ => unless clsName == ``Decidable do return .rfl
+  | .bvar .. => pure ()
+  | _ => return .rfl
+  let_expr Decidable p := (← Sym.inferType e) | return .rfl
+  decideStuckInstance p (fun cd => return mkRflResult (contextDependent := cd)) e
+
 def handleOpaqueConst : Simproc := fun e => do
   let .const constName _ := e | return .rfl
   if (← isCbvOpaque constName) then
@@ -240,6 +259,29 @@ def handleProj : Simproc := fun e => do
         let newProof ← mkEqOfHEq newProof (check := false)
         return .step (← Lean.Expr.updateProjS! e e') newProof cd
 
+/--
+Pre-pass handler for class-valued applications, e.g. `Decidable` instances such as
+`instDecidableOr p q dp dq`. These are evaluated by unfolding directly instead of
+letting the simplifier rewrite their arguments via congruence first: rewriting a
+`Prop` argument of an instance does not advance evaluation, but it forces the
+congruence machinery to re-synthesize the dependent instance arguments, which is
+prohibitively expensive for large propositions.
+-/
+def handleClassApp : Simproc := fun e => do
+  let fn := e.getAppFn
+  let .const declName _ := fn | return .rfl
+  let info ← getConstInfo declName
+  let .const clsName _ := info.type.getForallBody.getAppFn | return .rfl
+  unless isClass (← getEnv) clsName do return .rfl
+  -- Only bypass argument congruence when it would have to re-synthesize instance
+  -- arguments. For class-valued functions over plain values (e.g. `Nat.decEq`),
+  -- evaluating the arguments first is required: their unfolded bodies often match
+  -- *dependently* on an argument (e.g. `match h : Nat.beq n m with ...`), which can
+  -- only be reduced by `reduceRecMatcher` once the arguments are ground.
+  let .congrTheorem thm ← Sym.getCongrInfo fn | return .rfl
+  unless thm.argKinds.any (· matches .subsingletonInst) do return .rfl
+  handleApp e
+
 open Sym.Internal in
 /--
 For an application whose head is neither a constant nor a lambda (e.g. a projection
@@ -269,6 +311,8 @@ def handleConst : Simproc := fun e => do
   let .const n lvls := e | return .rfl
   let info ← getConstInfo n
   unless info.isDefinition do return .rfl
+  -- Fast path: a syntactically functional type cannot whnf to a non-function.
+  if info.type matches .forallE .. then return .rfl
   let eType ← Sym.inferType e
   let eType ← whnfD eType
   if eType matches .forallE .. then return .rfl
@@ -290,7 +334,7 @@ def cbvPreStep : Simproc := fun e => do
   | .lit .. => foldLit e
   | .proj .. => handleProj e
   | .const .. => handleOpaqueConst >> (tryCbvTheorems <|> handleConst) <| e
-  | .app .. => tryMatcher <|> simplifyAppFn <| e
+  | .app .. => tryMatcher <|> handleClassApp <|> simplifyAppFn <| e
   | .letE .. =>
     if e.letNondep! then
       let betaAppResult ← toBetaApp e
@@ -306,7 +350,7 @@ def cbvPre (simprocs : CbvSimprocs) : Simproc :=
 
 /-- Post-pass: evaluate ground arithmetic, then try eval simprocs, then try unfolding/beta-reducing applications and finally run post simprocs -/
 def cbvPost (simprocs : CbvSimprocs) : Simproc :=
-  evalGround <|> cbvSimprocDispatch simprocs.eval simprocs.erased <|> handleApp <|> cbvSimprocDispatch simprocs.post simprocs.erased
+  evalGround <|> cbvSimprocDispatch simprocs.eval simprocs.erased <|> handleApp <|> handleStuckDecidable <|> cbvSimprocDispatch simprocs.post simprocs.erased
 
 def mkCbvMethods (simprocs : CbvSimprocs) : Methods :=
   { pre := cbvPre simprocs, post := cbvPost simprocs }