From 3be437cad378e848da063ef16e67b8eca7ff73c0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 May 2022 19:49:33 -0700
Subject: [PATCH] fix: make sure `register_simp_attr` declares an simp-like
 attribute parser for user `simp` attributes

closes #1164
---
 src/Lean/Meta/Tactic/Simp/SimpTheorems.lean |  6 ++++-
 tests/pkg/user_attr/UserAttr/Tst.lean       | 27 +++++++++++++++++++++
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index f41f1f5196..631e1d1ac6 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -411,7 +411,11 @@ def SimpTheoremsArray.isErased (thmsArray : SimpTheoremsArray) (thmId : Name) :
 def SimpTheoremsArray.isDeclToUnfold (thmsArray : SimpTheoremsArray) (declName : Name) : Bool :=
   thmsArray.any fun thms => thms.isDeclToUnfold declName
 
-macro "register_simp_attr" id:ident descr:str : command => `(initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr)
+macro "register_simp_attr" id:ident descr:str : command => do
+  let str := id.getId.toString
+  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
+  `(initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr
+    syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? (prio)? : attr)
 
 end Meta
 
diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean
index d40fe1391e..1a08e5f333 100644
--- a/tests/pkg/user_attr/UserAttr/Tst.lean
+++ b/tests/pkg/user_attr/UserAttr/Tst.lean
@@ -1,3 +1,4 @@
+import Lean
 import UserAttr.BlaAttr
 
 @[bla] def f (x : Nat) := x + 2
@@ -21,3 +22,29 @@ macro "my_simp" : tactic => `(simp [my_simp])
 
 example : f x = id (x + 2) := by
   my_simp
+
+
+@[simp low, my_simp low]
+theorem expand_mul_add (x y z : Nat) : x * (y + z) = x * y + x * y := sorry
+@[simp high, my_simp high]
+theorem expand_add_mul (x y z : Nat) : (x + y) * z = x * z + y * z := sorry
+@[simp, my_simp]
+theorem lassoc_add (x y z : Nat) : x + (y + z) = x + y + z := sorry
+
+set_option trace.Meta.Tactic.simp.rewrite true
+
+-- Rewrites: expand_mul_add -> expand_mul_add -> lassoc_add
+theorem ex1 (x : Nat) : (x + x) * (x + x) = x * x + x * x + x * x + x * x := by simp only [my_simp]
+
+-- Rewrites: expand_add_mul -> expand_mul_add -> lassoc_add
+theorem ex2 (x : Nat) : (x + x) * (x + x) = x * x + x * x + x * x + x * x := by simp
+
+open Lean
+open Lean.Meta
+def checkProofs : MetaM Unit := do
+  let ConstantInfo.thmInfo info1 ← getConstInfo `ex1 | throwError "unexpected"
+  let ConstantInfo.thmInfo info2 ← getConstInfo `ex2 | throwError "unexpected"
+  unless info1.value == info2.value do
+    throwError "unexpected values"
+
+#eval checkProofs