feat: add sym_simproc and sym_discharger DSL syntax categories (#13026)

This PR adds the infrastructure for simproc and discharger DSLs used to
specify `pre`/`post` simproc chains and conditional rewrite dischargers
in `Sym.simp` variants.

**Syntax categories** (`src/Init/Sym/Simp/SimprocDSL.lean`):
- `sym_simproc` with primitives (`ground`, `telescope`, `rewrite`,
`self`, `none`) and combinators (`>>`, `<|>`)
- `sym_discharger` with primitives (`self`, `none`) for the `with`
clause of `rewrite`

**Elaboration attributes**
(`src/Lean/Elab/Tactic/Grind/SimprocDSL.lean`):
- `builtin_sym_simproc` / `sym_simproc` mapping syntax to `Syntax →
GrindTacticM Simproc`
- `builtin_sym_discharger` / `sym_discharger` mapping syntax to `Syntax
→ GrindTacticM Discharger`
- `elabSymSimproc`, `elabSymDischarger`, and `elabWithClause`
dispatchers

Built-in elaborators for each primitive/combinator will follow in a
subsequent PR after the stage0 update.

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

src/Init/Sym.lean

@@ -6,3 +6,4 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Init.Sym.Lemmas
+public import Init.Sym.Simp.SimprocDSL

src/Init/Sym/Simp/SimprocDSL.lean

@@ -0,0 +1,86 @@
+/-
+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 Init.Tactics
+public section
+namespace Lean.Parser.Sym.Simp
+
+/-!
+# Simproc and Discharger DSLs for `Sym.simp`
+
+## Simproc DSL (`sym_simproc`)
+
+A syntax category for specifying `pre` and `post` simproc chains in `Sym.simp` variants.
+
+### Primitives
+- `ground` — evaluates ground (fully concrete) terms
+- `telescope` — simplifies telescope binders (have-values, arrow hypotheses) but not the final body
+- `rewrite setName [with discharger]` — rewrites using a named theorem set
+- `rewrite [thm₁, thm₂, ...] [with discharger]` — rewrites using inline theorems
+- `self` — recursive simplification (calls the full simplifier)
+- `none` — identity (no simplification)
+
+### Combinators
+- `a >> b` — apply `a`, then apply `b` to the result (andThen)
+- `a <|> b` — try `a`, if no progress try `b` (orElse)
+
+## Discharger DSL (`sym_discharger`)
+
+A syntax category for specifying dischargers used in the `with` clause of `rewrite`.
+Dischargers attempt to prove side conditions of conditional rewrite rules.
+
+### Primitives
+- `self` — recursive simplifier discharge (`dischargeSimpSelf`)
+- `none` — no discharge, only unconditional rewrites apply (`dischargeNone`)
+-/
+
+declare_syntax_cat sym_simproc (behavior := both)
+declare_syntax_cat sym_discharger (behavior := both)
+
+-- Simproc primitives
+
+/-- Evaluate ground (fully concrete) terms. -/
+syntax (name := ground) "ground" : sym_simproc
+
+/-- Simplify telescope binders but not the final body. -/
+syntax (name := telescope) "telescope" : sym_simproc
+
+/-- Rewrite using a named theorem set. Optionally specify a discharger for conditional rewrites. -/
+syntax (name := rewriteSet) "rewrite" ident (" with " sym_discharger)? : sym_simproc
+
+/-- Rewrite using inline theorems. Optionally specify a discharger for conditional rewrites. -/
+syntax (name := rewriteInline) "rewrite" " [" ident,* "]" (" with " sym_discharger)? : sym_simproc
+
+/-- Recursive simplification (calls the full simplifier). -/
+syntax (name := self) "self" : sym_simproc
+
+/-- Identity simproc (no simplification). -/
+syntax (name := none) "none" : sym_simproc
+
+-- Simproc combinators
+
+/-- Apply `a`, then apply `b` to the result. -/
+syntax:60 (name := andThen) sym_simproc:61 " >> " sym_simproc:60 : sym_simproc
+
+/-- Try `a`, if no progress try `b`. -/
+syntax:20 (name := orElse) sym_simproc:21 " <|> " sym_simproc:20 : sym_simproc
+
+/-- Parenthesized simproc expression. -/
+syntax (name := simprocParen) "(" sym_simproc ")" : sym_simproc
+
+-- Discharger primitives
+
+/-- Recursive simplifier discharge. Calls the full simplifier to prove side conditions. -/
+syntax (name := dischSelf) "self" : sym_discharger
+
+/-- No discharge. Only unconditional rewrites will apply. -/
+syntax (name := dischNone) "none" : sym_discharger
+
+/-- Parenthesized discharger expression. -/
+syntax (name := dischParen) "(" sym_discharger ")" : sym_discharger
+
+end Lean.Parser.Sym.Simp

src/Lean/Elab/Tactic/Grind.lean

@@ -16,3 +16,4 @@ public import Lean.Elab.Tactic.Grind.Lint
 public import Lean.Elab.Tactic.Grind.LintExceptions
 public import Lean.Elab.Tactic.Grind.Annotated
 public import Lean.Elab.Tactic.Grind.Sym
+public import Lean.Elab.Tactic.Grind.SimprocDSL

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

@@ -0,0 +1,64 @@
+/-
+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.Elab.Tactic.Grind.Basic
+public import Lean.Meta.Sym.Simp.Discharger
+import Init.Sym.Simp.SimprocDSL
+public section
+namespace Lean.Elab.Tactic.Grind
+open Meta Sym.Simp
+
+/-- Elaboration function for `sym_simproc` syntax. -/
+abbrev SymSimprocElab := Syntax → GrindTacticM Simproc
+
+/-- Elaboration function for `sym_discharger` syntax. -/
+abbrev SymDischargerElab := Syntax → GrindTacticM Discharger
+
+unsafe builtin_initialize symSimprocElabAttribute : KeyedDeclsAttribute SymSimprocElab ←
+  mkElabAttribute SymSimprocElab `builtin_sym_simproc `sym_simproc
+    `Lean.Parser.Sym.Simp `Lean.Elab.Tactic.Grind.SymSimprocElab "sym_simproc"
+
+unsafe builtin_initialize symDischargerElabAttribute : KeyedDeclsAttribute SymDischargerElab ←
+  mkElabAttribute SymDischargerElab `builtin_sym_discharger `sym_discharger
+    `Lean.Parser.Sym.Simp `Lean.Elab.Tactic.Grind.SymDischargerElab "sym_discharger"
+
+/-- Elaborate a `sym_simproc` syntax node into a `Simproc`. -/
+partial def elabSymSimproc (stx : Syntax) : GrindTacticM Simproc := do
+  let elabFns := symSimprocElabAttribute.getEntries (← getEnv) stx.getKind
+  for elabFn in elabFns do
+    try
+      return (← elabFn.value stx)
+    catch ex =>
+      match ex with
+      | .internal id _ =>
+        if id == unsupportedSyntaxExceptionId then continue
+        else throw ex
+      | _ => throw ex
+  throwErrorAt stx "unsupported sym_simproc syntax `{stx.getKind}`"
+
+/-- Elaborate a `sym_discharger` syntax node into a `Discharger`. -/
+def elabSymDischarger (stx : Syntax) : GrindTacticM Discharger := do
+  let elabFns := symDischargerElabAttribute.getEntries (← getEnv) stx.getKind
+  for elabFn in elabFns do
+    try
+      return (← elabFn.value stx)
+    catch ex =>
+      match ex with
+      | .internal id _ =>
+        if id == unsupportedSyntaxExceptionId then continue
+        else throw ex
+      | _ => throw ex
+  throwErrorAt stx "unsupported sym_discharger syntax `{stx.getKind}`"
+
+/-- Get the `Discharger` from an optional `with` clause.
+Returns `dischargeNone` if the clause is absent. -/
+def elabWithClause (withClause : Syntax) : GrindTacticM Discharger := do
+  if withClause.isNone then
+    return dischargeNone
+  elabSymDischarger withClause[0][1]
+
+end Lean.Elab.Tactic.Grind

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {