diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean
index 08ccdfca5e..41dfdb1051 100644
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@@ -34,6 +34,17 @@ def elabGrindPattern : CommandElab := fun stx => do
         Grind.addEMatchTheorem declName xs.size patterns.toList
   | _ => throwUnsupportedSyntax
 
+open Command Term in
+@[builtin_command_elab Lean.Parser.Command.initGrindNorm]
+def elabInitGrindNorm : CommandElab := fun stx =>
+  match stx with
+  | `(init_grind_norm $pre:ident* | $post*) =>
+    Command.liftTermElabM do
+      let pre ← pre.mapM fun id => realizeGlobalConstNoOverloadWithInfo id
+      let post ← post.mapM fun id => realizeGlobalConstNoOverloadWithInfo id
+      Grind.registerNormTheorems pre post
+  | _ => throwUnsupportedSyntax
+
 def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
   let mut params := params
   for p in ps do
@@ -104,7 +115,7 @@ private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit
     pure auxDeclName
   unsafe evalConst (Grind.GoalM Unit) auxDeclName
 
-@[builtin_tactic Lean.Parser.Tactic.grind] def evalApplyRfl : Tactic := fun stx => do
+@[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
   match stx with
   | `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
     let fallback ← elabFallback fallback?
diff --git a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
index 26b0a71b89..36a72f33af 100644
--- a/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
+++ b/src/Lean/Meta/Tactic/Grind/SimpUtil.lean
@@ -11,6 +11,17 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
 
 namespace Lean.Meta.Grind
 
+builtin_initialize normExt : SimpExtension ← mkSimpExt
+
+def registerNormTheorems (preDeclNames : Array Name) (postDeclNames : Array Name) : MetaM Unit := do
+  let thms ← normExt.getTheorems
+  unless thms.lemmaNames.isEmpty do
+    throwError "`grind` normalization theorems have already been initialized"
+  for declName in preDeclNames do
+    addSimpTheorem normExt declName (post := false) (inv := false) .global (eval_prio default)
+  for declName in postDeclNames do
+    addSimpTheorem normExt declName (post := true) (inv := false) .global (eval_prio default)
+
 /-- Returns the array of simprocs used by `grind`. -/
 protected def getSimprocs : MetaM (Array Simprocs) := do
   let s ← grindNormSimprocExt.getSimprocs