diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Split.lean b/src/Lean/Elab/Tactic/Do/VCGen/Split.lean index 4f2ea0d45a..557c50539c 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen/Split.lean +++ b/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] diff --git a/tests/bench/mvcgen/sym/cases/Cases.lean b/tests/bench/mvcgen/sym/cases/Cases.lean index 1bb1551ac5..daa1c76683 100644 --- a/tests/bench/mvcgen/sym/cases/Cases.lean +++ b/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 diff --git a/tests/bench/mvcgen/sym/cases/Cases/DiteSplit.lean b/tests/bench/mvcgen/sym/cases/Cases/DiteSplit.lean new file mode 100644 index 0000000000..488f8a0532 --- /dev/null +++ b/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 diff --git a/tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean b/tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean new file mode 100644 index 0000000000..5a873ab2b4 --- /dev/null +++ b/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 diff --git a/tests/bench/mvcgen/sym/cases/Cases/MatchSplitState.lean b/tests/bench/mvcgen/sym/cases/Cases/MatchSplitState.lean new file mode 100644 index 0000000000..66384168cf --- /dev/null +++ b/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 diff --git a/tests/bench/mvcgen/sym/lakefile.lean b/tests/bench/mvcgen/sym/lakefile.lean index c1af299fcf..5cf7aea63a 100644 --- a/tests/bench/mvcgen/sym/lakefile.lean +++ b/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] diff --git a/tests/bench/mvcgen/sym/lib/VCGen.lean b/tests/bench/mvcgen/sym/lib/VCGen.lean index 466cc90610..9e3c5eba44 100644 --- a/tests/bench/mvcgen/sym/lib/VCGen.lean +++ b/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}" diff --git a/tests/bench/mvcgen/sym/test_vcgen.lean b/tests/bench/mvcgen/sym/test_vcgen.lean index 658b7aad23..5bd5aa9817 100644 --- a/tests/bench/mvcgen/sym/test_vcgen.lean +++ b/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] diff --git a/tests/bench/mvcgen/sym/vcgen_match_split.lean b/tests/bench/mvcgen/sym/vcgen_match_split.lean new file mode 100644 index 0000000000..2ff6170430 --- /dev/null +++ b/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]