diff --git a/src/Lean/Elab/Tactic/Simproc.lean b/src/Lean/Elab/Tactic/Simproc.lean
index 03034036d9..2905d87f2d 100644
--- a/src/Lean/Elab/Tactic/Simproc.lean
+++ b/src/Lean/Elab/Tactic/Simproc.lean
@@ -13,13 +13,17 @@ namespace Lean.Elab
 
 open Lean Meta Simp
 
-def elabPattern (stx : Syntax) : MetaM Expr := do
+def elabSimprocPattern (stx : Syntax) : MetaM Expr := do
   let go : TermElabM Expr := do
     let pattern ← Term.elabTerm stx none
     Term.synthesizeSyntheticMVars
     return pattern
   go.run'
 
+def elabSimprocKeys (stx : Syntax) : MetaM (Array Meta.SimpTheoremKey) := do
+  let pattern ← elabSimprocPattern stx
+  DiscrTree.mkPath pattern simpDtConfig
+
 def checkSimprocType (declName : Name) : CoreM Unit := do
   let decl ← getConstInfo declName
   match decl.type with
@@ -30,13 +34,23 @@ namespace Command
 
 @[builtin_command_elab Lean.Parser.simprocPattern] def elabSimprocPattern : CommandElab := fun stx => do
   let `(simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
-  let declName := declName.getId
+  let declName ← resolveGlobalConstNoOverload declName
   liftTermElabM do
     checkSimprocType declName
-    let pattern ← elabPattern pattern
-    let keys ← DiscrTree.mkPath pattern simpDtConfig
+    let keys ← elabSimprocKeys pattern
     registerSimproc declName keys
 
+@[builtin_command_elab Lean.Parser.simprocPatternBuiltin] def elabSimprocPatternBuiltin : CommandElab := fun stx => do
+  let `(builtin_simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
+  let declName ← resolveGlobalConstNoOverload declName
+  liftTermElabM do
+    checkSimprocType declName
+    let keys ← elabSimprocKeys pattern
+    registerSimproc declName keys
+    let val := mkAppN (mkConst ``registerBuiltinSimproc) #[toExpr declName, toExpr keys]
+    let initDeclName ← mkFreshUserName (declName ++ `declare)
+    declareBuiltin initDeclName val
+
 end Command
 
 builtin_initialize
@@ -53,4 +67,20 @@ builtin_initialize
     applicationTime := AttributeApplicationTime.afterCompilation
   }
 
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `simprocBuiltinAttr
+    descr           := "Builtin simplification procedure"
+    erase           := eraseSimprocAttr
+    add             := fun declName stx _ => do
+      let go : MetaM Unit := do
+        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
+        let val := mkAppN (mkConst ``addSimprocBuiltinAttr) #[toExpr declName, toExpr post, mkConst declName]
+        let initDeclName ← mkFreshUserName (declName ++ `declare)
+        declareBuiltin initDeclName val
+      go.run' {}
+    applicationTime := AttributeApplicationTime.afterCompilation
+  }
+
 end Lean.Elab
diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean
index dcee0a66f7..89c8fc82c0 100644
--- a/src/Lean/Meta/DiscrTreeTypes.lean
+++ b/src/Lean/Meta/DiscrTreeTypes.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Expr
+import Lean.ToExpr
 
 namespace Lean.Meta
 
@@ -34,6 +35,17 @@ protected def Key.hash : Key → UInt64
 
 instance : Hashable Key := ⟨Key.hash⟩
 
+instance : ToExpr Key where
+  toTypeExpr := mkConst ``Key
+  toExpr k   := match k with
+   | .const n a => mkApp2 (mkConst ``Key.const) (toExpr n) (toExpr a)
+   | .fvar id a => mkApp2 (mkConst ``Key.fvar) (toExpr id) (toExpr a)
+   | .lit l => mkApp (mkConst ``Key.lit) (toExpr l)
+   | .star => mkConst ``Key.star
+   | .other => mkConst ``Key.other
+   | .arrow => mkConst ``Key.arrow
+   | .proj n i a => mkApp3 (mkConst ``Key.proj) (toExpr n) (toExpr i) (toExpr a)
+
 /--
 Discrimination tree trie. See `DiscrTree`.
 -/
diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean
index 431b2427c3..f3033d77f5 100644
--- a/src/Lean/Meta/Tactic/Simp/Simproc.lean
+++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean
@@ -124,6 +124,14 @@ def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs
   else
     return { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
 
+def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit := do
+  let some keys := (← builtinSimprocDeclsRef.get).find? declName |
+    throw (IO.userError "invalid [builtin_simproc] attribute, '{declName}' is not a builtin simproc")
+  if post then
+    builtinSimprocsRef.modify fun s => { s with post := s.post.insertCore keys { declName, keys, post, proc } }
+  else
+    builtinSimprocsRef.modify fun s => { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+
 def getSimprocs : CoreM Simprocs :=
   return simprocExtension.getState (← getEnv)
 
diff --git a/src/Lean/ToExpr.lean b/src/Lean/ToExpr.lean
index 8b810a7bf3..34cdf386ce 100644
--- a/src/Lean/ToExpr.lean
+++ b/src/Lean/ToExpr.lean
@@ -100,6 +100,16 @@ instance [ToExpr α] [ToExpr β] : ToExpr (α × β) :=
   { toExpr     := fun ⟨a, b⟩ => mkApp4 (mkConst ``Prod.mk [levelZero, levelZero]) αType βType (toExpr a) (toExpr b),
     toTypeExpr := mkApp2 (mkConst ``Prod [levelZero, levelZero]) αType βType }
 
+instance : ToExpr Literal where
+  toTypeExpr := mkConst ``Literal
+  toExpr l   := match l with
+   | .natVal _ => mkApp (mkConst ``Literal.natVal) (.lit l)
+   | .strVal _ => mkApp (mkConst ``Literal.strVal) (.lit l)
+
+instance : ToExpr FVarId where
+  toTypeExpr    := mkConst ``FVarId
+  toExpr fvarId := mkApp (mkConst ``FVarId.mk) (toExpr fvarId.name)
+
 def Expr.toCtorIfLit : Expr → Expr
   | .lit (.natVal v) =>
     if v == 0 then mkConst ``Nat.zero