feat: add extensible state mechanism for SymM

This PR add `SymExtension`, a typed extensible state mechanism for `SymM`,
following the same pattern as `Grind.SolverExtension`. Extensions are
registered at initialization time via `registerSymExtension` and provide
typed `getState`/`modifyState` accessors. Extension state persists across
`simp` invocations within a `sym =>` block and is re-initialized on each
`SymM.run`.

This enables modules (e.g., the upcoming arithmetic normalizer) to
register persistent state without modifying `Sym.State` directly.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

src/Init/Data/Char/Lemmas.lean

@@ -98,8 +98,4 @@ theorem toNat_inj {c d : Char} : c.toNat = d.toNat ↔ c = d := by
 theorem isDigit_iff_toNat {c : Char} : c.isDigit ↔ '0'.toNat ≤ c.toNat ∧ c.toNat ≤ '9'.toNat := by
   simp [isDigit, UInt32.le_iff_toNat_le]
 
-@[simp]
-theorem toNat_mk {val : UInt32} {h} : (Char.mk val h).toNat = val.toNat := by
-  simp [← toNat_val]
-
 end Char

src/Init/Data/Nat/ToString.lean

@@ -298,7 +298,7 @@ theorem ofDigitChars_cons {c : Char} {cs : List Char} {init : Nat} :
   simp [ofDigitChars]
 
 theorem ofDigitChars_cons_digitChar_of_lt_ten {n : Nat} (hn : n < 10) {cs : List Char} {init : Nat} :
-    ofDigitChars b (n.digitChar :: cs) init = ofDigitChars b cs (b * init + n) := by
+    ofDigitChars 10 (n.digitChar :: cs) init = ofDigitChars 10 cs (10 * init + n) := by
   simp [ofDigitChars_cons, Nat.toNat_digitChar_sub_48_of_lt_ten hn]
 
 theorem ofDigitChars_eq_ofDigitChars_zero {l : List Char} {init : Nat} :
@@ -320,17 +320,15 @@ theorem ofDigitChars_replicate_zero {n : Nat} : ofDigitChars b (List.replicate n
   | zero => simp
   | succ n ih => simp [List.replicate_succ, ofDigitChars_cons, ih, Nat.pow_succ, Nat.mul_assoc]
 
-theorem ofDigitChars_toDigits {b n : Nat} (hb' : 1 < b) (hb : b ≤ 10) : ofDigitChars b (toDigits b n) 0 = n := by
-  induction n using base_induction b hb' with
-  | single m hm =>
-    simp [Nat.toDigits_of_lt_base hm, ofDigitChars_cons_digitChar_of_lt_ten (by omega : m < 10)]
-  | digit m k hk hm ih =>
-    rw [← Nat.toDigits_append_toDigits hb' hm hk,
-      ofDigitChars_append, ih, Nat.toDigits_of_lt_base hk,
-      ofDigitChars_cons_digitChar_of_lt_ten (Nat.lt_of_lt_of_le hk hb), ofDigitChars_nil]
-
 @[simp]
-theorem ofDigitChars_ten_toDigits {n : Nat} : ofDigitChars 10 (toDigits 10 n) 0 = n :=
-  ofDigitChars_toDigits (by decide) (by decide)
+theorem ofDigitChars_toDigits {n : Nat} : ofDigitChars 10 (toDigits 10 n) 0 = n := by
+  have : 1 < 10 := by decide
+  induction n using base_induction 10 this with
+  | single m hm =>
+    simp [Nat.toDigits_of_lt_base hm, ofDigitChars_cons_digitChar_of_lt_ten hm]
+  | digit m k hk hm ih =>
+    rw [← Nat.toDigits_append_toDigits this hm hk,
+      ofDigitChars_append, ih, Nat.toDigits_of_lt_base hk,
+      ofDigitChars_cons_digitChar_of_lt_ten hk, ofDigitChars_nil]
 
 end Nat

src/Init/Data/String/Defs.lean

@@ -187,9 +187,6 @@ theorem append_right_inj (s : String) {t₁ t₂ : String} :
 theorem append_assoc {s₁ s₂ s₃ : String} : s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃) := by
   simp [← toByteArray_inj, ByteArray.append_assoc]
 
-instance : Std.Associative (α := String) (· ++ ·) where
-  assoc _ _ _ := append_assoc
-
 @[simp]
 theorem utf8ByteSize_eq_zero_iff {s : String} : s.utf8ByteSize = 0 ↔ s = "" := by
   refine ⟨fun h => ?_, fun h => h ▸ utf8ByteSize_empty⟩

src/Init/Data/String/Iter/Intercalate.lean

@@ -17,7 +17,7 @@ namespace Std
 /--
 Appends all the elements in the iterator, in order.
 -/
-public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
+public def Iter.joinString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
     (it : Std.Iter (α := α) β) : String :=
   (it.map toString).fold (init := "") (· ++ ·)
 
@@ -25,7 +25,7 @@ public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
 Appends the elements of the iterator into a string, placing the separator {name}`s` between them.
 -/
 @[inline]
-public def Iter.intercalateString {α β : Type} [Iterator α Id β] [ToString β]
+public def Iter.intercalateString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
     (s : String.Slice) (it : Std.Iter (α := α) β) : String :=
   it.map toString
     |>.fold (init := none) (fun

src/Init/Data/String/Lemmas/Intercalate.lean

@@ -60,23 +60,6 @@ theorem toList_intercalate {s : String} {l : List String} :
   | nil => simp
   | cons hd tl ih => cases tl <;> simp_all
 
-theorem join_eq_foldl : join l = l.foldl (fun r s => r ++ s) "" :=
-  (rfl)
-
-@[simp]
-theorem join_nil : join [] = "" := by
-  simp [join]
-
-@[simp]
-theorem join_cons : join (s :: l) = s ++ join l := by
-  simp only [join, List.foldl_cons, empty_append]
-  conv => lhs; rw [← String.append_empty (s := s)]
-  rw [List.foldl_assoc]
-
-@[simp]
-theorem toList_join {l : List String} : (String.join l).toList = l.flatMap String.toList := by
-  induction l <;> simp_all
-
 namespace Slice
 
 @[simp]
@@ -93,10 +76,6 @@ theorem intercalate_eq {s : Slice} {l : List Slice} :
   | nil => simp [intercalate]
   | cons hd tl ih => cases tl <;> simp_all [intercalate, intercalate.go, intercalateGo_append]
 
-@[simp]
-theorem join_eq {l : List Slice} : join l = String.join (l.map copy) := by
-  simp [join, String.join, List.foldl_map]
-
 end Slice
 
 end String

src/Init/Data/String/Lemmas/Iter.lean

@@ -18,13 +18,14 @@ namespace Std.Iter
 
 @[simp]
 public theorem joinString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [ToString β] {it : Std.Iter (α := α) β} :
-    it.joinString = String.join (it.toList.map toString) := by
+    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β]
+    {it : Std.Iter (α := α) β} : it.joinString = String.join (it.toList.map toString) := by
   rw [joinString, String.join, ← foldl_toList, toList_map]
 
 @[simp]
 public theorem intercalateString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [ToString β] {s : String.Slice} {it : Std.Iter (α := α) β} :
+    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β] {s : String.Slice}
+    {it : Std.Iter (α := α) β} :
     it.intercalateString s = s.copy.intercalate (it.toList.map toString) := by
   simp only [intercalateString, String.appendSlice_eq, ← foldl_toList, toList_map]
   generalize s.copy = s

src/Init/Data/String/Slice.lean

@@ -1152,19 +1152,6 @@ where go (acc : String) (s : Slice) : List Slice → String
   | a :: as => go (acc ++ s ++ a) s as
   | []      => acc
 
-/--
-Appends all the slices in a list of slices, in order.
-
-Use {name}`String.Slice.intercalate` to place a separator string between the strings in a list.
-
-Examples:
- * {lean}`String.Slice.join ["gr", "ee", "n"] = "green"`
- * {lean}`String.Slice.join ["b", "", "l", "", "ue"] = "blue"`
- * {lean}`String.Slice.join [] = ""`
--/
-def join (l : List String.Slice) : String :=
-  l.foldl (fun (r : String) (s : String.Slice) => r ++ s) ""
-
 /--
 Converts a string to the Lean compiler's representation of names. The resulting name is
 hierarchical, and the string is split at the dots ({lean}`'.'`).

src/Lean/Compiler/LCNF/OtherDecl.lean

@@ -21,6 +21,6 @@ def getOtherDeclType (declName : Name) (us : List Level := []) : CompilerM Expr
   match (← getPhase) with
   | .base => getOtherDeclBaseType declName us
   | .mono => getOtherDeclMonoType declName
-  | .impure => throwError "getOtherDeclType unsupported for impure"
+  | .impure => getOtherDeclImpureType declName
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -154,18 +154,16 @@ mutual
       return f!"oset {← ppFVar fvarId} [{i}] := {← ppArg y};" ++ .line ++ (← ppCode k)
     | .setTag fvarId cidx k _ =>
       return f!"setTag {← ppFVar fvarId} := {cidx};" ++ .line ++ (← ppCode k)
-    | .inc fvarId n check persistent k _ =>
-      let ann := (if persistent then "[persistent]" else "") ++ (if !check then "[ref]" else "")
+    | .inc fvarId n _ _ k _ =>
       if n != 1 then
-        return f!"inc[{n}]{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"inc[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
       else
-        return f!"inc{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
-    | .dec fvarId n check persistent k _ =>
-      let ann := (if persistent then "[persistent]" else "") ++ (if !check then "[ref]" else "")
+        return f!"inc {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+    | .dec fvarId n _ _ k _ =>
       if n != 1 then
-        return f!"dec[{n}]{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"dec[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
       else
-        return f!"dec{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"dec {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
     | .del fvarId k _ =>
       return f!"del {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
 

src/Lean/Compiler/LCNF/ToImpureType.lean

@@ -240,4 +240,12 @@ where fillCache := do
       fieldInfo := fields
     }
 
+public def getOtherDeclImpureType (declName : Name) : CoreM Expr := do
+  match (← impureTypeExt.find? declName) with
+  | some type => return type
+  | none =>
+    let type ← toImpureType (← getOtherDeclMonoType declName)
+    monoTypeExt.insert declName type
+    return type
+
 end Lean.Compiler.LCNF

src/Lean/Expr.lean

@@ -73,7 +73,7 @@ inductive BinderInfo where
   | default
   /-- Implicit binder annotation, e.g., `{x : α}` -/
   | implicit
-  /-- Strict implicit binder annotation, e.g., `⦃x : α⦄` -/
+  /-- Strict implicit binder annotation, e.g., `{{ x : α }}` -/
   | strictImplicit
   /-- Local instance binder annotation, e.g., `[Decidable α]` -/
   | instImplicit
@@ -107,7 +107,7 @@ def BinderInfo.isImplicit : BinderInfo → Bool
   | BinderInfo.implicit => true
   | _                   => false
 
-/-- Return `true` if the given `BinderInfo` is a strict implicit annotation (e.g., `⦃α : Type u⦄`) -/
+/-- Return `true` if the given `BinderInfo` is a strict implicit annotation (e.g., `{{α : Type u}}`) -/
 def BinderInfo.isStrictImplicit : BinderInfo → Bool
   | BinderInfo.strictImplicit => true
   | _                         => false

src/Std/Do/Triple/SpecLemmas.lean

@@ -136,15 +136,6 @@ theorem Cursor.pos_at {l : List α} {n : Nat} (h : n < l.length) :
 theorem Cursor.pos_mk {l pre suff : List α} (h : pre ++ suff = l) :
     (Cursor.mk pre suff h).pos = pre.length := rfl
 
-theorem Cursor.pos_le_length {c : Cursor l} : c.pos ≤ l.length := by
-  simp [← congrArg List.length c.property]
-
-theorem Cursor.length_prefix_le_length {c : Cursor l} : c.prefix.length ≤ l.length :=
-  pos_le_length
-
-theorem Cursor.length_suffix_le_length {c : Cursor l} : c.suffix.length ≤ l.length := by
-  simp [← congrArg List.length c.property]
-
 @[grind →]
 theorem eq_of_range'_eq_append_cons (h : range' s n step = xs ++ cur :: ys) :
     cur = s + step * xs.length := by

tests/bench/mvcgen/sym/cases/Cases.lean

@@ -3,7 +3,7 @@ import Cases.AddSubCancelDeep
 import Cases.AddSubCancelSimp
 import Cases.DiteSplit
 import Cases.GetThrowSet
-import Cases.MatchIota
 import Cases.MatchSplit
+import Cases.MatchSplitState
 import Cases.PurePrecond
 import Cases.ReaderState

tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean

@@ -24,18 +24,17 @@ theorem Spec.get_M :
     ⦃fun s => Q.1 s s⦄ get (m := M) ⦃Q⦄ := by
   mvcgen
 
-/-- Matches on state `s` — the discriminant IS the excess state arg. -/
-def step : M Unit := do
+def step (v : Nat) : M Unit := do
   let s ← get
-  match s with
-  | 0 => throw "s is zero"
-  | n+1 => set n
+  match v with
+  | 0 => throw "v is zero"
+  | n+1 => set (s + n + 1); let s ← get; set (s - n)
 
 def loop (n : Nat) : M Unit := do
   match n with
   | 0 => pure ()
-  | n+1 => step; loop n
+  | n+1 => step n; loop n
 
-def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = n⌝⦄ loop n ⦃⇓_ s => ⌜s = 0⌝⦄
+def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s = n⌝⦄
 
 end MatchSplit

tests/bench/mvcgen/sym/cases/Cases/MatchSplitState.lean

@@ -3,7 +3,7 @@ import VCGen
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
-namespace MatchIota
+namespace MatchSplitState
 
 set_option mvcgen.warning false
 
@@ -24,17 +24,18 @@ theorem Spec.get_M :
     ⦃fun s => Q.1 s s⦄ get (m := M) ⦃Q⦄ := by
   mvcgen
 
-def step (v : Nat) : M Unit := do
+/-- Matches on state `s` — the discriminant IS the excess state arg. -/
+def step : M Unit := do
   let s ← get
-  match v with
-  | 0 => throw "v is zero"
-  | n+1 => set (s + n + 1); let s ← get; set (s - n)
+  match s with
+  | 0 => throw "s is zero"
+  | n+1 => set n
 
 def loop (n : Nat) : M Unit := do
   match n with
   | 0 => pure ()
-  | n+1 => step n; loop n
+  | n+1 => step; loop n
 
-def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = 0⌝⦄ loop n ⦃⇓_ s => ⌜s = n⌝⦄
+def Goal (n : Nat) : Prop := ⦃fun s => ⌜s = n⌝⦄ loop n ⦃⇓_ s => ⌜s = 0⌝⦄
 
-end MatchIota
+end MatchSplitState

tests/bench/mvcgen/sym/lakefile.lean

@@ -19,8 +19,7 @@ lean_lib Cases where
 @[default_target]
 lean_lib VCGenBench where
   roots := #[`vcgen_add_sub_cancel, `vcgen_add_sub_cancel_deep, `vcgen_add_sub_cancel_simp,
-             `vcgen_get_throw_set, `vcgen_get_throw_set_grind, `vcgen_pure_precond,
-             `vcgen_reader_state, `vcgen_match_split]
+             `vcgen_get_throw_set, `vcgen_pure_precond, `vcgen_reader_state, `vcgen_match_split]
   moreLeanArgs := #["--tstack=100000000"]
 
 @[default_target]

tests/bench/mvcgen/sym/lib/VCGen.lean

@@ -14,9 +14,6 @@ public meta import Lean.Meta.Match.Rewrite
 public meta import Lean.Elab.Tactic.Do.VCGen.Split
 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.Meta.Tactic.Grind.Solve
-meta import Lean.Elab.Tactic.Grind
 
 open Lean Parser Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do.SpecAttr
@@ -468,11 +465,6 @@ meta def mkBackwardRuleForSplit (splitInfo : SplitInfo) (m σs ps instWP : Expr)
 VC generation
 -/
 
-/-- Configuration specific to grind-mode VCGen. -/
-public structure GrindContext where
-  /-- Simp methods used to pre-simplify hypotheses before grind internalization. -/
-  hypSimpMethods : Sym.Simp.Methods
-
 public structure VCGen.Context where
   specThms : SpecTheoremsNew
   /-- The backward rule for `SPred.entails_cons_intro`. -/
@@ -483,8 +475,6 @@ public structure VCGen.Context where
   exceptCondsEntailsRflRule : BackwardRule
   /-- The backward rule for `Triple.of_entails_wp`. -/
   tripleOfEntailsWPRule : BackwardRule
-  /-- If `some`, VCGen runs in grind mode with the given configuration. -/
-  grindCtx? : Option GrindContext := none
 
 public structure VCGen.State where
   /--
@@ -507,14 +497,8 @@ public structure VCGen.State where
   The verification conditions that have been generated so far.
   -/
   vcs : Array MVarId := #[]
-  /--
-  Persistent cache for the `Sym.Simp` simplifier used to pre-simplify hypotheses
-  before grind internalization. Threading this cache across VCGen iterations avoids
-  re-simplifying shared subexpressions (e.g., `s + 1 + 1 + ...` chains).
-  -/
-  simpState : Sym.Simp.State := {}
 
-abbrev VCGenM := ReaderT VCGen.Context (StateRefT VCGen.State Grind.GrindM)
+abbrev VCGenM := ReaderT VCGen.Context (StateRefT VCGen.State SymM)
 
 namespace VCGen
 
@@ -635,16 +619,6 @@ meta partial def reduceProjBeta? (e : Expr) : SymM (Option Expr) :=
           pure (some (.letE x ty val body' nondep))
       | _ => pure lastReduction
 
-structure WorkItem where
-  mvarId : MVarId
-  grindGoal? : Option Grind.Goal := none
-
-@[inline] meta def WorkItem.withMVarId (item : WorkItem) (newGoal : MVarId) : WorkItem :=
-  { item with mvarId := newGoal, grindGoal? := item.grindGoal?.map fun g => { g with mvarId := newGoal } }
-
-@[inline] meta def WorkItem.forkTo (item : WorkItem) (subgoals : List MVarId) : List WorkItem :=
-  subgoals.map item.withMVarId
-
 inductive SolveResult where
   /-- `target` was not of the form `H ⊢ₛ T`. -/
   | noEntailment (target : Expr)
@@ -658,7 +632,7 @@ inductive SolveResult where
   -/
   | noSpecFoundForProgram (e : Expr) (monad : Expr) (thms : Array SpecTheoremNew)
   /-- Successfully discharged the goal. These are the subgoals. -/
-  | goals (subgoals : List WorkItem)
+  | goals (subgoals : List MVarId)
 
 open Sym Sym.Internal
 -- The following function is vendored until it is made public:
@@ -691,71 +665,6 @@ open Sym Sym.Internal
 meta def mkAppNS [Monad m] [Internal.MonadShareCommon m] (f : Expr) (args : Array Expr) : m Expr :=
   mkAppRangeS f 0 args.size args
 
-private meta def getNatLit? (e : Expr) : Option Nat := do
-  let_expr OfNat.ofNat _ n _ := e | failure
-  let .lit (.natVal n) := n | failure
-  return n
-
-/--
-A `Sym.Simp` post-simproc that reassociates Nat addition to fold nested literal additions.
-Rewrites `(a + m) + n` → `a + (m + n)` when `m` and `n` are Nat literals, using `Nat.add_assoc`.
-Since `m + n` reduces to a literal by kernel computation, this collapses chains like
-`s + 1 + 1 + 1` into `s + 3` in a single step.
--/
-meta def reassocNatAdd : Sym.Simp.Simproc := fun e => do
-  let_expr HAdd.hAdd α _ _ inst ab n := e | return .rfl
-  let_expr Nat := α | return .rfl
-  let some nVal := getNatLit? n | return .rfl
-  let_expr HAdd.hAdd _ _ _ _ a m := ab | return .rfl
-  let some mVal := getNatLit? m | return .rfl
-  -- (a + m) + n → a + (m + n), with m + n folded to a literal
-  let sumExpr ← share <| toExpr (mVal + nVal)
-  let result ← share <| mkApp6 (mkConst ``HAdd.hAdd [0, 0, 0]) α α α inst a sumExpr
-  -- Proof: Nat.add_assoc a m n : (a + m) + n = a + (m + n)
-  let proof := mkApp3 (mkConst ``Nat.add_assoc) a m n
-  return .step result proof
-
-/--
-Simplify types of not-yet-internalized hypotheses in the grind goal using `Sym.simp`.
-Only hypotheses with index `≥ grindGoal.nextDeclIdx` are simplified, since earlier ones
-have already been internalized into grind's E-graph.
-Returns the (possibly updated) `MVarId`.
--/
-meta def simpNewHyps (mvarId : MVarId) (nextDeclIdx : Nat) (methods : Sym.Simp.Methods) : VCGenM MVarId := do
-  mvarId.withContext do
-  let lctx ← getLCtx
-  let mut mvarId := mvarId
-  for decl in lctx do
-    if decl.index < nextDeclIdx then continue
-    if decl.isImplementationDetail then continue
-    let simpState := (← get).simpState
-    let (result, simpState') ← Sym.Simp.SimpM.run (Sym.Simp.simp decl.type) methods {} simpState
-    modify fun s => { s with simpState := simpState' }
-    match result with
-    | .rfl .. => pure ()
-    | .step newType _proof .. =>
-      mvarId ← mvarId.replaceLocalDeclDefEq decl.fvarId newType
-  return mvarId
-
-/-- Internalize pending hypotheses in the grind state before forking to multiple subgoals.
-If `processHypotheses` discovers a contradiction (`inconsistent = true`), the E-graph state
-contains stale proof data (the contradiction proof targets the parent's mvar, not the children's).
-In that case, restore the pre-internalization state so each child can discover the contradiction
-independently and construct its own proof via `closeGoal`.
-
--/
-meta def internalizePending (item : WorkItem) : VCGenM WorkItem := do
-  if let some grindGoal := item.grindGoal? then
-    let some grindCtx := (← read).grindCtx? | unreachable!
-    let mvarId ← simpNewHyps item.mvarId grindGoal.nextDeclIdx grindCtx.hypSimpMethods
-    let grindGoal := { grindGoal with mvarId }
-    let saved := grindGoal
-    let grindGoal ← Grind.processHypotheses grindGoal
-    if grindGoal.inconsistent then
-      return { item with grindGoal? := some saved }
-    return { item with grindGoal? := some grindGoal }
-  return item
-
 /--
 The main VC generation function.
 Looks at a goal of the form `P ⊢ₛ T`. Then
@@ -763,8 +672,7 @@ Looks at a goal of the form `P ⊢ₛ T`. Then
 * If `T` is of the form `wp⟦e⟧ Q s₁ ... sₙ`, look up a spec theorem for `e`. Produce the backward
   rule to apply this spec theorem and then apply it ot the goal.
 -/
-meta def solve (item : WorkItem) : VCGenM SolveResult := item.mvarId.withContext do
-  let goal := item.mvarId
+meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
   let target ← goal.getType
   trace[Elab.Tactic.Do.vcgen] "target: {target}"
   -- There are two layers of preprocessing before we get to taking apart program syntax.
@@ -774,16 +682,16 @@ meta def solve (item : WorkItem) : VCGenM SolveResult := item.mvarId.withContext
 
   if target.isForall then
     let IntrosResult.goal _ goal ← Sym.intros goal | throwError "Failed to introduce binders for {target}"
-    return .goals [item.withMVarId goal]
+    return .goals [goal]
 
   let f := target.getAppFn
   if f.isConstOf ``Triple then
     let goal ← tripleOfWP goal
-    return .goals [item.withMVarId goal]
+    return .goals [goal]
 
   if f.isConstOf ``PostCond.entails then
     let goal ← decomposePostCondEntails goal
-    return .goals [item.withMVarId goal]
+    return .goals [goal]
 
   let_expr ent@SPred.entails σs H T := target | return .noEntailment target
   -- The goal is of the form `H ⊢ₛ T`. Try some reductions to expose `wp⟦e⟧ Q s₁ ... sₙ` in `T`.
@@ -794,7 +702,7 @@ meta def solve (item : WorkItem) : VCGenM SolveResult := item.mvarId.withContext
     -- extra state arg `s` to reduce away the lambda.
     let .goals [goal] ← (← read).entailsConsIntroRule.apply goal
       | throwError "Applying {.ofConstName ``SPred.entails_cons_intro} to {target} failed. It should not."
-    return .goals [item.withMVarId goal]
+    return .goals [goal]
 
   /-
   Do a very targeted simplification to turn `H ⊢ₛ (fun _ => T, Q.snd).fst s` into `H ⊢ₛ T`, and
@@ -815,7 +723,7 @@ meta def solve (item : WorkItem) : VCGenM SolveResult := item.mvarId.withContext
   let T? ← reduceProjBeta? T
   if H?.isSome || T?.isSome then
     let goal ← goal.replaceTargetDefEq (← Sym.Internal.mkAppS₃ ent σs (H?.getD H) (T?.getD T))
-    return .goals [item.withMVarId goal]
+    return .goals [goal]
 
   -- Look for program syntax in `T`.
   T.withApp fun head args => do
@@ -838,85 +746,66 @@ meta def solve (item : WorkItem) : VCGenM SolveResult := item.mvarId.withContext
   let f := e.getAppFn
   withTraceNode `Elab.Tactic.Do.vcgen (msg := fun _ => return m!"Program: {e}") do
 
-  -- Replace the program in the goal with `e'` (which must be definitionally equal).
-  let replaceProgDefEq (e' : Expr) : VCGenM MVarId := do
-    let wp ← Sym.Internal.mkAppS₅ wpConst m ps instWP α e'
-    let T ← mkAppNS head (args.set! 2 wp)
-    let target ← mkAppS₃ ent σs H T
-    goal.replaceTargetDefEq target
-
   -- Zeta let-expressions
   if let .letE _x _ty val body _nonDep := f then
     let body' ← Sym.instantiateRevBetaS body #[val]
     let e' ← mkAppRevS body' e.getAppRevArgs
-    return .goals [item.withMVarId (← replaceProgDefEq e')]
+    let wp ← Sym.Internal.mkAppS₅ wpConst m ps instWP α e'
+    let T ← mkAppNS head (args.set! 2 wp)
+    let target ← mkAppS₃ ent σs H T
+    let goal ← goal.replaceTargetDefEq target
+    return .goals [goal]
 
   -- Split ite/dite/match
   if let some info ← liftMetaM <| Lean.Elab.Tactic.Do.getSplitInfo? e then
-    -- Try iota reduction first (reduces matcher/recursor with concrete discriminant)
-    if let some e' ← liftMetaM <| reduceRecMatcher? e then
-      return .goals [item.withMVarId (← replaceProgDefEq (← shareCommonInc e'))]
-    -- Internalize pending hypotheses before forking
-    let item ← internalizePending item
     let rule ← mkBackwardRuleFromSplitInfoCached info m σs ps instWP excessArgs
-    let ApplyResult.goals goals ← rule.apply item.mvarId
+    let ApplyResult.goals goals ← rule.apply goal
       | throwError "Failed to apply split rule for {indentExpr e}"
-    return .goals (item.forkTo goals)
+    return .goals goals
 
   -- Apply registered specifications (both triple and simp specs use cached backward rules).
   if f.isConst || f.isFVar then
-    -- Internalize pending hypotheses before potential multi-goal fork
-    let item ← internalizePending item
     trace[Elab.Tactic.Do.vcgen] "Applying a spec for {e}. Excess args: {excessArgs}"
     match ← (← read).specThms.findSpecs e with
     | .error thms => return .noSpecFoundForProgram e m thms
     | .ok thm =>
     trace[Elab.Tactic.Do.vcgen] "Spec for {e}: {thm.proof}"
     let rule ← mkBackwardRuleFromSpecCached thm m σs ps instWP excessArgs
-    let ApplyResult.goals goals ← rule.apply item.mvarId
+    let ApplyResult.goals goals ← rule.apply goal
       | throwError "Failed to apply rule {thm.proof} for {indentExpr e}"
-    return .goals (item.forkTo goals)
+    return .goals goals
 
   return .noStrategyForProgram e
 
 /--
 Called when decomposing the goal further did not succeed; in this case we emit a VC for the goal.
-In grind mode, tries to solve the VC using the accumulated `Grind.Goal` state (E-graph) via
-`Grind.withProtectedMCtx` + `Grind.processHypotheses` + `Grind.solve`.
 -/
-meta def emitVC (item : WorkItem) : VCGenM Unit := do
-  let ty ← item.mvarId.getType
+meta def emitVC (goal : MVarId) : VCGenM Unit := do
+  let ty ← goal.getType
+  goal.setKind .syntheticOpaque
   if ty.isAppOf ``Std.Do.Invariant then
-    item.mvarId.setKind .syntheticOpaque
-    modify fun s => { s with invariants := s.invariants.push item.mvarId }
-  else if let some grindGoal := item.grindGoal? then
-    let some grindCtx := (← read).grindCtx? | unreachable!
-    let mvarId ← simpNewHyps item.mvarId grindGoal.nextDeclIdx grindCtx.hypSimpMethods
-    let grindGoal := { grindGoal with mvarId }
-    let config ← Grind.getConfig
-    Grind.withProtectedMCtx config mvarId fun mvarId' => do
-      let grindGoal' := { grindGoal with mvarId := mvarId' }
-      let grindGoal' ← Grind.processHypotheses grindGoal'
-      unless ← mvarId'.isAssigned do
-        discard <| Grind.solve grindGoal'
-    unless ← mvarId.isAssigned do
-      mvarId.setKind .syntheticOpaque
-      modify fun s => { s with vcs := s.vcs.push mvarId }
+    modify fun s => { s with invariants := s.invariants.push goal }
   else
-    item.mvarId.setKind .syntheticOpaque
-    modify fun s => { s with vcs := s.vcs.push item.mvarId }
+    modify fun s => { s with vcs := s.vcs.push goal }
 
-meta def work (item : WorkItem) : VCGenM Unit := do
-  let goal ← preprocessMVar item.mvarId
-  let item := item.withMVarId goal
-  let mut worklist := Std.Queue.empty.enqueue item
+meta def work (goal : MVarId) : VCGenM Unit := do
+  -- 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 (item, worklist') := worklist.dequeue? | break
+    let some (goal, worklist') := worklist.dequeue? | break
     worklist := worklist'
-    let res ← solve item
+    let res ← solve goal
     match res with
     | .noEntailment .. | .noProgramFoundInTarget .. =>
-      emitVC item
+      emitVC goal
     | .noSpecFoundForProgram prog _ #[] =>
       throwError "No spec found for program {prog}."
     | .noSpecFoundForProgram prog monad thms =>
@@ -934,17 +823,9 @@ public structure Result where
 Generate verification conditions for a goal of the form `P ⊢ₛ wp⟦e⟧ Q s₁ ... sₙ` by repeatedly
 decomposing `e` using registered `@[spec]` theorems.
 Return the VCs and invariant goals.
-When `grindMode` is true, integrates grind into the VCGen loop for incremental context
-internalization, avoiding O(n) re-internalization per VC.
 -/
-public meta partial def main (goal : MVarId) (ctx : Context) : Grind.GrindM Result := do
-  let grindGoal? ←
-    if ctx.grindCtx?.isSome then
-      let g ← Grind.mkGoalCore goal
-      some <$> Grind.processHypotheses g
-    else pure none
-  let item : WorkItem := { mvarId := goal, grindGoal? }
-  let ((), state) ← StateRefT'.run (ReaderT.run (work item) ctx) {}
+public meta partial def main (goal : MVarId) (ctx : Context) : SymM Result := do
+  let ((), state) ← StateRefT'.run (ReaderT.run (work goal) ctx) {}
   _ ← state.invariants.mapIdxM fun idx mv => do
     mv.setTag (Name.mkSimple ("inv" ++ toString (idx + 1)))
   _ ← state.vcs.mapIdxM fun idx mv => do
@@ -1022,46 +903,14 @@ meta def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : TacticM VCGe
 end VCGen
 
 syntax (name := mvcgen') "mvcgen'"
-  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
-  (&" with " tactic)? : tactic
-
-/-- Parse grind configuration from the `with grind ...` clause and build `Grind.Params`.
-Overrides the internal simp step limit to accommodate large unrolled goals. -/
-private meta def mkGrindParamsFromSyntax (grindStx : Syntax) (goal : MVarId) : TacticM Grind.Params := do
-  let `(tactic| grind $config:optConfig $[only%$only]? $[ [$grindParams:grindParam,*] ]? $[=> $_:grindSeq]?) := grindStx
-    | throwUnsupportedSyntax
-  let grindConfig ← elabGrindConfig config
-  let params ← mkGrindParams grindConfig only.isSome (grindParams.getD {}).getElems goal
-  -- FIXME: Expose grind's internal simp step limit as a user-facing option instead of hardcoding.
-  -- Grind's `simpCore` uses the default `Simp.Config.maxSteps` (100k) which is too low for large
-  -- unrolled goals (fails around n=400 for GetThrowSet).
-  return { params with norm := ← params.norm.setConfig { params.norm.config with maxSteps := 10000000 } }
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")? : tactic
 
 @[tactic mvcgen']
 public meta def elabMVCGen' : Tactic := fun stx => withMainContext do
-  let goal ← getMainGoal
   let ctx ← VCGen.mkSpecContext stx[1]
-  -- `(&" with " tactic)?` produces a nullKind node with 2 children when present;
-  -- `getOptional?` requires exactly 1 child, so we check `getNumArgs` instead.
-  let withTac? := if stx[2].getNumArgs != 0 then some stx[2][1] else none
-  let isGrind := withTac?.any (·.getKind == ``Lean.Parser.Tactic.grind)
-  let mut params ← Grind.mkDefaultParams {}
-  let mut grindCtx? : Option GrindContext := none
-  if isGrind then
-    params ← mkGrindParamsFromSyntax withTac?.get! goal
-    grindCtx? := some { hypSimpMethods := { post := VCGen.reassocNatAdd } }
-  let ctx := { ctx with grindCtx? }
-
-  let result ← Grind.GrindM.run (VCGen.main goal ctx) params
-
-  let mut vcs := result.vcs
-  if let some tac := withTac? then
-    if !isGrind then
-      let mut remaining : Array MVarId := #[]
-      for vc in result.vcs do
-        remaining := remaining ++ (← try evalTacticAt tac vc catch _ => pure [vc]).toArray
-      vcs := remaining
-  replaceMainGoal (result.invariants ++ vcs).toList
+  let goal ← getMainGoal
+  let { invariants, vcs } ← SymM.run <| VCGen.main goal ctx
+  replaceMainGoal (invariants ++ vcs).toList
 
 /-!
 Local tests for faster iteration:

tests/bench/mvcgen/sym/test_vcgen.lean

@@ -19,8 +19,8 @@ Each case exercises a different aspect of the VC generation:
 - `PurePrecond`: Pure hypotheses `⌜φ⌝` in preconditions
 - `ReaderState`: `ReaderT`/`StateM` combination
 - `DiteSplit`: Dependent if-then-else (`if h : cond then ...`)
-- `MatchIota`: Pattern matching with concrete discriminants (iota-reduced, no split)
-- `MatchSplit`: Pattern matching with symbolic discriminant (state), exercising match split
+- `MatchSplit`: Pattern matching in monadic programs
+- `MatchSplitState`: Match on state variable (discriminant = excess state arg)
 -/
 
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
@@ -40,14 +40,6 @@ open AddSubCancelSimp in
 open GetThrowSet in
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10]
 
--- Test `mvcgen' with grind`: grind integrated into VCGen loop
-open GetThrowSet in
-#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| fail) [10]
-
--- Test `mvcgen' with grind` on AddSubCancel
-open AddSubCancel in
-#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| fail) [10]
-
 open PurePrecond in
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| fail) [10]
 
@@ -57,8 +49,8 @@ open ReaderState in
 open DiteSplit in
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10]
 
-open MatchIota in
+open MatchSplit in
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| sorry) [10]
 
-open MatchSplit in
+open MatchSplitState in
 #eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| grind) [10]

tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean

@@ -1,13 +0,0 @@
-import Cases.GetThrowSet
-import Driver
-
-open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
-open GetThrowSet
-
-set_option maxRecDepth 100000
-set_option maxHeartbeats 100000000
-
--- Benchmark `mvcgen' with grind`: grind integrated into VCGen loop for incremental
--- context internalization. This avoids O(n) re-internalization per VC.
-#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| fail)
-  [100, 250, 500]

tests/bench/mvcgen/sym/vcgen_match_split.lean

@@ -3,11 +3,11 @@ 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.MatchIota
+import Cases.MatchSplit
 import Driver
 
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
-open MatchIota
+open MatchSplit
 
 set_option maxRecDepth 10000
 set_option maxHeartbeats 10000000

tests/elab/borrowBug.lean

@@ -29,14 +29,14 @@ trace: [Compiler.explicitRc] size: 27
         let z := g x;
         let fst := oproj[0] z;
         inc fst;
-        dec[ref] z;
+        dec z;
         goto _jp.1 fst
       | Bool.true =>
         dec x;
         let z := g y;
         let fst := oproj[0] z;
         inc fst;
-        dec[ref] z;
+        dec z;
         goto _jp.1 fst
 [Compiler.explicitRc] size: 2
     def f._boxed x y : tagged :=

tests/elab/compile_borrowed_reset_jp.lean

@@ -27,8 +27,8 @@ trace: [Compiler.explicitRc] size: 17
 [Compiler.explicitRc] size: 4
     def testWithAnnotation._boxed n p q : obj :=
       let res := testWithAnnotation n p q;
-      dec[ref] q;
-      dec[ref] p;
+      dec q;
+      dec p;
       dec n;
       return res
 -/
@@ -55,11 +55,11 @@ trace: [Compiler.explicitRc] size: 20
       let isZero := Nat.decEq n zero;
       cases isZero : obj
       | Bool.true =>
-        dec[ref] q;
+        dec q;
         let _x.6 := 123;
         goto _jp.1 _x.6 p
       | Bool.false =>
-        dec[ref] p;
+        dec p;
         let one := 1;
         let n.7 := Nat.sub n one;
         let _x.8 := Nat.add n.7 one;

tests/elab/compile_recursive_array_access.lean

@@ -17,7 +17,7 @@ trace: [Compiler.explicitRc] size: 19
         cases path : obj
         | List.nil =>
           let x.1 := oproj[0] tree;
-          inc[ref] x.1;
+          inc x.1;
           return x.1
         | _ =>
           let _x.2 := instInhabitedNAryTree.default._closed_0;
@@ -39,7 +39,7 @@ trace: [Compiler.explicitRc] size: 19
     def followPath._boxed tree path : obj :=
       let res := followPath tree path;
       dec path;
-      dec[ref] tree;
+      dec tree;
       return res
 -/
 #guard_msgs in

tests/elab/compiler_push_proj.lean

@@ -61,7 +61,7 @@ trace: [Compiler.pushProj] size: 10
       | Option.some =>
         cases b : tobj
         | Option.none =>
-          inc[ref] a;
+          inc a;
           return a
         | Option.some =>
           let val.1 : tobj := oproj[0] a;
@@ -157,7 +157,7 @@ trace: [Compiler.pushProj] size: 14
         | Option.some =>
           let val.11 : tobj := oproj[0] a;
           inc val.11;
-          dec[ref] a;
+          dec a;
           let val.12 : tobj := oproj[0] b;
           jp resetjp.13 _x.14 isShared.15 : tobj :=
             let _x.16 : tobj := Nat.add val.11 val.12;
@@ -251,14 +251,14 @@ trace: [Compiler.pushProj] size: 18
         | Option.some =>
           cases c : tobj
           | Bool.false =>
-            dec[ref] b;
-            dec[ref] a;
+            dec b;
+            dec a;
             let _x.11 : tagged := ctor_0[Option.none];
             return _x.11
           | Bool.true =>
             let val.12 : tobj := oproj[0] a;
             inc val.12;
-            dec[ref] a;
+            dec a;
             let val.13 : tobj := oproj[0] b;
             jp resetjp.14 _x.15 isShared.16 : tobj :=
               let _x.17 : tobj := Nat.add val.12 val.13;

tests/elab/jpVoidArgs.lean

@@ -52,17 +52,17 @@ trace: [Compiler.saveMono] size: 25
       cases x : tobj
       | Enum.A =>
         let _x.6 := 0;
-        inc[ref] y;
+        inc y;
         let _x.7 := y _x.6 ◾;
         goto _jp.2
       | Enum.B =>
         let _x.8 := 1;
-        inc[ref] y;
+        inc y;
         let _x.9 := y _x.8 ◾;
         goto _jp.2
       | Enum.C =>
         let _x.10 := 2;
-        inc[ref] y;
+        inc y;
         let _x.11 := y _x.10 ◾;
         goto _jp.2
 [Compiler.saveImpure] size: 2

tests/elab/lcnf_borrow_expected_type.lean

@@ -168,7 +168,7 @@ trace: [Compiler.explicitRc] size: 22
 [Compiler.explicitRc] size: 2
     def cascadeDemo._boxed t : tobj :=
       let res := cascadeDemo t;
-      dec[ref] t;
+      dec t;
       return res
 -/
 #guard_msgs in
@@ -183,20 +183,20 @@ def cascadeDemo (t : @&Quad) : Nat :=
 trace: [Compiler.explicitRc] size: 33
     def cascadeDemo' t : tobj :=
       let left := oproj[0] t;
-      inc[ref] left;
+      inc left;
       let right := oproj[1] t;
-      inc[ref] right;
-      dec[ref] t;
+      inc right;
+      dec t;
       let fst := oproj[0] left;
       inc fst;
       let snd := oproj[1] left;
       inc snd;
-      dec[ref] left;
+      dec left;
       let fst := oproj[0] right;
       inc fst;
       let snd := oproj[1] right;
       inc snd;
-      dec[ref] right;
+      dec right;
       let _x.1 := wrap fst;
       let res := List.lengthTR._redArg _x.1;
       dec _x.1;
@@ -238,7 +238,7 @@ trace: [Compiler.explicitRc] size: 15
         dec a;
         let fst := oproj[0] x;
         inc fst;
-        dec[ref] x;
+        dec x;
         return fst
       | Bool.false =>
         let one := 1;

tests/elab/ugetBorrowed.lean

@@ -11,7 +11,7 @@ trace: [Compiler.explicitRc] size: 3
       let i.boxed := unbox i;
       dec i;
       let res := test._redArg xs i.boxed;
-      dec[ref] xs;
+      dec xs;
       let r := box res;
       return r
 [Compiler.explicitRc] size: 1
@@ -23,7 +23,7 @@ trace: [Compiler.explicitRc] size: 3
       let i.boxed := unbox i;
       dec i;
       let res := test xs i.boxed h;
-      dec[ref] xs;
+      dec xs;
       let r := box res;
       return r
 -/