feat: add interactive simp tactic for sym => mode

This PR adds the `simp` tactic to the `sym =>` interactive mode, completing
the `Sym.simp` interactive infrastructure.

The `simp` tactic supports:
- `simp` — default (identity) variant
- `simp myVariant` — named variant registered via `register_sym_simp`
- `simp [thm₁, thm₂]` — default variant with extra rewrite theorems
- `simp myVariant [thm₁, thm₂]` — named variant with extra theorems

Extra theorems are composed into the variant's `post` chain via `>>`.

Per-variant persistent caching: each unique (variant name, extra theorem list)
combination gets its own `Sym.Simp.State` cache, shared across invocations
within a `sym =>` block. This avoids redundant simplification of identical
subterms when `simp` is called repeatedly (e.g., in branching proofs).

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

src/Init/Grind/Interactive.lean

@@ -304,5 +304,16 @@ syntax (name := symInternalizeAll) "internalize_all" : grind
 Only available in `sym =>` mode. -/
 syntax (name := symByContra) "by_contra" : grind
 
+/--
+`simp` applies the structural simplifier to the goal target.
+Only available in `sym =>` mode.
+
+- `simp` — uses the default (identity) variant
+- `simp myVariant` — uses a named variant registered via `register_sym_simp`
+- `simp [thm₁, thm₂, ...]` — default variant with extra rewrite theorems appended to `post`
+- `simp myVariant [thm₁, thm₂, ...]` — named variant with extra theorems
+-/
+syntax (name := symSimp) "simp" (ppSpace colGt ident)? (" [" ident,* "]")? : grind
+
 end Grind
 end Lean.Parser.Tactic

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -10,6 +10,7 @@ public import Lean.Meta.Tactic.Grind.Main
 import Lean.Meta.Tactic.Grind.Intro
 public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.Util
+public import Lean.Meta.Sym.Simp.SimpM
 import Init.Omega
 public section
 namespace Lean.Elab.Tactic.Grind
@@ -24,11 +25,19 @@ structure Context extends Tactic.Context where
 
 open Meta.Grind (Goal)
 
+/-- Cache key for `Sym.simp` variant invocations: variant name + ordered extra theorem names. -/
+structure SimpCacheKey where
+  variant : Name
+  extras  : List Name
+  deriving BEq, Hashable
+
 structure Cache where
   /-- Cache for `BackwardRule`s created from declaration names (sym mode only). -/
   backwardRuleName : PHashMap Name Sym.BackwardRule := {}
   /-- Cache for `BackwardRule`s created from elaborated terms, keyed by syntax byte position range (sym mode only). -/
   backwardRuleSyntax : PHashMap (Nat × Nat) Sym.BackwardRule := {}
+  /-- Per-variant persistent `Sym.simp` cache. Keyed by variant name + extra theorem names. -/
+  simpState : Std.HashMap SimpCacheKey Sym.Simp.State := {}
 
 structure State where
   symState   : Meta.Sym.State

src/Lean/Elab/Tactic/Grind/Sym.lean

@@ -6,7 +6,15 @@ Authors: Leonardo de Moura
 module
 prelude
 import Lean.Elab.Tactic.Grind.Basic
+import Lean.Elab.Tactic.Grind.SimprocDSL
 import Lean.Meta.Sym.Grind
+import Lean.Meta.Sym.Simp.Variant
+import Lean.Meta.Sym.Simp.Rewrite
+import Lean.Meta.Sym.Simp.EvalGround
+import Lean.Meta.Sym.Simp.Goal
+import Lean.Meta.Sym.Simp.Attr
+import Lean.Meta.Sym.Simp.ControlFlow
+import Lean.Meta.Sym.Simp.Forall
 import Lean.Meta.Tactic.Apply
 import Lean.Elab.SyntheticMVars
 namespace Lean.Elab.Tactic.Grind
@@ -135,4 +143,60 @@ private def getOrCreateBackwardRuleFromTerm (term : Syntax) : GrindTacticM Sym.B
   let goal ← liftGrindM <| Grind.Goal.internalizeAll goal
   replaceMainGoal [goal]
 
+section
+open Sym.Simp
+
+def trivialSimproc : Simproc := fun _ =>
+  return .rfl
+
+def elabOptSimproc (stx? : Option Syntax) : GrindTacticM Simproc := do
+  let some stx := stx? | return trivialSimproc
+  elabSymSimproc stx
+
+def addExtraTheorems (post : Simproc) (extraNames : Array Name) : GrindTacticM Simproc := do
+  if extraNames.isEmpty then return post
+  let mut thms : Theorems := {}
+  for name in extraNames do
+    thms := thms.insert (← mkTheoremFromDecl name)
+  return post >> thms.rewrite
+
+def mkDefaultMethods (extraNames : Array Name) : GrindTacticM Sym.Simp.Methods := do
+  let thms ← getSymSimpTheorems
+  let pre := simpControl >> simpArrowTelescope
+  let post ← addExtraTheorems (evalGround >> thms.rewrite) extraNames
+  return { pre, post }
+
+def elabVariant (variantName : Name) (extraNames : Array Name) : GrindTacticM (Sym.Simp.Methods × Sym.Simp.Config) := do
+  if variantName.isAnonymous then
+    return (← mkDefaultMethods extraNames, {})
+  let some v := getSymSimpVariant? (← getEnv) variantName
+    | throwError "unknown Sym.simp variant `{variantName}`"
+  let pre ← elabOptSimproc v.pre?
+  let post ← addExtraTheorems (← elabOptSimproc v.post?) extraNames
+  return ({ pre, post}, v.config)
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symSimp] def evalSymSimp : GrindTactic := fun stx => do
+  ensureSym
+  let `(grind| simp $[$variantId?]? $[[ $[$extraIds],* ]]?) := stx | throwUnsupportedSyntax
+  -- Resolve variant
+  let variantName := variantId?.map (·.getId) |>.getD .anonymous
+  -- Compose extra theorems into post
+  let extraNames ← (extraIds.getD #[]).mapM fun id => realizeGlobalConstNoOverload id
+  -- Cache lookup/creation
+  let cacheKey : SimpCacheKey := { variant := variantName, extras := extraNames.toList }
+  let simpState := (← get).cache.simpState[cacheKey]?.getD {}
+  let (methods, config) ← elabVariant variantName extraNames
+  let goal ← getMainGoal
+  let (simpResult, simpState) ← liftGrindM <| goal.withContext do
+    Sym.Simp.SimpM.run (Sym.Simp.simp (← goal.mvarId.getType)) methods config simpState
+  -- Save updated cache
+  modify fun s => { s with cache.simpState := s.cache.simpState.insert cacheKey simpState }
+  -- Apply result to goal
+  match (← liftGrindM <| Sym.Simp.Result.toSimpGoalResult simpResult goal.mvarId) with
+  | .closed => replaceMainGoal []
+  | .goal mvarId => replaceMainGoal [{ goal with mvarId }]
+  | .noProgress => throwError "`Sym.simp` made no progress"
+
+end
+
 end Lean.Elab.Tactic.Grind

tests/elab/sym_simp_interactive1.lean

@@ -0,0 +1,113 @@
+import Lean
+
+/-! Tests for interactive `simp` tactic in `sym =>` mode -/
+
+theorem test_zero_add : 0 + n = n := Nat.zero_add n
+theorem test_add_zero : n + 0 = n := Nat.add_zero n
+
+/-! ## Test 1: `simp` with named variant -/
+
+register_sym_simp testNatSimp where
+  post := rewrite [test_zero_add, test_add_zero]
+
+example (x : Nat) : 0 + x = x := by
+  sym =>
+    simp testNatSimp
+    tactic => rfl
+
+/-! ## Test 2: named variant simplifies compound expression -/
+
+example (x : Nat) : 0 + (x + 0) = x := by
+  sym =>
+    simp testNatSimp
+    tactic => rfl
+
+/-! ## Test 3: named variant with extra theorems -/
+
+theorem test_succ_add : Nat.succ n + m = Nat.succ (n + m) := Nat.succ_add n m
+
+example (x : Nat) : 0 + (Nat.succ 0 + x) = Nat.succ (0 + x) := by
+  sym =>
+    simp testNatSimp [test_succ_add]
+    tactic => rfl
+
+/-! ## Test 4: variant with ground evaluation (closes goal) -/
+
+register_sym_simp groundSimp where
+  post := ground
+
+example : (3 + 4 : Nat) = 7 := by
+  sym =>
+    simp groundSimp
+
+/-! ## Test 5: variant with pre and post (ground in pre closes via evalGround in default) -/
+
+register_sym_simp prePostSimp where
+  pre  := ground
+  post := rewrite [test_zero_add]
+
+example (x : Nat) : 0 + x = x := by
+  sym =>
+    simp prePostSimp
+
+/-! ## Test 6: bare `simp` uses default methods (with `@[sym_simp]` set) -/
+
+attribute [sym_simp] test_zero_add
+
+example (x : Nat) : 0 + x = x := by
+  sym =>
+    simp
+
+/-! ## Test 7: unknown variant produces error -/
+
+/--
+error: unknown Sym.simp variant `nonExistent`
+-/
+#guard_msgs in
+example (x : Nat) : 0 + x = x := by
+  sym =>
+    simp nonExistent
+
+/-! ## Test 8: `simp` with `>>` combinator in variant -/
+
+register_sym_simp chainSimp where
+  post := ground >> rewrite [test_zero_add]
+
+example (x : Nat) : 0 + x = x := by
+  sym =>
+    simp chainSimp
+
+/-! ## Test 9: repeated simp shares cache -/
+
+example (x y : Nat) : 0 + x = x ∧ 0 + y = y := by
+  sym =>
+    apply And.intro
+    · simp testNatSimp; tactic => rfl
+    · simp testNatSimp; tactic => rfl
+
+/-! ## Test 10: verify persistent cache is shared across `simp` invocations.
+The second `simp` should hit the persistent cache for shared subterms like `0`.
+Enable trace to confirm (run manually to inspect). -/
+
+register_sym_simp simple where
+  post := ground >> rewrite [Nat.zero_add, Nat.add_zero, true_and, and_true]
+
+/--
+trace: [sym.simp.debug.cache] persistent cache hit: x
+[sym.simp.debug.cache] persistent cache hit: x
+[sym.simp.debug.cache] persistent cache hit: 0
+[sym.simp.debug.cache] persistent cache hit: x
+[sym.simp.debug.cache] persistent cache hit: f (f (f (f x)))
+[sym.simp.debug.cache] persistent cache hit: f (f (f (f x)))
+[sym.simp.debug.cache] persistent cache hit: y
+[sym.simp.debug.cache] persistent cache hit: f (f (f (f x))) = y
+---
+trace: [sym.simp.debug.cache] persistent cache hit: f (f (f (f x))) = y
+-/
+#guard_msgs in
+set_option trace.sym.simp.debug.cache true in
+example (f : Nat → Nat) (x y : Nat) (h : f (f (f (f x))) = y) : 0 + x = x ∧ 0 + f (f (f (f x))) = y := by
+  sym =>
+    simp simple
+    try simp simple
+    apply h