feat: decompose typeclass-method projections in mvcgen' (#13870)

This PR lets `mvcgen'` decompose programs whose head is a typeclass
method projection (e.g. `Add.add inst a b`) by reducing through the
kernel projection to the instance body.

`reduceHead?` reduces `.proj` at `.instances` transparency
(`withReducibleAndInstances`), so concrete instances unfold to their
`.mk` constructor without escalating to default transparency. An
`unfoldReducible` pass after projection reduction normalizes abbrevs
introduced by the instance body to match rule patterns. A new
`.proj`-gated `tryHeadReduceProg` strategy in `solve` calls
`reduceHead?` and rewrites the goal's program via `replaceProgDefEq`.

Author: sgraf812

src/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.lean

@@ -7,7 +7,8 @@ module
 
 prelude
 public import Lean.Meta.Sym.SymM
-public import Lean.Meta.WHNF
+import Lean.Meta.WHNF
+import Lean.Meta.Sym
 
 open Lean Meta Sym
 
@@ -48,6 +49,7 @@ public partial def reduceHead? (e : Expr) : SymM (Option Expr) :=
         -- projections
         if ← isProjectionFn name then
           let some e' ← Meta.unfoldDefinition? (mkAppRev f rargs) | return lastReduction
+          let e' ← Sym.unfoldReducible e'
           let e' ← Sym.shareCommonInc e'
           go lastReduction e'.getAppFn e'.getAppRevArgs  -- intentional lastReduction! see docstring
         -- iota reduction: match/recursor with concrete discriminant
@@ -56,10 +58,15 @@ public partial def reduceHead? (e : Expr) : SymM (Option Expr) :=
           go (some e') e'.getAppFn e'.getAppRevArgs
         else
           pure lastReduction
-      | .proj .. => match ← reduceProj? f with
+      | .proj .. =>
+        -- whnf at `instances` transparency: unfold `instMyAddInt32` (an instance) to
+        -- expose its `MyAdd.mk` constructor so `reduceProj?` can project the field,
+        -- but do not unfold arbitrary user definitions.
+        match ← withReducibleAndInstances (reduceProj? f) with
         | some f' =>
+          let f' ← Sym.unfoldReducible f'
+          let f' ← Sym.shareCommonInc f'
           let e' := mkAppRev f' rargs
-          let e' ← Sym.shareCommonInc e'
           go (some e') e'.getAppFn e'.getAppRevArgs
         | none    => pure lastReduction
       | _ => pure lastReduction

src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean

@@ -13,6 +13,7 @@ public import Lean.Meta.Sym.AlphaShareBuilder
 public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.InstantiateMVarsS
 public import Lean.Meta.Sym.Util
+import Lean.Meta.WHNF
 
 open Lean Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do.SpecAttr

src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean

@@ -162,6 +162,13 @@ private def tryFvarZeta (goal : MVarId) (head H σs ent : Expr) (args : Array Ex
   let e' ← shareCommonInc (val.betaRev e.getAppRevArgs)
   return some <| .goals [← replaceProgDefEq goal head H σs ent args wpConst m ps instWP α e']
 
+/-- Reduce a kernel `.proj` head in the program `e`. -/
+private def tryHeadReduceProg (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
+    (wpConst m ps instWP α e f : Expr) : VCGenM (Option SolveResult) := do
+  unless f matches .proj .. do return none
+  let some e' ← reduceHead? e | return none
+  return some <| .goals [← replaceProgDefEq goal head H σs ent args wpConst m ps instWP α e']
+
 /-- Look up a registered `@[spec]` theorem for the program head and apply its cached
 backward rule. Falls back to `.noSpecFoundForProgram` / `.noStrategyForProgram` when no
 spec applies. -/
@@ -258,6 +265,11 @@ public def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
     VCGen.burnOne
     return r
 
+  -- Reduce kernel `.proj` heads in the program (e.g., `instAddNat.1 a b`).
+  if let some r ← tryHeadReduceProg goal head H σs ent args wpConst m ps instWP α e f then
+    VCGen.burnOne
+    return r
+
   -- Apply registered specifications, or fall through to `.noStrategyForProgram`.
   VCGen.burnOne
   applySpec goal e excessArgs m σs ps instWP

tests/bench/mvcgen/sym/test_do_logic.lean

@@ -20,26 +20,6 @@ The deprecation warning emitted by `mvcgen` indicates which tests still need mig
 
 Tests whose proofs do not mention `mvcgen`/`mvcgen'` (manual `mspec`/`mintro` proofs)
 are intentionally not ported.
-
-## Remaining blockers (tests still using `mvcgen`)
-
-Each blocked test is annotated with a `BLOCKED:` comment explaining the cause:
-
-- **`fib_triple_step`** — `mvcgen'` does not support `optConfig` (no `stepLimit`).
-- **`fib_triple_erase`**, **`erase_unfold`** — `mvcgen' [-name]` errors with
-  "No spec found" instead of leaving an unsolved VC. Needs an `-errorOnMissingSpec`
-  flag (default true) to gate this.
-- **`mkFreshPair_triple`** — `mvcgen'` lacks the `+trivial` flag, so schematic
-  output-state VCs remain unsolved.
-- **`mem_mergeWithAll`** — `mvcgen'` errors "No spec found" for `forIn` on the
-  universe-polymorphic `ExtTreeMap`.
-
-## Notes on workarounds
-
-- Some tests need `+zetaDelta` because `mvcgen'` leaves let-bindings in VCs.
-- `test_ite` needs an extra `exact ExceptConds.entails_false` because `mvcgen'` doesn't
-  auto-discharge `ExceptConds.entails` for non-`.pure` PostShapes.
-- `fast_expo_correct` manually `obtain`s tuples that `mvcgen'` leaves un-destructured.
 -/
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
@@ -619,3 +599,46 @@ example (p : Nat → Prop) [DecidablePred p] (n : Nat) :
   with (simp_all [-Classical.not_forall]; try grind)
 
 end InvariantSyntaxTests
+
+namespace RflReducibility
+
+-- From `mvcgenRflReducibility.lean`. Asserts that decomposing `MyShl.shl a 32` does
+-- not whnf at default reducibility, otherwise `UInt64.ofNat 32.toInt.toNat` would
+-- unfold deeply and timeout. `mvcgen'` keeps reduction at `.instances` transparency
+-- when stepping through class projections (`reduceProj?` in `Reduce.lean`), so this
+-- example decomposes cleanly.
+
+abbrev RustM := Except String
+
+class MyAddU (Self : Type) (Rhs : Type) where
+  add : (Self → Rhs → RustM Self)
+
+instance : MyAddU UInt64 UInt64 := {
+  add x y := if BitVec.uaddOverflow x.toBitVec y.toBitVec then Except.error "" else pure (x + y)
+}
+
+class MyShl (Self : Type) (Rhs : Type) where
+  shl : (Self → Rhs → RustM Self)
+
+instance : MyShl UInt64 Int32 := {
+  shl x y := pure (x <<< (UInt64.ofNat y.toInt.toNat))
+}
+
+/--
+error: unsolved goals
+case vc1
+a : UInt64
+h✝ : (UInt64.toBitVec 0).uaddOverflow (a <<< UInt64.ofNat (Int32.toInt 32).toNat).toBitVec = true
+⊢ ⊢ₛ wp⟦Except.error ""⟧ (fun r => ⌜True⌝, ExceptConds.false)
+-/
+#guard_msgs in
+example (a : UInt64) :
+    ⦃⌜True⌝⦄
+      do
+        let a ← MyShl.shl a (32: Int32)
+        let a ← MyAddU.add (0 : UInt64) a
+        pure a
+    ⦃PostCond.noThrow fun r => ⌜True⌝⦄ := by
+  mvcgen' (errorOnMissingSpec := false) [MyShl.shl, MyAddU.add]
+
+end RflReducibility