test: add simplifying_assumptions clause to mvcgen' tactic (#13156)
This PR adds a `simplifying_assumptions` clause to the `mvcgen'` tactic that allows users to specify Sym.simp rewrite theorems for simplifying hypotheses during VC generation. The syntax is `mvcgen' simplifying_assumptions [thm₁, thm₂, ...]`. This replaces the previous approach of hardcoding `reassocNatAdd` in `mvcgen' with grind` mode, making hypothesis simplification user-extensible and independent of grind. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Sebastian Graf
GitHub
parent
938c19aace
commit
210d4d00fa
2 changed files with 156 additions and 144 deletions
|
|
@ -676,46 +676,66 @@ meta def mkAppNS [Monad m] [Internal.MonadShareCommon m] (f : Expr) (args : Arra
|
|||
|
||||
meta def simp (e : Expr) (methods : Sym.Simp.Methods) : VCGenM Sym.Simp.Result := do
|
||||
let simpState := (← get).simpState
|
||||
let (result, simpState') ← Sym.Simp.SimpM.run (Sym.simp e) methods {} simpState
|
||||
let (result, simpState') ← Sym.Simp.SimpM.run (Sym.Simp.simp e) methods {} simpState
|
||||
modify fun s => { s with simpState := simpState' }
|
||||
return result
|
||||
|
||||
/--
|
||||
Simplify types of not-yet-internalized hypotheses in the grind goal using `Sym.simp`.
|
||||
Only hypotheses with index `≥ grindGoal.nextDeclIdx` are simplified, since earlier ones
|
||||
have already been internalized into grind's E-graph.
|
||||
Returns the (possibly updated) `MVarId`.
|
||||
Simplify leading non-dependent forall domains in `target` using `Sym.Simp`.
|
||||
Returns `(newTarget, proof?)` where `proof : target = newTarget`, or `none` if no change.
|
||||
Skips dependent foralls (where the body references the binder).
|
||||
-/
|
||||
meta def simpNewHyps (mvarId : MVarId) (nextDeclIdx : Nat) (methods : Sym.Simp.Methods) : VCGenM MVarId := do
|
||||
mvarId.withContext do
|
||||
let lctx ← getLCtx
|
||||
let mut mvarId := mvarId
|
||||
for decl in lctx do
|
||||
-- TODO: Start this loop at index nextDeclIdx. Yields much less convenient code.
|
||||
if decl.index < nextDeclIdx then continue
|
||||
if decl.isImplementationDetail then continue
|
||||
match ← simp decl.type methods with
|
||||
| .rfl .. => pure ()
|
||||
| .step newType _proof .. =>
|
||||
mvarId ← mvarId.replaceLocalDeclDefEq decl.fvarId newType
|
||||
return mvarId
|
||||
meta partial def simpForallDomains (target : Expr) (methods : Sym.Simp.Methods) : VCGenM (Expr × Option Expr) := do
|
||||
if !target.isForall then return (target, none)
|
||||
-- Skip dependent foralls
|
||||
if target.bindingBody!.hasLooseBVar 0 then return (target, none)
|
||||
let domain := target.bindingDomain!
|
||||
let body := target.bindingBody!
|
||||
-- Simplify domain
|
||||
let (domain', domainProof?) ← match ← simp domain methods with
|
||||
| .rfl .. => pure (domain, none)
|
||||
| .step d' p .. => pure (d', some p)
|
||||
-- Recurse on body (for remaining forall domains)
|
||||
let (body', bodyProof?) ← simpForallDomains body methods
|
||||
match domainProof?, bodyProof? with
|
||||
| none, none => return (target, none)
|
||||
| _, _ =>
|
||||
let newTarget := mkForall target.bindingName! target.bindingInfo! domain' body'
|
||||
-- Build proof using implies_congr: (A → B) = (A' → B')
|
||||
let dp ← match domainProof? with | some p => pure p | none => Meta.mkEqRefl domain
|
||||
let bp ← match bodyProof? with | some p => pure p | none => Meta.mkEqRefl body
|
||||
let proof ← mkImpCongr dp bp
|
||||
return (newTarget, some proof)
|
||||
|
||||
meta def simpTargetForallDomains (mvarId : MVarId) : VCGenM MVarId := do
|
||||
let some methods := (← read).hypSimpMethods | return mvarId
|
||||
let target ← mvarId.getType
|
||||
let (newTarget, proof?) ← simpForallDomains target methods
|
||||
let mvarId ← match proof? with
|
||||
| none => pure mvarId
|
||||
| some proof =>
|
||||
mvarId.replaceTargetEq newTarget proof
|
||||
|
||||
/--
|
||||
Simplify leading forall domains in the target, then introduce all binders via `Sym.intros`.
|
||||
For each non-dependent forall `∀ (_ : A), B`, simplifies `A` using the given `Sym.Simp.Methods`
|
||||
and uses `implies_congr` to update the target before introduction.
|
||||
-/
|
||||
meta def introsSimp (mvarId : MVarId) : VCGenM IntrosResult := do
|
||||
let mvarId ← simpTargetForallDomains mvarId
|
||||
Sym.intros mvarId
|
||||
|
||||
/-- Internalize pending hypotheses into the E-graph for sharing before forking to multiple subgoals.
|
||||
Skips `simpNewHyps` so it is safe to call even when the mvar is assigned (e.g., after a
|
||||
backward rule has been applied). `simpNewHyps` will run later per-VC in `emitVC`.
|
||||
If `processHypotheses` discovers a contradiction (`inconsistent = true`), the E-graph state
|
||||
contains stale proof data (the contradiction proof targets the parent's mvar, not the children's).
|
||||
In that case, restore the pre-internalization state so each child can discover the contradiction
|
||||
independently and construct its own proof via `closeGoal`.
|
||||
-/
|
||||
meta def PreTac.processHypotheses (preTac : PreTac) (goal : Grind.Goal) : VCGenM Grind.Goal := do
|
||||
let mut goal := goal
|
||||
if let some methods := (← read).hypSimpMethods then
|
||||
let mvarId ← simpNewHyps goal.mvarId goal.nextDeclIdx methods
|
||||
goal := { goal with mvarId }
|
||||
if preTac.isGrind then
|
||||
goal ← Grind.processHypotheses goal
|
||||
return goal
|
||||
Grind.processHypotheses goal
|
||||
else
|
||||
return goal
|
||||
|
||||
/--
|
||||
The main VC generation step. Operates on a plain `MVarId` with no knowledge of grind.
|
||||
|
|
@ -747,7 +767,7 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
|
|||
-- and `T` is of the form `wp⟦e⟧ Q s₁ ... sₙ`.
|
||||
|
||||
if target.isForall then
|
||||
let IntrosResult.goal _ goal ← Sym.intros goal | throwError "Failed to introduce binders for {target}"
|
||||
let IntrosResult.goal _ goal ← introsSimp goal | throwError "Failed to introduce binders for {target}"
|
||||
return .goals [goal]
|
||||
|
||||
let f := target.getAppFn
|
||||
|
|
@ -859,7 +879,6 @@ meta def PreTac.run : PreTac → Grind.Goal → VCGenM (List MVarId)
|
|||
| .none, goal => return [goal.mvarId]
|
||||
| .grind, goal => do
|
||||
let savedMCtx ← getMCtx
|
||||
let goal ← goal.internalizeAll
|
||||
match ← goal.grind with
|
||||
| .closed => return []
|
||||
| .failed .. =>
|
||||
|
|
@ -881,6 +900,7 @@ meta def emitVC (goal : Grind.Goal) : VCGenM Unit := do
|
|||
goal.mvarId.setKind .syntheticOpaque
|
||||
modify fun s => { s with invariants := s.invariants.push goal.mvarId }
|
||||
return
|
||||
let goal ← (← read).preTac.processHypotheses goal
|
||||
let goals ← (← read).preTac.run goal
|
||||
for g in goals do g.setKind .syntheticOpaque
|
||||
modify fun s => { s with vcs := s.vcs ++ goals.toArray }
|
||||
|
|
@ -906,8 +926,8 @@ meta def work (goal : Grind.Goal) : VCGenM Unit := do
|
|||
| .goals subgoals =>
|
||||
-- In grind mode with multiple subgoals, preprocess pending hypotheses
|
||||
-- to share E-graph context before forking.
|
||||
if (← read).preTac.isGrind && subgoals.length > 1 then
|
||||
goal ← Grind.processHypotheses goal
|
||||
if subgoals.length > 1 then
|
||||
goal ← (← read).preTac.processHypotheses goal
|
||||
worklist := worklist.enqueueAll (subgoals.map ({ goal with mvarId := · }))
|
||||
|
||||
public structure Result where
|
||||
|
|
@ -923,9 +943,6 @@ internalization, avoiding O(n) re-internalization per VC.
|
|||
-/
|
||||
public meta partial def main (goal : MVarId) (ctx : Context) : Grind.GrindM Result := do
|
||||
let grindGoal ← Grind.mkGoalCore goal
|
||||
let grindGoal ← if ctx.preTac.isGrind then
|
||||
Grind.processHypotheses grindGoal
|
||||
else pure grindGoal
|
||||
let ((), state) ← StateRefT'.run (ReaderT.run (work grindGoal) ctx) {}
|
||||
_ ← state.invariants.mapIdxM fun idx mv => do
|
||||
mv.setTag (Name.mkSimple ("inv" ++ toString (idx + 1)))
|
||||
|
|
@ -1005,35 +1022,12 @@ end VCGen
|
|||
|
||||
syntax (name := mvcgen') "mvcgen'"
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
|
||||
(&" simplifying_assumptions" (ppSpace colGt ident)? (" [" ident,* "]")?)?
|
||||
(&" with " tactic)? : tactic
|
||||
|
||||
private meta def getNatLit? (e : Expr) : Option Nat := do
|
||||
let_expr OfNat.ofNat _ n _ := e | failure
|
||||
let .lit (.natVal n) := n | failure
|
||||
return n
|
||||
|
||||
/--
|
||||
A `Sym.Simp` post-simproc that reassociates Nat addition to fold nested literal additions.
|
||||
Rewrites `(a + m) + n` → `a + (m + n)` when `m` and `n` are Nat literals, using `Nat.add_assoc`.
|
||||
Since `m + n` reduces to a literal by kernel computation, this collapses chains like
|
||||
`s + 1 + 1 + 1` into `s + 3` in a single step.
|
||||
-/
|
||||
private meta def reassocNatAdd : Sym.Simp.Simproc := fun e => do
|
||||
let_expr HAdd.hAdd α _ _ inst ab n := e | return .rfl
|
||||
let_expr Nat := α | return .rfl
|
||||
let some nVal := getNatLit? n | return .rfl
|
||||
let_expr HAdd.hAdd _ _ _ _ a m := ab | return .rfl
|
||||
let some mVal := getNatLit? m | return .rfl
|
||||
-- (a + m) + n → a + (m + n), with m + n folded to a literal
|
||||
let sumExpr ← share <| toExpr (mVal + nVal)
|
||||
let result ← share <| mkApp6 (mkConst ``HAdd.hAdd [0, 0, 0]) α α α inst a sumExpr
|
||||
-- Proof: Nat.add_assoc a m n : (a + m) + n = a + (m + n)
|
||||
let proof := mkApp3 (mkConst ``Nat.add_assoc) a m n
|
||||
return .step result proof
|
||||
|
||||
/-- Parse grind configuration from the `with grind ...` clause and build `Grind.Params`.
|
||||
Overrides the internal simp step limit to accommodate large unrolled goals. -/
|
||||
private meta def mkGrindParamsFromSyntax (grindStx : Syntax) (goal : MVarId) : TacticM Grind.Params := do
|
||||
private meta def elabGrindParams (grindStx : Syntax) (goal : MVarId) : TacticM Grind.Params := do
|
||||
let `(tactic| grind $config:optConfig $[only%$only]? $[ [$grindParams:grindParam,*] ]? $[=> $_:grindSeq]?) := grindStx
|
||||
| throwUnsupportedSyntax
|
||||
let grindConfig ← elabGrindConfig config
|
||||
|
|
@ -1043,64 +1037,68 @@ private meta def mkGrindParamsFromSyntax (grindStx : Syntax) (goal : MVarId) : T
|
|||
-- unrolled goals (fails around n=400 for GetThrowSet).
|
||||
return { params with norm := ← params.norm.setConfig { params.norm.config with maxSteps := 10000000 } }
|
||||
|
||||
/--
|
||||
Build `Sym.Simp.Methods` from a variant name and extra theorems.
|
||||
Supports the anonymous (default) variant. Named variants require a public
|
||||
`elabSimpMethods` API in `Lean.Elab.Tactic.Grind.Sym` (see TODO below).
|
||||
-/
|
||||
private meta def elabSymSimpParts
|
||||
(variantId? : Option (TSyntax `ident))
|
||||
(extraIds? : Option (Array (TSyntax `ident)))
|
||||
: TacticM Sym.Simp.Methods := do
|
||||
let variantName := variantId?.map (·.getId) |>.getD .anonymous
|
||||
if !variantName.isAnonymous then
|
||||
-- TODO: `resolveExtraTheorems`, `elabVariant`, and `elabSymSimproc` in
|
||||
-- `Lean.Elab.Tactic.Grind.Sym` are module-private (non-`public section`).
|
||||
-- To support named variants here, we need a public API such as:
|
||||
-- `public def elabSymSimp (syn : Syntax) : GrindTacticM (Sym.Simp.Methods × ...)`
|
||||
-- exposed from that module, plus a lightweight `GrindTacticM` runner
|
||||
-- (the simproc elaborators only use `CoreM`/`MetaM` capabilities).
|
||||
throwError "named Sym.simp variants are not yet supported in `mvcgen'`; \
|
||||
use `mvcgen' simplifying_assumptions [thm₁, thm₂, ...]` with the default variant instead"
|
||||
-- Resolve extra theorems (local hypotheses first, then global constants)
|
||||
let mut extraThms : Array Sym.Simp.Theorem := #[]
|
||||
if let some ids := extraIds? then
|
||||
let lctx ← getLCtx
|
||||
for id in ids do
|
||||
if let some decl := lctx.findFromUserName? id.getId then
|
||||
extraThms := extraThms.push (← Sym.Simp.mkTheoremFromExpr decl.toExpr)
|
||||
else
|
||||
let declName ← realizeGlobalConstNoOverload id
|
||||
extraThms := extraThms.push (← Sym.Simp.mkTheoremFromDecl declName)
|
||||
-- Build default variant methods
|
||||
let symThms ← Sym.Simp.getSymSimpTheorems
|
||||
let pre := Sym.Simp.simpControl >> Sym.Simp.simpArrowTelescope
|
||||
let mut post : Sym.Simp.Simproc := Sym.Simp.evalGround >> symThms.rewrite
|
||||
if !extraThms.isEmpty then
|
||||
let mut thms : Sym.Simp.Theorems := {}
|
||||
for thm in extraThms do thms := thms.insert thm
|
||||
post := post >> thms.rewrite
|
||||
return { pre, post }
|
||||
|
||||
private meta def elabSimplifyingAssumptions (simpClause : Syntax) : TacticM (Option Sym.Simp.Methods) := do
|
||||
if simpClause.getNumArgs == 0 then return none
|
||||
let variantId? := if simpClause[1].getNumArgs != 0 then some ⟨simpClause[1][0]⟩ else none
|
||||
let extraIds? := if simpClause[2].getNumArgs != 0
|
||||
then some (simpClause[2][1].getSepArgs.map (⟨·⟩)) else none
|
||||
pure (some (← elabSymSimpParts variantId? extraIds?))
|
||||
|
||||
private meta def elabPreTac (goal : MVarId) (withPreTac : Syntax) : TacticM (VCGen.PreTac × Grind.Params) := do
|
||||
let mut params ← Grind.mkDefaultParams {}
|
||||
if withPreTac.getNumArgs == 0 then return (.none, params)
|
||||
let preTac := withPreTac[1]
|
||||
if preTac.getKind == ``Lean.Parser.Tactic.grind then
|
||||
params ← elabGrindParams preTac goal
|
||||
return (.grind, params)
|
||||
else
|
||||
return (.tactic preTac, params)
|
||||
|
||||
@[tactic mvcgen']
|
||||
public meta def elabMVCGen' : Tactic := fun stx => withMainContext do
|
||||
let goal ← getMainGoal
|
||||
let ctx ← VCGen.mkSpecContext stx[1]
|
||||
-- `(&" with " tactic)?` produces a nullKind node with 2 children when present;
|
||||
-- `getOptional?` requires exactly 1 child, so we check `getNumArgs` instead.
|
||||
let withTac? := if stx[2].getNumArgs != 0 then some stx[2][1] else none
|
||||
let isGrind := withTac?.any (·.getKind == ``Lean.Parser.Tactic.grind)
|
||||
let mut params ← Grind.mkDefaultParams {}
|
||||
let mut preTac : VCGen.PreTac := .none
|
||||
let mut hypSimpMethods : Option Sym.Simp.Methods := none
|
||||
if isGrind then
|
||||
params ← mkGrindParamsFromSyntax withTac?.get! goal
|
||||
preTac := .grind
|
||||
hypSimpMethods := some { post := reassocNatAdd } -- TODO: Make this user-extensible
|
||||
else if let some tac := withTac? then
|
||||
preTac := .tactic tac
|
||||
let hypSimpMethods ← elabSimplifyingAssumptions stx[2]
|
||||
let (preTac, params) ← elabPreTac goal stx[3]
|
||||
let ctx := { ctx with preTac, hypSimpMethods }
|
||||
|
||||
let result ← Grind.GrindM.run (VCGen.main goal ctx) params
|
||||
|
||||
replaceMainGoal (result.invariants ++ result.vcs).toList
|
||||
|
||||
/-!
|
||||
Local tests for faster iteration:
|
||||
-/
|
||||
|
||||
/-
|
||||
def step (lim : Nat) : ExceptT String (StateM Nat) Unit := do
|
||||
let s ← get
|
||||
if s > lim then
|
||||
throw "s is too large"
|
||||
set (s + 1)
|
||||
|
||||
def loop (n : Nat) : ExceptT String (StateM Nat) Unit := do
|
||||
match n with
|
||||
| 0 => pure ()
|
||||
| n+1 => loop n; step n
|
||||
|
||||
set_option maxRecDepth 10000
|
||||
set_option maxHeartbeats 10000000
|
||||
|
||||
-- set_option trace.Elab.Tactic.Do.vcgen true in
|
||||
set_option trace.profiler true in
|
||||
example : ⦃fun s => ⌜s = 0⌝⦄ loop 50 ⦃⇓_ s => ⌜s = 50⌝⦄ := by
|
||||
simp only [loop, step]
|
||||
mvcgen'
|
||||
-- all_goals grind
|
||||
all_goals sorry
|
||||
|
||||
set_option trace.Elab.Tactic.Do.vcgen true in
|
||||
example :
|
||||
⦃⌜True⌝⦄
|
||||
do
|
||||
let s ← get (m := ExceptT String (StateM Nat))
|
||||
if s > 20 then
|
||||
throw "s is too large"
|
||||
set (m := ExceptT String (StateM Nat)) (s + 1)
|
||||
⦃post⟨fun _r s => ⌜s ≤ 21⌝, fun _err s => ⌜s > 20⌝⟩⦄ := by
|
||||
mvcgen' <;> grind
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -28,37 +28,51 @@ open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
|
|||
set_option maxRecDepth 10000
|
||||
set_option maxHeartbeats 10000000
|
||||
|
||||
open AddSubCancel in
|
||||
#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind) [10]
|
||||
|
||||
open AddSubCancelDeep in
|
||||
#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind) [10]
|
||||
|
||||
open AddSubCancelSimp in
|
||||
#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind) [10]
|
||||
#eval do
|
||||
runBenchUsingTactic ``AddSubCancel.Goal [``AddSubCancel.loop, ``AddSubCancel.step]
|
||||
`(tactic| mvcgen') `(tactic| grind) [10]
|
||||
runBenchUsingTactic ``AddSubCancelDeep.Goal [``AddSubCancelDeep.loop, ``AddSubCancelDeep.step]
|
||||
`(tactic| mvcgen') `(tactic| grind) [10]
|
||||
runBenchUsingTactic ``AddSubCancelSimp.Goal [``AddSubCancelSimp.loop, ``AddSubCancelSimp.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
|
||||
runBenchUsingTactic ``GetThrowSet.Goal [``GetThrowSet.loop, ``GetThrowSet.step]
|
||||
`(tactic| mvcgen' with grind) `(tactic| fail) [10]
|
||||
-- `mvcgen' with grind` on AddSubCancel
|
||||
runBenchUsingTactic ``AddSubCancel.Goal [``AddSubCancel.loop, ``AddSubCancel.step]
|
||||
`(tactic| mvcgen' with grind) `(tactic| fail) [10]
|
||||
runBenchUsingTactic ``PurePrecond.Goal [``PurePrecond.loop, ``PurePrecond.step]
|
||||
`(tactic| mvcgen') `(tactic| fail) [10]
|
||||
runBenchUsingTactic ``ReaderState.Goal [``ReaderState.loop, ``ReaderState.step]
|
||||
`(tactic| mvcgen') `(tactic| sorry) [10]
|
||||
runBenchUsingTactic ``DiteSplit.Goal [``DiteSplit.loop, ``DiteSplit.step]
|
||||
`(tactic| mvcgen') `(tactic| sorry) [10]
|
||||
runBenchUsingTactic ``MatchIota.Goal [``MatchIota.loop, ``MatchIota.step]
|
||||
`(tactic| mvcgen') `(tactic| sorry) [10]
|
||||
runBenchUsingTactic ``MatchSplit.Goal [``MatchSplit.loop, ``MatchSplit.step]
|
||||
`(tactic| mvcgen') `(tactic| grind) [10]
|
||||
|
||||
-- Verify `simplifying_assumptions [Nat.add_assoc]` works end-to-end with `simp only` unfolding.
|
||||
/--
|
||||
trace: s✝ : Nat
|
||||
h✝⁹ : ¬0 < s✝
|
||||
h✝⁸ : ¬1 < s✝ + 1
|
||||
h✝⁷ : ¬2 < s✝ + 2
|
||||
h✝⁶ : ¬3 < s✝ + 3
|
||||
h✝⁵ : ¬4 < s✝ + 4
|
||||
h✝⁴ : ¬5 < s✝ + 5
|
||||
h✝³ : ¬6 < s✝ + 6
|
||||
h✝² : ¬7 < s✝ + 7
|
||||
h✝¹ : ¬8 < s✝ + 8
|
||||
h✝ : ¬9 < s✝ + 9
|
||||
⊢ ⌜s✝ = 0⌝ ⊢ₛ ⌜s✝ + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 = 10⌝
|
||||
-/
|
||||
#guard_msgs in
|
||||
open GetThrowSet in
|
||||
#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10]
|
||||
|
||||
-- Test `mvcgen' with grind`: grind integrated into VCGen loop
|
||||
open GetThrowSet in
|
||||
#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| fail) [10]
|
||||
|
||||
-- Test `mvcgen' with grind` on AddSubCancel
|
||||
open AddSubCancel in
|
||||
#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| fail) [10]
|
||||
|
||||
open PurePrecond in
|
||||
#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| fail) [10]
|
||||
|
||||
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 MatchIota in
|
||||
#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10]
|
||||
|
||||
open MatchSplit in
|
||||
#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind) [10]
|
||||
example : Goal 10 := by
|
||||
simp only [Goal, loop, step]
|
||||
mvcgen' simplifying_assumptions [Nat.add_assoc]
|
||||
case vc11 => trace_state; grind
|
||||
all_goals grind
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue