test: add dite and match splitting to sym-based MVCGen (#12903)

This PR generalizes the sym MVCGen's match splitting from `ite`-only to
`ite`, `dite`, and arbitrary matchers. Previously, only `ite` was
supported; `dite` and match expressions were rejected with an error.

`mkBackwardRuleForSplit` uses `SplitInfo.splitWith` to build the
splitting proof. Hypothesis types are discovered via `rwIfOrMatcher`
inside the splitter telescope, and `TransformAltFVars.all` provides the
proper fvars for `mkForallFVars`. Subgoal type metavariables use
`mkFreshExprSyntheticOpaqueMVar` so that `rwIfOrMatcher`'s internal
`assumption` tactic cannot assign them.

Adds `DiteSplit`, `MatchSplit`, and `MatchSplitState` test cases and a
`vcgen_match_split` benchmark.

---------

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

src/Lean/Elab/Tactic/Do/VCGen/Split.lean

@@ -51,6 +51,82 @@ def altInfos (info : SplitInfo) : Array (Nat × Expr) := match info with
   | matcher matcherApp => matcherApp.altNumParams.mapIdx fun idx numParams =>
       (numParams, matcherApp.alts[idx]!)
 
+/-- The expression represented by a `SplitInfo`. -/
+def expr : SplitInfo → Expr
+  | .ite e => e
+  | .dite e => e
+  | .matcher matcherApp => matcherApp.toExpr
+
+/--
+Introduces fvars for all varying parts of a `SplitInfo` and provides the abstract
+`SplitInfo` and fvars to the continuation.
+
+For `ite`/`dite`, introduces `c : Prop`, `dec : Decidable c`, `t : mα` (or `t : c → mα`),
+`e : mα` (or `e : ¬c → mα`).
+For `matcher`, introduces discriminant fvars and alternative fvars, builds a non-dependent
+motive `fun _ ... _ => mα`, and adjusts matcher universe levels.
+
+The abstract `SplitInfo` satisfies `abstractInfo.expr = abstractProgram`.
+
+For `matcher`, the abstract `MatcherApp` stores eta-expanded fvar alts so that
+`splitWith`/`matcherApp.transform` can `instantiateLambda` them directly (no patching needed).
+Since eta-expanded alts like `fun n => alt n` can cause expensive higher-order unification in
+backward rule patterns, callers building backward rules should eta-reduce them first (e.g.
+via `Expr.eta` on the alt arguments of `abstractInfo.expr`).
+-/
+def withAbstract {n} {α} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [Inhabited α]
+    (info : SplitInfo) (resTy : Expr)
+    (k : (abstractInfo : SplitInfo) → (splitFVars : Array Expr) → n α) : n α :=
+  match info with
+  | .ite _ =>
+    withLocalDeclD `c (mkSort 0) fun c =>
+    withLocalDeclD `dec (mkApp (mkConst ``Decidable) c) fun dec =>
+    withLocalDeclD `t resTy fun t =>
+    withLocalDeclD `e resTy fun e => do
+    let u ← liftMetaM <| getLevel resTy
+    k (.ite <| mkApp5 (mkConst ``_root_.ite [u]) resTy c dec t e) #[c, dec, t, e]
+  | .dite _ =>
+    withLocalDeclD `c (mkSort 0) fun c =>
+    withLocalDeclD `dec (mkApp (mkConst ``Decidable) c) fun dec => do
+    let tTy ← liftMetaM <| mkArrow c resTy
+    let eTy ← liftMetaM <| mkArrow (mkNot c) resTy
+    withLocalDeclD `t tTy fun t =>
+    withLocalDeclD `e eTy fun e => do
+    let u ← liftMetaM <| getLevel resTy
+    k (.dite <| mkApp5 (mkConst ``_root_.dite [u]) resTy c dec t e) #[c, dec, t, e]
+  | .matcher matcherApp => do
+    let discrNamesTypes ← matcherApp.discrs.mapIdxM fun i discr => do
+      return ((`discr).appendIndexAfter (i+1), ← liftMetaM <| inferType discr)
+    withLocalDeclsDND discrNamesTypes fun discrs => do
+    -- Non-dependent motive: fun _ ... _ => mα
+    let motive ← liftMetaM <| lambdaTelescope matcherApp.motive fun motiveArgs _ =>
+      mkLambdaFVars motiveArgs resTy
+    -- The matcher's universe levels include a `uElimPos` slot for the elimination target level.
+    -- Our abstract motive `fun _ ... _ => mα` may target a different level than the original
+    -- dependent motive, so we update `matcherLevels[uElimPos]` to `getLevel mα`.
+    let matcherLevels ← match matcherApp.uElimPos? with
+      | none => pure matcherApp.matcherLevels
+      | some pos => do
+        let uElim ← liftMetaM <| getLevel resTy
+        pure <| matcherApp.matcherLevels.set! pos uElim
+    -- Build partial application to infer alt types
+    let matcherPartial := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params
+    let matcherPartial := mkApp matcherPartial motive
+    let matcherPartial := mkAppN matcherPartial discrs
+    let origAltTypes ← liftMetaM <| inferArgumentTypesN matcherApp.alts.size matcherPartial
+    let altNamesTypes := origAltTypes.mapIdx fun i ty => ((`alt).appendIndexAfter (i+1), ty)
+    withLocalDeclsDND altNamesTypes fun alts => do
+    -- Eta-expand fvar alts so `splitWith`/`matcherApp.transform` can `instantiateLambda` them.
+    let abstractMatcherApp : MatcherApp := {
+      matcherApp with
+      matcherLevels := matcherLevels
+      discrs        := discrs
+      motive        := motive
+      alts          := (← liftMetaM <| alts.mapM etaExpand)
+      remaining     := #[]
+    }
+    k (.matcher abstractMatcherApp) (discrs ++ alts)
+
 def splitWith
   {n} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadEnv n] [MonadLog n]
   [AddMessageContext n] [MonadOptions n]

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

@@ -1,6 +1,9 @@
 import Cases.AddSubCancel
 import Cases.AddSubCancelDeep
 import Cases.AddSubCancelSimp
+import Cases.DiteSplit
 import Cases.GetThrowSet
+import Cases.MatchSplit
+import Cases.MatchSplitState
 import Cases.PurePrecond
 import Cases.ReaderState

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

@@ -0,0 +1,42 @@
+import Lean
+import VCGen
+
+open Lean Meta Elab Tactic Sym Std Do SpecAttr
+
+namespace DiteSplit
+
+set_option mvcgen.warning false
+
+abbrev M := ExceptT String <| StateM Nat
+
+@[spec high]
+theorem Spec.throw_M {e : String} :
+    ⦃Q.2.1 e⦄ throw (m := M) e ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.set_M {s : Nat} :
+    ⦃fun _ => Q.1 ⟨⟩ s⦄ set (m := M) s ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.get_M :
+    ⦃fun s => Q.1 s s⦄ get (m := M) ⦃Q⦄ := by
+  mvcgen
+
+def step (v : Nat) : M Unit := do
+  let s ← get
+  if _ : s > v then
+    throw "s is too large"
+  set (s + v)
+  let s ← get
+  set (s - v)
+
+def loop (n : Nat) : M Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step n; loop n
+
+def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s = 0⌝⦄
+
+end DiteSplit

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

@@ -0,0 +1,40 @@
+import Lean
+import VCGen
+
+open Lean Meta Elab Tactic Sym Std Do SpecAttr
+
+namespace MatchSplit
+
+set_option mvcgen.warning false
+
+abbrev M := ExceptT String <| StateM Nat
+
+@[spec high]
+theorem Spec.throw_M {e : String} :
+    ⦃Q.2.1 e⦄ throw (m := M) e ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.set_M {s : Nat} :
+    ⦃fun _ => Q.1 ⟨⟩ s⦄ set (m := M) s ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.get_M :
+    ⦃fun s => Q.1 s s⦄ get (m := M) ⦃Q⦄ := by
+  mvcgen
+
+def step (v : Nat) : 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)
+
+def loop (n : Nat) : M Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step n; loop n
+
+def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s = n⌝⦄
+
+end MatchSplit

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

@@ -0,0 +1,41 @@
+import Lean
+import VCGen
+
+open Lean Meta Elab Tactic Sym Std Do SpecAttr
+
+namespace MatchSplitState
+
+set_option mvcgen.warning false
+
+abbrev M := ExceptT String <| StateM Nat
+
+@[spec high]
+theorem Spec.throw_M {e : String} :
+    ⦃Q.2.1 e⦄ throw (m := M) e ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+theorem Spec.set_M {s : Nat} :
+    ⦃fun _ => Q.1 ⟨⟩ s⦄ set (m := M) s ⦃Q⦄ := by
+  mvcgen
+
+@[spec high]
+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
+  let s ← get
+  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; loop n
+
+def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = n⌝⦄ loop n ⦃⇓_ s => ⌜s = 0⌝⦄
+
+end MatchSplitState

tests/bench/mvcgen/sym/lakefile.lean

@@ -19,7 +19,7 @@ lean_lib Cases where
 @[default_target]
 lean_lib VCGenBench where
   roots := #[`vcgen_add_sub_cancel, `vcgen_add_sub_cancel_deep, `vcgen_add_sub_cancel_simp,
-             `vcgen_get_throw_set, `vcgen_pure_precond, `vcgen_reader_state]
+             `vcgen_get_throw_set, `vcgen_pure_precond, `vcgen_reader_state, `vcgen_match_split]
   moreLeanArgs := #["--tstack=100000000"]
 
 @[default_target]

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

@@ -155,6 +155,28 @@ meta def SpecTheoremsNew.findSpecs (database : SpecTheoremsNew) (e : Expr) :
 
 end Lean.Elab.Tactic.Do.SpecAttr
 
+
+-- Normalize universe levels in an expression so that `max u v` and `max v u` have a canonical
+-- representation. This is needed because backward rule pattern matching is structural and
+-- level expressions from different sources (e.g., instance synthesis, type inference) may have
+-- different but equivalent `max` orderings.
+meta def normalizeLevelsExpr (e : Expr) : CoreM Expr :=
+  Core.transform e (pre := fun e => do
+    match e with
+    | .sort u => return .done <| e.updateSort! u.normalize
+    | .const _ us => return .done <| e.updateConst! (us.map Level.normalize)
+    | _ => return .continue)
+
+/-- Build goal: `P ⊢ₛ wp⟦prog⟧ Q ss...`. Meant to be partially applied for convenience. -/
+private meta def mkGoal (u v : Level) (m σs ps instWP α : Expr) (ss : Array Expr) (P Q : Expr) (prog : Expr) : Expr :=
+  mkApp3 (mkConst ``SPred.entails [u]) σs P
+    (mkAppN (mkApp4 (mkConst ``PredTrans.apply [u]) ps α
+      (mkApp5 (mkConst ``WP.wp [u, v]) m ps instWP α prog) Q) ss)
+
+/-- Extract the program from a goal built by `mkGoal`. -/
+private meta def extractProgFromGoal (goal : Expr) : Expr :=
+  goal.getArg! 2 |>.getArg! 2 |>.getArg! 4
+
 /--
 Create a backward rule for the `SpecTheoremNew` that was looked up in the database.
 In order for the backward rule to apply, we need to instantiate both `m` and `ps` with the ones
@@ -217,18 +239,6 @@ prf : ∀ (α : Type) (x : StateT Nat Id α) (β : Type) (f : α → StateT Nat
 We are still investigating how to get rid of more unfolding overhead, such as for `wp` and
 `List.rec`.
 -/
-
--- Normalize universe levels in an expression so that `max u v` and `max v u` have a canonical
--- representation. This is needed because backward rule pattern matching is structural and
--- level expressions from different sources (e.g., instance synthesis, type inference) may have
--- different but equivalent `max` orderings.
-meta def normalizeLevelsExpr (e : Expr) : CoreM Expr :=
-  Core.transform e (pre := fun e => do
-    match e with
-    | .sort u => return .done <| e.updateSort! u.normalize
-    | .const _ us => return .done <| e.updateConst! (us.map Level.normalize)
-    | _ => return .continue)
-
 meta def mkBackwardRuleFromSpec (specThm : SpecTheoremNew) (m σs ps instWP : Expr) (excessArgs : Array Expr) : SymM BackwardRule := do
   let preprocessExpr : Expr → SymM Expr := shareCommon <=< liftMetaM ∘ unfoldReducible
   -- Create a backward rule for the spec we look up in the database.
@@ -398,54 +408,54 @@ meta def mkBackwardRuleFromSimpSpec (specThm : SpecTheoremNew) (m σs ps instWP
 
 open Lean.Elab.Tactic.Do in
 /--
-Creates a reusable backward rule for `ite`. It proves a theorem of the following form:
-```
-example {m} {σ} {ps} [WP m (.arg σ ps)] -- These are fixed. The other arguments are parameters of the rule:
-  {α} {c : Prop} [Decidable c] {t e : m α} {s : σ} {P : Assertion ps} {Q : PostCond α (.arg σ ps)}
-  (hthen : P ⊢ₛ wp⟦t⟧ Q s) (helse : P ⊢ₛ wp⟦e⟧ Q s)
-  : P ⊢ₛ wp⟦ite c t e⟧ Q s
-```
+Creates a reusable backward rule for splitting `ite`, `dite`, or matchers.
+
+Uses `SplitInfo.withAbstract` to open fvars for the split, then `SplitInfo.splitWith`
+to build the splitting proof. Hypothesis types are discovered via `rwIfOrMatcher` inside
+the splitter telescope.
 -/
-meta def mkBackwardRuleForIte (m σs ps instWP : Expr) (excessArgs : Array Expr) : SymM BackwardRule := do
+meta def mkBackwardRuleForSplit (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : SymM BackwardRule := do
   let preprocessExpr : Expr → SymM Expr := shareCommon <=< liftMetaM ∘ unfoldReducible
-  let prf ← do
-    let us := instWP.getAppFn.constLevels!
-    let u := us[0]!
-    let v := us[1]!
+  let us := instWP.getAppFn.constLevels!
+  let u := us[0]!
+  let v := us[1]!
+  let prf ←
     withLocalDeclD `α (mkSort u.succ) fun α => do
     let mα ← preprocessExpr <| mkApp m α
-    withLocalDeclD `c (mkSort 0) fun c => do
-    withLocalDeclD `dec (mkApp (mkConst ``Decidable) c) fun dec => do
-    withLocalDeclD `t mα fun t => do
-    withLocalDeclD `e mα fun e => do
-    let prog ← preprocessExpr (mkApp5 (mkConst ``ite [v.succ]) mα c dec t e)
-    let excessArgNamesTypes ← excessArgs.mapM fun arg =>
-      return (`s, ← Meta.inferType arg)
+    splitInfo.withAbstract mα fun abstractInfo splitFVars => do
+    -- Eta-reduce alts so the backward rule pattern uses clean fvar alts, avoiding expensive
+    -- higher-order unification. The alts are eta-expanded in `withAbstract` so that
+    -- `splitWith`/`matcherApp.transform` can `instantiateLambda` them.
+    let abstractProg := match abstractInfo with
+      | .ite e | .dite e => e
+      | .matcher matcherApp =>
+        { matcherApp with alts := matcherApp.alts.map Expr.eta }.toExpr
+    let excessArgNamesTypes ← excessArgs.mapM fun arg => return (`s, ← Meta.inferType arg)
     withLocalDeclsDND excessArgNamesTypes fun ss => do
     withLocalDeclD `P (← preprocessExpr <| mkApp (mkConst ``SPred [u]) σs) fun P => do
     withLocalDeclD `Q (← preprocessExpr <| mkApp2 (mkConst ``PostCond [u]) α ps) fun Q => do
-    let goalWithProg prog :=
-      let wp := mkApp5 (mkConst ``WP.wp [u, v]) m ps instWP α prog
-      let wpApplyQ := mkApp4 (mkConst ``PredTrans.apply [u]) ps α wp Q  -- wp⟦prog⟧ Q
-      let wpApplyQ := mkAppN wpApplyQ ss  -- wp⟦prog⟧ Q s₁ ... sₙ
-      mkApp3 (mkConst ``SPred.entails [u]) σs P wpApplyQ
-    let thenType ← mkArrow c (goalWithProg t)
-    withLocalDeclD `hthen (← preprocessExpr thenType) fun hthen => do
-    let elseType ← mkArrow (mkNot c) (goalWithProg e)
-    withLocalDeclD `helse (← preprocessExpr elseType) fun helse => do
-    let onAlt (hc : Expr) (hcase : Expr) := do
-      let res ← rwIfWith hc prog
-      -- When `rw` fails, it returns `proof? := none`. We throw an error.
-      if res.proof?.isNone then
-        throwError "`rwIfWith` failed to rewrite {indentExpr e}."
-      -- context = fun e => P ⊢ₛ wp⟦e⟧ Q s₁ ... sₙ
-      let context ← withLocalDecl `e .default mα fun e => mkLambdaFVars #[e] (goalWithProg e)
-      let res ← Simp.mkCongrArg context res
-      res.mkEqMPR hcase
-    let ht ← withLocalDecl `h .default c fun h => do mkLambdaFVars #[h] (← onAlt h (mkApp hthen h))
-    let he ← withLocalDecl `h .default (mkNot c) fun h => do mkLambdaFVars #[h] (← onAlt h (mkApp helse h))
-    let prf := mkApp5 (mkConst ``dite [0]) (goalWithProg prog) c dec ht he
-    mkLambdaFVars (#[α, c, dec, t, e] ++ ss ++ #[P, Q, hthen, helse]) prf
+    let mkGoal := mkGoal u v m σs ps instWP α ss P Q
+    -- Subgoal types are synthetic opaque metavariables, filled in the `splitWith` callback below.
+    -- Synthetic opaque so that `rwIfOrMatcher`'s `assumption` tactic cannot assign them.
+    let subgoals ← splitInfo.altInfos.mapM fun _ =>
+      liftMetaM <| mkFreshExprSyntheticOpaqueMVar (mkSort 0)
+    let namedSubgoals := subgoals.mapIdx fun i mv => ((`h).appendIndexAfter (i+1), mv)
+    withLocalDeclsDND namedSubgoals fun subgoalHyps => do
+    let prf ← liftMetaM <|
+      abstractInfo.splitWith
+        (useSplitter := true)
+        (mkGoal abstractProg)
+        (fun _name bodyType idx altFVars => do
+          let prog := extractProgFromGoal bodyType
+          let res ← rwIfOrMatcher idx prog
+          if res.proof?.isNone then
+            throwError "mkBackwardRuleForSplit: rwIfOrMatcher failed for alt {idx}\n{indentExpr prog}"
+          let boundFVars := altFVars.all
+          subgoals[idx]!.mvarId!.assign (← mkForallFVars boundFVars (mkGoal res.expr))
+          let context ← withLocalDecl `e .default mα fun e =>
+            mkLambdaFVars #[e] (mkGoal e)
+          (← Simp.mkCongrArg context res).mkEqMPR (mkAppN subgoalHyps[idx]! boundFVars))
+    mkLambdaFVars (#[α] ++ splitFVars ++ ss ++ #[P, Q] ++ subgoalHyps) prf
   let prf ← instantiateMVars prf
   let res ← abstractMVars prf
   let expr ← normalizeLevelsExpr res.expr
@@ -516,12 +526,15 @@ meta def mkBackwardRuleFromSpecCached (specThm : SpecTheoremNew) (m σs ps instW
   return res
 
 open Lean.Elab.Tactic.Do in
-/-- See the documentation for `SpecTheoremNew.mkBackwardRuleForIte` for more details. -/
+/-- Creates and caches a backward rule for splitting `ite`, `dite`, or matchers. -/
 meta def mkBackwardRuleFromSplitInfoCached (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : _root_.VCGenM BackwardRule := do
-  unless splitInfo matches .ite .. do throwError "Only `ite` is currently supported for splitting."
-  let mkRuleSlow := mkBackwardRuleForIte m σs ps instWP excessArgs
+  let cacheKey := match splitInfo with
+    | .ite .. => ``ite
+    | .dite .. => ``dite
+    | .matcher matcherApp => matcherApp.matcherName
+  let mkRuleSlow := mkBackwardRuleForSplit splitInfo m σs ps instWP excessArgs
   let s ← get
-  let (res, splitBackwardRuleCache) ← s.splitBackwardRuleCache.getDM (``ite, m, excessArgs.size) mkRuleSlow
+  let (res, splitBackwardRuleCache) ← s.splitBackwardRuleCache.getDM (cacheKey, m, excessArgs.size) mkRuleSlow
   set { s with splitBackwardRuleCache }
   return res
 
@@ -743,9 +756,8 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
     let goal ← goal.replaceTargetDefEq target
     return .goals [goal]
 
-  -- Hard-code match splitting for `ite` for now.
-  if f.isAppOf ``ite then
-    let some info ← Lean.Elab.Tactic.Do.getSplitInfo? e | return .noStrategyForProgram e
+  -- Split ite/dite/match
+  if let some info ← liftMetaM <| Lean.Elab.Tactic.Do.getSplitInfo? e then
     let rule ← mkBackwardRuleFromSplitInfoCached info m σs ps instWP excessArgs
     let ApplyResult.goals goals ← rule.apply goal
       | throwError "Failed to apply split rule for {indentExpr e}"

tests/bench/mvcgen/sym/test_vcgen.lean

@@ -18,6 +18,9 @@ Each case exercises a different aspect of the VC generation:
 - `GetThrowSet`: Exception handling with `ExceptT`/`StateM`
 - `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)
 -/
 
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
@@ -42,3 +45,12 @@ open PurePrecond in
 
 open ReaderState in
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10]
+
+open DiteSplit in
+#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10]
+
+open MatchSplit in
+#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10]
+
+open MatchSplitState in
+#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind) [10]

tests/bench/mvcgen/sym/vcgen_match_split.lean

@@ -0,0 +1,16 @@
+/-
+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 Driver
+
+open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
+open MatchSplit
+
+set_option maxRecDepth 10000
+set_option maxHeartbeats 10000000
+
+#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry)
+  [100, 500, 1000]