test: lazy let-binding unfolding in sym mvcgen (#13210)

This PR replaces eager let-expression zeta-reduction in the sym-based
mvcgen with on-demand unfolding that mirrors the production mvcgen's
behavior.

Previously, all let-expressions in the program head were immediately
zeta-reduced. Now, let-expressions are hoisted to the top of the goal
target, and the value is only inlined if it is duplicable (literals,
fvars, consts, `OfNat.ofNat`). Complex values are introduced into the
local context via `introsSimp`, preserving SymM's maximal sharing
invariants, and unfolded on demand when the fvar later appears as the
program head.

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

tests/bench/mvcgen/sym/cases/Cases.lean

@@ -3,6 +3,7 @@ import Cases.AddSubCancelDeep
 import Cases.AddSubCancelSimp
 import Cases.DiteSplit
 import Cases.GetThrowSet
+import Cases.LetBinding
 import Cases.MatchIota
 import Cases.MatchSplit
 import Cases.PurePrecond

tests/bench/mvcgen/sym/cases/Cases/LetBinding.lean

@@ -0,0 +1,37 @@
+import Lean
+import VCGen
+
+open Lean Meta Elab Tactic Sym Std Do SpecAttr
+
+namespace LetBinding
+
+set_option mvcgen.warning false
+
+-- Partially evaluated specs for best performance.
+
+@[spec high]
+theorem Spec.MonadState_get {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond σ (.arg σ ps)} :
+    ⦃fun s => Q.fst s s⦄ get (m := StateT σ m) ⦃Q⦄ := by
+  mvcgen'
+
+@[spec high]
+theorem Spec.MonadStateOf_set {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond PUnit (.arg σ ps)} {s : σ} :
+    ⦃fun _ => Q.fst ⟨⟩ s⦄ set (m := StateT σ m) s ⦃Q⦄ := by
+  mvcgen'
+
+def step (v : Nat) : StateM Nat Unit := do
+  let s ← get
+  -- Pure let binding: `let offset := ...` produces a letE node in the elaborated term
+  let offset := v + 1
+  set (s + offset)
+  let s ← get
+  set (s - offset)
+
+def loop (n : Nat) : StateM Nat Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step n; loop n
+
+def Goal (n : Nat) : Prop := ∀ post, ⦃post⦄ loop n ⦃⇓_ => post⦄
+
+end LetBinding

tests/bench/mvcgen/sym/lib/VCGen.lean

@@ -720,12 +720,22 @@ The function performs the following steps in order:
 5. **Proj/beta reduction**: Reduce `Prod.fst`/`Prod.snd` projections and beta redexes in
    both `H` and `T` (e.g., `(fun _ => T, Q.snd).fst s` → `T`).
 6. **Syntactic rfl**: If `T` is not a `PredTrans.apply`, try closing by `SPred.entails.refl`.
-7. **Let-zeta**: Zeta-reduce let-expressions in the program head.
+7. **Let-hoisting**: Hoist let-expressions from the program head to the goal target.
+7a. **Let-zeta/intro**: If the target starts with `let`, zeta immediately if duplicable, else
+    introduce into the local context via `introsSimp`.
+7b. **Fvar zeta**: Unfold local let-bound fvars on demand when they appear as the program head.
 8. **Iota reduction**: Reduce matchers/recursors with concrete discriminants.
 9. **ite/dite/match splitting**: Apply the appropriate split backward rule.
 10. **Spec application**: Look up a registered `@[spec]` theorem (triple or simp) and apply
     its cached backward rule.
 -/
+
+private meta def isDuplicable (e : Expr) : Bool := match e with
+  | .bvar .. | .mvar .. | .fvar .. | .const .. | .lit .. | .sort .. => true
+  | .mdata _ e | .proj _ _ e => isDuplicable e
+  | .lam .. | .forallE .. | .letE .. => false
+  | .app .. => e.isAppOf ``OfNat.ofNat
+
 meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
   let target ← goal.getType
   trace[Elab.Tactic.Do.vcgen] "target: {target}"
@@ -738,6 +748,19 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
     let IntrosResult.goal _ goal ← introsSimp goal | throwError "Failed to introduce binders for {target}"
     return .goals [goal]
 
+  if target.isLet then
+    if isDuplicable target.letValue! then
+      trace[Elab.Tactic.Do.vcgen] "let-zeta-dup: {target.letName!}"
+      -- Zeta right away: substitute value into body with sharing
+      let target' ← Sym.instantiateRevBetaS target.letBody! #[target.letValue!]
+      return .goals [← goal.replaceTargetDefEq target']
+    else
+      trace[Elab.Tactic.Do.vcgen] "let-intro: {target.letName!}"
+      -- Introduce let binding into the local context with proper sharing
+      let IntrosResult.goal _ goal ← introsSimp goal
+        | throwError "Failed to introduce let binding"
+      return .goals [goal]
+
   let f := target.getAppFn
   if f.isConstOf ``Triple then
     let goal ← tripleOfWP goal
@@ -807,11 +830,15 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
     let target ← mkAppS₃ ent σs H T
     goal.replaceTargetDefEq target
 
-  -- Zeta let-expressions
-  if let .letE _x _ty val body _nonDep := f then
-    let body' ← Sym.instantiateRevBetaS body #[val]
-    let e' ← mkAppRevS body' e.getAppRevArgs
-    return .goals [← replaceProgDefEq e']
+  -- Let-expressions: hoist to top of goal
+  if let .letE x ty val body nonDep := f then
+    trace[Elab.Tactic.Do.vcgen] "let-hoist: {x}"
+    let e' ← mkAppRevS body e.getAppRevArgs  -- body still has #0 for the let-bound var
+    let wp' ← Sym.Internal.mkAppS₅ wpConst m ps instWP α e'
+    let T' ← mkAppNS head (args.set! 2 wp')
+    let target' ← mkAppS₃ ent σs H T'
+    let hoisted := Expr.letE x ty val target' nonDep
+    return .goals [← goal.replaceTargetDefEq hoisted]
 
   -- Split ite/dite/match
   if let some info ← liftMetaM <| Lean.Elab.Tactic.Do.getSplitInfo? e then
@@ -823,6 +850,13 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
       | throwError "Failed to apply split rule for {indentExpr e}"
     return .goals goals
 
+  -- Zeta-unfold local let bindings on demand
+  if let some fvarId := f.fvarId? then
+    if let some val ← fvarId.getValue? then
+      trace[Elab.Tactic.Do.vcgen] "fvar-zeta: {(← fvarId.getUserName)}"
+      let e' ← shareCommonInc (val.betaRev e.getAppRevArgs)
+      return .goals [← replaceProgDefEq e']
+
   -- Apply registered specifications (both triple and simp specs use cached backward rules).
   if f.isConst || f.isFVar then
     trace[Elab.Tactic.Do.vcgen] "Applying a spec for {e}. Excess args: {excessArgs}"

tests/bench/mvcgen/sym/test_vcgen.lean

@@ -35,6 +35,8 @@ set_option maxHeartbeats 10000000
     `(tactic| mvcgen') `(tactic| grind) [10]
   runBenchUsingTactic ``AddSubCancelSimp.Goal [``AddSubCancelSimp.loop, ``AddSubCancelSimp.step]
     `(tactic| mvcgen') `(tactic| grind) [10]
+  runBenchUsingTactic ``LetBinding.Goal [``LetBinding.loop, ``LetBinding.step]
+    `(tactic| mvcgen') `(tactic| grind) [10]
   runBenchUsingTactic ``GetThrowSet.Goal [``GetThrowSet.loop, ``GetThrowSet.step]
     `(tactic| mvcgen') `(tactic| sorry) [10]
   -- `mvcgen' with grind`: grind integrated into VCGen loop
@@ -76,3 +78,14 @@ example : Goal 10 := by
   mvcgen' simplifying_assumptions [Nat.add_assoc]
   case vc11 => trace_state; grind
   all_goals grind
+
+-- Verify that the let-binding code paths are exercised.
+-- `unfold` (unlike `simp only`) preserves letE nodes in the program, exercising:
+-- let-hoist, let-intro (non-duplicable value), and fvar-zeta (let-bound program head).
+-- Run with `set_option trace.Elab.Tactic.Do.vcgen true` to see the traces.
+open LetBinding in
+example : ∀ post, ⦃post⦄ step 5 ⦃⇓_ => post⦄ := by
+  unfold step
+  intro post
+  mvcgen'
+  grind