From 973062e4e1a0e1d13a2d82e82e36232a20f80245 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 20 Mar 2026 20:53:39 -0700
Subject: [PATCH] feat: add Sym.simp theorem set attributes (#13018)

This PR adds named theorem sets for `Sym.simp` with associated
attributes, following the same pattern as `Meta.simp`'s
`register_simp_attr`.

- `register_sym_simp_attr my_set` creates a named set with its own
`PersistentEnvExtension` and attribute
- `@[my_set] theorem ...` adds a rewrite theorem
- `@[my_set] def ...` adds equation theorems from the definition
- `builtin_initialize symSimpExtension` registers a default
`@[sym_simp]` set
- `getSymSimpTheorems` / `getSymSimpExtension?` retrieve theorem sets at
tactic time

New files:
- `Sym/Simp/Attr.lean`: attribute logic (`mkSymSimpAttr`,
`registerSymSimpAttr`)
- `Sym/Simp/RegisterCommand.lean`: `register_sym_simp_attr` macro

Tests:
- `tests/pkg/sym_simp_attr/`: package test with user-defined set
(`my_sym_simp`)
- `tests/elab/sym_simp_set.lean`: tests for the builtin `@[sym_simp]`
set
---
 src/Lean/Meta/Sym/Simp.lean                   |  2 +
 src/Lean/Meta/Sym/Simp/Attr.lean              | 74 +++++++++++++++++++
 src/Lean/Meta/Sym/Simp/RegisterCommand.lean   | 22 ++++++
 src/Lean/Meta/Sym/Simp/Theorems.lean          | 32 ++++++++
 tests/elab/sym_simp_set.lean                  | 38 ++++++++++
 tests/pkg/sym_simp_attr/SymSimpAttr.lean      | 40 ++++++++++
 tests/pkg/sym_simp_attr/SymSimpAttr/Decl.lean |  9 +++
 tests/pkg/sym_simp_attr/lakefile.lean         |  5 ++
 tests/pkg/sym_simp_attr/lean-toolchain        |  1 +
 tests/pkg/sym_simp_attr/run_test.sh           |  2 +
 10 files changed, 225 insertions(+)
 create mode 100644 src/Lean/Meta/Sym/Simp/Attr.lean
 create mode 100644 src/Lean/Meta/Sym/Simp/RegisterCommand.lean
 create mode 100644 tests/elab/sym_simp_set.lean
 create mode 100644 tests/pkg/sym_simp_attr/SymSimpAttr.lean
 create mode 100644 tests/pkg/sym_simp_attr/SymSimpAttr/Decl.lean
 create mode 100644 tests/pkg/sym_simp_attr/lakefile.lean
 create mode 100644 tests/pkg/sym_simp_attr/lean-toolchain
 create mode 100755 tests/pkg/sym_simp_attr/run_test.sh

diff --git a/src/Lean/Meta/Sym/Simp.lean b/src/Lean/Meta/Sym/Simp.lean
index 632ebbfae8..6a8ced4dce 100644
--- a/src/Lean/Meta/Sym/Simp.lean
+++ b/src/Lean/Meta/Sym/Simp.lean
@@ -23,3 +23,5 @@ public import Lean.Meta.Sym.Simp.Discharger
 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.RegisterCommand
diff --git a/src/Lean/Meta/Sym/Simp/Attr.lean b/src/Lean/Meta/Sym/Simp/Attr.lean
new file mode 100644
index 0000000000..95157d50a0
--- /dev/null
+++ b/src/Lean/Meta/Sym/Simp/Attr.lean
@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. 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.Theorems
+import Lean.Meta.Tactic.Simp.SimpTheorems -- for ignoreEquations
+import Lean.Meta.Eqns -- for getEqnsFor?
+public section
+namespace Lean.Meta.Sym.Simp
+
+/--
+Adds a `Sym.Simp` theorem (an equality) to the given extension.
+-/
+def addSymSimpTheorem (ext : SymSimpExtension) (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do
+  let thm ← mkTheoremFromDecl declName
+  ext.add thm attrKind
+
+/--
+Creates a `Sym.Simp` attribute for a named theorem set.
+When a proposition is tagged, it is added as a rewrite theorem.
+When a definition is tagged, its equation theorems are added.
+-/
+def mkSymSimpAttr (attrName : Name) (attrDescr : String) (ext : SymSimpExtension)
+    (ref : Name := by exact decl_name%) : IO Unit :=
+  registerBuiltinAttribute {
+    ref   := ref
+    name  := attrName
+    descr := attrDescr
+    applicationTime := AttributeApplicationTime.afterCompilation
+    add   := fun declName _ attrKind => do
+      let go : MetaM Unit := do
+        let info ← getAsyncConstInfo declName
+        if (← isProp info.sig.get.type) then
+          addSymSimpTheorem ext declName attrKind
+        else if info.kind matches .defn then
+          if (← Simp.ignoreEquations declName) then
+            throwError "Cannot add `{attrName}` attribute to `{.ofConstName declName}`: \
+              It is a reducible definition or projection. `Sym.simp` does not support unfolding."
+          else if let some eqns ← getEqnsFor? declName then
+            for eqn in eqns do
+              addSymSimpTheorem ext eqn attrKind
+          else
+            throwError "Cannot add `{attrName}` attribute to `{.ofConstName declName}`: \
+              No equation theorems found."
+        else
+          throwError "Cannot add `{attrName}` attribute to `{.ofConstName declName}`: \
+            It is not a proposition nor a definition with equation theorems."
+      discard <| go.run {} {}
+    erase := fun _declName => do
+      throwError "Erasing `Sym.simp` attributes is not supported yet."
+  }
+
+/--
+Registers a named `Sym.Simp` theorem set. Each set gets its own attribute
+and its own `SymSimpExtension` (persistent environment extension).
+
+Must be called during initialization.
+-/
+def registerSymSimpAttr (attrName : Name) (attrDescr : String)
+    (ref : Name := by exact decl_name%) : IO SymSimpExtension := do
+  let ext ← mkSymSimpExt ref
+  mkSymSimpAttr attrName attrDescr ext ref
+  symSimpExtensionMapRef.modify fun map => map.insert attrName ext
+  return ext
+
+builtin_initialize symSimpExtension : SymSimpExtension ← registerSymSimpAttr `sym_simp "Sym.simp theorem"
+
+def getSymSimpTheorems : CoreM Theorems :=
+  symSimpExtension.getTheorems
+
+end Lean.Meta.Sym.Simp
diff --git a/src/Lean/Meta/Sym/Simp/RegisterCommand.lean b/src/Lean/Meta/Sym/Simp/RegisterCommand.lean
new file mode 100644
index 0000000000..0034f602eb
--- /dev/null
+++ b/src/Lean/Meta/Sym/Simp/RegisterCommand.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. 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.Attr
+public meta import Init.Data.ToString.Name
+public meta import Init.Data.String.Extra
+public section
+namespace Lean.Meta.Sym.Simp
+
+macro (name := _root_.Lean.Parser.Command.registerSymSimpAttr) doc:(docComment)?
+  "register_sym_simp_attr" id:ident : command => do
+  let str := id.getId.toString
+  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
+  let descr := quote ((doc.map (·.getDocString) |>.getD s!"Sym.simp set for {id.getId.toString}").removeLeadingSpaces)
+  `($[$doc:docComment]? public meta initialize ext : SymSimpExtension ← registerSymSimpAttr $(quote id.getId) $descr
+    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)
+
+end Lean.Meta.Sym.Simp
diff --git a/src/Lean/Meta/Sym/Simp/Theorems.lean b/src/Lean/Meta/Sym/Simp/Theorems.lean
index 5207558b76..c888e3cd05 100644
--- a/src/Lean/Meta/Sym/Simp/Theorems.lean
+++ b/src/Lean/Meta/Sym/Simp/Theorems.lean
@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Sym.Pattern
 public import Lean.Meta.DiscrTree
 import Lean.Meta.Sym.Simp.DiscrTree
+import Lean.ExtraModUses
 public section
 namespace Lean.Meta.Sym.Simp
 
@@ -32,6 +33,7 @@ instance : BEq Theorem where
 /-- Collection of simplification theorems available to the simplifier. -/
 structure Theorems where
   thms : DiscrTree Theorem := {}
+  deriving Inhabited
 
 def Theorems.insert (thms : Theorems) (thm : Theorem) : Theorems :=
   { thms with thms := insertPattern thms.thms thm.pattern thm }
@@ -46,4 +48,34 @@ def mkTheoremFromDecl (declName : Name) : MetaM Theorem := do
   let (pattern, rhs) ← mkEqPatternFromDecl declName
   return { expr := mkConst declName, pattern, rhs }
 
+/--
+Environment extension storing a set of `Sym.Simp` theorems.
+Each named set gets its own extension, created by `registerSymSimpAttr`.
+-/
+abbrev SymSimpExtension := SimpleScopedEnvExtension Theorem Theorems
+
+def SymSimpExtension.getTheorems (ext : SymSimpExtension) : CoreM Theorems :=
+  return ext.getState (← getEnv)
+
+def mkSymSimpExt (name : Name := by exact decl_name%) : IO SymSimpExtension :=
+  registerSimpleScopedEnvExtension {
+    name     := name
+    initial  := {}
+    addEntry := fun thms thm => thms.insert thm
+    exportEntry? := fun lvl thm => do
+      let .const declName _ := thm.expr | return thm
+      guard (lvl == .private || !isPrivateName declName)
+      return thm
+  }
+
+abbrev SymSimpExtensionMap := Std.HashMap Name SymSimpExtension
+
+builtin_initialize symSimpExtensionMapRef : IO.Ref SymSimpExtensionMap ← IO.mkRef {}
+
+def getSymSimpExtension? (attrName : Name) : CoreM (Option SymSimpExtension) := do
+  let ext? := (← symSimpExtensionMapRef.get)[attrName]?
+  if let some ext := ext? then
+    recordExtraModUseFromDecl (isMeta := true) ext.ext.name
+  return ext?
+
 end Lean.Meta.Sym.Simp
diff --git a/tests/elab/sym_simp_set.lean b/tests/elab/sym_simp_set.lean
new file mode 100644
index 0000000000..9605efec54
--- /dev/null
+++ b/tests/elab/sym_simp_set.lean
@@ -0,0 +1,38 @@
+/-
+Tests for the builtin `@[sym_simp]` attribute.
+-/
+import Lean
+
+open Lean Elab Tactic Meta
+
+-- Add rewrite theorems to the default set
+@[sym_simp] theorem add_zero_nat (a : Nat) : a + 0 = a := Nat.add_zero a
+@[sym_simp] theorem zero_add_nat (a : Nat) : 0 + a = a := Nat.zero_add a
+
+-- Add a definition (equation theorems)
+@[sym_simp] def myMul : Nat → Nat → Nat
+  | 0, _ => 0
+  | a + 1, b => b + myMul a b
+
+-- Tactic that uses the default sym_simp set
+elab "sym_simp_default" : tactic => do
+  let thms ← Sym.Simp.getSymSimpTheorems
+  let rewrite := thms.rewrite
+  let methods : Sym.Simp.Methods := {
+    post := Sym.Simp.evalGround.andThen rewrite
+  }
+  liftMetaTactic1 fun mvarId => Sym.SymM.run do
+    let mvarId ← Sym.preprocessMVar mvarId
+    (← Sym.simpGoal mvarId methods).toOption
+
+-- Test: ground evaluation
+example : 2 + 3 = 5 := by sym_simp_default
+
+-- Test: rewrite theorem
+example (n : Nat) : n + 0 = n := by sym_simp_default
+
+-- Test: both rewrite theorems
+example (n : Nat) : 0 + n + 0 = n := by sym_simp_default
+
+-- Test: equation theorems from definition
+example : myMul 3 2 = 6 := by sym_simp_default
\ No newline at end of file
diff --git a/tests/pkg/sym_simp_attr/SymSimpAttr.lean b/tests/pkg/sym_simp_attr/SymSimpAttr.lean
new file mode 100644
index 0000000000..473a916903
--- /dev/null
+++ b/tests/pkg/sym_simp_attr/SymSimpAttr.lean
@@ -0,0 +1,40 @@
+/-
+Tests for `Sym.simp` theorem set attributes.
+-/
+module
+
+import SymSimpAttr.Decl
+public meta import Lean.Elab.Tactic.Basic
+public meta import Lean.Meta.Sym
+
+open Lean Elab Tactic Meta
+
+-- Add a proposition as a rewrite theorem
+@[my_sym_simp] theorem add_zero_nat (a : Nat) : a + 0 = a := Nat.add_zero a
+
+-- Add a definition (equation theorems)
+@[my_sym_simp] def myAdd : Nat → Nat → Nat
+  | 0, b => b
+  | a + 1, b => (myAdd a b) + 1
+
+-- Tactic that uses the theorem set
+elab "sym_simp_set" "[" id:ident "]" : tactic => do
+  let some ext ← Sym.Simp.getSymSimpExtension? id.getId
+    | throwError "Unknown Sym.simp set: {id.getId}"
+  let thms ← ext.getTheorems
+  let rewrite := thms.rewrite
+  let methods : Sym.Simp.Methods := {
+    post := Sym.Simp.evalGround.andThen rewrite
+  }
+  liftMetaTactic1 fun mvarId => Sym.SymM.run do
+    let mvarId ← Sym.preprocessMVar mvarId
+    (← Sym.simpGoal mvarId methods).toOption
+
+-- Test: ground evaluation
+example : 2 + 3 = 5 := by sym_simp_set [my_sym_simp]
+
+-- Test: rewrite theorem from the set
+example (n : Nat) : n + 0 = n := by sym_simp_set [my_sym_simp]
+
+-- Test: equation theorems from definition
+example : myAdd 3 2 = 5 := by sym_simp_set [my_sym_simp]
diff --git a/tests/pkg/sym_simp_attr/SymSimpAttr/Decl.lean b/tests/pkg/sym_simp_attr/SymSimpAttr/Decl.lean
new file mode 100644
index 0000000000..862b83b062
--- /dev/null
+++ b/tests/pkg/sym_simp_attr/SymSimpAttr/Decl.lean
@@ -0,0 +1,9 @@
+/-
+Declare a `Sym.simp` theorem set.
+-/
+module
+
+public import Lean
+public meta import Lean.Meta.Sym.Simp.Attr
+
+register_sym_simp_attr my_sym_simp
diff --git a/tests/pkg/sym_simp_attr/lakefile.lean b/tests/pkg/sym_simp_attr/lakefile.lean
new file mode 100644
index 0000000000..c6ad3fbe5a
--- /dev/null
+++ b/tests/pkg/sym_simp_attr/lakefile.lean
@@ -0,0 +1,5 @@
+import Lake
+open System Lake DSL
+
+package sym_simp_attr
+@[default_target] lean_lib SymSimpAttr
diff --git a/tests/pkg/sym_simp_attr/lean-toolchain b/tests/pkg/sym_simp_attr/lean-toolchain
new file mode 100644
index 0000000000..03eeda634a
--- /dev/null
+++ b/tests/pkg/sym_simp_attr/lean-toolchain
@@ -0,0 +1 @@
+../../../build/release/stage1
\ No newline at end of file
diff --git a/tests/pkg/sym_simp_attr/run_test.sh b/tests/pkg/sym_simp_attr/run_test.sh
new file mode 100755
index 0000000000..b911bf4de8
--- /dev/null
+++ b/tests/pkg/sym_simp_attr/run_test.sh
@@ -0,0 +1,2 @@
+rm -rf .lake/build
+lake build