feat: add register_sym_simp command and SymSimpVariant infrastructure

This PR adds the `register_sym_simp` command for declaring named `Sym.simp`
variants with `pre`/`post` simproc chains and optional config overrides.

- `SymSimpVariant` structure storing `pre`/`post` syntax (elaborated at use
  time) and `Config` overrides
- `SimpleScopedEnvExtension` for persistent cross-module variant storage
- `register_sym_simp` command syntax with `sym_simp_field` category
- Command elaborator parsing fields and registering variants
- `getSymSimpVariant?` lookup function
- `deriving Inhabited` on `Simp.Config` for extension support

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

src/Init/Sym/Simp/SimprocDSL.lean

@@ -83,4 +83,47 @@ syntax (name := dischNone) "none" : sym_discharger
 /-- Parenthesized discharger expression. -/
 syntax (name := dischParen) "(" sym_discharger ")" : sym_discharger
 
-end Lean.Parser.Sym.Simp
+end Lean.Parser.Sym.Simp
+
+/-!
+## `register_sym_simp` command
+
+Declares a named `Sym.simp` variant with `pre`/`post` simproc chains and optional config overrides.
+
+```
+register_sym_simp myVariant where
+  pre  := telescope
+  post := ground >> rewrite mySet with self
+```
+-/
+
+namespace Lean.Parser.Command
+
+declare_syntax_cat sym_simp_field (behavior := both)
+
+/-- Pre-processing simproc chain. -/
+syntax (name := symSimpFieldPre) "pre" " := " sym_simproc : sym_simp_field
+
+/-- Post-processing simproc chain. -/
+syntax (name := symSimpFieldPost) "post" " := " sym_simproc : sym_simp_field
+
+/-- Maximum number of simplification steps. -/
+syntax (name := symSimpFieldMaxSteps) "maxSteps" " := " num : sym_simp_field
+
+/-- Maximum depth of recursive discharge attempts. -/
+syntax (name := symSimpFieldMaxDischargeDepth) "maxDischargeDepth" " := " num : sym_simp_field
+
+/--
+Register a named `Sym.simp` variant.
+
+```
+register_sym_simp myVariant where
+  pre  := telescope
+  post := ground >> rewrite [thm1, thm2] with self
+  maxSteps := 50000
+```
+-/
+syntax (name := registerSymSimp) "register_sym_simp" ident "where"
+  (colGt sym_simp_field)* : command
+
+end Lean.Parser.Command

src/Lean/Elab/Tactic/Grind.lean

@@ -18,3 +18,4 @@ public import Lean.Elab.Tactic.Grind.Annotated
 public import Lean.Elab.Tactic.Grind.Sym
 public import Lean.Elab.Tactic.Grind.SimprocDSL
 public import Lean.Elab.Tactic.Grind.SimprocDSLBuiltin
+public import Lean.Elab.Tactic.Grind.RegisterSymSimp

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

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+import Init.Sym.Simp.SimprocDSL
+import Lean.Meta.Sym.Simp.Variant
+import Lean.Elab.Command
+namespace Lean.Elab.Command
+open Meta Sym.Simp
+
+@[builtin_command_elab Lean.Parser.Command.registerSymSimp]
+def elabRegisterSymSimp : CommandElab := fun stx => do
+  let id := stx[1]
+  let name := id.getId
+  let fields := stx[3].getArgs
+  let mut pre? : Option Syntax := none
+  let mut post? : Option Syntax := none
+  let mut maxSteps? : Option Nat := none
+  let mut maxDischargeDepth? : Option Nat := none
+  for field in fields do
+    match field with
+    | `(sym_simp_field| maxSteps := $val:num) =>
+      unless maxSteps?.isNone do throwErrorAt field "duplicate `maxSteps` field"
+      maxSteps? := some val.getNat
+    | `(sym_simp_field| maxDischargeDepth := $val:num) =>
+      unless maxDischargeDepth?.isNone do throwErrorAt field "duplicate `maxDischargeDepth` field"
+      maxDischargeDepth? := some val.getNat
+    | `(sym_simp_field| pre := $proc) =>
+      unless pre?.isNone do throwErrorAt field "duplicate `pre` field"
+      pre? := some proc
+    | `(sym_simp_field| post := $proc) =>
+      unless post?.isNone do throwErrorAt field "duplicate `post` field"
+      post? := some proc
+    | _ => throwErrorAt field "unexpected field"
+  let config :=  { maxSteps := maxSteps?.getD 100_000, maxDischargeDepth := maxDischargeDepth?.getD 2 }
+  let variant : SymSimpVariant := { pre?, post?, config }
+  modifyEnv fun env => symSimpVariantExtension.addEntry env { name, variant }
+
+end Lean.Elab.Command

src/Lean/Meta/Sym/Simp.lean

@@ -24,4 +24,5 @@ public import Lean.Meta.Sym.Simp.ControlFlow
 public import Lean.Meta.Sym.Simp.Goal
 public import Lean.Meta.Sym.Simp.Telescope
 public import Lean.Meta.Sym.Simp.Attr
+public import Lean.Meta.Sym.Simp.Variant
 public import Lean.Meta.Sym.Simp.RegisterCommand

src/Lean/Meta/Sym/Simp/RegisterCommand.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Simp.Attr
+public import Lean.Meta.Sym.Simp.Variant
 public meta import Init.Data.ToString.Name
 public meta import Init.Data.String.Extra
 public section

src/Lean/Meta/Sym/Simp/SimpM.lean

@@ -106,6 +106,7 @@ structure Config where
   Prevents infinite loops when conditional rewrite rules trigger recursive discharge attempts.
   -/
   maxDischargeDepth : Nat := 2
+  deriving Inhabited
 
 /--
 The result of simplifying an expression `e`.

src/Lean/Meta/Sym/Simp/Variant.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Simp.SimpM
+import Lean.ScopedEnvExtension
+public section
+namespace Lean.Meta.Sym.Simp
+
+/--
+A named `Sym.simp` variant. Stores `pre`/`post` simproc chains as syntax
+(elaborated at use time in `GrindTacticM`) and configuration overrides.
+-/
+structure SymSimpVariant where
+  /-- Pre-processing simproc chain (elaborated at use time). -/
+  pre?   : Option Syntax := none
+  /-- Post-processing simproc chain (elaborated at use time). -/
+  post?  : Option Syntax := none
+  /-- Configuration overrides. -/
+  config : Config := {}
+  deriving Inhabited
+
+/-- Entry for the scoped environment extension. -/
+structure SymSimpVariantEntry where
+  name    : Name
+  variant : SymSimpVariant
+  deriving Inhabited
+
+/-- Persistent environment extension mapping variant names to their definitions. -/
+builtin_initialize symSimpVariantExtension :
+    SimpleScopedEnvExtension SymSimpVariantEntry (Std.HashMap Name SymSimpVariant) ←
+  registerSimpleScopedEnvExtension {
+    name     := `symSimpVariantExtension
+    initial  := {}
+    addEntry := fun map entry => map.insert entry.name entry.variant
+  }
+
+/-- Look up a named `Sym.simp` variant. -/
+def getSymSimpVariant? (env : Environment) (name : Name) : Option SymSimpVariant :=
+  (symSimpVariantExtension.getState env)[name]?
+
+end Lean.Meta.Sym.Simp

tests/elab/sym_register_variant1.lean

@@ -0,0 +1,63 @@
+import Lean
+
+open Lean Meta Sym.Simp
+
+/-! Tests for `register_sym_simp` command -/
+
+-- Basic variant with pre and post
+register_sym_simp testVariant1 where
+  pre  := ground
+  post := rewrite [Nat.zero_add]
+
+-- Variant with only post
+register_sym_simp testVariant2 where
+  post := ground >> rewrite [Nat.zero_add, Nat.add_zero]
+
+-- Variant with only pre
+register_sym_simp testVariant3 where
+  pre := telescope
+
+-- Variant with config overrides
+register_sym_simp testVariant4 where
+  pre := ground
+  post := rewrite [Nat.zero_add]
+  maxSteps := 50000
+  maxDischargeDepth := 3
+
+-- Variant with discharger
+register_sym_simp testVariant5 where
+  post := rewrite [Nat.zero_add] with self
+
+-- Variant with combinators
+register_sym_simp testVariant6 where
+  post := ground >> rewrite [Nat.zero_add] <|> rewrite [Nat.add_zero]
+
+-- Empty variant (no fields)
+register_sym_simp testVariantEmpty where
+
+-- Verify variants are registered
+#eval show MetaM Unit from do
+  let env ← getEnv
+  let some v1 := getSymSimpVariant? env `testVariant1 | throwError "testVariant1 not found"
+  guard v1.pre?.isSome
+  guard v1.post?.isSome
+  let some v2 := getSymSimpVariant? env `testVariant2 | throwError "testVariant2 not found"
+  guard v2.pre?.isNone
+  guard v2.post?.isSome
+  let some v3 := getSymSimpVariant? env `testVariant3 | throwError "testVariant3 not found"
+  guard v3.pre?.isSome
+  guard v3.post?.isNone
+  let some v4 := getSymSimpVariant? env `testVariant4 | throwError "testVariant4 not found"
+  guard (v4.config.maxSteps == 50000)
+  guard (v4.config.maxDischargeDepth == 3)
+  let some _ := getSymSimpVariant? env `testVariantEmpty | throwError "testVariantEmpty not found"
+  guard (getSymSimpVariant? env `nonExistent |>.isNone)
+
+-- Duplicate field detection
+/--
+error: duplicate `pre` field
+-/
+#guard_msgs in
+register_sym_simp testBadDuplicate where
+  pre := ground
+  pre := telescope