From 9deb9ab59d33eee741a4deb46d68bf4c67c626d2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Jan 2026 16:17:53 -0800 Subject: [PATCH] refactor: move commonly shared expressions to `SymM` (#12145) This PR moves the pre-shared commonly used expressions from `GrindM` to `SymM`. --- src/Lean/Elab/Tactic/Grind/Basic.lean | 13 ++++--- src/Lean/Meta/Sym.lean | 16 ++++---- src/Lean/Meta/Sym/Simp/ControlFlow.lean | 24 ++++++------ src/Lean/Meta/Sym/Simp/EvalGround.lean | 18 ++++----- src/Lean/Meta/Sym/SymM.lean | 50 +++++++++++++++++++++++-- src/Lean/Meta/Tactic/Grind/Main.lean | 11 +----- src/Lean/Meta/Tactic/Grind/Types.lean | 37 +----------------- 7 files changed, 87 insertions(+), 82 deletions(-) diff --git a/src/Lean/Elab/Tactic/Grind/Basic.lean b/src/Lean/Elab/Tactic/Grind/Basic.lean index 7f76cbee67..6861e4b7ba 100644 --- a/src/Lean/Elab/Tactic/Grind/Basic.lean +++ b/src/Lean/Elab/Tactic/Grind/Basic.lean @@ -16,6 +16,7 @@ open Meta structure Context extends Tactic.Context where ctx : Meta.Grind.Context + sctx : Meta.Sym.Context methods : Grind.Methods params : Grind.Params @@ -289,7 +290,7 @@ open Grind def liftGrindM (k : GrindM α) : GrindTacticM α := do let ctx ← read let s ← get - let ((a, grindState), symState) ← liftMetaM <| StateRefT'.run ((Grind.withGTransparency k) ctx.methods.toMethodsRef ctx.ctx |>.run s.grindState) s.symState + let ((a, grindState), symState) ← liftMetaM <| StateRefT'.run (((Grind.withGTransparency k) ctx.methods.toMethodsRef ctx.ctx |>.run s.grindState) ctx.sctx) s.symState modify fun s => { s with grindState, symState } return a @@ -358,12 +359,13 @@ def mkEvalTactic' (elaborator : Name) (params : Params) : TermElabM (Goal → TS let eval (goal : Goal) (stx : TSyntax `grind) : GrindM (List Goal) := do let methods ← getMethods let grindCtx ← readThe Meta.Grind.Context + let symCtx ← readThe Meta.Sym.Context let grindState ← get let symState ← getThe Sym.State -- **Note**: we discard changes to `Term.State` let (subgoals, grindState', symState') ← Term.TermElabM.run' (ctx := termCtx) (s := termState) do let (_, s) ← GrindTacticM.run - (ctx := { recover := false, methods, ctx := grindCtx, params, elaborator }) + (ctx := { recover := false, methods, ctx := grindCtx, sctx := symCtx, params, elaborator }) (s := { grindState, symState, goals := [goal] }) do evalGrindTactic stx.raw pruneSolvedGoals @@ -383,7 +385,7 @@ def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM Reconsider the option `useSorry`. -/ let params' := { params with config.useSorry := false } - let (methods, ctx, state) ← liftMetaM <| GrindM.runAtGoal mvarId params' (evalTactic? := some evalTactic) fun goal => do + let (methods, ctx, sctx, state) ← liftMetaM <| GrindM.runAtGoal mvarId params' (evalTactic? := some evalTactic) fun goal => do let a : Action := Action.intros 0 >> Action.assertAll let goals ← match (← a.run goal) with | .closed _ => pure [] @@ -392,10 +394,11 @@ def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM let ctx ← readThe Meta.Grind.Context /- Restore original config -/ let ctx := { ctx with config := params.config } + let sctx ← readThe Meta.Sym.Context let grindState ← get let symState ← getThe Sym.State - return (methods, ctx, { grindState, symState, goals }) + return (methods, ctx, sctx, { grindState, symState, goals }) let tctx ← read - k { tctx with methods, ctx, params } |>.run state + k { tctx with methods, ctx, sctx, params } |>.run state end Lean.Elab.Tactic.Grind diff --git a/src/Lean/Meta/Sym.lean b/src/Lean/Meta/Sym.lean index 3eb4d1981f..bd49ceadd3 100644 --- a/src/Lean/Meta/Sym.lean +++ b/src/Lean/Meta/Sym.lean @@ -26,11 +26,11 @@ public import Lean.Meta.Sym.Util public import Lean.Meta.Sym.Grind /-! -# Symbolic simulation support. +# Symbolic computation support. -This module provides `SymM`, a monad for implementing symbolic simulators (e.g., verification condition generators) -using Lean. The monad addresses performance issues found in symbolic simulators built on top of user-facing -tactics (e.g., `apply` and `intros`). +This module provides `SymM`, a monad for implementing symbolic computation (e.g., decision procedures and +verification condition generators) using Lean. The monad addresses performance issues found in symbolic +computation engines built on top of user-facing tactics (e.g., `apply` and `intros`). ## Overview @@ -66,14 +66,14 @@ whether `maxFVar[e]` is in `?m.lctx` — a single hash lookup, O(1). **The problem:** The `isDefEq` predicate in `MetaM` is designed for elaboration and user-facing tactics. It supports reduction, type-class resolution, and many other features that can be expensive or have -unpredictable running time. For symbolic simulation, where pattern matching is called frequently on +unpredictable running time. For symbolic computation, where pattern matching is called frequently on large ground terms, these features become performance bottlenecks. **The solution:** In `SymM`, pattern matching and definitional equality are restricted to a more syntactic, predictable subset. Key design choices: 1. **Reducible declarations are abbreviations.** Reducible declarations are eagerly expanded when indexing - terms and when entering symbolic simulation mode. During matching, we assume abbreviations have already + terms and when entering symbolic computation mode. During matching, we assume abbreviations have already been expanded. **Why `MetaM` `simp` cannot make this assumption**: The simplifier in `MetaM` is designed for interactive use, @@ -100,7 +100,7 @@ predictable subset. Key design choices: 4. **Types must be indexed.** Unlike proofs and instances, types cannot be ignored, without indexing them, pattern matching produces too many candidates. Like other abbreviations, type abbreviations are expanded. Note that given `def Foo : Type := Bla`, the terms `Foo` and `Bla` are *not* considered structurally - equal in the symbolic simulator framework. + equal in the symbolic computation framework. ### Skipping type checks on assignment @@ -118,7 +118,7 @@ so the check is almost always skipped. ### `GrindM` state -**The problem:** In symbolic simulation, we often want to discharge many goals using proof automation such +**The problem:** In symbolic computation, we often want to discharge many goals using proof automation such as `grind`. Many of these goals share very similar local contexts. If we invoke `grind` on each goal independently, we repeatedly reprocess the same hypotheses. diff --git a/src/Lean/Meta/Sym/Simp/ControlFlow.lean b/src/Lean/Meta/Sym/Simp/ControlFlow.lean index 51095c2d19..4fcc254675 100644 --- a/src/Lean/Meta/Sym/Simp/ControlFlow.lean +++ b/src/Lean/Meta/Sym/Simp/ControlFlow.lean @@ -27,16 +27,16 @@ def simpIte : Simproc := fun e => do let_expr f@ite α c _ a b := e | return .rfl match (← simp c) with | .rfl _ => - if c.isTrue then + if isSameExpr c (← getTrueExpr) then return .step a <| mkApp3 (mkConst ``ite_true f.constLevels!) α a b - else if c.isFalse then + else if isSameExpr c (← getFalseExpr) then return .step b <| mkApp3 (mkConst ``ite_false f.constLevels!) α a b else return .rfl (done := true) | .step c' h _ => - if c'.isTrue then + if isSameExpr c' (← getTrueExpr) then return .step a <| mkApp (e.replaceFn ``ite_cond_eq_true) h - else if c'.isFalse then + else if isSameExpr c' (← getFalseExpr) then return .step b <| mkApp (e.replaceFn ``ite_cond_eq_false) h else let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) c') | return .rfl @@ -56,20 +56,20 @@ def simpDIte : Simproc := fun e => do let_expr f@dite α c _ a b := e | return .rfl match (← simp c) with | .rfl _ => - if c.isTrue then + if isSameExpr c (← getTrueExpr) then let a' ← share <| a.betaRev #[mkConst ``True.intro] return .step a' <| mkApp3 (mkConst ``dite_true f.constLevels!) α a b - else if c.isFalse then + else if isSameExpr c (← getFalseExpr) then let b' ← share <| b.betaRev #[mkConst ``not_false] return .step b' <| mkApp3 (mkConst ``dite_false f.constLevels!) α a b else return .rfl (done := true) | .step c' h _ => - if c'.isTrue then + if isSameExpr c' (← getTrueExpr) then let h' ← shareCommon <| mkOfEqTrueCore c h let a ← share <| a.betaRev #[h'] return .step a <| mkApp (e.replaceFn ``dite_cond_eq_true) h - else if c'.isFalse then + else if isSameExpr c' (← getFalseExpr) then let h' ← shareCommon <| mkOfEqFalseCore c h let b ← share <| b.betaRev #[h'] return .step b <| mkApp (e.replaceFn ``dite_cond_eq_false) h @@ -94,16 +94,16 @@ def simpCond : Simproc := fun e => do let_expr f@cond α c a b := e | return .rfl match (← simp c) with | .rfl _ => - if c.isConstOf ``true then + if isSameExpr c (← getBoolTrueExpr) then return .step a <| mkApp3 (mkConst ``cond_true f.constLevels!) α a b - else if c.isConstOf ``false then + else if isSameExpr c (← getBoolFalseExpr) then return .step b <| mkApp3 (mkConst ``cond_false f.constLevels!) α a b else return .rfl (done := true) | .step c' h _ => - if c'.isConstOf ``true then + if isSameExpr c' (← getBoolTrueExpr) then return .step a <| mkApp (e.replaceFn ``Sym.cond_cond_eq_true) h - else if c'.isConstOf ``false then + else if isSameExpr c' (← getBoolFalseExpr) then return .step b <| mkApp (e.replaceFn ``Sym.cond_cond_eq_false) h else let e' := e.getBoundedAppFn 3 diff --git a/src/Lean/Meta/Sym/Simp/EvalGround.lean b/src/Lean/Meta/Sym/Simp/EvalGround.lean index 281ed53dd0..dd5597291c 100644 --- a/src/Lean/Meta/Sym/Simp/EvalGround.lean +++ b/src/Lean/Meta/Sym/Simp/EvalGround.lean @@ -344,10 +344,10 @@ abbrev evalBinPred (toValue? : Expr → Option α) (trueThm falseThm : Expr) (op let some va := toValue? a | return .rfl let some vb := toValue? b | return .rfl if op va vb then - let e ← share <| mkConst ``True + let e ← getTrueExpr return .step e (mkApp3 trueThm a b eagerReflBoolTrue) (done := true) else - let e ← share <| mkConst ``False + let e ← getFalseExpr return .step e (mkApp3 falseThm a b eagerReflBoolFalse) (done := true) def evalBitVecPred (n : Expr) (trueThm falseThm : Expr) (op : {n : Nat} → BitVec n → BitVec n → Bool) (a b : Expr) : SimpM Result := do @@ -355,10 +355,10 @@ def evalBitVecPred (n : Expr) (trueThm falseThm : Expr) (op : {n : Nat} → BitV let some vb := getBitVecValue? b | return .rfl if h : va.n = vb.n then if op va.val (h ▸ vb.val) then - let e ← share <| mkConst ``True + let e ← getTrueExpr return .step e (mkApp4 trueThm n a b eagerReflBoolTrue) (done := true) else - let e ← share <| mkConst ``False + let e ← getFalseExpr return .step e (mkApp4 falseThm n a b eagerReflBoolFalse) (done := true) else return .rfl @@ -368,10 +368,10 @@ def evalFinPred (n : Expr) (trueThm falseThm : Expr) (op : {n : Nat} → Fin n let some vb := getFinValue? b | return .rfl if h : va.n = vb.n then if op va.val (h ▸ vb.val) then - let e ← share <| mkConst ``True + let e ← getTrueExpr return .step e (mkApp4 trueThm n a b eagerReflBoolTrue) (done := true) else - let e ← share <| mkConst ``False + let e ← getFalseExpr return .step e (mkApp4 falseThm n a b eagerReflBoolFalse) (done := true) else return .rfl @@ -418,7 +418,7 @@ def evalLE (α : Expr) (a b : Expr) : SimpM Result := def evalEq (α : Expr) (a b : Expr) : SimpM Result := if isSameExpr a b then do - let e ← share <| mkConst ``True + let e ← getTrueExpr let u ← getLevel α return .step e (mkApp2 (mkConst ``eq_self [u]) α a) (done := true) else match_expr α with @@ -512,8 +512,8 @@ def evalNot (a : Expr) : SimpM Result := **Note**: We added `evalNot` because some abbreviations expanded into `Not`s. -/ match_expr a with - | True => return .step (← mkConstS ``False) (mkConst ``Sym.not_true_eq) (done := true) - | False => return .step (← mkConstS ``True) (mkConst ``Sym.not_false_eq) (done := true) + | True => return .step (← getFalseExpr) (mkConst ``Sym.not_true_eq) (done := true) + | False => return .step (← getTrueExpr) (mkConst ``Sym.not_false_eq) (done := true) | _ => return .rfl public structure EvalStepConfig where diff --git a/src/Lean/Meta/Sym/SymM.lean b/src/Lean/Meta/Sym/SymM.lean index 4df22d1546..d3c31015df 100644 --- a/src/Lean/Meta/Sym/SymM.lean +++ b/src/Lean/Meta/Sym/SymM.lean @@ -83,7 +83,21 @@ inductive CongrInfo where -/ congrTheorem (thm : CongrTheorem) -/-- Mutable state for the symbolic simulator framework. -/ +/-- Pre-shared expressions for commonly used terms. -/ +structure SharedExprs where + trueExpr : Expr + falseExpr : Expr + natZExpr : Expr + btrueExpr : Expr + bfalseExpr : Expr + ordEqExpr : Expr + intExpr : Expr + +/-- Readonly context for the symbolic computation framework. -/ +structure Context where + sharedExprs : SharedExprs + +/-- Mutable state for the symbolic computation framework. -/ structure State where /-- `ShareCommon` (aka `Hash-consing`) state. -/ share : AlphaShareCommon.State := {} @@ -120,11 +134,41 @@ structure State where congrInfo : PHashMap ExprPtr CongrInfo := {} debug : Bool := false -abbrev SymM := StateRefT State MetaM +abbrev SymM := ReaderT Context <| StateRefT State MetaM + +private def mkSharedExprs : AlphaShareCommonM SharedExprs := do + let falseExpr ← shareCommonAlphaInc <| mkConst ``False + let trueExpr ← shareCommonAlphaInc <| mkConst ``True + let bfalseExpr ← shareCommonAlphaInc <| mkConst ``Bool.false + let btrueExpr ← shareCommonAlphaInc <| mkConst ``Bool.true + let natZExpr ← shareCommonAlphaInc <| mkNatLit 0 + let ordEqExpr ← shareCommonAlphaInc <| mkConst ``Ordering.eq + let intExpr ← shareCommonAlphaInc <| Int.mkType + return { falseExpr, trueExpr, bfalseExpr, btrueExpr, natZExpr, ordEqExpr, intExpr } def SymM.run (x : SymM α) : MetaM α := do + let (sharedExprs, share) := mkSharedExprs |>.run {} let debug := sym.debug.get (← getOptions) - x |>.run' { debug } + x { sharedExprs } |>.run' { debug, share } + +/-- Returns maximally shared commonly used terms -/ +def getSharedExprs : SymM SharedExprs := + return (← read).sharedExprs + +/-- Returns the internalized `True` constant. -/ +def getTrueExpr : SymM Expr := return (← getSharedExprs).trueExpr +/-- Returns the internalized `False` constant. -/ +def getFalseExpr : SymM Expr := return (← getSharedExprs).falseExpr +/-- Returns the internalized `Bool.true`. -/ +def getBoolTrueExpr : SymM Expr := return (← getSharedExprs).btrueExpr +/-- Returns the internalized `Bool.false`. -/ +def getBoolFalseExpr : SymM Expr := return (← getSharedExprs).bfalseExpr +/-- Returns the internalized `0 : Nat` numeral. -/ +def getNatZeroExpr : SymM Expr := return (← getSharedExprs).natZExpr +/-- Returns the internalized `Ordering.eq`. -/ +def getOrderingEqExpr : SymM Expr := return (← getSharedExprs).ordEqExpr +/-- Returns the internalized `Int`. -/ +def getIntExpr : SymM Expr := return (← getSharedExprs).intExpr /-- Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean index 46d6fb6096..e9ae5f73c9 100644 --- a/src/Lean/Meta/Tactic/Grind/Main.lean +++ b/src/Lean/Meta/Tactic/Grind/Main.lean @@ -107,13 +107,6 @@ private def discharge? (e : Expr) : SimpM (Option Expr) := do open Sym def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTactic := none) : MetaM α := Sym.SymM.run do - let falseExpr ← share <| mkConst ``False - let trueExpr ← share <| mkConst ``True - let bfalseExpr ← share <| mkConst ``Bool.false - let btrueExpr ← share <| mkConst ``Bool.true - let natZExpr ← share <| mkNatLit 0 - let ordEqExpr ← share <| mkConst ``Ordering.eq - let intExpr ← share <| Int.mkType /- **Note**: Consider using `Sym.simp` in the future. -/ let simprocs := params.normProcs let simpMethods := Simp.mkMethods simprocs discharge? (wellBehavedDischarge := true) @@ -124,9 +117,7 @@ def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTacti let anchorRefs? := params.anchorRefs? let debug := grind.debug.get (← getOptions) x (← mkMethods evalTactic?).toMethodsRef - { config, anchorRefs?, simpMethods, simp, extensions, symPrios - trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr - debug } + { config, anchorRefs?, simpMethods, simp, extensions, symPrios, debug } |>.run' {} private def mkCleanState (mvarId : MVarId) : GrindM Clean.State := mvarId.withContext do diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 352b5a8c3b..d19131d149 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -160,15 +160,10 @@ structure Context where /-- Symbol priorities for inferring E-matching patterns -/ symPrios : SymbolPriorities extensions : ExtensionStateArray := #[] - trueExpr : Expr - falseExpr : Expr - natZExpr : Expr - btrueExpr : Expr - bfalseExpr : Expr - ordEqExpr : Expr -- `Ordering.eq` - intExpr : Expr -- `Int` debug : Bool -- Cached `grind.debug (← getOptions)` +export Sym (getTrueExpr getFalseExpr getBoolTrueExpr getBoolFalseExpr getNatZeroExpr getOrderingEqExpr getIntExpr) + /-- Key for the congruence theorem cache. -/ structure CongrTheoremCacheKey where f : Expr @@ -305,34 +300,6 @@ abbrev withGTransparency [MonadControlT MetaM n] [MonadLiftT GrindM n] [Monad n] let m := if (← getConfig).reducible then .reducible else .default withTransparency m k -/-- Returns the internalized `True` constant. -/ -def getTrueExpr : GrindM Expr := do - return (← readThe Context).trueExpr - -/-- Returns the internalized `False` constant. -/ -def getFalseExpr : GrindM Expr := do - return (← readThe Context).falseExpr - -/-- Returns the internalized `Bool.true`. -/ -def getBoolTrueExpr : GrindM Expr := do - return (← readThe Context).btrueExpr - -/-- Returns the internalized `Bool.false`. -/ -def getBoolFalseExpr : GrindM Expr := do - return (← readThe Context).bfalseExpr - -/-- Returns the internalized `0 : Nat` numeral. -/ -def getNatZeroExpr : GrindM Expr := do - return (← readThe Context).natZExpr - -/-- Returns the internalized `Ordering.eq`. -/ -def getOrderingEqExpr : GrindM Expr := do - return (← readThe Context).ordEqExpr - -/-- Returns the internalized `Int`. -/ -def getIntExpr : GrindM Expr := do - return (← readThe Context).intExpr - /-- Returns the anchor references (if any) being used to restrict the search. -/ def getAnchorRefs : GrindM (Option (Array AnchorRef)) := do return (← readThe Context).anchorRefs?