From b626c6d326043613ba296ef9869c19148c4f4297 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 11 Mar 2026 01:15:04 +0800 Subject: [PATCH] test: apply simp theorems in SymM mvcgen' (#12872) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds support for simp/equational spec theorems in the SymM-based `mvcgen'` tactic, catching up with a feature that the original `mvcgen` has supported for a long time. Users can write `@[spec] theorem : get (m := StateT σ m) = fun s => pure (s, s) := rfl` instead of manually specifying equivalent Hoare triples. The equational form is more concise and natural for specs that simply unfold definitions. The universe level normalization (`normalizeLevelsExpr`) applied in `work` and the backward rule constructors is a workaround; ideally this should be integrated into `preprocessMVar`/`preprocessExpr` in the SymM framework so all users benefit. Changes: - Add `SpecTheoremKind` to distinguish triple vs simp specs in `SpecTheoremNew` - Add `mkSpecTheoremNewFromSimpDecl?` to create spec entries from equational lemmas, filtering no-op equations - Add `mkBackwardRuleFromSimpSpec` to build backward rules via `Eq.mpr`/`congrArg`, with instance synthesis, projection reduction, and `unfoldReducible` on the RHS - Migrate simp theorems from `SimpTheorems` database during `migrateSpecTheoremsDatabase` - Normalize universe levels so structural matching in `BackwardRule.apply` succeeds when `max u v` vs `max v u` arise from different code paths - Simplify `mkSpecContext` by removing the mock `simp` context construction - Use `mkBackwardRuleFromExpr` instead of `mkAuxLemma` for triple specs, since the proof may contain free variables from the goal context - Add `AddSubCancelSimp` benchmark case and test exercising the simp spec code path - Change `AddSubCancel` spec proofs from `mvcgen` to `mvcgen'` (dogfooding) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 --- tests/bench/mvcgen/sym/cases/Cases.lean | 1 + .../mvcgen/sym/cases/Cases/AddSubCancel.lean | 4 +- .../sym/cases/Cases/AddSubCancelSimp.lean | 36 +++ tests/bench/mvcgen/sym/lakefile.lean | 2 +- tests/bench/mvcgen/sym/lib/VCGen.lean | 273 ++++++++++++------ tests/bench/mvcgen/sym/test_vcgen.lean | 4 + .../mvcgen/sym/vcgen_add_sub_cancel_simp.lean | 16 + 7 files changed, 242 insertions(+), 94 deletions(-) create mode 100644 tests/bench/mvcgen/sym/cases/Cases/AddSubCancelSimp.lean create mode 100644 tests/bench/mvcgen/sym/vcgen_add_sub_cancel_simp.lean diff --git a/tests/bench/mvcgen/sym/cases/Cases.lean b/tests/bench/mvcgen/sym/cases/Cases.lean index be56bafc73..1bb1551ac5 100644 --- a/tests/bench/mvcgen/sym/cases/Cases.lean +++ b/tests/bench/mvcgen/sym/cases/Cases.lean @@ -1,5 +1,6 @@ import Cases.AddSubCancel import Cases.AddSubCancelDeep +import Cases.AddSubCancelSimp import Cases.GetThrowSet import Cases.PurePrecond import Cases.ReaderState diff --git a/tests/bench/mvcgen/sym/cases/Cases/AddSubCancel.lean b/tests/bench/mvcgen/sym/cases/Cases/AddSubCancel.lean index 49c186b0e9..0084e199c1 100644 --- a/tests/bench/mvcgen/sym/cases/Cases/AddSubCancel.lean +++ b/tests/bench/mvcgen/sym/cases/Cases/AddSubCancel.lean @@ -14,12 +14,12 @@ set_option mvcgen.warning false @[spec high] theorem Spec.MonadState_get {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond σ (.arg σ ps)} : ⦃fun s => Q.fst s s⦄ get (m := StateT σ m) ⦃Q⦄ := by - mvcgen + mvcgen' @[spec high] theorem Spec.MonadStateOf_set {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond PUnit (.arg σ ps)} {s : σ} : ⦃fun _ => Q.fst ⟨⟩ s⦄ set (m := StateT σ m) s ⦃Q⦄ := by - mvcgen + mvcgen' def step (v : Nat) : StateM Nat Unit := do let s ← get diff --git a/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelSimp.lean b/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelSimp.lean new file mode 100644 index 0000000000..28f11ae4db --- /dev/null +++ b/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelSimp.lean @@ -0,0 +1,36 @@ +import Lean +import VCGen + +open Lean Meta Elab Tactic Sym Std Do SpecAttr + +namespace AddSubCancelSimp + +set_option mvcgen.warning false + +-- Same benchmark as `AddSubCancel` but using simp spec equations instead of triple specs +-- for `get` and `set`. This exercises the `reduceSimpSpec` + `replaceTargetEq` code path. + +@[spec high] +theorem Spec.MonadState_get {m} [Monad m] {σ} : + get (m := StateT σ m) = fun s => pure (s, s) := by + rfl + +@[spec high] +theorem Spec.MonadStateOf_set {m} [Monad m] {σ} {s : σ} : + set (m := StateT σ m) s = fun _ => pure (⟨⟩, s) := by + rfl + +def step (v : Nat) : StateM Nat Unit := do + let s ← get + set (s + v) + let s ← get + set (s - v) + +def loop (n : Nat) : StateM Nat Unit := do + match n with + | 0 => pure () + | n+1 => step n; loop n + +def Goal (n : Nat) : Prop := ∀ post, ⦃post⦄ loop n ⦃⇓_ => post⦄ + +end AddSubCancelSimp diff --git a/tests/bench/mvcgen/sym/lakefile.lean b/tests/bench/mvcgen/sym/lakefile.lean index a46bf7614b..c1af299fcf 100644 --- a/tests/bench/mvcgen/sym/lakefile.lean +++ b/tests/bench/mvcgen/sym/lakefile.lean @@ -18,7 +18,7 @@ lean_lib Cases where @[default_target] lean_lib VCGenBench where - roots := #[`vcgen_add_sub_cancel, `vcgen_add_sub_cancel_deep, + 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] moreLeanArgs := #["--tstack=100000000"] diff --git a/tests/bench/mvcgen/sym/lib/VCGen.lean b/tests/bench/mvcgen/sym/lib/VCGen.lean index d6a0ef01e2..466cc90610 100644 --- a/tests/bench/mvcgen/sym/lib/VCGen.lean +++ b/tests/bench/mvcgen/sym/lib/VCGen.lean @@ -19,73 +19,42 @@ open Lean Parser Meta Elab Tactic Sym open Lean.Elab.Tactic.Do.SpecAttr open Std.Do --- Normally, we'd support the following two specs by unfolding: - -@[spec] -theorem Spec.monadLift_trans [Monad o] [WPMonad o ps] [MonadLift n o] [MonadLiftT m n] (x : m α) : - ⦃wp⟦MonadLift.monadLift (m := n) (n := o) (monadLift x)⟧ Q⦄ (MonadLiftT.monadLift x : o α) ⦃Q⦄ := SPred.entails.rfl - -@[spec] -theorem Spec.monadLift_refl [WP m ps] (x : m α) : - ⦃wp⟦x⟧ Q⦄ (monadLift (n := m) x) ⦃Q⦄ := SPred.entails.rfl - -@[spec] -theorem Spec.MonadState_get_StateT {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond σ (.arg σ ps)} : - ⦃fun s => Q.fst s s⦄ get (m := StateT σ m) ⦃Q⦄ := by - simp only [Triple, WP.get_MonadState, WP.get_StateT, SPred.entails.refl] - -@[spec] -theorem Spec.MonadState_get_ExceptT [Monad m] [MonadStateOf σ m] [WP m ps] : - ⦃wp⟦monadLift (n := ExceptT ε m) (get : m σ)⟧ Q⦄ (get : ExceptT ε m σ) ⦃Q⦄ := SPred.entails.rfl - -@[spec] -theorem Spec.MonadState_get_ReaderT [Monad m] [MonadStateOf σ m] [WP m ps] : - ⦃wp⟦monadLift (n := ReaderT ε m) (get : m σ)⟧ Q⦄ (get : ReaderT ε m σ) ⦃Q⦄ := SPred.entails.rfl - -@[spec] -theorem Spec.MonadStateOf_get_ExceptT [Monad m] [MonadStateOf σ m] [WP m ps] : - ⦃wp⟦monadLift (n := ExceptT ε m) (get : m σ)⟧ Q⦄ (MonadStateOf.get : ExceptT ε m σ) ⦃Q⦄ := SPred.entails.rfl - -@[spec] -theorem Spec.MonadStateOf_get_ReaderT [Monad m] [MonadStateOf σ m] [WP m ps] : - ⦃wp⟦monadLift (n := ReaderT ε m) (get : m σ)⟧ Q⦄ (MonadStateOf.get : ReaderT ε m σ) ⦃Q⦄ := SPred.entails.rfl - -@[spec] -theorem Spec.MonadStateOf_get_StateT_lift {m ps} [Monad m] [MonadStateOf σ m] [WP m ps] {Q : PostCond σ (.arg σ' ps)} : - ⦃wp⟦monadLift (n := StateT σ' m) (get : m σ)⟧ Q⦄ (MonadStateOf.get (σ := σ) : StateT σ' m σ) ⦃Q⦄ := SPred.entails.rfl - -@[spec] -theorem Spec.MonadStateOf_set_ExceptT [Monad m] [MonadStateOf σ m] [WP m ps] {s : σ} : - ⦃wp⟦monadLift (n := ExceptT ε m) (set (m := m) s)⟧ Q⦄ set (m := ExceptT ε m) s ⦃Q⦄ := SPred.entails.rfl - -@[spec] -theorem Spec.MonadStateOf_set_ReaderT [Monad m] [MonadStateOf σ m] [WP m ps] {s : σ} : - ⦃wp⟦monadLift (n := ReaderT ε m) (set (m := m) s)⟧ Q⦄ set (m := ReaderT ε m) s ⦃Q⦄ := SPred.entails.rfl - -@[spec] -theorem Spec.MonadStateOf_set_StateT_lift [Monad m] [MonadStateOf σ m] [WP m ps] {s : σ} : - ⦃wp⟦monadLift (n := StateT σ' m) (set (m := m) s)⟧ Q⦄ set (m := StateT σ' m) s ⦃Q⦄ := SPred.entails.rfl - /-! Creating backward rules for registered specifications -/ namespace Lean.Elab.Tactic.Do.SpecAttr +/-- +The kind of a spec theorem. +-/ +public inductive SpecTheoremKind where + /-- + A Hoare triple spec: `⦃P⦄ prog ⦃Q⦄`. + If `etaPotential` is non-zero, then the precondition contains meta variables that can be + instantiated after applying `mintro ∀s` `etaPotential` many times. + -/ + | triple (etaPotential : Nat := 0) + /-- + A simp/equational spec: `lhs = rhs`. + The pattern is the LHS. + When matched, the VCGen rewrites the program from `lhs` to `rhs` and continues. + -/ + | simp + deriving Inhabited + public structure SpecTheoremNew where /-- Pattern for the program expression. This is the key used in the discrimination tree. If the proof has type `∀ a b c, Triple prog P Q`, then the pattern is `prog[a:=#2, b:=#1, c:=#0]`. + For simp specs with type `∀ a b c, lhs = rhs`, the pattern is `lhs[a:=#2, b:=#1, c:=#0]`. -/ pattern : Sym.Pattern /-- The proof for the theorem. -/ proof : SpecProof - /-- - If `etaPotential` is non-zero, then the precondition contains meta variables that can be - instantiated after applying `mintro ∀s` `etaPotential` many times. - -/ - etaPotential : Nat := 0 + /-- The kind of spec theorem: triple or simp. -/ + kind : SpecTheoremKind priority : Nat := eval_prio default deriving Inhabited @@ -121,13 +90,50 @@ meta def mkSpecTheoremNew (proof : SpecProof) (prio : Nat) : SymM SpecTheoremNew let etaPotential ← computeMVarBetaPotentialForSPred xs σs P -- logInfo m!"Beta potential {etaPotential} for {P}" -- logInfo m!"mkSpecTheorem: {keys}, proof: {proof}" - return { pattern, proof, etaPotential, priority := prio } + return { pattern, proof, kind := .triple etaPotential, priority := prio } -meta def migrateSpecTheoremsDatabase (database : SpecTheorems) : SymM SpecTheoremsNew := do +/-- +Create a `SpecTheoremNew` from a simp/equational declaration `declName : ∀ xs, lhs = rhs`. +The pattern is keyed on `lhs`. +-/ +meta def mkSpecTheoremNewFromSimpDecl? (declName : Name) (prio : Nat) : MetaM (Option SpecTheoremNew) := do + let (pattern, rhs) ← Sym.mkEqPatternFromDecl declName + -- Skip no-op equations where LHS and RHS are the same after `unfoldReducible`. + -- E.g., `getThe.eq_1 : getThe σ = MonadStateOf.get` becomes a no-op because + -- `preprocessDeclPattern` unfolds `getThe` to `MonadStateOf.get`. + -- We use `==` (structural equality) rather than `isSameExpr` (pointer equality) + -- because the LHS and RHS are independently constructed. + if pattern.pattern == rhs then return none + return some { pattern, proof := .global declName, kind := .simp, priority := prio } + +meta def migrateSpecTheoremsDatabase (database : SpecTheorems) (simpThms : SimpTheorems) : + SymM SpecTheoremsNew := do let mut specs : DiscrTree SpecTheoremNew := DiscrTree.empty for spec in database.specs.values do let newSpec ← mkSpecTheoremNew spec.proof spec.priority specs := Sym.insertPattern specs newSpec.pattern newSpec + -- Migrate simp spec theorems (equational lemmas registered via `@[spec]`) + for simpThm in simpThms.post.values do + if let .decl declName .. := simpThm.origin then + try + if let some newSpec ← mkSpecTheoremNewFromSimpDecl? declName simpThm.priority then + specs := Sym.insertPattern specs newSpec.pattern newSpec + catch e => + trace[Elab.Tactic.Do.vcgen] "Failed to migrate simp spec {declName}: {e.toMessageData}" + -- Migrate definitions to unfold (registered via `attribute [spec] foo`) + for declName in simpThms.toUnfold.toList do + let eqThms ← match simpThms.toUnfoldThms.find? declName with + | some eqThms => pure eqThms + | none => + -- No explicit equational theorems stored; generate them via `getEqnsFor?` + let some eqThms ← liftMetaM <| Meta.getEqnsFor? declName | continue + pure eqThms + for eqThm in eqThms do + try + if let some newSpec ← mkSpecTheoremNewFromSimpDecl? eqThm (prio := eval_prio default) then + specs := Sym.insertPattern specs newSpec.pattern newSpec + catch e => + trace[Elab.Tactic.Do.vcgen] "Failed to migrate unfold spec {declName}/{eqThm}: {e.toMessageData}" return { database with specs } /-- @@ -144,7 +150,6 @@ meta def SpecTheoremsNew.findSpecs (database : SpecTheoremsNew) (e : Expr) : let candidates := candidates.insertionSort (·.priority > ·.priority) for spec in candidates do let some _res ← spec.pattern.match? e | continue - -- TODO: Maybe we can use _res to pre instantiate the BackwardRule? return .ok spec return .error candidates @@ -212,6 +217,18 @@ 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. @@ -293,11 +310,91 @@ meta def mkBackwardRuleFromSpec (specThm : SpecTheoremNew) (m σs ps instWP : Ex newQ := Q' -- check prf return prf + -- We use `mkBackwardRuleFromExpr` instead of `mkAuxLemma` + `mkBackwardRuleFromDecl` because + -- the proof may contain free variables from the goal context (e.g., generic `m`, `ps`), + -- which would cause `mkAuxLemma`'s `addDecl` to fail with a kernel error. + let spec ← instantiateMVars spec let res ← abstractMVars spec - let type ← preprocessExpr (← Meta.inferType res.expr) - trace[Elab.Tactic.Do.vcgen] "Type of new auxiliary spec apply theorem: {type}" - let spec ← Meta.mkAuxLemma res.paramNames.toList type res.expr - mkBackwardRuleFromDecl spec + -- Normalize levels so structural matching in `BackwardRule.apply` succeeds even when + -- different code paths produce `max u v` vs `max v u` (semantically equal but structurally not). + let expr ← normalizeLevelsExpr res.expr + mkBackwardRuleFromExpr expr res.paramNames.toList + +/-- +Create a backward rule for a simp/equational spec `∀ xs, lhs = rhs`. + +Instantiates the equation, unifies with the monad `m`, synthesizes typeclass instances, +reduces projections and applies `unfoldReducible` to the RHS. Then builds a backward rule +of the form: +``` +∀ Q s₁ ... sₙ P (h : P ⊢ₛ wp⟦rhs_reduced⟧ Q s₁ ... sₙ), P ⊢ₛ wp⟦lhs⟧ Q s₁ ... sₙ +``` +using `Eq.mpr` with a `congrArg` proof. + +For example, `MonadState.get.eq_1 : get = self.1` with `m = StateT σ m'` yields a rule +that rewrites `wp⟦get⟧` to `wp⟦MonadStateOf.get⟧` (after instance synthesis + projection +reduction + unfoldReducible). +-/ +meta 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 + let us := wpType.getAppFn.constLevels! + let u := us[0]! + let v := us[1]! + let (xs, _, eqPrf, eqType) ← specThm.proof.instantiate + let_expr Eq eqα lhs rhs := eqType + | liftMetaM <| throwError "simp spec is not an equation: {eqType}" + let α ← mkFreshExprMVar (mkSort u.succ) + unless ← isDefEqGuarded eqα (mkApp m α) do + throwError "Simp spec: could not unify equation type {eqα} with {mkApp m α}" + for x in xs do + if x.isMVar && !(← x.mvarId!.isAssigned) then + let xType ← Meta.inferType x + try liftMetaM <| Meta.synthInstance xType >>= x.mvarId!.assign catch _ => pure () + let eqPrf ← instantiateMVarsS eqPrf + let lhs ← instantiateMVarsS lhs + let rhs ← instantiateMVarsS rhs + -- Reduce projections (e.g., `inst.1` → `getThe σ` when inst is a concrete dictionary). + let rhs ← liftMetaM <| Meta.transform rhs (pre := fun e => do + if let .proj .. := e then + if let some r ← withDefault <| Meta.reduceProj? e then return .done r + return .continue) + let rhs ← shareCommon (← liftMetaM <| unfoldReducible rhs) + -- Build the backward rule + let excessArgNamesTypes ← excessArgs.mapM fun arg => + return (← mkFreshUserName `s, ← Meta.inferType arg) + let typeQ ← preprocessExpr (mkApp2 (mkConst ``PostCond [u]) α ps) + let spec ← + withLocalDeclD `Q typeQ fun Q => do + withLocalDeclsDND excessArgNamesTypes fun ss => do + let mkWpApplyQss prog := do + let wp ← Sym.Internal.mkAppS₅ (mkConst ``WP.wp [u, v]) m ps instWP α prog + let mut t ← Sym.Internal.mkAppS₄ (mkConst ``PredTrans.apply [u]) ps α wp Q + for s in ss do t ← Sym.Internal.mkAppS t s + pure t + let lhsWp ← mkWpApplyQss lhs + let rhsWp ← mkWpApplyQss rhs + let typeP ← preprocessExpr (mkApp (mkConst ``SPred [u]) σs) + withLocalDeclD `P typeP fun P => do + let conclusionType ← preprocessExpr <| mkApp3 (mkConst ``SPred.entails [u]) σs P lhsWp + let premiseType ← preprocessExpr <| mkApp3 (mkConst ``SPred.entails [u]) σs P rhsWp + withLocalDeclD `h premiseType fun h => do + -- Build: Eq.mpr (congrArg motive eqPrf) h + -- motive = fun prog => P ⊢ₛ wp⟦prog⟧ Q s₁ ... sₙ + let mα ← instantiateMVarsS (mkApp m α) + let motiveBody := mkApp3 (mkConst ``SPred.entails [u]) σs P + (mkAppN (mkApp4 (mkConst ``PredTrans.apply [u]) ps α + (mkApp5 (mkConst ``WP.wp [u, v]) m ps instWP α (.bvar 0)) Q) ss) + let motive := Expr.lam `prog mα motiveBody .default + let eqProof ← liftMetaM <| Meta.mkCongrArg motive eqPrf + let prf := mkApp4 (mkConst ``Eq.mpr [0]) conclusionType premiseType eqProof h + liftMetaM <| mkLambdaFVars (#[Q] ++ ss ++ #[P, h]) prf + let spec ← instantiateMVars spec + let res ← abstractMVars spec + -- Normalize universe levels so the backward rule's pattern matches structurally. + let expr ← normalizeLevelsExpr res.expr + mkBackwardRuleFromExpr expr res.paramNames.toList open Lean.Elab.Tactic.Do in /-- @@ -349,11 +446,10 @@ meta def mkBackwardRuleForIte (m σs ps instWP : Expr) (excessArgs : Array Expr) 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 prf ← instantiateMVars prf let res ← abstractMVars prf - let type ← preprocessExpr (← Meta.inferType res.expr) - let prf ← Meta.mkAuxLemma res.paramNames.toList type res.expr - trace[Elab.Tactic.Do.vcgen] "Type of new auxiliary spec apply theorem for `ite`: {type}" - mkBackwardRuleFromDecl prf + let expr ← normalizeLevelsExpr res.expr + mkBackwardRuleFromExpr expr res.paramNames.toList /-! VC generation @@ -407,9 +503,12 @@ meta def _root_.Std.HashMap.getDM [Monad m] [BEq α] [Hashable α] meta def SpecTheoremNew.global? (specThm : SpecTheoremNew) : Option Name := match specThm.proof with | .global decl => some decl | _ => none -/-- See the documentation for `SpecTheoremNew.mkBackwardRuleFromSpec` for more details. -/ -meta def mkBackwardRuleFromSpecCached (specThm : SpecTheoremNew) (m σs ps instWP : Expr) (excessArgs : Array Expr) : VCGenM BackwardRule := do - let mkRuleSlow := mkBackwardRuleFromSpec specThm m σs ps instWP excessArgs +/-- See the documentation for `mkBackwardRuleFromSpec` and `mkBackwardRuleFromSimpSpec`. -/ +meta 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 + | .simp => mkBackwardRuleFromSimpSpec specThm m σs ps instWP excessArgs let s ← get let some decl := SpecTheoremNew.global? specThm | mkRuleSlow let (res, specBackwardRuleCache) ← s.specBackwardRuleCache.getDM (decl, m, excessArgs.size) mkRuleSlow @@ -652,7 +751,7 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do | throwError "Failed to apply split rule for {indentExpr e}" return .goals goals - -- Apply registered specifications. + -- Apply registered specifications (both triple and simp specs use cached backward rules). if f.isConst || f.isFVar then trace[Elab.Tactic.Do.vcgen] "Applying a spec for {e}. Excess args: {excessArgs}" match ← (← read).specThms.findSpecs e with @@ -660,7 +759,6 @@ meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do | .ok thm => trace[Elab.Tactic.Do.vcgen] "Spec for {e}: {thm.proof}" let rule ← mkBackwardRuleFromSpecCached thm m σs ps instWP excessArgs - trace[Elab.Tactic.Do.vcgen] "Applying rule {indentExpr rule.pattern.pattern}\n at {indentExpr target}" let ApplyResult.goals goals ← rule.apply goal | throwError "Failed to apply rule {thm.proof} for {indentExpr e}" return .goals goals @@ -679,7 +777,15 @@ meta def emitVC (goal : MVarId) : VCGenM Unit := do modify fun s => { s with vcs := s.vcs.push goal } meta def work (goal : MVarId) : VCGenM Unit := do - let mut worklist := Std.Queue.empty.enqueue (← preprocessMVar goal) + -- Normalize universe levels (one-time, cold path) so that backward rule pattern matching + -- is structural. E.g., `max u v` and `max v u` get a canonical representation. + let goal ← do + let goal ← preprocessMVar goal + let target ← goal.getType + let target' ← normalizeLevelsExpr target + if isSameExpr target target' then pure goal + else liftMetaM <| goal.replaceTargetDefEq target' + let mut worklist := Std.Queue.empty.enqueue goal -- while let some (goal, worklist') := worklist.dequeue? do repeat do let some (goal, worklist') := worklist.dequeue? | break @@ -722,13 +828,10 @@ and is more complex than necessary ATM. -/ meta def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : TacticM VCGen.Context := do let mut specThms ← getSpecTheorems - let mut simpStuff := #[] let mut starArg := false for arg in lemmas[1].getSepArgs do if arg.getKind == ``simpErase then try - -- Try and build SpecTheorems for the lemma to erase to see if it's - -- meant to be interpreted by SpecTheorems. Otherwise fall back to SimpTheorems. let specThm ← if let some fvar ← Term.isLocalIdent? arg[1] then mkSpecTheoremFromLocal fvar.fvarId! @@ -739,43 +842,31 @@ meta def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : TacticM VCGe else withRef id <| throwUnknownConstant id.getId.eraseMacroScopes specThms := specThms.erase specThm.proof - catch _ => - simpStuff := simpStuff.push ⟨arg⟩ -- simp tracks its own erase stuff + catch _ => pure () -- TODO: handle erasure of simp specs else if arg.getKind == ``simpLemma then unless arg[0].isNone && arg[1].isNone do - -- When there is ←, →, ↑ or ↓ then this is for simp - simpStuff := simpStuff.push ⟨arg⟩ - continue + throwError "← and ↑/↓ modifiers are not supported for spec lemmas" let term := arg[2] match ← Term.resolveId? term (withInfo := true) <|> Term.elabCDotFunctionAlias? ⟨term⟩ with | some (.const declName _) => - let info ← getConstInfo declName try let thm ← mkSpecTheoremFromConst declName specThms := specThms.insert thm catch _ => - simpStuff := simpStuff.push ⟨arg⟩ + -- TODO: handle user-provided simp specs + throwError "Could not build spec theorem from {declName}" | some (.fvar fvar) => - let decl ← getFVarLocalDecl (.fvar fvar) try let thm ← mkSpecTheoremFromLocal fvar specThms := specThms.insert thm catch _ => - simpStuff := simpStuff.push ⟨arg⟩ + throwError "Could not build spec theorem from local {mkFVar fvar}" | _ => withRef term <| throwError "Could not resolve {repr term}" else if arg.getKind == ``simpStar then starArg := true - simpStuff := simpStuff.push ⟨arg⟩ else throwUnsupportedSyntax - -- Build a mock simp call to build a simp context that corresponds to `simp [simpStuff]` - let stx ← `(tactic| simp +unfoldPartialApp -zeta [$(Syntax.TSepArray.ofElems simpStuff),*]) - -- logInfo s!"{stx}" - let res ← mkSimpContext stx.raw - (eraseLocal := false) - (simpTheorems := getSpecSimpTheorems) - (ignoreStarArg := ignoreStarArg) - -- trace[Elab.Tactic.Do.vcgen] "{res.ctx.simpTheorems.map (·.toUnfold.toList)}" + let simpThms ← getSpecSimpTheorems if starArg && !ignoreStarArg then let fvars ← getPropHyps for fvar in fvars do @@ -788,7 +879,7 @@ meta def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : TacticM VCGe let postCondEntailsMkRule ← mkBackwardRuleFromDecl ``PostCond.entails.mk let exceptCondsEntailsRflRule ← mkBackwardRuleFromDecl ``ExceptConds.entails.rfl let tripleOfEntailsWPRule ← mkBackwardRuleFromDecl ``Triple.of_entails_wp - let specThmsNew ← SymM.run <| migrateSpecTheoremsDatabase specThms + let specThmsNew ← SymM.run <| migrateSpecTheoremsDatabase specThms simpThms return { specThms := specThmsNew, entailsConsIntroRule, diff --git a/tests/bench/mvcgen/sym/test_vcgen.lean b/tests/bench/mvcgen/sym/test_vcgen.lean index bd53b144d0..658b7aad23 100644 --- a/tests/bench/mvcgen/sym/test_vcgen.lean +++ b/tests/bench/mvcgen/sym/test_vcgen.lean @@ -14,6 +14,7 @@ Each case exercises a different aspect of the VC generation: - `AddSubCancel`: Basic add/sub loop in `StateM` - `AddSubCancelDeep`: Same loop through a deep monad transformer stack +- `AddSubCancelSimp`: Like `AddSubCancel` but using simp/equational specs - `GetThrowSet`: Exception handling with `ExceptT`/`StateM` - `PurePrecond`: Pure hypotheses `⌜φ⌝` in preconditions - `ReaderState`: `ReaderT`/`StateM` combination @@ -30,6 +31,9 @@ open AddSubCancel in 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] + open GetThrowSet in #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10] diff --git a/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_simp.lean b/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_simp.lean new file mode 100644 index 0000000000..8bd3513656 --- /dev/null +++ b/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_simp.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.AddSubCancelSimp +import Driver + +open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr +open AddSubCancelSimp + +set_option maxRecDepth 10000 +set_option maxHeartbeats 10000000 + +#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind) + [100, 500, 1000]