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

@@ -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

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.
 

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

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

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

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

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?