feat: mvcgen', an experimental SymM-based implementation mvcgen (#13644)
This PR adds an experimental tactic `mvcgen'` that will soon replace `mvcgen`. It has been reimplemented from the ground up using the new `SymM`-based framework for efficient symbolic evaluation and can outperform `mvcgen` by a factor of >100x for some synthetic benchmarks. `mvcgen'` aspires to be feature-complete with `mvcgen`. Known exceptions currently are join point sharing, introduction of local specs and smaller bugs. The implementation of `mvgen'` used to live in the benchmark suite for rapid prototyping; this commit merely moves it into the Lean toolchain. Doing so results in an build time instruction count increase in seemingly unrelated tests such as `elab/delayed_assign//instructions`; the reason is that the builtin elaborator attribute now pulls in substantially more import code on startup. --------- Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This commit is contained in:
Sebastian Graf
GitHub
parent
049b7ebee2
commit
422920f643
37 changed files with 263 additions and 188 deletions
|
|
@ -2302,6 +2302,10 @@ theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
|
|||
macro (name := mvcgenMacro) (priority:=low) "mvcgen" : tactic =>
|
||||
Macro.throwError "to use `mvcgen`, please include `import Std.Tactic.Do`"
|
||||
|
||||
/-- Experimental Sym-based drop-in for `mvcgen`; see `mvcgen` for documentation. -/
|
||||
macro (name := mvcgen'Macro) (priority:=low) "mvcgen'" : tactic =>
|
||||
Macro.throwError "to use `mvcgen'`, please include `import Std.Tactic.Do`"
|
||||
|
||||
/--
|
||||
`cbv` performs simplification that closely mimics call-by-value evaluation.
|
||||
It reduces terms by unfolding definitions using their defining equations and
|
||||
|
|
|
|||
|
|
@ -12,3 +12,4 @@ public import Lean.Elab.Tactic.Do.Attr
|
|||
public import Lean.Elab.Tactic.Do.LetElim
|
||||
public import Lean.Elab.Tactic.Do.Spec
|
||||
public import Lean.Elab.Tactic.Do.VCGen
|
||||
public import Lean.Elab.Tactic.Do.Internal
|
||||
|
|
|
|||
9
src/Lean/Elab/Tactic/Do/Internal.lean
Normal file
9
src/Lean/Elab/Tactic/Do/Internal.lean
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
/-
|
||||
Copyright (c) 2026 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen
|
||||
|
|
@ -4,16 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public meta import VCGen.Reduce
|
||||
public meta import VCGen.SpecDB
|
||||
public meta import VCGen.RuleConstruction
|
||||
public meta import VCGen.Context
|
||||
public meta import VCGen.Util
|
||||
public meta import VCGen.RuleCache
|
||||
public meta import VCGen.Entails
|
||||
public meta import VCGen.Solve
|
||||
public meta import VCGen.Driver
|
||||
public meta import VCGen.Frontend
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Reduce
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.RuleConstruction
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Util
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Entails
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Solve
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Driver
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Frontend
|
||||
|
||||
/-!
|
||||
The `mvcgen'` tactic, split across the modules above.
|
||||
|
|
@ -4,20 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public import Lean.Elab
|
||||
public import Lean.Meta
|
||||
public meta import Lean.Elab
|
||||
public meta import Lean.Meta
|
||||
meta import Lean.Meta.Sym.Pattern
|
||||
meta import Lean.Meta.Sym.Simp.DiscrTree
|
||||
public meta import Lean.Meta.Tactic.Grind.Main
|
||||
public meta import Lean.Elab.Tactic.Do.VCGen.Basic
|
||||
public meta import VCGen.SpecDB
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Do.VCGen.Basic
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB
|
||||
public import Lean.Meta.Sym.Apply
|
||||
public import Lean.Meta.Sym.Simp.SimpM
|
||||
public import Lean.Meta.Tactic.Grind.Types
|
||||
|
||||
open Lean Meta Elab Tactic Sym
|
||||
open Lean.Elab.Tactic.Do Lean.Elab.Tactic.Do.SpecAttr
|
||||
open Std.Do
|
||||
|
||||
namespace Lean.Elab.Tactic.Do.Internal
|
||||
|
||||
/-!
|
||||
The `VCGenM` monad: its read-only `Context` (spec database + a fixed bundle of
|
||||
pre-built `BackwardRule`s + user-customisable simp methods + pre-tactic) and
|
||||
|
|
@ -33,7 +33,7 @@ public inductive VCGen.PreTac where
|
|||
/-- Use a user-provided tactic syntax. -/
|
||||
| tactic (tac : Syntax)
|
||||
|
||||
public meta def VCGen.PreTac.isGrind : VCGen.PreTac → Bool
|
||||
public def VCGen.PreTac.isGrind : VCGen.PreTac → Bool
|
||||
| .grind .. => true
|
||||
| _ => false
|
||||
|
||||
|
|
@ -160,21 +160,23 @@ namespace VCGen
|
|||
|
||||
/-- Register a join-point `JumpSiteInfo` for the given fvar. Called when a
|
||||
`let __do_jp := …` is detected as a shared continuation. -/
|
||||
public meta def registerJP (fv : FVarId) (info : JumpSiteInfo) : _root_.VCGenM Unit :=
|
||||
public def registerJP (fv : FVarId) (info : JumpSiteInfo) : VCGenM Unit :=
|
||||
modify fun s => { s with jps := s.jps.insert fv info }
|
||||
|
||||
/-- Look up a previously-registered join point by fvar id. -/
|
||||
public meta def knownJP? (fv : FVarId) : _root_.VCGenM (Option JumpSiteInfo) :=
|
||||
public def knownJP? (fv : FVarId) : VCGenM (Option JumpSiteInfo) :=
|
||||
return (← get).jps.get? fv
|
||||
|
||||
/-- True iff fuel has been exhausted (`Fuel.limited 0`). -/
|
||||
public meta def outOfFuel : _root_.VCGenM Bool :=
|
||||
public def outOfFuel : VCGenM Bool :=
|
||||
return match (← get).fuel with | .limited 0 => true | _ => false
|
||||
|
||||
/-- Decrement remaining fuel by one. No-op when fuel is `.unlimited` or already at zero. -/
|
||||
public meta def burnOne : _root_.VCGenM Unit :=
|
||||
public def burnOne : VCGenM Unit :=
|
||||
modify fun s => { s with fuel := match s.fuel with
|
||||
| .limited (n+1) => .limited n
|
||||
| other => other }
|
||||
|
||||
end VCGen
|
||||
|
||||
end Lean.Elab.Tactic.Do.Internal
|
||||
|
|
@ -4,20 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public import Lean.Elab
|
||||
public import Lean.Meta
|
||||
public meta import Lean.Elab
|
||||
public meta import Lean.Meta
|
||||
public meta import Lean.Meta.Tactic.Grind.Main
|
||||
public meta import Lean.Meta.Tactic.Grind.Solve
|
||||
public meta import VCGen.Context
|
||||
public meta import VCGen.Util
|
||||
public meta import VCGen.Solve
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Meta
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Solve
|
||||
public import Lean.Meta.Sym.Grind
|
||||
|
||||
open Lean Meta Elab Tactic Sym
|
||||
open Lean.Elab.Tactic.Do.SpecAttr
|
||||
open Std.Do
|
||||
|
||||
namespace Lean.Elab.Tactic.Do.Internal
|
||||
|
||||
/-!
|
||||
Worklist driver for `mvcgen'`. Wraps `solve` with a queue of pending goals,
|
||||
emits VCs (or invariant holes) for those `solve` cannot decompose further,
|
||||
|
|
@ -33,7 +32,7 @@ Runs the `preTac` on the VC:
|
|||
- `.tactic`: runs the user-provided tactic on the VC, potentially emitting multiple subgoals.
|
||||
- `.none`: returns the VC as-is.
|
||||
-/
|
||||
public meta def PreTac.run : PreTac → Grind.Goal → VCGenM (List MVarId)
|
||||
public def PreTac.run : PreTac → Grind.Goal → VCGenM (List MVarId)
|
||||
| .none, goal => return [goal.mvarId]
|
||||
| .grind silent, goal => do
|
||||
let savedMCtx ← getMCtx
|
||||
|
|
@ -59,7 +58,7 @@ succeeded. Numbering is 1-based; out-of-order labelled forms (e.g. `| inv2 =>
|
|||
before `| inv1 => …`) are supported because the map is keyed by parsed number,
|
||||
not position.
|
||||
-/
|
||||
private meta def tryInlineInvariant (n : Nat) (mv : MVarId) : VCGenM Bool := do
|
||||
private def tryInlineInvariant (n : Nat) (mv : MVarId) : VCGenM Bool := do
|
||||
let some alt := (← read).invariantAlts[n]? | return false
|
||||
try
|
||||
let tac ← match alt with
|
||||
|
|
@ -87,7 +86,7 @@ each in `State.invariants` (1-based stable index) and try to inline-elaborate
|
|||
its matching user alt. Returns the remaining non-invariant subgoals for `work`
|
||||
to enqueue. Eager handling here ensures dependent VCs see `?inv` assigned by
|
||||
the time they reach `emitVC`/`preTac`. -/
|
||||
private meta def handleInvariantSubgoals (subgoals : List MVarId) : VCGenM (Array MVarId) := do
|
||||
private def handleInvariantSubgoals (subgoals : List MVarId) : VCGenM (Array MVarId) := do
|
||||
let env ← getEnv
|
||||
let mut others : Array MVarId := #[]
|
||||
for sg in subgoals do
|
||||
|
|
@ -107,7 +106,7 @@ Called when decomposing the goal further did not succeed; in this case we emit a
|
|||
Invariant subgoals are handled separately by `handleInvariantSubgoals` directly inside `work`,
|
||||
so they never reach this path.
|
||||
-/
|
||||
public meta def emitVC (goal : Grind.Goal) : VCGenM Unit := do
|
||||
public def emitVC (goal : Grind.Goal) : VCGenM Unit := do
|
||||
let goal ← (← read).preTac.processHypotheses goal
|
||||
let mut vcs := #[]
|
||||
-- `trivial`: when false, skip `repeatAndRfl` (which collapses And-chains via rfl);
|
||||
|
|
@ -124,7 +123,7 @@ public meta def emitVC (goal : Grind.Goal) : VCGenM Unit := do
|
|||
vcs := vcs.push mvarId
|
||||
modify fun s => { s with vcs := s.vcs ++ vcs }
|
||||
|
||||
public meta def work (goal : Grind.Goal) : VCGenM Unit := do
|
||||
public def work (goal : Grind.Goal) : VCGenM Unit := do
|
||||
let mvarId ← preprocessMVar goal.mvarId
|
||||
let goal := { goal with mvarId }
|
||||
let mut worklist := #[goal] -- worklist is LIFO (popped from the back)
|
||||
|
|
@ -183,7 +182,7 @@ Return the VCs and invariant goals.
|
|||
|
||||
`stepLimit?`, when `some n`, seeds the fuel counter to `n`; when `none`, fuel is unlimited.
|
||||
-/
|
||||
public meta partial def main (goal : MVarId) (ctx : Context) (stepLimit? : Option Nat := none) :
|
||||
public partial def main (goal : MVarId) (ctx : Context) (stepLimit? : Option Nat := none) :
|
||||
Grind.GrindM Result := do
|
||||
let grindGoal ← Grind.mkGoalCore goal
|
||||
let initState : State := { fuel := match stepLimit? with | some n => .limited n | none => .unlimited }
|
||||
|
|
@ -200,3 +199,5 @@ public meta partial def main (goal : MVarId) (ctx : Context) (stepLimit? : Optio
|
|||
preTacFailed := state.preTacFailed }
|
||||
|
||||
end VCGen
|
||||
|
||||
end Lean.Elab.Tactic.Do.Internal
|
||||
|
|
@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public import Lean.Elab
|
||||
public import Lean.Meta
|
||||
public meta import Lean.Elab
|
||||
public meta import Lean.Meta
|
||||
public meta import Lean.Elab.Tactic.Do.VCGen.Split
|
||||
public meta import VCGen.Context
|
||||
public meta import VCGen.Reduce
|
||||
public meta import VCGen.Util
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Util
|
||||
public import Lean.Meta.Sym.Util
|
||||
|
||||
open Lean Meta Elab Tactic Sym Sym.Internal
|
||||
open Lean.Elab.Tactic.Do.SpecAttr
|
||||
open Lean.Elab.Tactic.Do.Internal
|
||||
open Std.Do
|
||||
|
||||
/-!
|
||||
|
|
@ -23,13 +21,15 @@ Entailment-shaped goal decomposition: unfolding `Triple.of_entails_wp`, splittin
|
|||
that drives `H ⊢ₛ T` to either a closed goal or a residual.
|
||||
-/
|
||||
|
||||
namespace Lean.Elab.Tactic.Do.Internal
|
||||
|
||||
namespace VCGen
|
||||
|
||||
/--
|
||||
Unfold `⦃P⦄ x ⦃Q⦄` into `P ⊢ₛ wp⟦x⟧ Q` by applying `Tiple.of_wp`, ensuring that `PostShape.args ps`
|
||||
is reduced.
|
||||
-/
|
||||
public meta def tripleOfWP (goal : MVarId) : _root_.VCGenM MVarId := goal.withContext do
|
||||
public def tripleOfWP (goal : MVarId) : VCGenM MVarId := goal.withContext do
|
||||
let .goals [goal] ← (← read).tripleOfEntailsWPRule.applyChecked goal
|
||||
| throwError "Applying {.ofConstName ``Triple.of_entails_wp} to {goal} failed"
|
||||
goal.withContext do
|
||||
|
|
@ -39,7 +39,7 @@ public meta def tripleOfWP (goal : MVarId) : _root_.VCGenM MVarId := goal.withCo
|
|||
goal.replaceTargetDefEq (← Sym.Internal.mkAppS₃ ent σs P Q)
|
||||
|
||||
open Lean.Elab.Tactic.Do in
|
||||
public meta def solveExceptCondsEntails (goal : MVarId) : _root_.VCGenM (Option MVarId) := goal.withContext do
|
||||
public def solveExceptCondsEntails (goal : MVarId) : VCGenM (Option MVarId) := goal.withContext do
|
||||
let target ← goal.getType
|
||||
let_expr ent@ExceptConds.entails ps P Q := target | return none
|
||||
let P ← reduceHead P
|
||||
|
|
@ -56,7 +56,7 @@ public meta def solveExceptCondsEntails (goal : MVarId) : _root_.VCGenM (Option
|
|||
return some goal
|
||||
|
||||
open Lean.Elab.Tactic.Do in
|
||||
public meta def solvePostCondEntails (goal : MVarId) : _root_.VCGenM (Option (List MVarId)) := goal.withContext do
|
||||
public def solvePostCondEntails (goal : MVarId) : VCGenM (Option (List MVarId)) := goal.withContext do
|
||||
let target ← goal.getType
|
||||
let_expr PostCond.entails _α _ps _P _Q := target | return none
|
||||
-- Try closing the whole entailment by reflexivity first.
|
||||
|
|
@ -88,7 +88,7 @@ then peel a leading `SPred.pure (σ::σs) φ s` from each side of `⊢ₛ` via
|
|||
Performs the pure-cons cleanup at the exact iteration the state variable is introduced,
|
||||
so the goal stays in canonical form throughout the eta-expansion loop.
|
||||
-/
|
||||
public meta def consIntroAndSimpStep (goal : MVarId) : VCGenM (Option MVarId) := do
|
||||
public def consIntroAndSimpStep (goal : MVarId) : VCGenM (Option MVarId) := do
|
||||
let ctx ← read
|
||||
let .goals [g'] ← ctx.entailsConsIntroRule.applyChecked goal | return none
|
||||
let mut goal ← introsSimp g' m!"after applying {.ofConstName ``SPred.entails_cons_intro}"
|
||||
|
|
@ -98,7 +98,7 @@ public meta def consIntroAndSimpStep (goal : MVarId) : VCGenM (Option MVarId) :=
|
|||
goal := g''
|
||||
return some goal
|
||||
|
||||
public meta def neededStateIntro (thm : SpecTheoremNew) (goal : MVarId) (excessArgs : Array Expr) : VCGenM (Option MVarId) := do
|
||||
public def neededStateIntro (thm : SpecTheoremNew) (goal : MVarId) (excessArgs : Array Expr) : VCGenM (Option MVarId) := do
|
||||
let .triple potential := thm.kind | return none
|
||||
let mut n := potential - excessArgs.size
|
||||
if n = 0 then return none
|
||||
|
|
@ -121,7 +121,7 @@ Break down `H ⊢ₛ T` as far as possible, reporting `none` when no progress wa
|
|||
5. If either `T` was pure `⌜φ₂⌝` (and `H` was not), we turn `T.down` into `φ₂`.
|
||||
(NB: If `H` was pure, then we have already lifted `φ₁` to the local context.)
|
||||
-/
|
||||
public meta def solveSPredEntails (goal : MVarId) : VCGenM (Option MVarId) := goal.withContext do
|
||||
public def solveSPredEntails (goal : MVarId) : VCGenM (Option MVarId) := goal.withContext do
|
||||
let_expr SPred.entails _σs H T := (← goal.getType) | return none
|
||||
let mut progress := false
|
||||
let mut goal := goal
|
||||
|
|
@ -189,3 +189,5 @@ public meta def solveSPredEntails (goal : MVarId) : VCGenM (Option MVarId) := go
|
|||
return none
|
||||
|
||||
end VCGen
|
||||
|
||||
end Lean.Elab.Tactic.Do.Internal
|
||||
|
|
@ -4,25 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public import Lean.Elab
|
||||
public import Lean.Meta
|
||||
public import Lean.Parser
|
||||
public meta import Lean.Elab
|
||||
public meta import Lean.Meta
|
||||
public meta import Lean.Meta.Tactic.Grind.Main
|
||||
public meta import Lean.Meta.Tactic.Grind.Solve
|
||||
public meta import Lean.Elab.Tactic.Do.VCGen.Basic
|
||||
public meta import Lean.Elab.Tactic.Do.LetElim
|
||||
public meta import Lean.Elab.Tactic.Do.VCGen.SuggestInvariant
|
||||
public meta import Lean.Elab.Tactic.Do.VCGen
|
||||
meta import Lean.Elab.Tactic.Grind
|
||||
public meta import VCGen.Context
|
||||
public meta import VCGen.Driver
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Do.VCGen.SuggestInvariant
|
||||
public import Lean.Elab.Tactic.Do.VCGen
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Driver
|
||||
public import Lean.Meta.Sym.Simp.Attr
|
||||
public import Lean.Meta.Sym.Simp.ControlFlow
|
||||
public import Lean.Meta.Sym.Simp.EvalGround
|
||||
public import Lean.Meta.Sym.Simp.Forall
|
||||
public import Lean.Meta.Sym.Simp.Rewrite
|
||||
public import Lean.Meta.Sym.Simp.Simproc
|
||||
import Lean.Elab.Tactic.Grind.Main
|
||||
|
||||
open Lean Parser Meta Elab Tactic Sym
|
||||
open Lean.Elab.Tactic.Do Lean.Elab.Tactic.Do.SpecAttr
|
||||
open Std.Do
|
||||
|
||||
namespace Lean.Elab.Tactic.Do.Internal
|
||||
|
||||
/-!
|
||||
`mvcgen'` tactic frontend: parse the user-facing argument syntax into a
|
||||
`VCGen.Context`, run `VCGen.main`, and replace the main goal with the
|
||||
|
|
@ -37,7 +38,7 @@ spec theorems and simp lemmas. Follows the same approach as
|
|||
`Lean.Elab.Tactic.Do.VCGen.mkSpecContext`: each entry is first tried as a spec theorem,
|
||||
and on failure falls back to a simp/unfold lemma processed via `mkSimpContext`.
|
||||
-/
|
||||
public meta def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : TacticM VCGen.Context := do
|
||||
public def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : TacticM VCGen.Context := do
|
||||
let mut specThms ← getSpecTheorems
|
||||
let mut simpStuff := #[]
|
||||
let mut starArg := false
|
||||
|
|
@ -139,24 +140,18 @@ public meta def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : Tacti
|
|||
|
||||
end VCGen
|
||||
|
||||
syntax (name := mvcgen') "mvcgen'" optConfig
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
|
||||
(invariantAlts)?
|
||||
(&" simplifying_assumptions" (ppSpace colGt ident)? (" [" ident,* "]")?)?
|
||||
(&" with " tactic)? : tactic
|
||||
|
||||
/-- Warn about `mvcgen'` config options that are accepted by the parser but currently
|
||||
ignored at runtime. As more options gain implementation support, drop their checks
|
||||
here. Options with implemented semantics (`trivial`, `elimLets`, `stepLimit`,
|
||||
`invariants?`) are silently accepted. -/
|
||||
private meta def warnIgnoredConfig (config : VCGen.Config) : TacticM Unit := do
|
||||
private def warnIgnoredConfig (config : VCGen.Config) : TacticM Unit := do
|
||||
let default : VCGen.Config := {}
|
||||
if config.leave != default.leave then
|
||||
logWarning "mvcgen': the `leave` config option is currently ignored."
|
||||
|
||||
/-- 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 elabGrindParams (grindStx : Syntax) (goal : MVarId) : TacticM Grind.Params := do
|
||||
private 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
|
||||
|
|
@ -167,7 +162,7 @@ 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
|
||||
private def elabSymSimpParts
|
||||
(variantId? : Option (TSyntax `ident))
|
||||
(extraIds? : Option (Array (TSyntax `ident)))
|
||||
: TacticM Sym.Simp.Methods := do
|
||||
|
|
@ -201,14 +196,14 @@ private meta def elabSymSimpParts
|
|||
post := post >> thms.rewrite
|
||||
return { pre, post }
|
||||
|
||||
private meta def elabSimplifyingAssumptions (simpClause : Syntax) : TacticM (Option Sym.Simp.Methods) := do
|
||||
private 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
|
||||
private 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]
|
||||
|
|
@ -235,7 +230,7 @@ and `none` when no `invariants` clause is provided. Errors on mixed bullet/label
|
|||
forms (one or the other is enforced by the `dotOrCase` flag in the upstream
|
||||
elaborator; we replicate that check here).
|
||||
-/
|
||||
private meta def parseInvariantMap (stx : Syntax) :
|
||||
private def parseInvariantMap (stx : Syntax) :
|
||||
TacticM (Option (Std.HashMap Nat Syntax)) := do
|
||||
let some altsStx := stx.getOptional? | return none
|
||||
-- The `invariants?` (suggest) form is handled separately by upstream's `elabInvariants`.
|
||||
|
|
@ -279,7 +274,7 @@ position (which equals the `inv<n>` tag the entry carries — `Driver.main` assi
|
|||
tags consecutively), and elaborate the matching alt. Invariants that were already
|
||||
elaborated inline by `Driver.emitVC` (tracked in `inlineHandled`) are skipped, so
|
||||
we don't warn about alts that were already consumed there. -/
|
||||
private meta def elabRemainingInvariants (alts : Std.HashMap Nat Syntax)
|
||||
private def elabRemainingInvariants (alts : Std.HashMap Nat Syntax)
|
||||
(invariants : Array MVarId) (inlineHandled : Std.HashSet Nat) : TacticM Unit := do
|
||||
let mut handled := inlineHandled
|
||||
for h : i in 0...invariants.size do
|
||||
|
|
@ -297,8 +292,11 @@ private meta def elabRemainingInvariants (alts : Std.HashMap Nat Syntax)
|
|||
unless handled.contains n do
|
||||
logWarningAt alt s!"Invariant alternative `inv{n}` does not match any invariant goal."
|
||||
|
||||
@[tactic mvcgen']
|
||||
public meta def elabMVCGen' : Tactic := fun stx => withMainContext do
|
||||
@[builtin_tactic Lean.Parser.Tactic.mvcgen']
|
||||
public def elabMVCGen' : Tactic := fun stx => withMainContext do
|
||||
if mvcgen.warning.get (← getOptions) then
|
||||
logWarningAt stx "The `mvcgen'` tactic is an experimental drop-in replacement for `mvcgen` \
|
||||
that will eventually replace it. Avoid using it in production projects."
|
||||
let config ← elabConfig stx[1]
|
||||
warnIgnoredConfig config
|
||||
let goal ← getMainGoal
|
||||
|
|
@ -329,3 +327,5 @@ public meta def elabMVCGen' : Tactic := fun stx => withMainContext do
|
|||
replaceMainGoal (invariants ++ result.vcs).toList
|
||||
if result.preTacFailed then
|
||||
throwError "pre-tactic failed on at least one VC; see errors above"
|
||||
|
||||
end Lean.Elab.Tactic.Do.Internal
|
||||
|
|
@ -4,12 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public import Lean.Meta
|
||||
public meta import Lean.Meta
|
||||
meta import Lean.Meta.Sym.Pattern
|
||||
|
||||
prelude
|
||||
public import Lean.Meta.Sym.SymM
|
||||
public import Lean.Meta.WHNF
|
||||
|
||||
open Lean Meta Sym
|
||||
|
||||
namespace Lean.Elab.Tactic.Do.Internal
|
||||
|
||||
namespace VCGen
|
||||
|
||||
/-!
|
||||
SymM-level head-redex reducer used throughout VCGen.
|
||||
-/
|
||||
|
|
@ -27,7 +32,7 @@ no further progress is made:
|
|||
|
||||
Returns `none` when no reduction was possible. Maintains maximal sharing via `shareCommonInc`.
|
||||
-/
|
||||
public meta partial def reduceHead? (e : Expr) : SymM (Option Expr) :=
|
||||
public partial def reduceHead? (e : Expr) : SymM (Option Expr) :=
|
||||
withReducible <| go none e.getAppFn e.getAppRevArgs
|
||||
where
|
||||
go lastReduction f rargs := do
|
||||
|
|
@ -59,5 +64,8 @@ public meta partial def reduceHead? (e : Expr) : SymM (Option Expr) :=
|
|||
| none => pure lastReduction
|
||||
| _ => pure lastReduction
|
||||
|
||||
public meta def reduceHead (e : Expr) : SymM Expr :=
|
||||
public def reduceHead (e : Expr) : SymM Expr :=
|
||||
return (← reduceHead? e).getD e
|
||||
|
||||
end VCGen
|
||||
end Lean.Elab.Tactic.Do.Internal
|
||||
|
|
@ -4,18 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public import Lean.Elab
|
||||
public import Lean.Meta
|
||||
public meta import Lean.Elab
|
||||
public meta import Lean.Meta
|
||||
public meta import Lean.Elab.Tactic.Do.VCGen.Split
|
||||
public meta import VCGen.Context
|
||||
public meta import VCGen.RuleConstruction
|
||||
public meta import VCGen.Util
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Do.VCGen.Split
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.RuleConstruction
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Util
|
||||
|
||||
open Lean Meta Elab Tactic Sym
|
||||
open Lean.Elab.Tactic.Do.SpecAttr
|
||||
open VCGen
|
||||
open Lean.Elab.Tactic.Do.Internal
|
||||
open Std.Do
|
||||
|
||||
/-!
|
||||
|
|
@ -23,21 +21,23 @@ open Std.Do
|
|||
`VCGen.RuleConstruction`. The cache key is `(declName, m, excessArgs.size)`.
|
||||
-/
|
||||
|
||||
namespace VCGen
|
||||
namespace Lean.Elab.Tactic.Do.Internal
|
||||
|
||||
@[inline]
|
||||
public meta def Std.HashMap.getDM [Monad m] [BEq α] [Hashable α]
|
||||
def Std.HashMap.getDM [Monad m] [BEq α] [Hashable α]
|
||||
(cache : Std.HashMap α β) (key : α) (fallback : m β) : m (β × Std.HashMap α β) := do
|
||||
if let some b := cache.get? key then
|
||||
return (b, cache)
|
||||
let b ← fallback
|
||||
return (b, cache.insert key b)
|
||||
|
||||
public meta def SpecTheoremNew.global? (specThm : SpecTheoremNew) : Option Name :=
|
||||
namespace VCGen
|
||||
|
||||
public def SpecTheoremNew.global? (specThm : SpecTheoremNew) : Option Name :=
|
||||
match specThm.proof with | .global decl => some decl | _ => none
|
||||
|
||||
/-- See the documentation for `mkBackwardRuleFromSpec` and `mkBackwardRuleFromSimpSpec`. -/
|
||||
public meta def mkBackwardRuleFromSpecCached (specThm : SpecTheoremNew) (m σs ps instWP : Expr)
|
||||
public def mkBackwardRuleFromSpecCached (specThm : SpecTheoremNew) (m σs ps instWP : Expr)
|
||||
(excessArgs : Array Expr) : VCGenM BackwardRule := do
|
||||
let mkRuleSlow := match specThm.kind with
|
||||
| .triple _ => mkBackwardRuleFromSpec specThm m σs ps instWP excessArgs
|
||||
|
|
@ -50,7 +50,7 @@ public meta def mkBackwardRuleFromSpecCached (specThm : SpecTheoremNew) (m σs p
|
|||
|
||||
open Lean.Elab.Tactic.Do in
|
||||
/-- Creates and caches a backward rule for splitting `ite`, `dite`, or matchers. -/
|
||||
public meta def mkBackwardRuleFromSplitInfoCached (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : _root_.VCGenM BackwardRule := do
|
||||
public def mkBackwardRuleFromSplitInfoCached (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : VCGenM BackwardRule := do
|
||||
let cacheKey := match splitInfo with
|
||||
| .ite .. => ``ite
|
||||
| .dite .. => ``dite
|
||||
|
|
@ -62,3 +62,5 @@ public meta def mkBackwardRuleFromSplitInfoCached (splitInfo : SplitInfo) (m σs
|
|||
return res
|
||||
|
||||
end VCGen
|
||||
|
||||
end Lean.Elab.Tactic.Do.Internal
|
||||
|
|
@ -4,21 +4,24 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public import Lean.Elab
|
||||
public import Lean.Meta
|
||||
public import Lean.Expr
|
||||
public meta import Lean.Elab
|
||||
public meta import Lean.Meta
|
||||
public meta import Lean.Meta.Match.Rewrite
|
||||
public meta import Lean.Elab.Tactic.Do.VCGen.Split
|
||||
meta import Lean.Meta.Sym.Pattern
|
||||
public meta import VCGen.Reduce
|
||||
public meta import VCGen.SpecDB
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Do.VCGen.Split
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Reduce
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB
|
||||
public import Lean.Meta.Sym.AlphaShareBuilder
|
||||
public import Lean.Meta.Sym.Apply
|
||||
public import Lean.Meta.Sym.InstantiateMVarsS
|
||||
public import Lean.Meta.Sym.Util
|
||||
|
||||
open Lean Meta Elab Tactic Sym
|
||||
open Lean.Elab.Tactic.Do.SpecAttr
|
||||
open Std.Do
|
||||
|
||||
namespace Lean.Elab.Tactic.Do.Internal
|
||||
|
||||
namespace VCGen
|
||||
|
||||
/-!
|
||||
Construction of `BackwardRule`s from `SpecTheoremNew`s and split info. Pure
|
||||
`SymM` — no knowledge of `VCGenM`. The `VCGenM` cache wrappers live in
|
||||
|
|
@ -26,13 +29,13 @@ Construction of `BackwardRule`s from `SpecTheoremNew`s and split info. Pure
|
|||
-/
|
||||
|
||||
/-- 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 :=
|
||||
private 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 :=
|
||||
private def extractProgFromGoal (goal : Expr) : Expr :=
|
||||
goal.getArg! 2 |>.getArg! 2 |>.getArg! 4
|
||||
|
||||
/--
|
||||
|
|
@ -121,7 +124,7 @@ prf : ∀ (α : Type) (x : StateT Nat Id α) (β : Type) (f : α → StateT Nat
|
|||
We are still investigating how to get rid of more kernel unfolding overhead, such as for `wp` and
|
||||
`List.rec`.
|
||||
-/
|
||||
public meta def mkBackwardRuleFromSpec (specThm : SpecTheoremNew) (m σs ps instWP : Expr) (excessArgs : Array Expr) : SymM BackwardRule := do
|
||||
public 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.
|
||||
-- In order for the backward rule to apply, we need to instantiate both `m` and `ps` with the ones
|
||||
|
|
@ -236,7 +239,7 @@ For example, `MonadState.get.eq_1 : get = self.1` with `m = StateT σ m'` yields
|
|||
that rewrites `wp⟦get⟧` to `wp⟦MonadStateOf.get⟧` (after instance synthesis + projection
|
||||
reduction + unfoldReducible).
|
||||
-/
|
||||
public meta def mkBackwardRuleFromSimpSpec (specThm : SpecTheoremNew) (m σs ps instWP : Expr)
|
||||
public def mkBackwardRuleFromSimpSpec (specThm : SpecTheoremNew) (m σs ps instWP : Expr)
|
||||
(excessArgs : Array Expr) : SymM BackwardRule := do
|
||||
let preprocessExpr : Expr → SymM Expr := shareCommon <=< liftMetaM ∘ unfoldReducible
|
||||
let wpType ← liftMetaM <| Meta.inferType instWP
|
||||
|
|
@ -303,7 +306,7 @@ Uses `SplitInfo.withAbstract` to open fvars for the split, then `SplitInfo.split
|
|||
to build the splitting proof. Hypothesis types are discovered via `rwIfOrMatcher` inside
|
||||
the splitter telescope.
|
||||
-/
|
||||
public meta def mkBackwardRuleForSplit (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : SymM BackwardRule := do
|
||||
public def mkBackwardRuleForSplit (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : SymM BackwardRule := do
|
||||
let preprocessExpr : Expr → SymM Expr := shareCommon <=< liftMetaM ∘ unfoldReducible
|
||||
let wpType ← liftMetaM <| Meta.inferType instWP
|
||||
let us := wpType.getAppFn.constLevels!
|
||||
|
|
@ -349,3 +352,6 @@ public meta def mkBackwardRuleForSplit (splitInfo : SplitInfo) (m σs ps instWP
|
|||
let prf ← instantiateMVars prf
|
||||
let res ← abstractMVars prf
|
||||
mkBackwardRuleFromExpr res.expr res.paramNames.toList
|
||||
|
||||
end VCGen
|
||||
end Lean.Elab.Tactic.Do.Internal
|
||||
|
|
@ -4,22 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public import Lean.Elab
|
||||
public import Lean.Meta
|
||||
public meta import Lean.Elab
|
||||
public meta import Lean.Meta
|
||||
public meta import Lean.Meta.Match.Rewrite
|
||||
public meta import Lean.Elab.Tactic.Do.VCGen.Split
|
||||
public meta import VCGen.Context
|
||||
public meta import VCGen.Reduce
|
||||
public meta import VCGen.Util
|
||||
public meta import VCGen.RuleCache
|
||||
public meta import VCGen.Entails
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Entails
|
||||
public import Lean.Meta.Sym.InstantiateS
|
||||
|
||||
open Lean Meta Elab Tactic Sym Sym.Internal
|
||||
open Lean.Elab.Tactic.Do.SpecAttr
|
||||
open Lean.Elab.Tactic.Do.Internal
|
||||
open Std.Do
|
||||
|
||||
namespace Lean.Elab.Tactic.Do.Internal
|
||||
|
||||
|
||||
/-!
|
||||
The main `solve` step. Runs once per worklist iteration and either fully
|
||||
|
|
@ -44,14 +42,14 @@ public inductive SolveResult where
|
|||
/-- Successfully decomposed the goal. These are the subgoals. -/
|
||||
| goals (subgoals : List MVarId)
|
||||
|
||||
private meta def isDuplicable (e : Expr) : Bool := match e with
|
||||
private 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
|
||||
|
||||
/-- Strategy 1: introduce binders if the target is a `∀`. -/
|
||||
private meta def tryForallIntro (goal : MVarId) (target : Expr) :
|
||||
private def tryForallIntro (goal : MVarId) (target : Expr) :
|
||||
VCGenM (Option SolveResult) := do
|
||||
unless target.isForall do return none
|
||||
return some <| .goals [← introsSimp goal m!"foralls in `solve`"]
|
||||
|
|
@ -65,7 +63,7 @@ at the point where the upstream `mvcgen.onJoinPoint` would set up shared-continu
|
|||
proof construction. That port (Phase 6 of the plan) is not yet done; we throw an
|
||||
explicit error here so that enabling `jp := true` is honest about the gap rather
|
||||
than silently ignored. -/
|
||||
private meta def tryLetIntro (goal : MVarId) (target : Expr) :
|
||||
private def tryLetIntro (goal : MVarId) (target : Expr) :
|
||||
VCGenM (Option SolveResult) := do
|
||||
unless target.isLet do return none
|
||||
if (← read).useJP && Lean.Elab.Tactic.Do.isJP target.letName! then
|
||||
|
|
@ -84,14 +82,14 @@ private meta def tryLetIntro (goal : MVarId) (target : Expr) :
|
|||
return some <| .goals [← introsSimp goal m!"let-intro: {target.letName!}"]
|
||||
|
||||
/-- Strategy 2: unfold a `Triple` target into the underlying `P ⊢ₛ wp⟦x⟧ Q`. -/
|
||||
private meta def tryTripleUnfold (goal : MVarId) (target : Expr) :
|
||||
private def tryTripleUnfold (goal : MVarId) (target : Expr) :
|
||||
VCGenM (Option SolveResult) := do
|
||||
unless target.getAppFn.isConstOf ``Triple do return none
|
||||
let goal ← tripleOfWP goal
|
||||
return some <| .goals [goal]
|
||||
|
||||
/-- Strategy 4: eta-expand a lambda RHS via `entails_cons_intro`. -/
|
||||
private meta def tryTargetLambdaIntro (goal : MVarId) (T : Expr) :
|
||||
private def tryTargetLambdaIntro (goal : MVarId) (T : Expr) :
|
||||
VCGenM (Option SolveResult) := do
|
||||
unless T.isLambda do return none
|
||||
let .goals [goal] ← (← read).entailsConsIntroRule.applyChecked goal
|
||||
|
|
@ -99,7 +97,7 @@ private meta def tryTargetLambdaIntro (goal : MVarId) (T : Expr) :
|
|||
return some <| .goals [goal]
|
||||
|
||||
/-- Strategy 5: head-reduce `H` and/or `T` and replace the target if either side reduced. -/
|
||||
private meta def tryHeadReduceHT (goal : MVarId) (ent σs H T : Expr) :
|
||||
private def tryHeadReduceHT (goal : MVarId) (ent σs H T : Expr) :
|
||||
VCGenM (Option SolveResult) := do
|
||||
let H? ← reduceHead? H
|
||||
let T? ← reduceHead? T
|
||||
|
|
@ -110,7 +108,7 @@ private meta def tryHeadReduceHT (goal : MVarId) (ent σs H T : Expr) :
|
|||
/-- Strategy 6: when the target's RHS isn't `wp⟦e⟧ Q s₁ ... sₙ`, attempt syntactic
|
||||
reflexivity, fall back to `solveSPredEntails`, otherwise classify as
|
||||
`.noProgramFoundInTarget`. -/
|
||||
private meta def tryRflOrSPred (goal : MVarId) (ent σs H T : Expr) :
|
||||
private def tryRflOrSPred (goal : MVarId) (ent σs H T : Expr) :
|
||||
VCGenM SolveResult := do
|
||||
trace[Elab.Tactic.Do.vcgen] "Trying rfl {goal}"
|
||||
if ← withAssignableSyntheticOpaque <| isDefEqS H T then
|
||||
|
|
@ -122,7 +120,7 @@ private meta def tryRflOrSPred (goal : MVarId) (ent σs H T : Expr) :
|
|||
return .noProgramFoundInTarget T
|
||||
|
||||
/-- Replace the program in `goal`'s target with `e'` (which must be definitionally equal). -/
|
||||
private meta def replaceProgDefEq (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
|
||||
private def replaceProgDefEq (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
|
||||
(wpConst m ps instWP α e' : Expr) : VCGenM MVarId := do
|
||||
let wp ← Sym.Internal.mkAppS₅ wpConst m ps instWP α e'
|
||||
let T ← mkAppNS head (args.set! 2 wp)
|
||||
|
|
@ -130,7 +128,7 @@ private meta def replaceProgDefEq (goal : MVarId) (head H σs ent : Expr) (args
|
|||
goal.replaceTargetDefEq target
|
||||
|
||||
/-- Hoist a `letE` from the program head to the goal target. -/
|
||||
private meta def tryLetHoist (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
|
||||
private def tryLetHoist (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
|
||||
(wpConst m ps instWP α e f : Expr) : VCGenM (Option SolveResult) := do
|
||||
let .letE x ty val body nonDep := f | return none
|
||||
trace[Elab.Tactic.Do.vcgen] "let-hoist: {x}"
|
||||
|
|
@ -143,7 +141,7 @@ private meta def tryLetHoist (goal : MVarId) (head H σs ent : Expr) (args : Arr
|
|||
|
||||
/-- Split an `ite`/`dite`/match program head, or iota-reduce if the discriminant is
|
||||
constructor-shaped. Returns `none` when the program isn't a split. -/
|
||||
private meta def trySplit (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
|
||||
private def trySplit (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
|
||||
(wpConst m ps instWP α e : Expr) (excessArgs : Array Expr) : VCGenM (Option SolveResult) := do
|
||||
let some info ← liftMetaM <| Lean.Elab.Tactic.Do.getSplitInfo? e | return none
|
||||
-- Try iota reduction first (reduces matcher/recursor with concrete discriminant)
|
||||
|
|
@ -156,7 +154,7 @@ private meta def trySplit (goal : MVarId) (head H σs ent : Expr) (args : Array
|
|||
return some <| .goals goals
|
||||
|
||||
/-- Zeta-unfold a local `let`-bound fvar that appears as the program head. -/
|
||||
private meta def tryFvarZeta (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
|
||||
private def tryFvarZeta (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
|
||||
(wpConst m ps instWP α e f : Expr) : VCGenM (Option SolveResult) := do
|
||||
let some fvarId := f.fvarId? | return none
|
||||
let some val ← fvarId.getValue? | return none
|
||||
|
|
@ -167,7 +165,7 @@ private meta def tryFvarZeta (goal : MVarId) (head H σs ent : Expr) (args : Arr
|
|||
/-- Look up a registered `@[spec]` theorem for the program head and apply its cached
|
||||
backward rule. Falls back to `.noSpecFoundForProgram` / `.noStrategyForProgram` when no
|
||||
spec applies. -/
|
||||
private meta def applySpec (goal : MVarId) (e : Expr) (excessArgs : Array Expr)
|
||||
private def applySpec (goal : MVarId) (e : Expr) (excessArgs : Array Expr)
|
||||
(m σs ps instWP : Expr) : VCGenM SolveResult := do
|
||||
let f := e.getAppFn
|
||||
if f.isConst || f.isFVar then
|
||||
|
|
@ -210,7 +208,7 @@ The function performs the following steps in order:
|
|||
10. **Spec application**: Look up a registered `@[spec]` theorem (triple or simp) and apply
|
||||
its cached backward rule.
|
||||
-/
|
||||
public meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
|
||||
public def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
|
||||
let target ← goal.getType
|
||||
trace[Elab.Tactic.Do.vcgen] "🎯 Target: {target}"
|
||||
-- Phase 1: simplify `target` until it is of the form `H ⊢ₛ T`.
|
||||
|
|
@ -265,3 +263,5 @@ public meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext d
|
|||
applySpec goal e excessArgs m σs ps instWP
|
||||
|
||||
end VCGen
|
||||
|
||||
end Lean.Elab.Tactic.Do.Internal
|
||||
|
|
@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public import Lean.Elab
|
||||
public import Lean.Meta
|
||||
public meta import Lean.Elab
|
||||
public meta import Lean.Meta
|
||||
meta import Lean.Meta.Sym.Pattern
|
||||
meta import Lean.Meta.Sym.Simp.DiscrTree
|
||||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Do.Attr
|
||||
public import Lean.Meta.Sym.Pattern
|
||||
import Lean.Meta.Sym.Simp.DiscrTree
|
||||
public import Lean.Meta.DiscrTree.Util
|
||||
|
||||
open Lean Meta Elab Tactic Sym
|
||||
open Lean.Elab.Tactic.Do.SpecAttr
|
||||
|
|
@ -59,7 +59,7 @@ public structure SpecTheoremNew where
|
|||
priority : Nat := eval_prio default
|
||||
deriving Inhabited
|
||||
|
||||
public meta instance : BEq SpecTheoremNew where
|
||||
public instance : BEq SpecTheoremNew where
|
||||
beq thm₁ thm₂ := thm₁.proof == thm₂.proof
|
||||
|
||||
/--
|
||||
|
|
@ -72,7 +72,7 @@ This method applies `congrFun` for each leading forall to reduce the equation to
|
|||
values of type `m α`, introducing fresh metavariables for the extra arguments.
|
||||
The number of extra args is stored in `SpecTheoremKind.simp etaArgs`.
|
||||
-/
|
||||
public meta def SpecTheoremNew.instantiate (specThm : SpecTheoremNew) :
|
||||
public def SpecTheoremNew.instantiate (specThm : SpecTheoremNew) :
|
||||
MetaM (Array Expr × Array BinderInfo × Expr × Expr) := do
|
||||
let (xs, bs, eqPrf, eqType) ← specThm.proof.instantiate
|
||||
let .simp etaArgs := specThm.kind | return (xs, bs, eqPrf, eqType)
|
||||
|
|
@ -89,12 +89,12 @@ public structure SpecTheoremsNew where
|
|||
erased : PHashSet SpecProof := {}
|
||||
deriving Inhabited
|
||||
|
||||
public meta def mkTriplePatternFromExpr (expr : Expr) (levelParams : List Name := []) : SymM Pattern := do
|
||||
public def mkTriplePatternFromExpr (expr : Expr) (levelParams : List Name := []) : SymM Pattern := do
|
||||
Prod.fst <$> Sym.mkPatternFromExprWithKey expr levelParams fun type => do
|
||||
let_expr Triple _m _ps _inst _α prog _P _Q := type | throwError "conclusion is not a Triple {indentExpr type}"
|
||||
return (prog, ())
|
||||
|
||||
public meta def mkSpecTheoremNew (proof : SpecProof) (prio : Nat) : SymM SpecTheoremNew := do
|
||||
public def mkSpecTheoremNew (proof : SpecProof) (prio : Nat) : SymM SpecTheoremNew := do
|
||||
-- cf. mkSimpTheoremCore
|
||||
let (levelParams, expr) ← proof.getProof
|
||||
let type ← Meta.inferType expr
|
||||
|
|
@ -130,7 +130,7 @@ This function takes a pattern (keyed on the LHS), the equation type `eqTy`, and:
|
|||
|
||||
Returns the eta-expanded pattern and the number of extra args (0 if no expansion needed).
|
||||
-/
|
||||
private meta def etaExpandEqPattern (pattern : Sym.Pattern) (eqTy : Expr) : Sym.Pattern × Nat :=
|
||||
private def etaExpandEqPattern (pattern : Sym.Pattern) (eqTy : Expr) : Sym.Pattern × Nat :=
|
||||
if !eqTy.isForall then (pattern, 0)
|
||||
else
|
||||
-- Collect forall domains from eqTy
|
||||
|
|
@ -160,7 +160,7 @@ For unfold equations of class projections (e.g., `MonadState.modifyGet.eq_1`), t
|
|||
may be between functions rather than values. In that case, the pattern is eta-expanded
|
||||
so the discrimination tree key includes all arguments.
|
||||
-/
|
||||
public meta def mkSpecTheoremNewFromSimpDecl? (declName : Name) (prio : Nat) : MetaM (Option SpecTheoremNew) := do
|
||||
public def mkSpecTheoremNewFromSimpDecl? (declName : Name) (prio : Nat) : MetaM (Option SpecTheoremNew) := do
|
||||
let (pattern, (eqTy, rhs)) ← Sym.mkPatternFromDeclWithKey declName fun body => do
|
||||
let_expr Eq eqTy lhs rhs := body | throwError "conclusion is not an equality{indentExpr body}"
|
||||
return (lhs, (eqTy, rhs))
|
||||
|
|
@ -174,7 +174,7 @@ public meta def mkSpecTheoremNewFromSimpDecl? (declName : Name) (prio : Nat) : M
|
|||
if etaArgs == 0 && pattern.pattern == rhs then return none
|
||||
return some { pattern, proof := .global declName, kind := .simp etaArgs, priority := prio }
|
||||
|
||||
public meta def migrateSpecTheoremsDatabase (database : SpecTheorems) (simpThms : SimpTheorems) :
|
||||
public def migrateSpecTheoremsDatabase (database : SpecTheorems) (simpThms : SimpTheorems) :
|
||||
SymM SpecTheoremsNew := do
|
||||
let mut specs : DiscrTree SpecTheoremNew := DiscrTree.empty
|
||||
for spec in database.specs.values do
|
||||
|
|
@ -211,12 +211,14 @@ public meta def migrateSpecTheoremsDatabase (database : SpecTheorems) (simpThms
|
|||
Look up `SpecTheoremNew`s in the `@[spec]` database.
|
||||
Takes all specs that match the given program `e` and sorts by descending priority.
|
||||
-/
|
||||
public meta def SpecTheoremsNew.findSpecs (database : SpecTheoremsNew) (e : Expr) :
|
||||
public def SpecTheoremsNew.findSpecs (database : SpecTheoremsNew) (e : Expr) :
|
||||
SymM (Except (Array SpecTheoremNew) SpecTheoremNew) := do
|
||||
let e ← instantiateMVars e
|
||||
let e ← shareCommon e
|
||||
let candidates := Sym.getMatch database.specs e
|
||||
if h : candidates.size = 1 then return .ok candidates[0]
|
||||
if h : candidates.size = 1 then
|
||||
have : 0 < candidates.size := h ▸ Nat.zero_lt_one
|
||||
return .ok candidates[0]
|
||||
-- It appears that insertion sort is *much* faster than qsort here.
|
||||
let candidates := candidates.insertionSort (·.priority > ·.priority)
|
||||
for spec in candidates do
|
||||
|
|
@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
public import Lean.Meta
|
||||
public meta import Lean.Meta
|
||||
meta import Lean.Meta.Sym.Pattern
|
||||
meta import Lean.Meta.Sym.Simp.DiscrTree
|
||||
public meta import Lean.Meta.Sym.Util
|
||||
public meta import Lean.Meta.Tactic.Grind.Main
|
||||
public meta import Lean.Meta.Tactic.Grind.Solve
|
||||
public meta import VCGen.Context
|
||||
public meta import VCGen.Reduce
|
||||
|
||||
prelude
|
||||
public import Lean.Meta.Tactic.Grind.Main
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
|
||||
public import Lean.Elab.Tactic.Do.Internal.VCGen.Reduce
|
||||
public import Lean.Meta.Sym.AlphaShareBuilder
|
||||
public import Lean.Meta.Sym.Intro
|
||||
public import Lean.Meta.Sym.Simp.Telescope
|
||||
public import Lean.Meta.Sym.Util
|
||||
|
||||
open Lean Meta Sym
|
||||
open Std.Do
|
||||
|
|
@ -24,6 +24,8 @@ generalization of `applyRflAndAndIntro`. None of these know anything about
|
|||
`SPred` entailment specifically.
|
||||
-/
|
||||
|
||||
namespace Lean.Elab.Tactic.Do.Internal
|
||||
|
||||
/--
|
||||
`VCGenM` wrapper around `BackwardRule.apply`. Behaves identically to
|
||||
`rule.apply goal` unless the application fails and `Context.debug` is on.
|
||||
|
|
@ -35,8 +37,11 @@ the missing reduction.
|
|||
`ruleDesc?` describes the rule for debug output. When `none`, the description
|
||||
is reconstructed from `rule.expr.getAppFn` — works for the common case of a
|
||||
constant rule. Pass a custom message for dynamically-built rules.
|
||||
|
||||
Designed for dot notation: `rule.applyChecked goal`. Requires
|
||||
`open Lean.Elab.Tactic.Do.Internal` in scope so that the dot lookup resolves.
|
||||
-/
|
||||
public meta def _root_.Lean.Meta.Sym.BackwardRule.applyChecked (rule : BackwardRule) (goal : MVarId)
|
||||
public def Lean.Meta.Sym.BackwardRule.applyChecked (rule : BackwardRule) (goal : MVarId)
|
||||
(ruleDesc? : Option MessageData := none) : VCGenM ApplyResult := do
|
||||
let r ← rule.apply goal
|
||||
match r with
|
||||
|
|
@ -65,23 +70,26 @@ public meta def _root_.Lean.Meta.Sym.BackwardRule.applyChecked (rule : BackwardR
|
|||
namespace VCGen
|
||||
|
||||
open Sym Sym.Internal
|
||||
open Lean.Elab.Tactic.Do.Internal
|
||||
|
||||
public meta def simpTargetTelescope (mvarId : MVarId) : VCGenM (MVarId × Bool) := do
|
||||
public def simpTargetTelescope (mvarId : MVarId) : VCGenM (MVarId × Bool) := do
|
||||
let some methods := (← read).hypSimpMethods | return (mvarId, false)
|
||||
let target ← mvarId.getType
|
||||
let simpState := (← get).simpState
|
||||
let methods := { methods with pre := Sym.Simp.simpTelescope }
|
||||
let (result, simpState') ← Sym.Simp.SimpM.run (Sym.Simp.simp target) methods {} simpState
|
||||
modify fun s => { s with simpState := simpState' }
|
||||
let mvarId ← match result with
|
||||
| .rfl .. => pure (mvarId, false)
|
||||
| .step newTarget proof .. => pure (← mvarId.replaceTargetEq newTarget proof, true)
|
||||
match result with
|
||||
| .rfl .. => return (mvarId, false)
|
||||
| .step newTarget proof .. =>
|
||||
let mvarId' ← mvarId.replaceTargetEq newTarget proof
|
||||
return (mvarId', true)
|
||||
|
||||
/--
|
||||
Simplify the forall telescope of the target using `Sym.Simp.simpTelescope`,
|
||||
then introduce all binders via `Sym.intros`.
|
||||
-/
|
||||
public meta def introsSimp (mvarId : MVarId) (errorMsg : MessageData) : VCGenM MVarId := do
|
||||
public def introsSimp (mvarId : MVarId) (errorMsg : MessageData) : VCGenM MVarId := do
|
||||
let (mvarId, progress) ← simpTargetTelescope mvarId
|
||||
match ← Sym.intros mvarId with
|
||||
| .failed =>
|
||||
|
|
@ -98,7 +106,7 @@ contains stale proof data (the contradiction proof targets the parent's mvar, no
|
|||
In that case, restore the pre-internalization state so each child can discover the contradiction
|
||||
independently and construct its own proof via `closeGoal`.
|
||||
-/
|
||||
public meta def PreTac.processHypotheses (preTac : PreTac) (goal : Grind.Goal) : VCGenM Grind.Goal := do
|
||||
public def PreTac.processHypotheses (preTac : PreTac) (goal : Grind.Goal) : VCGenM Grind.Goal := do
|
||||
if preTac.isGrind then
|
||||
Grind.processHypotheses goal
|
||||
else
|
||||
|
|
@ -110,7 +118,7 @@ exactly the conjuncts that could not be solved.
|
|||
This procedure may assign metavariables in `e₁`/`e₂`, for example for `e = ?m` it will assign
|
||||
`?m := e`.
|
||||
-/
|
||||
public meta partial def repeatAndRfl (goal : MVarId) : VCGenM (Option MVarId) :=
|
||||
public partial def repeatAndRfl (goal : MVarId) : VCGenM (Option MVarId) :=
|
||||
goal.withContext do
|
||||
let ctx ← read
|
||||
let ty ← instantiateMVars (← goal.getType)
|
||||
|
|
@ -145,3 +153,4 @@ public meta partial def repeatAndRfl (goal : MVarId) : VCGenM (Option MVarId) :=
|
|||
return some goal
|
||||
|
||||
end VCGen
|
||||
end Lean.Elab.Tactic.Do.Internal
|
||||
|
|
@ -425,3 +425,12 @@ A hint tactic that expands to `mvcgen invariants?`.
|
|||
-/
|
||||
syntax (name := mvcgenHint) "mvcgen?" optConfig
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")? : tactic
|
||||
|
||||
-- Prototypical Sym-based variant of `mvcgen`; see `mvcgen` for documentation.
|
||||
-- Same surface syntax modulo `vcAlts`, replaced by `simplifying_assumptions … with …`.
|
||||
@[tactic_alt Lean.Parser.Tactic.mvcgen'Macro]
|
||||
syntax (name := mvcgen') "mvcgen'" optConfig
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
|
||||
(invariantAlts)?
|
||||
(&" simplifying_assumptions" (ppSpace colGt ident)? (" [" ident,* "]")?)?
|
||||
(&" with " tactic)? : tactic
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import Lean
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||||
|
||||
|
|
|
|||
|
|
@ -4,9 +4,6 @@ open System Lake DSL
|
|||
package mvcgen_bench where
|
||||
precompileModules := true
|
||||
|
||||
lean_lib VCGen where
|
||||
srcDir := "lib"
|
||||
|
||||
lean_lib Baseline where
|
||||
srcDir := "lib"
|
||||
|
||||
|
|
|
|||
|
|
@ -4,6 +4,8 @@ MWE: `mvcgen'` loses precondition facts in postcondition entailment VCs.
|
|||
import Cases
|
||||
import Driver
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
open Lean Std Do
|
||||
|
||||
@[irreducible] def myFun (n : Nat) : StateM Nat Nat := return n
|
||||
|
|
|
|||
|
|
@ -3,10 +3,11 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
module
|
||||
import Lean
|
||||
import Std
|
||||
import VCGen
|
||||
import Std.Tactic.Do
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
/-!
|
||||
# Do-logic tests for `mvcgen'`
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ Authors: Sebastian Graf
|
|||
import Cases
|
||||
import Driver
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
/-!
|
||||
# VCGen Test Suite
|
||||
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ Authors: Sebastian Graf
|
|||
import Cases.AddSubCancel
|
||||
import Driver
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
|
||||
open AddSubCancel
|
||||
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ Authors: Sebastian Graf
|
|||
import Cases.AddSubCancelDeep
|
||||
import Driver
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
|
||||
open AddSubCancelDeep
|
||||
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ Authors: Sebastian Graf
|
|||
import Cases.AddSubCancelSimp
|
||||
import Driver
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
|
||||
open AddSubCancelSimp
|
||||
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ Authors: Sebastian Graf
|
|||
import Cases.GetThrowSet
|
||||
import Driver
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
|
||||
open GetThrowSet
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,8 @@
|
|||
import Cases.GetThrowSet
|
||||
import Driver
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
|
||||
open GetThrowSet
|
||||
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ Authors: Sebastian Graf
|
|||
import Cases.MatchIota
|
||||
import Driver
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
|
||||
open MatchIota
|
||||
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ Authors: Sebastian Graf
|
|||
import Cases.PurePrecond
|
||||
import Driver
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
|
||||
open PurePrecond
|
||||
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ Authors: Sebastian Graf
|
|||
import Cases.ReaderState
|
||||
import Driver
|
||||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
|
||||
open ReaderState
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue