feat: simp [-decl]

src/Init/Notation.lean

@@ -259,10 +259,11 @@ def expandERwSeq : Macro :=
 
 syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
 
-syntax simpPre := "↓"
-syntax simpPost := "↑"
+syntax simpPre   := "↓"
+syntax simpPost  := "↑"
 syntax simpLemma := (simpPre <|> simpPost)? term
-syntax (name := simp) "simp " (&"only ")? ("[" simpLemma,* "]")? (colGt term)? (location)? : tactic
+syntax simpErase := "-" ident
+syntax (name := simp) "simp " (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (colGt term)? (location)? : tactic
 
 syntax (name := «have») "have " haveDecl : tactic
 syntax (name := «suffices») "suffices " sufficesDecl : tactic

src/Lean/Elab/Tactic/Simp.lean

@@ -82,31 +82,37 @@ private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) : TacticM Simp.Co
     syntax simpPre := "↓"
     syntax simpPost := "↑"
     syntax simpLemma := (simpPre <|> simpPost)? term
-     -/
+
+    syntax simpErase := "-" ident
+    -/
     let (g, _) ← getMainGoal
     withMVarContext g do
       let mut lemmas := ctx.simpLemmas
       let mut toUnfold : NameSet := {}
-      for (arg : Syntax) in stx[1].getSepArgs do
-        let post :=
-          if arg[0].isNone then
-            true
-          else
-            arg[0][0].getKind == ``Parser.Tactic.simpPost
-        match (← resolveSimpIdLemma? arg[1]) with
-        | some e =>
-          if e.isConst then
-            let declName := e.constName!
-            let info ← getConstInfo declName
-            if (← isProp info.type) then
-              lemmas ← lemmas.addConst declName post
+      for arg in stx[1].getSepArgs do
+        if arg.getKind == ``Lean.Parser.Tactic.simpErase then
+          let declName ← resolveGlobalConstNoOverload arg[1].getId
+          lemmas ← lemmas.erase declName
+        else
+          let post :=
+            if arg[0].isNone then
+              true
             else
-              toUnfold := toUnfold.insert declName
-          else
-            lemmas ← lemmas.add e post
-        | _ =>
-          let arg ← elabTerm arg[1] none (mayPostpone := false)
-          lemmas ← lemmas.add arg post
+              arg[0][0].getKind == ``Parser.Tactic.simpPost
+          match (← resolveSimpIdLemma? arg[1]) with
+          | some e =>
+            if e.isConst then
+              let declName := e.constName!
+              let info ← getConstInfo declName
+              if (← isProp info.type) then
+                lemmas ← lemmas.addConst declName post
+              else
+                toUnfold := toUnfold.insert declName
+            else
+              lemmas ← lemmas.add e post
+          | _ =>
+            let arg ← elabTerm arg[1] none (mayPostpone := false)
+            lemmas ← lemmas.add arg post
       return { ctx with simpLemmas := lemmas, toUnfold := toUnfold }
 where
   resolveSimpIdLemma? (simpArgTerm : Syntax) : TacticM (Option Expr) := do

src/Lean/Meta/Tactic/Simp/SimpLemmas.lean

@@ -63,12 +63,14 @@ where
     | none => s
     | some name => s.insert name
 
-private def eraseSimpLemma (d : SimpLemmas) (declName : Name) : SimpLemmas :=
-  { d with erased := d.erased.insert declName, lemmaNames := d.lemmaNames.erase declName }
-
-def isSimpLemma (d : SimpLemmas) (declName : Name) : Bool :=
+def SimpLemmas.isLemma (d : SimpLemmas) (declName : Name) : Bool :=
   d.lemmaNames.contains declName
 
+def SimpLemmas.erase [Monad m] [MonadError m] (d : SimpLemmas) (declName : Name) : m SimpLemmas := do
+  unless d.isLemma declName do
+    throwError! "'{declName}' does not have [simp] attribute"
+  return { d with erased := d.erased.insert declName, lemmaNames := d.lemmaNames.erase declName }
+
 builtin_initialize simpExtension : SimpleScopedEnvExtension SimpLemma SimpLemmas ←
   registerSimpleScopedEnvExtension {
     name     := `simpExt
@@ -127,9 +129,8 @@ builtin_initialize
       discard <| addSimpLemma declName post attrKind prio |>.run {} {}
     erase := fun declName => do
       let s ← simpExtension.getState (← getEnv)
-      unless isSimpLemma s declName do
-        throwError! "'{declName}' does not have [simp] attribute"
-      modifyEnv fun env => simpExtension.modifyState env fun s => eraseSimpLemma s declName
+      let s ← s.erase declName
+      modifyEnv fun env => simpExtension.modifyState env fun _ => s 
   }
 
 def getSimpLemmas : MetaM SimpLemmas :=

tests/lean/eraseSimp.lean

@@ -22,3 +22,8 @@ end
 theorem ex3 {a b : Nat} (h₁ : a = b) : 0 + a = b := by
   simp
   assumption
+
+theorem ex4 {a b : Nat} (h₁ : a = b) : 0 + a = b := by
+  simp [-Nat.zero_add]
+  rw [Nat.zero_add]
+  assumption