test: add iota reduction via reduceRecMatcher? to sym-based mvcgen' (#13100)

This PR adds iota reduction to the sym-based `mvcgen'` tactic by calling
`reduceRecMatcher?` before falling back to the match split backward
rule.
When a matcher/recursor has a concrete discriminant, it is reduced
directly
instead of constructing and applying a splitting backward rule, which is
significantly faster for benchmarks like `MatchIota` (previously
`MatchSplit`)
where `loop n` unrolls into `n` nested matches with known `Nat`
discriminants.

The old `MatchSplit` test case (concrete discriminants) is renamed to
`MatchIota`
and a new `MatchSplit` test case with symbolic discriminants (matching
on state)
is added to keep exercising the split backward rule code path.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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

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

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

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

@@ -3,7 +3,7 @@ import VCGen
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
-namespace MatchSplitState
+namespace MatchIota
 
 set_option mvcgen.warning false
 
@@ -24,18 +24,17 @@ theorem Spec.get_M :
     ⦃fun s => Q.1 s s⦄ get (m := M) ⦃Q⦄ := by
   mvcgen
 
-/-- Matches on state `s` — the discriminant IS the excess state arg. -/
-def step : M Unit := do
+def step (v : Nat) : M Unit := do
   let s ← get
-  match s with
-  | 0 => throw "s is zero"
-  | n+1 => set n
+  match v with
+  | 0 => throw "v is zero"
+  | n+1 => set (s + n + 1); let s ← get; set (s - n)
 
 def loop (n : Nat) : M Unit := do
   match n with
   | 0 => pure ()
-  | n+1 => step; loop n
+  | n+1 => step n; loop n
 
-def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = n⌝⦄ loop n ⦃⇓_ s => ⌜s = 0⌝⦄
+def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s = n⌝⦄
 
-end MatchSplitState
+end MatchIota

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

@@ -24,17 +24,18 @@ theorem Spec.get_M :
     ⦃fun s => Q.1 s s⦄ get (m := M) ⦃Q⦄ := by
   mvcgen
 
-def step (v : Nat) : M Unit := do
+/-- Matches on state `s` — the discriminant IS the excess state arg. -/
+def step : M Unit := do
   let s ← get
-  match v with
-  | 0 => throw "v is zero"
-  | n+1 => set (s + n + 1); let s ← get; set (s - n)
+  match s with
+  | 0 => throw "s is zero"
+  | n+1 => set n
 
 def loop (n : Nat) : M Unit := do
   match n with
   | 0 => pure ()
-  | n+1 => step n; loop n
+  | n+1 => step; loop n
 
-def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s = n⌝⦄
+def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = n⌝⦄ loop n ⦃⇓_ s => ⌜s = 0⌝⦄
 
 end MatchSplit

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

@@ -838,18 +838,24 @@ meta def solve (item : WorkItem) : VCGenM SolveResult := item.mvarId.withContext
   let f := e.getAppFn
   withTraceNode `Elab.Tactic.Do.vcgen (msg := fun _ => return m!"Program: {e}") do
 
+  -- Replace the program in the goal with `e'` (which must be definitionally equal).
+  let replaceProgDefEq (e' : Expr) : VCGenM MVarId := do
+    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
+    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
-    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 goal ← goal.replaceTargetDefEq target
-    return .goals [item.withMVarId goal]
+    return .goals [item.withMVarId (← replaceProgDefEq e')]
 
   -- Split ite/dite/match
   if let some info ← liftMetaM <| Lean.Elab.Tactic.Do.getSplitInfo? e then
+    -- Try iota reduction first (reduces matcher/recursor with concrete discriminant)
+    if let some e' ← liftMetaM <| reduceRecMatcher? e then
+      return .goals [item.withMVarId (← replaceProgDefEq (← shareCommonInc e'))]
     -- Internalize pending hypotheses before forking
     let item ← internalizePending item
     let rule ← mkBackwardRuleFromSplitInfoCached info m σs ps instWP excessArgs

tests/bench/mvcgen/sym/test_vcgen.lean

@@ -19,8 +19,8 @@ Each case exercises a different aspect of the VC generation:
 - `PurePrecond`: Pure hypotheses `⌜φ⌝` in preconditions
 - `ReaderState`: `ReaderT`/`StateM` combination
 - `DiteSplit`: Dependent if-then-else (`if h : cond then ...`)
-- `MatchSplit`: Pattern matching in monadic programs
-- `MatchSplitState`: Match on state variable (discriminant = excess state arg)
+- `MatchIota`: Pattern matching with concrete discriminants (iota-reduced, no split)
+- `MatchSplit`: Pattern matching with symbolic discriminant (state), exercising match split
 -/
 
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
@@ -57,8 +57,8 @@ open ReaderState in
 open DiteSplit in
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10]
 
-open MatchSplit in
+open MatchIota in
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10]
 
-open MatchSplitState in
+open MatchSplit in
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind) [10]

tests/bench/mvcgen/sym/vcgen_match_split.lean

@@ -3,11 +3,11 @@ Copyright (c) 2026 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
-import Cases.MatchSplit
+import Cases.MatchIota
 import Driver
 
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
-open MatchSplit
+open MatchIota
 
 set_option maxRecDepth 10000
 set_option maxHeartbeats 10000000