From dab5e17bf92c982827ee95d14225438efda36490 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 26 Feb 2024 13:19:51 -0800
Subject: [PATCH 1/5] fix: allow simproc to be erased using `attribute` command

---
 src/Lean/Meta/Tactic/Simp/Simproc.lean | 25 +++++++++++--------------
 1 file changed, 11 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean
index 5afc964ffedc..3f2a5e32b297 100644
--- a/src/Lean/Meta/Tactic/Simp/Simproc.lean
+++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean
@@ -127,7 +127,7 @@ def toSimprocEntry (e : SimprocOLeanEntry) : ImportM SimprocEntry := do
 def eraseSimprocAttr (ext : SimprocExtension) (declName : Name) : AttrM Unit := do
   let s := ext.getState (← getEnv)
   unless s.simprocNames.contains declName do
-    throwError "'{declName}' does not have [simproc] attribute"
+    throwError "'{declName}' does not have a simproc attribute"
   modifyEnv fun env => ext.modifyState env fun s => s.erase declName
 
 def addSimprocAttr (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
@@ -136,16 +136,20 @@ def addSimprocAttr (ext : SimprocExtension) (declName : Name) (kind : AttributeK
     throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
   ext.add { declName, post, keys, proc } kind
 
+def Simprocs.addCore (s : Simprocs) (keys : Array SimpTheoremKey) (declName : Name) (post : Bool) (proc : Simproc) : Simprocs :=
+  let s := { s with simprocNames := s.simprocNames.insert declName, erased := s.erased.erase declName }
+  if post then
+    { s with post := s.post.insertCore keys { declName, keys, post, proc } }
+  else
+    { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+
 /--
 Implements attributes `builtin_simproc` and `builtin_sevalproc`.
 -/
 def addSimprocBuiltinAttrCore (ref : IO.Ref Simprocs) (declName : Name) (post : Bool) (proc : Simproc) : IO Unit := do
   let some keys := (← builtinSimprocDeclsRef.get).keys.find? declName |
     throw (IO.userError "invalid [builtin_simproc] attribute, '{declName}' is not a builtin simproc")
-  if post then
-    ref.modify fun s => { s with post := s.post.insertCore keys { declName, keys, post, proc } }
-  else
-    ref.modify fun s => { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+  ref.modify fun s => s.addCore keys declName post proc
 
 def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit :=
   addSimprocBuiltinAttrCore builtinSimprocsRef declName post proc
@@ -166,10 +170,7 @@ def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs
         throw e
   let some keys ← getSimprocDeclKeys? declName |
     throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
-  if post then
-    return { s with post := s.post.insertCore keys { declName, keys, post, proc } }
-  else
-    return { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+  return s.addCore keys declName post proc
 
 def SimprocEntry.try (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM Step := do
   let mut extraArgs := #[]
@@ -276,11 +277,7 @@ def mkSimprocExt (name : Name := by exact decl_name%) (ref? : Option (IO.Ref Sim
         return {}
     ofOLeanEntry  := fun _ => toSimprocEntry
     toOLeanEntry  := fun e => e.toSimprocOLeanEntry
-    addEntry      := fun s e =>
-      if e.post then
-        { s with post := s.post.insertCore e.keys e }
-      else
-        { s with pre := s.pre.insertCore e.keys e }
+    addEntry      := fun s e => s.addCore e.keys e.declName e.post e.proc
   }
 
 def mkSimprocAttr (attrName : Name) (attrDescr : String) (ext : SimprocExtension) (name : Name) : IO Unit := do

From dde5e2d65782459b5305b00aad3b55f945635430 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 26 Feb 2024 13:44:49 -0800
Subject: [PATCH 2/5] refactor: move `simp` attribute declaration to
 `Simp/Attr.lean`

Motivation: we want to be able to reference the associated simproc
attribute.
---
 src/Lean/Meta/Tactic/NormCast.lean          |  2 +-
 src/Lean/Meta/Tactic/Simp.lean              |  1 +
 src/Lean/Meta/Tactic/Simp/Attr.lean         | 64 +++++++++++++++++++++
 src/Lean/Meta/Tactic/Simp/Rewrite.lean      |  1 +
 src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 48 ----------------
 src/Lean/Meta/Tactic/Simp/Types.lean        |  3 -
 6 files changed, 67 insertions(+), 52 deletions(-)
 create mode 100644 src/Lean/Meta/Tactic/Simp/Attr.lean

diff --git a/src/Lean/Meta/Tactic/NormCast.lean b/src/Lean/Meta/Tactic/NormCast.lean
index c0cc81cf2256..d727d309c841 100644
--- a/src/Lean/Meta/Tactic/NormCast.lean
+++ b/src/Lean/Meta/Tactic/NormCast.lean
@@ -5,7 +5,7 @@ Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
 -/
 prelude
 import Lean.Meta.CongrTheorems
-import Lean.Meta.Tactic.Simp.SimpTheorems
+import Lean.Meta.Tactic.Simp.Attr
 import Lean.Meta.CoeAttr
 
 namespace Lean.Meta.NormCast
diff --git a/src/Lean/Meta/Tactic/Simp.lean b/src/Lean/Meta/Tactic/Simp.lean
index 3afb43498f00..6987220330c7 100644
--- a/src/Lean/Meta/Tactic/Simp.lean
+++ b/src/Lean/Meta/Tactic/Simp.lean
@@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Simp.SimpAll
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 import Lean.Meta.Tactic.Simp.RegisterCommand
+import Lean.Meta.Tactic.Simp.Attr
 
 namespace Lean
 
diff --git a/src/Lean/Meta/Tactic/Simp/Attr.lean b/src/Lean/Meta/Tactic/Simp/Attr.lean
new file mode 100644
index 000000000000..bf5755534407
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Simp/Attr.lean
@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2024 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
+-/
+prelude
+import Lean.Meta.Tactic.Simp.SimpTheorems
+import Lean.Meta.Tactic.Simp.Types
+
+namespace Lean.Meta
+
+def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
+    (ref : Name := by exact decl_name%) : IO Unit :=
+  registerBuiltinAttribute {
+    ref   := ref
+    name  := attrName
+    descr := attrDescr
+    applicationTime := AttributeApplicationTime.afterCompilation
+    add   := fun declName stx attrKind =>
+      let go : MetaM Unit := do
+        let info ← getConstInfo declName
+        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
+        let prio ← getAttrParamOptPrio stx[2]
+        if (← isProp info.type) then
+          addSimpTheorem ext declName post (inv := false) attrKind prio
+        else if info.hasValue then
+          if let some eqns ← getEqnsFor? declName then
+            for eqn in eqns do
+              addSimpTheorem ext eqn post (inv := false) attrKind prio
+            ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind
+            if hasSmartUnfoldingDecl (← getEnv) declName then
+              ext.add (SimpEntry.toUnfold declName) attrKind
+          else
+            ext.add (SimpEntry.toUnfold declName) attrKind
+        else
+          throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
+      discard <| go.run {} {}
+    erase := fun declName => do
+      let s := ext.getState (← getEnv)
+      let s ← s.erase (.decl declName)
+      modifyEnv fun env => ext.modifyState env fun _ => s
+  }
+
+def registerSimpAttr (attrName : Name) (attrDescr : String)
+    (ref : Name := by exact decl_name%) : IO SimpExtension := do
+  let ext ← mkSimpExt ref
+  mkSimpAttr attrName attrDescr ext ref -- Remark: it will fail if it is not performed during initialization
+  simpExtensionMapRef.modify fun map => map.insert attrName ext
+  return ext
+
+builtin_initialize simpExtension : SimpExtension ← registerSimpAttr `simp "simplification theorem"
+
+builtin_initialize sevalSimpExtension : SimpExtension ← registerSimpAttr `seval "symbolic evaluator theorem"
+
+def getSimpTheorems : CoreM SimpTheorems :=
+  simpExtension.getTheorems
+
+def getSEvalTheorems : CoreM SimpTheorems :=
+  sevalSimpExtension.getTheorems
+
+def Simp.Context.mkDefault : MetaM Context :=
+  return { config := {}, simpTheorems := #[(← Meta.getSimpTheorems)], congrTheorems := (← Meta.getSimpCongrTheorems) }
+
+end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 39197f24fcd4..90e83f5235df 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -12,6 +12,7 @@ import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.LinearArith.Simp
 import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Simp.Attr
 
 namespace Lean.Meta.Simp
 
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 44816e98a6e1..143f226246e3 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -362,37 +362,6 @@ def addSimpTheorem (ext : SimpExtension) (declName : Name) (post : Bool) (inv :
   for simpThm in simpThms do
     ext.add (SimpEntry.thm simpThm) attrKind
 
-def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
-    (ref : Name := by exact decl_name%) : IO Unit :=
-  registerBuiltinAttribute {
-    ref   := ref
-    name  := attrName
-    descr := attrDescr
-    applicationTime := AttributeApplicationTime.afterCompilation
-    add   := fun declName stx attrKind =>
-      let go : MetaM Unit := do
-        let info ← getConstInfo declName
-        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-        let prio ← getAttrParamOptPrio stx[2]
-        if (← isProp info.type) then
-          addSimpTheorem ext declName post (inv := false) attrKind prio
-        else if info.hasValue then
-          if let some eqns ← getEqnsFor? declName then
-            for eqn in eqns do
-              addSimpTheorem ext eqn post (inv := false) attrKind prio
-            ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind
-            if hasSmartUnfoldingDecl (← getEnv) declName then
-              ext.add (SimpEntry.toUnfold declName) attrKind
-          else
-            ext.add (SimpEntry.toUnfold declName) attrKind
-        else
-          throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
-      discard <| go.run {} {}
-    erase := fun declName => do
-      let s := ext.getState (← getEnv)
-      let s ← s.erase (.decl declName)
-      modifyEnv fun env => ext.modifyState env fun _ => s
-  }
 
 def mkSimpExt (name : Name := by exact decl_name%) : IO SimpExtension :=
   registerSimpleScopedEnvExtension {
@@ -409,26 +378,9 @@ abbrev SimpExtensionMap := HashMap Name SimpExtension
 
 builtin_initialize simpExtensionMapRef : IO.Ref SimpExtensionMap ← IO.mkRef {}
 
-def registerSimpAttr (attrName : Name) (attrDescr : String)
-    (ref : Name := by exact decl_name%) : IO SimpExtension := do
-  let ext ← mkSimpExt ref
-  mkSimpAttr attrName attrDescr ext ref -- Remark: it will fail if it is not performed during initialization
-  simpExtensionMapRef.modify fun map => map.insert attrName ext
-  return ext
-
-builtin_initialize simpExtension : SimpExtension ← registerSimpAttr `simp "simplification theorem"
-
-builtin_initialize sevalSimpExtension : SimpExtension ← registerSimpAttr `seval "symbolic evaluator theorem"
-
 def getSimpExtension? (attrName : Name) : IO (Option SimpExtension) :=
   return (← simpExtensionMapRef.get).find? attrName
 
-def getSimpTheorems : CoreM SimpTheorems :=
-  simpExtension.getTheorems
-
-def getSEvalTheorems : CoreM SimpTheorems :=
-  sevalSimpExtension.getTheorems
-
 /-- Auxiliary method for adding a global declaration to a `SimpTheorems` datastructure. -/
 def SimpTheorems.addConst (s : SimpTheorems) (declName : Name) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM SimpTheorems := do
   let s := { s with erased := s.erased.erase (.decl declName post inv) }
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index b778788bbb70..bc722b8870e5 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -92,9 +92,6 @@ structure Context where
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
-def Context.mkDefault : MetaM Context :=
-  return { config := {}, simpTheorems := #[(← getSimpTheorems)], congrTheorems := (← getSimpCongrTheorems) }
-
 abbrev UsedSimps := HashMap Origin Nat
 
 structure State where

From 5171aed6889a5948425590cfb185ca4a28622be0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 26 Feb 2024 14:09:07 -0800
Subject: [PATCH 3/5] feat: invoke simproc attribute handlers from `simp`
 attribute handlers

---
 src/Lean/Meta/Tactic/Simp/Attr.lean           | 52 +++++++++++--------
 .../Meta/Tactic/Simp/RegisterCommand.lean     |  1 +
 src/Lean/Meta/Tactic/Simp/Simproc.lean        | 14 ++---
 3 files changed, 40 insertions(+), 27 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Simp/Attr.lean b/src/Lean/Meta/Tactic/Simp/Attr.lean
index bf5755534407..7b5433d910c6 100644
--- a/src/Lean/Meta/Tactic/Simp/Attr.lean
+++ b/src/Lean/Meta/Tactic/Simp/Attr.lean
@@ -4,10 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.Tactic.Simp.Types
+import Lean.Meta.Tactic.Simp.SimpTheorems
+import Lean.Meta.Tactic.Simp.Simproc
 
 namespace Lean.Meta
+open Simp
 
 def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
     (ref : Name := by exact decl_name%) : IO Unit :=
@@ -16,29 +18,37 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
     name  := attrName
     descr := attrDescr
     applicationTime := AttributeApplicationTime.afterCompilation
-    add   := fun declName stx attrKind =>
-      let go : MetaM Unit := do
-        let info ← getConstInfo declName
-        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-        let prio ← getAttrParamOptPrio stx[2]
-        if (← isProp info.type) then
-          addSimpTheorem ext declName post (inv := false) attrKind prio
-        else if info.hasValue then
-          if let some eqns ← getEqnsFor? declName then
-            for eqn in eqns do
-              addSimpTheorem ext eqn post (inv := false) attrKind prio
-            ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind
-            if hasSmartUnfoldingDecl (← getEnv) declName then
+    add   := fun declName stx attrKind => do
+      if (← isSimproc declName <||> isBuiltinSimproc declName) then
+        let simprocAttrName := simpAttrNameToSimprocAttrName attrName
+        Attribute.add declName simprocAttrName stx attrKind
+      else
+        let go : MetaM Unit := do
+          let info ← getConstInfo declName
+          let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
+          let prio ← getAttrParamOptPrio stx[2]
+          if (← isProp info.type) then
+            addSimpTheorem ext declName post (inv := false) attrKind prio
+          else if info.hasValue then
+            if let some eqns ← getEqnsFor? declName then
+              for eqn in eqns do
+                addSimpTheorem ext eqn post (inv := false) attrKind prio
+              ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind
+              if hasSmartUnfoldingDecl (← getEnv) declName then
+                ext.add (SimpEntry.toUnfold declName) attrKind
+            else
               ext.add (SimpEntry.toUnfold declName) attrKind
           else
-            ext.add (SimpEntry.toUnfold declName) attrKind
-        else
-          throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
-      discard <| go.run {} {}
+            throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
+        discard <| go.run {} {}
     erase := fun declName => do
-      let s := ext.getState (← getEnv)
-      let s ← s.erase (.decl declName)
-      modifyEnv fun env => ext.modifyState env fun _ => s
+      if (← isSimproc declName <||> isBuiltinSimproc declName) then
+        let simprocAttrName := simpAttrNameToSimprocAttrName attrName
+        Attribute.erase declName simprocAttrName
+      else
+        let s := ext.getState (← getEnv)
+        let s ← s.erase (.decl declName)
+        modifyEnv fun env => ext.modifyState env fun _ => s
   }
 
 def registerSimpAttr (attrName : Name) (attrDescr : String)
diff --git a/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean b/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean
index 7f8829a8dab7..67a393a3ee5d 100644
--- a/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean
+++ b/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Simp.Attr
 
 namespace Lean.Meta.Simp
 
diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean
index 3f2a5e32b297..8d74f7dd8fed 100644
--- a/src/Lean/Meta/Tactic/Simp/Simproc.lean
+++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean
@@ -130,7 +130,7 @@ def eraseSimprocAttr (ext : SimprocExtension) (declName : Name) : AttrM Unit :=
     throwError "'{declName}' does not have a simproc attribute"
   modifyEnv fun env => ext.modifyState env fun s => s.erase declName
 
-def addSimprocAttr (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
+def addSimprocAttrCore (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
   let proc ← getSimprocFromDecl declName
   let some keys ← getSimprocDeclKeys? declName |
     throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
@@ -280,17 +280,19 @@ def mkSimprocExt (name : Name := by exact decl_name%) (ref? : Option (IO.Ref Sim
     addEntry      := fun s e => s.addCore e.keys e.declName e.post e.proc
   }
 
+def addSimprocAttr (ext : SimprocExtension) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
+  let go : MetaM Unit := do
+    let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
+    addSimprocAttrCore ext declName attrKind post
+  discard <| go.run {} {}
+
 def mkSimprocAttr (attrName : Name) (attrDescr : String) (ext : SimprocExtension) (name : Name) : IO Unit := do
   registerBuiltinAttribute {
     ref   := name
     name  := attrName
     descr := attrDescr
     applicationTime := AttributeApplicationTime.afterCompilation
-    add   := fun declName stx attrKind =>
-      let go : MetaM Unit := do
-        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-        addSimprocAttr ext declName attrKind post
-      discard <| go.run {} {}
+    add   := addSimprocAttr ext
     erase := eraseSimprocAttr ext
   }
 

From e26a962dc661072970571ce3273c40fbc6085220 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 26 Feb 2024 14:17:35 -0800
Subject: [PATCH 4/5] test: `attribute` command for simprocs

---
 tests/lean/run/simproc_erase.lean | 49 +++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 tests/lean/run/simproc_erase.lean

diff --git a/tests/lean/run/simproc_erase.lean b/tests/lean/run/simproc_erase.lean
new file mode 100644
index 000000000000..ed1704eda080
--- /dev/null
+++ b/tests/lean/run/simproc_erase.lean
@@ -0,0 +1,49 @@
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs
+
+def foo (x : Nat) : Nat :=
+  x + 10
+
+open Lean Meta
+
+/-- doc-comment for reduceFoo -/
+simproc reduceFoo (foo _) := fun e => do
+  unless e.isAppOfArity ``foo 1 do return .continue
+  let some n ← Nat.fromExpr? e.appArg! | return .continue
+  return .done { expr := mkNatLit (n+10) }
+
+example : x + foo 2 = 12 + x := by
+  simp
+  rw [Nat.add_comm]
+
+attribute [-simp] reduceFoo
+
+example : x + foo 2 = 12 + x := by
+  fail_if_success simp
+  simp [foo]
+  rw [Nat.add_comm]
+
+attribute [simp] reduceFoo
+
+example : x + foo 2 = 12 + x := by
+  simp
+  rw [Nat.add_comm]
+
+example (h : 12 = x) : 10 + 2 = x := by
+  simp
+  guard_target =ₛ 12 = x
+  assumption
+
+attribute [-simp] Nat.reduceAdd
+
+example (h : 12 = x) : 10 + 2 = x := by
+  fail_if_success simp
+  simp [Nat.reduceAdd]
+  guard_target =ₛ 12 = x
+  assumption
+
+attribute [simp] Nat.reduceAdd
+
+example (h : 12 = x) : 10 + 2 = x := by
+  simp
+  guard_target =ₛ 12 = x
+  assumption

From bf8f40addf635d371f0ef1179909b2c93a785523 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 26 Feb 2024 14:38:49 -0800
Subject: [PATCH 5/5] fix: allow builtin simprocs to be deleted even when we
 have not imported the file defining them

---
 src/Lean/Elab/Declaration.lean            | 16 +++++++++++++++-
 tests/lean/run/simproc_builtin_erase.lean | 12 ++++++++++++
 2 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/simproc_builtin_erase.lean

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 931c4674bb44..c8af67d77a30 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -347,7 +347,21 @@ def elabMutual : CommandElab := fun stx => do
   let attrs ← elabAttrs attrInsts
   let idents := stx[4].getArgs
   for ident in idents do withRef ident <| liftTermElabM do
-    let declName ← resolveGlobalConstNoOverloadWithInfo ident
+    /-
+    HACK to allow `attribute` command to disable builtin simprocs.
+    TODO: find a better solution. Example: have some "fake" declaration
+    for builtin simprocs.
+    -/
+    let declNames ←
+       try
+         resolveGlobalConst ident
+       catch _ =>
+         let name := ident.getId.eraseMacroScopes
+         if (← Simp.isBuiltinSimproc name) then
+           pure [name]
+         else
+           throwUnknownConstant name
+    let declName ← ensureNonAmbiguous ident declNames
     Term.applyAttributes declName attrs
     for attrName in toErase do
       Attribute.erase declName attrName
diff --git a/tests/lean/run/simproc_builtin_erase.lean b/tests/lean/run/simproc_builtin_erase.lean
new file mode 100644
index 000000000000..4a9310eb9dfa
--- /dev/null
+++ b/tests/lean/run/simproc_builtin_erase.lean
@@ -0,0 +1,12 @@
+example (h : 12 = x) : 10 + 2 = x := by
+  simp
+  guard_target =ₛ 12 = x
+  assumption
+
+attribute [-simp] Nat.reduceAdd
+
+example (h : 12 = x) : 10 + 2 = x := by
+  fail_if_success simp
+  simp [Nat.reduceAdd]
+  guard_target =ₛ 12 = x
+  assumption