feat: add sanity checks to register_sym_simp (#13040)

This PR adds validation to the `register_sym_simp` command:

- Reject duplicate variant names
- Validate `pre`/`post` syntax by elaborating them via `elabSymSimproc`
  in a minimal `GrindTacticM` context, catching unknown theorem names
  and unknown theorem set references at registration time

Adds `withGrindTacticM` helper for running `GrindTacticM` from
`CommandElabM`,
and `validateOptionSimprocSyntax` for optional syntax validation.

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

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

@@ -7,14 +7,42 @@ module
 prelude
 import Init.Sym.Simp.SimprocDSL
 import Lean.Meta.Sym.Simp.Variant
+import Lean.Elab.Tactic.Grind.SimprocDSL
 import Lean.Elab.Command
 namespace Lean.Elab.Command
 open Meta Sym.Simp
 
+/--
+Runs a `GrindTacticM` computation in a minimal context for validation.
+-/
+def withGrindTacticM (k : Tactic.Grind.GrindTacticM α) : CommandElabM α := do
+  liftTermElabM do
+  let params ← Grind.mkDefaultParams {}
+  let (ctx, state) ← Grind.GrindM.run (params := params) do
+    let methods ← Grind.getMethods
+    let grindCtx ← readThe Meta.Grind.Context
+    let symCtx ← readThe Sym.Context
+    let grindState ← get
+    let symState ← getThe Sym.State
+    let ctx := {
+      elaborator := `registerSymSimp,
+      ctx := grindCtx, sctx := symCtx, methods, params
+    }
+    return (ctx, { grindState, symState, goals := [] })
+  let (a, _) ← Tactic.Grind.GrindTacticM.run k ctx state
+  return a
+
+def validateOptionSimprocSyntax (proc? : Option Syntax) : CommandElabM Unit := do
+  let some proc := proc? | return ()
+  discard <| withGrindTacticM <| Tactic.Grind.elabSymSimproc proc
+
 @[builtin_command_elab Lean.Parser.Command.registerSymSimp]
 def elabRegisterSymSimp : CommandElab := fun stx => do
   let id := stx[1]
   let name := id.getId
+  -- Check for duplicate variant
+  if (getSymSimpVariant? (← getEnv) name).isSome then
+    throwErrorAt id "Sym.simp variant `{name}` is already registered"
   let fields := stx[3].getArgs
   let mut pre? : Option Syntax := none
   let mut post? : Option Syntax := none
@@ -35,7 +63,10 @@ def elabRegisterSymSimp : CommandElab := fun stx => do
       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 }
+  -- Validate pre/post by elaborating them
+  validateOptionSimprocSyntax pre?
+  validateOptionSimprocSyntax post?
+  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 }
 

tests/elab/sym_simp_interactive1.lean

@@ -111,3 +111,29 @@ example (f : Nat → Nat) (x y : Nat) (h : f (f (f (f x))) = y) : 0 + x = x ∧
     simp simple
     try simp simple
     apply h
+
+/-! ## Test 11: duplicate variant name is rejected -/
+
+/--
+error: Sym.simp variant `simple` is already registered
+-/
+#guard_msgs in
+register_sym_simp simple where
+
+/-! ## Test 12: unknown theorem in `rewrite [...]` is rejected -/
+
+/--
+error: Unknown constant `bla`
+-/
+#guard_msgs in
+register_sym_simp simple₁ where
+  pre := rewrite [bla]
+
+/-! ## Test 13: unknown theorem set in `rewrite setName` is rejected -/
+
+/--
+error: unknown Sym.simp theorem set `boo`
+-/
+#guard_msgs in
+register_sym_simp simple₃ where
+  pre := rewrite boo