From 173b95696129f5efeac9d2cd5a83a724c48cf7ae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 14 Mar 2024 17:33:22 -0700
Subject: [PATCH] feat: reserved names  (#3675)

- Add support for reserved declaration names. We use them for theorems
generated on demand.
- Equation theorems are not private declarations anymore.
- Generate equation theorems on demand when resolving symbols.
- Prevent users from creating declarations using reserved names. Users
can bypass it using meta-programming.

See next test for examples.
---
 src/Init/Core.lean                            |   2 +-
 src/Init/Prelude.lean                         |   6 +
 src/Init/PropLemmas.lean                      |   2 +-
 src/Lean.lean                                 |   1 +
 src/Lean/Compiler/ImplementedByAttr.lean      |   2 +-
 src/Lean/Compiler/InitAttr.lean               |   2 +-
 src/Lean/Elab/BuiltinCommand.lean             |   4 +-
 src/Lean/Elab/BuiltinTerm.lean                |   2 +-
 src/Lean/Elab/DeclModifiers.lean              |   2 +
 src/Lean/Elab/Declaration.lean                |   4 +-
 src/Lean/Elab/Deriving/Basic.lean             |   8 +-
 src/Lean/Elab/GenInjective.lean               |   2 +-
 src/Lean/Elab/InfoTree/Main.lean              |  22 ++-
 src/Lean/Elab/InheritDoc.lean                 |   2 +-
 src/Lean/Elab/MutualDef.lean                  |   2 +-
 src/Lean/Elab/PreDefinition/Eqns.lean         |  20 +--
 src/Lean/Elab/PreDefinition/Main.lean         |   1 +
 .../Elab/PreDefinition/Structural/Eqns.lean   |   3 +-
 src/Lean/Elab/PreDefinition/WF/Eqns.lean      |   3 +-
 src/Lean/Elab/Print.lean                      |   6 +-
 src/Lean/Elab/Quotation/Precheck.lean         |   2 +-
 src/Lean/Elab/Structure.lean                  |   2 +-
 src/Lean/Elab/Tactic/Conv/Delta.lean          |   2 +-
 src/Lean/Elab/Tactic/Conv/Unfold.lean         |   2 +-
 src/Lean/Elab/Tactic/Delta.lean               |   2 +-
 src/Lean/Elab/Tactic/Ext.lean                 |   4 +-
 src/Lean/Elab/Tactic/NormCast.lean            |   2 +-
 src/Lean/Elab/Tactic/Rewrite.lean             |   6 +-
 src/Lean/Elab/Tactic/Simp.lean                |   2 +-
 src/Lean/Elab/Tactic/Simproc.lean             |   5 +-
 src/Lean/Elab/Tactic/Unfold.lean              |   2 +-
 src/Lean/Elab/Term.lean                       |   3 +-
 src/Lean/Environment.lean                     |   9 +-
 src/Lean/Linter/Deprecated.lean               |   2 +-
 src/Lean/Linter/MissingDocs.lean              |   2 +-
 src/Lean/Meta/Eqns.lean                       | 167 ++++++++++++------
 src/Lean/Meta/Tactic/FunInd.lean              |   2 +-
 src/Lean/ParserCompiler/Attribute.lean        |   2 +-
 src/Lean/PrettyPrinter/Delaborator/Basic.lean |   2 +-
 src/Lean/ReservedNameAction.lean              |  80 +++++++++
 src/Lean/ResolveName.lean                     | 140 ++++++++++-----
 src/Lean/Server/CodeActions/Attr.lean         |   4 +-
 tests/lean/run/matchEqs.lean                  |   2 +-
 tests/lean/run/matchEqsBug.lean               |   2 +-
 tests/lean/run/printEqns.lean                 |  14 +-
 tests/lean/run/reserved.lean                  |  90 ++++++++++
 46 files changed, 470 insertions(+), 178 deletions(-)
 create mode 100644 src/Lean/ReservedNameAction.lean
 create mode 100644 tests/lean/run/reserved.lean

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 4b8acf3190..d27672e927 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -19,7 +19,7 @@ which applies to all applications of the function).
 -/
 @[simp] def inline {α : Sort u} (a : α) : α := a
 
-theorem id.def {α : Sort u} (a : α) : id a = a := rfl
+theorem id_def {α : Sort u} (a : α) : id a = a := rfl
 
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 918ff44428..23d7468443 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -4581,6 +4581,12 @@ def resolveNamespace (n : Name) : MacroM (List Name) := do
 Resolves the given name to an overload list of global definitions.
 The `List String` in each alternative is the deduced list of projections
 (which are ambiguous with name components).
+
+Remark: it will not trigger actions associated with reserved names. Recall that Lean
+has reserved names. For example, a definition `foo` has a reserved name `foo.def` for theorem
+containing stating that `foo` is equal to its definition. The action associated with `foo.def`
+automatically proves the theorem. At the macro level, the name is resolved, but the action is not
+executed. The actions are executed by the elaborator when converting `Syntax` into `Expr`.
 -/
 def resolveGlobalName (n : Name) : MacroM (List (Prod Name (List String))) := do
   (← getMethods).resolveGlobalName n
diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index 2a7a55aa70..27bd1db1c8 100644
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -21,7 +21,7 @@ set_option linter.missingDocs true -- keep it documented
   | rfl, rfl, _ => rfl
 
 @[simp] theorem eq_true_eq_id : Eq True = id := by
-  funext _; simp only [true_iff, id.def, eq_iff_iff]
+  funext _; simp only [true_iff, id_def, eq_iff_iff]
 
 /-! ## not -/
 
diff --git a/src/Lean.lean b/src/Lean.lean
index 0fdcd21991..e026559b8b 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -24,6 +24,7 @@ import Lean.Eval
 import Lean.Structure
 import Lean.PrettyPrinter
 import Lean.CoreM
+import Lean.ReservedNameAction
 import Lean.InternalExceptionId
 import Lean.Server
 import Lean.ScopedEnvExtension
diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean
index 70f00fc251..9d2aae8115 100644
--- a/src/Lean/Compiler/ImplementedByAttr.lean
+++ b/src/Lean/Compiler/ImplementedByAttr.lean
@@ -17,7 +17,7 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
   getParam := fun declName stx => do
     let decl ← getConstInfo declName
     let fnNameStx ← Attribute.Builtin.getIdent stx
-    let fnName ← Elab.resolveGlobalConstNoOverloadWithInfo fnNameStx
+    let fnName ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
     let fnDecl ← getConstInfo fnName
     unless decl.levelParams.length == fnDecl.levelParams.length do
       throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}"
diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean
index 4e9dc2455e..4e723152fa 100644
--- a/src/Lean/Compiler/InitAttr.lean
+++ b/src/Lean/Compiler/InitAttr.lean
@@ -44,7 +44,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
       let decl ← getConstInfo declName
       match (← Attribute.Builtin.getIdent? stx) with
       | some initFnName =>
-        let initFnName ← Elab.resolveGlobalConstNoOverloadWithInfo initFnName
+        let initFnName ← Elab.realizeGlobalConstNoOverloadWithInfo initFnName
         let initDecl ← getConstInfo initFnName
         match getIOTypeArg initDecl.type with
         | none => throwError "initialization function '{initFnName}' must have type of the form `IO <type>`"
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 472d15a463..3fb3954ddf 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -536,7 +536,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
     -- show signature for `#check id`/`#check @id`
     if let `($id:ident) := term then
       try
-        for c in (← resolveGlobalConstWithInfos term) do
+        for c in (← realizeGlobalConstWithInfos term) do
           addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
           logInfoAt tk <| .ofPPFormat { pp := fun
             | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
@@ -760,7 +760,7 @@ def elabRunMeta : CommandElab := fun stx =>
 @[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do
   match stx with
   | `($doc:docComment add_decl_doc $id) =>
-    let declName ← resolveGlobalConstNoOverloadWithInfo id
+    let declName ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
     unless ((← getEnv).getModuleIdxFor? declName).isNone do
       throwError "invalid 'add_decl_doc', declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index e19559062b..89f786a36d 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -223,7 +223,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
   | none     => throwIllFormedSyntax
 
 @[builtin_term_elab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ =>
-  return toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
+  return toExpr (← realizeGlobalConstNoOverloadWithInfo stx[2])
 
 @[builtin_term_elab declName] def elabDeclName : TermElab := adaptExpander fun _ => do
   let some declName ← getDeclName?
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index 31fc18ebf8..90f792a233 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -27,6 +27,8 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
     match privateToUserName? declName with
     | none          => throwError "'{declName}' has already been declared"
     | some declName => throwError "private declaration '{declName}' has already been declared"
+  if isReservedName env declName then
+    throwError "'{declName}' is a reserved name"
   if env.contains (mkPrivateName env declName) then
     addInfo (mkPrivateName env declName)
     throwError "a private declaration '{declName}' has already been declared"
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 70ea51f354..0dd887c66c 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -166,7 +166,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
     return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
   let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
     return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
-  let classes ← getOptDerivingClasses decl[6]
+  let classes ← liftCoreM <| getOptDerivingClasses decl[6]
   return {
     ref             := decl
     shortDeclName   := name
@@ -354,7 +354,7 @@ def elabMutual : CommandElab := fun stx => do
     -/
     let declNames ←
        try
-         resolveGlobalConst ident
+         realizeGlobalConst ident
        catch _ =>
          let name := ident.getId.eraseMacroScopes
          if (← Simp.isBuiltinSimproc name) then
diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
index b8d093309a..4db97520d5 100644
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -100,10 +100,10 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
 
 @[builtin_command_elab «deriving»] def elabDeriving : CommandElab
   | `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
-     let declNames ← declNames.mapM resolveGlobalConstNoOverloadWithInfo
+     let declNames ← liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
      for cls in classes, args? in argss? do
        try
-         let className ← resolveGlobalConstNoOverloadWithInfo cls
+         let className ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo cls
          withRef cls do
            if declNames.size == 1 && args?.isNone then
              if (← tryApplyDefHandler className declNames[0]!) then
@@ -118,12 +118,12 @@ structure DerivingClassView where
   className : Name
   args? : Option (TSyntax ``Parser.Term.structInst)
 
-def getOptDerivingClasses [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadInfoTree m] (optDeriving : Syntax) : m (Array DerivingClassView) := do
+def getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassView) := do
   match optDeriving with
   | `(Parser.Command.optDeriving| deriving $[$classes $[with $argss?]?],*) =>
     let mut ret := #[]
     for cls in classes, args? in argss? do
-      let className ← resolveGlobalConstNoOverloadWithInfo cls
+      let className ← realizeGlobalConstNoOverloadWithInfo cls
       ret := ret.push { ref := cls, className := className, args? }
     return ret
   | _ => return #[]
diff --git a/src/Lean/Elab/GenInjective.lean b/src/Lean/Elab/GenInjective.lean
index 5df6250eb7..1cd98882f9 100644
--- a/src/Lean/Elab/GenInjective.lean
+++ b/src/Lean/Elab/GenInjective.lean
@@ -10,8 +10,8 @@ import Lean.Meta.Injective
 namespace Lean.Elab.Command
 
 @[builtin_command_elab genInjectiveTheorems] def elabGenInjectiveTheorems : CommandElab := fun stx => do
-  let declName ← resolveGlobalConstNoOverloadWithInfo stx[1]
   liftTermElabM do
+    let declName ← realizeGlobalConstNoOverloadWithInfo stx[1]
     Meta.mkInjectiveTheorems declName
 
 end Lean.Elab.Command
diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index 6e85ddf873..fd95d794ba 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Meta.PPGoal
+import Lean.ReservedNameAction
 
 namespace Lean.Elab.CommandContextInfo
 
@@ -281,31 +282,28 @@ def addConstInfo [MonadEnv m] [MonadError m]
     expectedType?
   }
 
-/-- This does the same job as `resolveGlobalConstNoOverload`; resolving an identifier
+/-- This does the same job as `realizeGlobalConstNoOverload`; resolving an identifier
 syntax to a unique fully resolved name or throwing if there are ambiguities.
 But also adds this resolved name to the infotree. This means that when you hover
 over a name in the sourcefile you will see the fully resolved name in the hover info.-/
-def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m]
-    (id : Syntax) (expectedType? : Option Expr := none) : m Name := do
-  let n ← resolveGlobalConstNoOverload id
+def realizeGlobalConstNoOverloadWithInfo (id : Syntax) (expectedType? : Option Expr := none) : CoreM Name := do
+  let n ← realizeGlobalConstNoOverload id
   if (← getInfoState).enabled then
     -- we do not store a specific elaborator since identifiers are special-cased by the server anyway
     addConstInfo id n expectedType?
   return n
 
-/-- Similar to `resolveGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list. -/
-def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
-    (id : Syntax) (expectedType? : Option Expr := none) : m (List Name) := do
-  let ns ← resolveGlobalConst id
+/-- Similar to `realizeGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list. -/
+def realizeGlobalConstWithInfos (id : Syntax) (expectedType? : Option Expr := none) : CoreM (List Name) := do
+  let ns ← realizeGlobalConst id
   if (← getInfoState).enabled then
     for n in ns do
       addConstInfo id n expectedType?
   return ns
 
-/-- Similar to `resolveGlobalName`, but it also adds the resolved name to the info tree. -/
-def resolveGlobalNameWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
-    (ref : Syntax) (id : Name) : m (List (Name × List String)) := do
-  let ns ← resolveGlobalName id
+/-- Similar to `realizeGlobalName`, but it also adds the resolved name to the info tree. -/
+def realizeGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name × List String)) := do
+  let ns ← realizeGlobalName id
   if (← getInfoState).enabled then
     for (n, _) in ns do
       addConstInfo ref n
diff --git a/src/Lean/Elab/InheritDoc.lean b/src/Lean/Elab/InheritDoc.lean
index 8b0c1cd100..0897ffc7ca 100644
--- a/src/Lean/Elab/InheritDoc.lean
+++ b/src/Lean/Elab/InheritDoc.lean
@@ -20,7 +20,7 @@ builtin_initialize
       | `(attr| inherit_doc $[$id?:ident]?) => withRef stx[0] do
         let some id := id?
           | throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
-        let declName ← Elab.resolveGlobalConstNoOverloadWithInfo id
+        let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
         if (← findDocString? (← getEnv) decl).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
         let some doc ← findDocString? (← getEnv) declName
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 564d0de960..ed8c16c386 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -833,7 +833,7 @@ where
     for header in headers, view in views do
       if let some classNamesStx := view.deriving? then
         for classNameStx in classNamesStx do
-          let className ← resolveGlobalConstNoOverload classNameStx
+          let className ← realizeGlobalConstNoOverload classNameStx
           withRef classNameStx do
             unless (← processDefDeriving className header.declName) do
               throwError "failed to synthesize instance '{className}' for '{header.declName}'"
diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index e0cc1c4f05..30d5ab5c7a 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -317,14 +317,6 @@ def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withCo
 def tryContradiction (mvarId : MVarId) : MetaM Bool := do
   mvarId.contradictionCore { genDiseq := true }
 
-structure UnfoldEqnExtState where
-  map : PHashMap Name Name := {}
-  deriving Inhabited
-
-/- We generate the unfold equation on demand, and do not save them on .olean files. -/
-builtin_initialize unfoldEqnExt : EnvExtension UnfoldEqnExtState ←
-  registerEnvExtension (pure {})
-
 /--
   Auxiliary method for `mkUnfoldEq`. The structure is based on `mkEqnTypes`.
   `mvarId` is the goal to be proved. It is a goal of the form
@@ -370,9 +362,8 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
 
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {} {} do
-  let env ← getEnv
   withOptions (tactic.hygienic.set · false) do
-    let baseName := mkPrivateName env declName
+    let baseName := declName
     lambdaTelescope info.value fun xs body => do
       let us := info.levelParams.map mkLevelParam
       let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -388,13 +379,8 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
       return name
 
 def getUnfoldFor? (declName : Name) (getInfo? : Unit → Option EqnInfoCore) : MetaM (Option Name) := do
-  let env ← getEnv
-  if let some eq := unfoldEqnExt.getState env |>.map.find? declName then
-    return some eq
-  else if let some info := getInfo? () then
-    let eq ← mkUnfoldEq declName info
-    modifyEnv fun env => unfoldEqnExt.modifyState env fun s => { s with map := s.map.insert declName eq }
-    return some eq
+  if let some info := getInfo? () then
+    return some (← mkUnfoldEq declName info)
   else
     return none
 
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 037b0ca600..200fa29f5c 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -105,6 +105,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       See issue #2321
       -/
       let preDef ← eraseRecAppSyntax preDefs[0]!
+      ensureEqnReservedNamesAvailable preDef.declName
       if preDef.modifiers.isNoncomputable then
         addNonRec preDef
       else
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index 5ee888c748..1fb4f3b514 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -63,7 +63,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
     mkEqnTypes #[info.declName] goal.mvarId!
-  let baseName := mkPrivateName (← getEnv) info.declName
+  let baseName := info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!
@@ -81,6 +81,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDef : PreDefinition) (recArgPos : Nat) : CoreM Unit := do
+  ensureEqnReservedNamesAvailable preDef.declName
   modifyEnv fun env => eqnInfoExt.insert env preDef.declName { preDef with recArgPos }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index 85997209d8..09923db147 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -109,7 +109,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
 
 def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set · false) do
-  let baseName := mkPrivateName (← getEnv) declName
+  let baseName := declName
   let eqnTypes ← withNewMCtxDepth <| lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -133,6 +133,7 @@ builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclara
 
 def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat)
     (argsPacker : ArgsPacker) : MetaM Unit := do
+  preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   /-
   See issue #2327.
   Remark: we could do better for mutual declarations that mix theorems and definitions. However, this is a rare
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index 77d77a0842..010ce76034 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -80,7 +80,7 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
 
 private def printId (id : Syntax) : CommandElabM Unit := do
   addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
-  let cs ← resolveGlobalConstWithInfos id
+  let cs ← liftCoreM <| realizeGlobalConstWithInfos id
   cs.forM printIdCore
 
 @[builtin_command_elab «print»] def elabPrint : CommandElab
@@ -125,7 +125,7 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
 
 @[builtin_command_elab «printAxioms»] def elabPrintAxioms : CommandElab
   | `(#print%$tk axioms $id) => withRef tk do
-    let cs ← resolveGlobalConstWithInfos id
+    let cs ← liftCoreM <| realizeGlobalConstWithInfos id
     cs.forM printAxiomsOf
   | _ => throwUnsupportedSyntax
 
@@ -140,7 +140,7 @@ private def printEqnsOf (constName : Name) : CommandElabM Unit := do
 
 @[builtin_command_elab «printEqns»] def elabPrintEqns : CommandElab := fun stx => do
   let id := stx[2]
-  let cs ← resolveGlobalConstWithInfos id
+  let cs ← liftCoreM <| realizeGlobalConstWithInfos id
   cs.forM printEqnsOf
 
 end Lean.Elab.Command
diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean
index 05dc94f734..71b51107c9 100644
--- a/src/Lean/Elab/Quotation/Precheck.lean
+++ b/src/Lean/Elab/Quotation/Precheck.lean
@@ -92,7 +92,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
        notation "x++" => x.foo
        ```
     -/
-    if let _::_ ← resolveGlobalNameWithInfos stx val then
+    if let _::_ ← realizeGlobalNameWithInfos stx val then
       return
     if (← read).quotLCtx.contains val then
       return
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 137178c4c1..8bbba0a17b 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -892,7 +892,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
   let exts      := stx[3]
   let parents   := if exts.isNone then #[] else exts[0][1].getSepArgs
   let optType   := stx[4]
-  let derivingClassViews ← getOptDerivingClasses stx[6]
+  let derivingClassViews ← liftCoreM <| getOptDerivingClasses stx[6]
   let type ← if optType.isNone then `(Sort _) else pure optType[0][1]
   let declName ←
     runTermElabM fun scopeVars => do
diff --git a/src/Lean/Elab/Tactic/Conv/Delta.lean b/src/Lean/Elab/Tactic/Conv/Delta.lean
index f14c6e945c..c26b461868 100644
--- a/src/Lean/Elab/Tactic/Conv/Delta.lean
+++ b/src/Lean/Elab/Tactic/Conv/Delta.lean
@@ -11,7 +11,7 @@ namespace Lean.Elab.Tactic.Conv
 open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.delta] def evalDelta : Tactic := fun stx => withMainContext do
-  let declNames ← stx[1].getArgs.mapM resolveGlobalConstNoOverloadWithInfo
+  let declNames ← stx[1].getArgs.mapM fun stx => realizeGlobalConstNoOverloadWithInfo stx
   let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) declNames.contains
   changeLhs lhsNew
 
diff --git a/src/Lean/Elab/Tactic/Conv/Unfold.lean b/src/Lean/Elab/Tactic/Conv/Unfold.lean
index 96d26e8d9e..01ee6fdfbc 100644
--- a/src/Lean/Elab/Tactic/Conv/Unfold.lean
+++ b/src/Lean/Elab/Tactic/Conv/Unfold.lean
@@ -12,7 +12,7 @@ open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do
   for declNameId in stx[1].getArgs do
-    let declName ← resolveGlobalConstNoOverloadWithInfo declNameId
+    let declName ← realizeGlobalConstNoOverloadWithInfo declNameId
     applySimpResult (← unfold (← getLhs) declName)
 
 end Lean.Elab.Tactic.Conv
diff --git a/src/Lean/Elab/Tactic/Delta.lean b/src/Lean/Elab/Tactic/Delta.lean
index 854ee9d195..a185725df1 100644
--- a/src/Lean/Elab/Tactic/Delta.lean
+++ b/src/Lean/Elab/Tactic/Delta.lean
@@ -29,7 +29,7 @@ def deltaTarget (declNames : Array Name) : TacticM Unit := do
 
 /-- "delta " ident+ (location)? -/
 @[builtin_tactic Lean.Parser.Tactic.delta] def evalDelta : Tactic := fun stx => do
-  let declNames ← stx[1].getArgs.mapM resolveGlobalConstNoOverloadWithInfo
+  let declNames ← stx[1].getArgs.mapM fun stx => realizeGlobalConstNoOverloadWithInfo stx
   let loc := expandOptLocation stx[2]
   withLocation loc (deltaLocalDecl declNames) (deltaTarget declNames)
     (throwTacticEx `delta · m!"did not delta reduce {declNames}")
diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean
index 1aefa29a69..2545846a8c 100644
--- a/src/Lean/Elab/Tactic/Ext.lean
+++ b/src/Lean/Elab/Tactic/Ext.lean
@@ -153,7 +153,7 @@ elaborating to `x.1 = y.1 → x.2 = y.2 → x = y`, for example.
 @[builtin_term_elab extType] def elabExtType : TermElab := fun stx _ => do
   match stx with
   | `(ext_type%  $flat:term $struct:ident) => do
-    withExtHyps (← resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
+    withExtHyps (← realizeGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
       let ty := hyps.foldr (init := ← mkEq x y) fun (f, h) ty =>
         mkForall f BinderInfo.default h ty
       mkForallFVars (params |>.push x |>.push y) ty
@@ -166,7 +166,7 @@ elaborating to `x = y ↔ x.1 = y.1 ∧ x.2 = y.2`, for example.
 @[builtin_term_elab extIffType] def elabExtIffType : TermElab := fun stx _ => do
   match stx with
   | `(ext_iff_type% $flat:term $struct:ident) => do
-    withExtHyps (← resolveGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
+    withExtHyps (← realizeGlobalConstNoOverloadWithInfo struct) flat fun params x y hyps => do
       mkForallFVars (params |>.push x |>.push y) <|
         mkIff (← mkEq x y) <| mkAndN (hyps.map (·.2)).toList
   | _ => throwUnsupportedSyntax
diff --git a/src/Lean/Elab/Tactic/NormCast.lean b/src/Lean/Elab/Tactic/NormCast.lean
index f6bfcc97d9..d9a630b4b7 100644
--- a/src/Lean/Elab/Tactic/NormCast.lean
+++ b/src/Lean/Elab/Tactic/NormCast.lean
@@ -268,7 +268,7 @@ open Command in
   match stx with
   | `(norm_cast_add_elim $id:ident) =>
     Elab.Command.liftCoreM do MetaM.run' do
-     addElim (← resolveGlobalConstNoOverload id)
+     addElim (← realizeGlobalConstNoOverload id)
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.NormCast
diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index 0e2397b7fe..b2e76ba6aa 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -51,11 +51,13 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool)
             x symm term
           else
             -- Try to get equation theorems for `id`.
-            let declName ← try resolveGlobalConstNoOverload id catch _ => return (← x symm term)
+            let declName ← try realizeGlobalConstNoOverload id catch _ => return (← x symm term)
             let some eqThms ← getEqnsFor? declName (nonRec := true) | x symm term
             let rec go : List Name →  TacticM Unit
               | [] => throwError "failed to rewrite using equation theorems for '{declName}'"
-              | eqThm::eqThms => (x symm (mkIdentFrom id eqThm)) <|> go eqThms
+              -- Remark: we prefix `eqThm` with `_root_` to ensure it is resolved correctly.
+              -- See test: `rwPrioritizesLCtxOverEnv.lean`
+              | eqThm::eqThms => (x symm (mkIdentFrom id (`_root_ ++ eqThm))) <|> go eqThms
             go eqThms.toList
             discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx)
         match term with
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index d34f2f9f1e..c51b1cf43b 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -179,7 +179,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
             let id := arg[1]
-            let declNames? ← try pure (some (← resolveGlobalConst id)) catch _ => pure none
+            let declNames? ← try pure (some (← realizeGlobalConst id)) catch _ => pure none
             if let some declNames := declNames? then
               let declName ← ensureNonAmbiguous id declNames
               if (← Simp.isSimproc declName) then
diff --git a/src/Lean/Elab/Tactic/Simproc.lean b/src/Lean/Elab/Tactic/Simproc.lean
index 1a13305f25..1104ae6abd 100644
--- a/src/Lean/Elab/Tactic/Simproc.lean
+++ b/src/Lean/Elab/Tactic/Simproc.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Simproc
+import Lean.ReservedNameAction
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
@@ -37,16 +38,16 @@ namespace Command
 
 @[builtin_command_elab Lean.Parser.simprocPattern] def elabSimprocPattern : CommandElab := fun stx => do
   let `(simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
-  let declName ← resolveGlobalConstNoOverload declName
   liftTermElabM do
+    let declName ← realizeGlobalConstNoOverload declName
     discard <| checkSimprocType declName
     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
+    let declName ← realizeGlobalConstNoOverload declName
     let dsimp ← checkSimprocType declName
     let keys ← elabSimprocKeys pattern
     let registerProcName := if dsimp then ``registerBuiltinDSimproc else ``registerBuiltinSimproc
diff --git a/src/Lean/Elab/Tactic/Unfold.lean b/src/Lean/Elab/Tactic/Unfold.lean
index d0c3284e33..7ad2b05203 100644
--- a/src/Lean/Elab/Tactic/Unfold.lean
+++ b/src/Lean/Elab/Tactic/Unfold.lean
@@ -24,7 +24,7 @@ def unfoldTarget (declName : Name) : TacticM Unit := do
     go declNameId loc
 where
   go (declNameId : Syntax) (loc : Location) : TacticM Unit := do
-    let declName ← resolveGlobalConstNoOverloadWithInfo declNameId
+    let declName ← realizeGlobalConstNoOverloadWithInfo declNameId
     withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
 
 end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index c1abb89cb5..f255160ac5 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
+import Lean.ReservedNameAction
 import Lean.Meta.AppBuilder
 import Lean.Meta.CollectMVars
 import Lean.Meta.Coe
@@ -1653,7 +1654,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
   if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
     return [(e, projs)]  -- section variables should shadow global decls
   if preresolved.isEmpty then
-    process (← resolveGlobalName n)
+    process (← realizeGlobalName n)
   else
     process preresolved
 where
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 7d4062ad62..f8b736c03d 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -209,8 +209,13 @@ def getModuleIdxFor? (env : Environment) (declName : Name) : Option ModuleIdx :=
 
 def isConstructor (env : Environment) (declName : Name) : Bool :=
   match env.find? declName with
-  | ConstantInfo.ctorInfo _ => true
-  | _                       => false
+  | some (.ctorInfo _) => true
+  | _                  => false
+
+def isSafeDefinition (env : Environment) (declName : Name) : Bool :=
+  match env.find? declName with
+  | some (.defnInfo { safety := .safe, .. }) => true
+  | _ => false
 
 def getModuleIdx? (env : Environment) (moduleName : Name) : Option ModuleIdx :=
   env.header.moduleNames.findIdx? (· == moduleName)
diff --git a/src/Lean/Linter/Deprecated.lean b/src/Lean/Linter/Deprecated.lean
index 8b5463945c..206c3853da 100644
--- a/src/Lean/Linter/Deprecated.lean
+++ b/src/Lean/Linter/Deprecated.lean
@@ -23,7 +23,7 @@ builtin_initialize deprecatedAttr : ParametricAttribute (Option Name) ←
      match stx with
      | `(attr| deprecated $[$id?]?) =>
        let some id := id? | return none
-       let declNameNew ← Elab.resolveGlobalConstNoOverloadWithInfo id
+       let declNameNew ← Elab.realizeGlobalConstNoOverloadWithInfo id
        return some declNameNew
      | _  => throwError "invalid `[deprecated]` attribute"
   }
diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean
index 81930a1a7c..30bda95f9f 100644
--- a/src/Lean/Linter/MissingDocs.lean
+++ b/src/Lean/Linter/MissingDocs.lean
@@ -87,7 +87,7 @@ builtin_initialize
         throwError "invalid attribute '{name}', declaration is in an imported module"
       let decl ← getConstInfo declName
       let fnNameStx ← Attribute.Builtin.getIdent stx
-      let key ← Elab.resolveGlobalConstNoOverloadWithInfo fnNameStx
+      let key ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx
       unless decl.levelParams.isEmpty && (decl.type == .const ``Handler [] || decl.type == .const ``SimpleHandler []) do
         throwError "unexpected missing docs handler at '{declName}', `MissingDocs.Handler` or `MissingDocs.SimpleHandler` expected"
       if builtin then
diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index 46d43ea713..5ac5d16e09 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -4,46 +4,71 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.ReservedNameAction
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 
 namespace Lean.Meta
+/-- Returns `true` if `s` is of the form `eq_<idx>` -/
+def isEqnReservedNameSuffix (s : String) : Bool :=
+  "eq_".isPrefixOf s && (s.drop 3).isNat
+
+/-- Returns `true` if `s == "def"` -/
+def isUnfoldReservedNameSuffix (s : String) : Bool :=
+  s == "def"
+
+/--
+Throw an error if names for equation theorems for `declName` are not available.
+-/
+def ensureEqnReservedNamesAvailable (declName : Name) : CoreM Unit := do
+  ensureReservedNameAvailable declName "def"
+  ensureReservedNameAvailable declName "eq_1"
+  -- TODO: `declName` may need to reserve multiple `eq_<idx>` names, but we check only the first one.
+  -- Possible improvement: try to efficiently compute the number of equation theorems at declaration time, and check all of them.
+
+/--
+Ensures that `f.def` and `f.eq_<idx>` are reserved names if `f` is a safe definition.
+-/
+builtin_initialize registerReservedNamePredicate fun env n =>
+  match n with
+  | .str p s => (isEqnReservedNameSuffix s || isUnfoldReservedNameSuffix s) && env.isSafeDefinition p
+  | _ => false
 
 def GetEqnsFn := Name → MetaM (Option (Array Name))
 
 private builtin_initialize getEqnsFnsRef : IO.Ref (List GetEqnsFn) ← IO.mkRef []
 
 /--
-  Register a new function for retrieving equation theorems.
-  We generate equations theorems on demand, and they are generated by more than one module.
-  For example, the structural and well-founded recursion modules generate them.
-  Most recent getters are tried first.
+Registers a new function for retrieving equation theorems.
+We generate equations theorems on demand, and they are generated by more than one module.
+For example, the structural and well-founded recursion modules generate them.
+Most recent getters are tried first.
 
-  A getter returns an `Option (Array Name)`. The result is `none` if the getter failed.
-  Otherwise, it is a sequence of theorem names where each one of them corresponds to
-  an alternative. Example: the definition
+A getter returns an `Option (Array Name)`. The result is `none` if the getter failed.
+Otherwise, it is a sequence of theorem names where each one of them corresponds to
+an alternative. Example: the definition
 
-  ```
-  def f (xs : List Nat) : List Nat :=
-    match xs with
-    | [] => []
-    | x::xs => (x+1)::f xs
-  ```
-  should have two equational theorems associated with it
-  ```
-  f [] = []
-  ```
-  and
-  ```
-  (x : Nat) → (xs : List Nat) → f (x :: xs) = (x+1) :: f xs
-  ```
+```
+def f (xs : List Nat) : List Nat :=
+  match xs with
+  | [] => []
+  | x::xs => (x+1)::f xs
+```
+should have two equational theorems associated with it
+```
+f [] = []
+```
+and
+```
+(x : Nat) → (xs : List Nat) → f (x :: xs) = (x+1) :: f xs
+```
 -/
 def registerGetEqnsFn (f : GetEqnsFn) : IO Unit := do
   unless (← initializing) do
     throw (IO.userError "failed to register equation getter, this kind of extension can only be registered during initialization")
   getEqnsFnsRef.modify (f :: ·)
 
-/-- Return true iff `declName` is a definition and its type is not a proposition. -/
+/-- Returns `true` iff `declName` is a definition and its type is not a proposition. -/
 private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
     return !(← isProp info.type)
@@ -52,23 +77,23 @@ private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
 
 structure EqnsExtState where
   map    : PHashMap Name (Array Name) := {}
-  mapInv : PHashMap Name Name := {}
+  mapInv : PHashMap Name Name := {} -- TODO: delete?
   deriving Inhabited
 
-/- We generate the equations on demand, and do not save them on .olean files. -/
+/- We generate the equations on demand. -/
 builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
   registerEnvExtension (pure {})
 
 /--
-  Simple equation theorem for nonrecursive definitions.
+Simple equation theorem for nonrecursive definitions.
 -/
-private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
+private def mkSimpleEqThm (declName : Name) (suffix := `def) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
     lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
       let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
       let type  ← mkForallFVars xs (← mkEq lhs body)
       let value ← mkLambdaFVars xs (← mkEqRefl lhs)
-      let name := mkPrivateName (← getEnv) declName ++ `_eq_1
+      let name := declName ++ suffix
       addDecl <| Declaration.thmDecl {
         name, type, value
         levelParams := info.levelParams
@@ -93,20 +118,41 @@ private def registerEqnThms (declName : Name) (eqThms : Array Name) : CoreM Unit
   }
 
 /--
-  Returns equation theorems for the given declaration.
-  By default, we do not create equation theorems for nonrecursive definitions.
-  You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
+Equation theorems are generated on demand, check whether they were generated in an imported file.
+-/
+private partial def alreadyGenerated? (declName : Name) : MetaM (Option (Array Name)) := do
+  let env ← getEnv
+  let eq1 := declName ++ `eq_1
+  if env.contains eq1 then
+    let rec loop (idx : Nat) (eqs : Array Name) : MetaM (Array Name) := do
+      let nextEq := declName ++ (`eq).appendIndexAfter idx
+      if env.contains nextEq then
+        loop (idx+1) (eqs.push nextEq)
+      else
+        return eqs
+    let eqs ← loop 2 #[eq1]
+    registerEqnThms declName eqs
+    return some eqs
+  else
+    return none
+
+/--
+Returns equation theorems for the given declaration.
+By default, we do not create equation theorems for nonrecursive definitions.
+You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
 -/
 def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)) := withLCtx {} {} do
   if let some eqs := eqnsExt.getState (← getEnv) |>.map.find? declName then
     return some eqs
+  else if let some eqs ← alreadyGenerated? declName then
+    return some eqs
   else if (← shouldGenerateEqnThms declName) then
     for f in (← getEqnsFnsRef.get) do
       if let some r ← f declName then
         registerEqnThms declName r
         return some r
     if nonRec then
-      let some eqThm ← mkSimpleEqThm declName | return none
+      let some eqThm ← mkSimpleEqThm declName (suffix := `eq_1) | return none
       let r := #[eqThm]
       registerEqnThms declName r
       return some r
@@ -117,29 +163,29 @@ def GetUnfoldEqnFn := Name → MetaM (Option Name)
 private builtin_initialize getUnfoldEqnFnsRef : IO.Ref (List GetUnfoldEqnFn) ← IO.mkRef []
 
 /--
-  Register a new function for retrieving a "unfold" equation theorem.
+Registers a new function for retrieving a "unfold" equation theorem.
 
-  We generate this kind of equation theorem on demand, and it is generated by more than one module.
-  For example, the structural and well-founded recursion modules generate it.
-  Most recent getters are tried first.
+We generate this kind of equation theorem on demand, and it is generated by more than one module.
+For example, the structural and well-founded recursion modules generate it.
+Most recent getters are tried first.
 
-  A getter returns an `Option Name`. The result is `none` if the getter failed.
-  Otherwise, it is a theorem name. Example: the definition
+A getter returns an `Option Name`. The result is `none` if the getter failed.
+Otherwise, it is a theorem name. Example: the definition
 
-  ```
-  def f (xs : List Nat) : List Nat :=
+```
+def f (xs : List Nat) : List Nat :=
+  match xs with
+  | [] => []
+  | x::xs => (x+1)::f xs
+```
+should have the theorem
+```
+(xs : Nat) →
+  f xs =
     match xs with
     | [] => []
     | x::xs => (x+1)::f xs
-  ```
-  should have the theorem
-  ```
-  (xs : Nat) →
-    f xs =
-      match xs with
-      | [] => []
-      | x::xs => (x+1)::f xs
-  ```
+```
 -/
 def registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit := do
   unless (← initializing) do
@@ -147,18 +193,33 @@ def registerGetUnfoldEqnFn (f : GetUnfoldEqnFn) : IO Unit := do
   getUnfoldEqnFnsRef.modify (f :: ·)
 
 /--
-  Return an "unfold" theorem for the given declaration.
-  By default, we do not create unfold theorems for nonrecursive definitions.
-  You can use `nonRec := true` to override this behavior.
+Returns an "unfold" theorem for the given declaration.
+By default, we do not create unfold theorems for nonrecursive definitions.
+You can use `nonRec := true` to override this behavior.
 -/
 def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := withLCtx {} {} do
+  let env ← getEnv
+  let unfoldName := declName ++ `def
+  if env.contains unfoldName then
+    return some unfoldName
   if (← shouldGenerateEqnThms declName) then
     for f in (← getUnfoldEqnFnsRef.get) do
       if let some r ← f declName then
+        unless r == unfoldName do
+          throwError "invalid unfold theorem name `{r}` has been generated expected `{unfoldName}`"
         return some r
     if nonRec then
-      let some #[eqThm] ← getEqnsFor? declName (nonRec := true) | return none
-      return some eqThm
+      return (← mkSimpleEqThm declName)
    return none
 
+builtin_initialize
+  registerReservedNameAction fun name => do
+    let .str p s := name | return false
+    unless (← getEnv).isSafeDefinition p do return false
+    if isEqnReservedNameSuffix s then
+      return (← MetaM.run' <| getEqnsFor? p (nonRec := true)).isSome
+    if isUnfoldReservedNameSuffix s then
+      return (← MetaM.run' <| getUnfoldEqnFor? p (nonRec := true)).isSome
+    return false
+
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 71f2eec234..f20ba206d7 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -725,7 +725,7 @@ def deriveInduction (name : Name) : MetaM Unit := do
 @[builtin_command_elab Parser.Command.deriveInduction]
 def elabDeriveInduction : Command.CommandElab := fun stx => Command.runTermElabM fun _xs => do
   let ident := stx[1]
-  let name ← resolveGlobalConstNoOverloadWithInfo ident
+  let name ← realizeGlobalConstNoOverloadWithInfo ident
   deriveInduction name
 
 end Lean.Tactic.FunInd
diff --git a/src/Lean/ParserCompiler/Attribute.lean b/src/Lean/ParserCompiler/Attribute.lean
index 3ebd7eba6e..a8bc59e060 100644
--- a/src/Lean/ParserCompiler/Attribute.lean
+++ b/src/Lean/ParserCompiler/Attribute.lean
@@ -30,7 +30,7 @@ def registerCombinatorAttribute (name : Name) (descr : String) (ref : Name := by
     descr := descr,
     add   := fun decl stx _ => do
       let env ← getEnv
-      let parserDeclName ← Elab.resolveGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
+      let parserDeclName ← Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
       setEnv <| ext.addEntry env (parserDeclName, decl)
   }
   registerBuiltinAttribute attrImpl
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 1a7f1a49e4..1899fcd68a 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -373,7 +373,7 @@ passed the result of pre-pretty printing the application *without* implicitly pa
 to true or `pp.notation` is set to false, it will not be called at all.",
     valueTypeName := `Lean.PrettyPrinter.Unexpander
     evalKey := fun _ stx => do
-      Elab.resolveGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
+      Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
   } `Lean.PrettyPrinter.Delaborator.appUnexpanderAttribute
 @[builtin_init mkAppUnexpanderAttribute] opaque appUnexpanderAttribute : KeyedDeclsAttribute Unexpander
 
diff --git a/src/Lean/ReservedNameAction.lean b/src/Lean/ReservedNameAction.lean
new file mode 100644
index 0000000000..6ce8346514
--- /dev/null
+++ b/src/Lean/ReservedNameAction.lean
@@ -0,0 +1,80 @@
+/-
+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.CoreM
+
+namespace Lean
+
+/--
+When trying to resolve a reserved name, an action can be executed to generate the actual definition/theorem.
+The action returns `true` if it "handled" the given name.
+
+Remark: usually when one install a reserved name predicate, an associated action is also installed.
+-/
+def ReservedNameAction := Name → CoreM Bool
+
+private builtin_initialize reservedNameActionsRef : IO.Ref (Array ReservedNameAction) ← IO.mkRef #[]
+
+/--
+Register a new function that is invoked when trying to resolve a reserved name.
+-/
+def registerReservedNameAction (act : ReservedNameAction) : IO Unit := do
+  unless (← initializing) do
+    throw (IO.userError "failed to register reserved name action, this kind of extension can only be registered during initialization")
+  reservedNameActionsRef.modify (·.push act)
+
+/--
+Execute a registered reserved action for the given reserved name.
+Note that the handler can throw an exception.
+-/
+def executeReservedNameAction (name : Name) : CoreM Unit := do
+  for act in (← reservedNameActionsRef.get) do
+    if (← act name) then
+      return ()
+
+/--
+Similar to `resolveGlobalName`, but also executes reserved name actions.
+-/
+def realizeGlobalName (id : Name) : CoreM (List (Name × List String)) := do
+  let cs ← resolveGlobalName id
+  cs.filterM fun (c, _) => do
+    if (← getEnv).contains c then
+      return true
+    else
+      try
+        executeReservedNameAction c
+        return (← getEnv).contains c
+      catch ex =>
+        -- We record the error produced by then reserved name action generator
+        logError ex.toMessageData
+        return false
+
+/--
+Similar to `resolveGlobalConstCore`, but also executes reserved name actions.
+-/
+def realizeGlobalConstCore (n : Name) : CoreM (List Name) := do
+  let cs ← realizeGlobalName n
+  filterFieldList n cs
+
+/--
+Similar to `realizeGlobalConstNoOverloadCore`, but also executes reserved name actions.
+-/
+def realizeGlobalConstNoOverloadCore (n : Name) : CoreM Name := do
+  ensureNoOverload n (← realizeGlobalConstCore n)
+
+/--
+Similar to `resolveGlobalConst`, but also executes reserved name actions.
+-/
+def realizeGlobalConst (stx : Syntax) : CoreM (List Name) :=
+  withRef stx do preprocessSyntaxAndResolve stx realizeGlobalConstCore
+
+/--
+Similar to `realizeGlobalConstNoOverload`, but also executes reserved name actions.
+-/
+def realizeGlobalConstNoOverload (id : Syntax) : CoreM Name := do
+  ensureNonAmbiguous id (← realizeGlobalConst id)
+
+end Lean
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index cd4fae2018..42ca57b8b5 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -10,6 +10,43 @@ import Lean.Modifiers
 import Lean.Exception
 
 namespace Lean
+/-!
+Reserved names.
+
+We use reserved names for automatically generated theorems (e.g., equational theorems).
+Automation may register new reserved name predicates.
+In this module, we just check the registered predicates, but do not trigger actions associated with them.
+For example, give a definition `foo`, we flag `foo.def` as reserved symbol.
+-/
+
+def throwReservedNameNotAvailable [Monad m] [MonadError m] (declName : Name) (reservedName : Name) : m Unit := do
+  throwError "failed to declare `{declName}` because `{reservedName}` has already been declared"
+
+def ensureReservedNameAvailable [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (suffix : String) : m Unit := do
+  let reservedName := .str declName suffix
+  if (← getEnv).contains reservedName then
+    throwReservedNameNotAvailable declName reservedName
+
+/-- Global reference containing all reserved name predicates. -/
+builtin_initialize reservedNamePredicatesRef : IO.Ref (Array (Environment → Name → Bool)) ← IO.mkRef #[]
+
+/--
+Registers a new reserved name predicate.
+-/
+def registerReservedNamePredicate (p : Environment → Name → Bool) : IO Unit := do
+  unless (← initializing) do
+    throw (IO.userError "failed to register reserved name suffix predicate, this operation can only be performed during initialization")
+  reservedNamePredicatesRef.modify fun ps => ps.push p
+
+builtin_initialize reservedNamePredicatesExt : EnvExtension (Array (Environment → Name → Bool)) ←
+  registerEnvExtension reservedNamePredicatesRef.get
+
+/--
+Returns `true` if `name` is a reserved name.
+-/
+def isReservedName (env : Environment) (name : Name) : Bool :=
+  reservedNamePredicatesExt.getState env |>.any (· env name)
+
 /-!
   We use aliases to implement the `export <id> (<id>+)` command.
   An `export A (x)` in the namespace `B` produces an alias `B.x ~> A.x`.
@@ -113,6 +150,13 @@ private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl →
         resolvedIds
     resolveOpenDecls env id openDecls resolvedIds
 
+/--
+Primitive global name resolution procedure. It does not trigger actions associated with reserved names.
+Recall that Lean has reserved names. For example, a definition `foo` has a reserved name `foo.def` for theorem
+containing stating that `foo` is equal to its definition. The action associated with `foo.def`
+automatically proves the theorem. At the macro level, the name is resolved, but the action is not
+executed.
+-/
 def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List (Name × List String) :=
   -- decode macro scopes from name before recursion
   let extractionResult := extractMacroScopes id
@@ -127,9 +171,9 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
         match resolveExact env id with
         | some newId => [(newId, projs)]
         | none =>
-          let resolvedIds := if env.contains id then [id] else []
+          let resolvedIds := if env.contains id || isReservedName env id then [id] else []
           let idPrv       := mkPrivateName env id
-          let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds
+          let resolvedIds := if env.contains idPrv || isReservedName env idPrv then [idPrv] ++ resolvedIds else resolvedIds
           let resolvedIds := resolveOpenDecls env id openDecls resolvedIds
           let resolvedIds := getAliases env id (skipProtected := id.isAtomic) ++ resolvedIds
           match resolvedIds with
@@ -183,27 +227,27 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where
   getOpenDecls     := liftM (m:=m) getOpenDecls
 
 /--
-  Given a name `n`, return a list of possible interpretations.
-  Each interpretation is a pair `(declName, fieldList)`, where `declName`
-  is the name of a declaration in the current environment, and `fieldList` are
-  (potential) field names.
-  The pair is needed because in Lean `.` may be part of a qualified name or
-  a field (aka dot-notation).
-  As an example, consider the following definitions
-  ```
-  def Boo.x   := 1
-  def Foo.x   := 2
-  def Foo.x.y := 3
-  ```
-  After `open Foo`, we have
-  - `resolveGlobalName x`     => `[(Foo.x, [])]`
-  - `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
-  - `resolveGlobalName x.z.w` => `[(Foo.x, [z, w])]`
+Given a name `n`, return a list of possible interpretations.
+Each interpretation is a pair `(declName, fieldList)`, where `declName`
+is the name of a declaration in the current environment, and `fieldList` are
+(potential) field names.
+The pair is needed because in Lean `.` may be part of a qualified name or
+a field (aka dot-notation).
+As an example, consider the following definitions
+```
+def Boo.x   := 1
+def Foo.x   := 2
+def Foo.x.y := 3
+```
+After `open Foo`, we have
+- `resolveGlobalName x`     => `[(Foo.x, [])]`
+- `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
+- `resolveGlobalName x.z.w` => `[(Foo.x, [z, w])]`
 
-  After `open Foo open Boo`, we have
-  - `resolveGlobalName x`     => `[(Foo.x, []), (Boo.x, [])]`
-  - `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
-  - `resolveGlobalName x.z.w` => `[(Foo.x, [z, w]), (Boo.x, [z, w])]`
+After `open Foo open Boo`, we have
+- `resolveGlobalName x`     => `[(Foo.x, []), (Boo.x, [])]`
+- `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
+- `resolveGlobalName x.z.w` => `[(Foo.x, [z, w]), (Boo.x, [z, w])]`
 -/
 def resolveGlobalName [Monad m] [MonadResolveName m] [MonadEnv m] (id : Name) : m (List (Name × List String)) := do
   return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
@@ -236,24 +280,44 @@ def resolveUniqueNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadErr
   | [ns] => return ns
   | nss => throwError s!"ambiguous namespace '{id.getId}', possible interpretations: '{nss}'"
 
-/-- Given a name `n`, return a list of possible interpretations for global constants.
-
-Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty.
-For identifiers taken from syntax, use `resolveGlobalConst` instead, which respects preresolved names. -/
-def resolveGlobalConstCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m (List Name) := do
-  let cs ← resolveGlobalName n
+/-- Helper function for `resolveGlobalConstCore`. -/
+def filterFieldList [Monad m] [MonadError m] (n : Name) (cs : List (Name × List String)) : m (List Name) := do
   let cs := cs.filter fun (_, fieldList) => fieldList.isEmpty
   if cs.isEmpty then throwUnknownConstant n
   return cs.map (·.1)
 
-/-- For identifiers taken from syntax, use `resolveGlobalConstNoOverload` instead, which respects preresolved names. -/
-def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m Name := do
-  let cs ← resolveGlobalConstCore n
+/-- Given a name `n`, return a list of possible interpretations for global constants.
+
+Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty.
+For identifiers taken from syntax, use `resolveGlobalConst` instead, which respects preresolved names. -/
+private def resolveGlobalConstCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m (List Name) := do
+  let cs ← resolveGlobalName n
+  filterFieldList n cs
+
+/-- Helper function for `resolveGlobalConstNoOverloadCore` -/
+def ensureNoOverload [Monad m] [MonadError m] (n : Name) (cs : List Name) : m Name := do
   match cs with
   | [c] => pure c
   | _   => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}"
 
-/-- Interpret the syntax `n` as an identifier for a global constant, and return a list of resolved
+/-- For identifiers taken from syntax, use `resolveGlobalConstNoOverload` instead, which respects preresolved names. -/
+def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m Name := do
+  ensureNoOverload n (← resolveGlobalConstCore n)
+
+def preprocessSyntaxAndResolve [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
+  match stx with
+  | .ident _ _ n pre => do
+    let pre := pre.filterMap fun
+      | .decl n [] => some n
+      | _          => none
+    if pre.isEmpty then
+      withRef stx <| k n
+    else
+      return pre
+  | _ => throwErrorAt stx s!"expected identifier"
+
+/--
+Interpret the syntax `n` as an identifier for a global constant, and return a list of resolved
 constant names that it could be referring to based on the currently open namespaces.
 This should be used instead of `resolveGlobalConstCore` for identifiers taken from syntax
 because `Syntax` objects may have names that have already been resolved.
@@ -274,16 +338,8 @@ After `open Foo open Boo`, we have
 - `resolveGlobalConst x.y`   => `[Foo.x.y]`
 - `resolveGlobalConst x.z.w` => error: unknown constant
 -/
-def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] : Syntax → m (List Name)
-  | stx@(Syntax.ident _ _ n pre) => do
-    let pre := pre.filterMap fun
-      | .decl n [] => some n
-      | _          => none
-    if pre.isEmpty then
-      withRef stx <| resolveGlobalConstCore n
-    else
-      return pre
-  | stx => throwErrorAt stx s!"expected identifier"
+def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) : m (List Name) :=
+  preprocessSyntaxAndResolve stx resolveGlobalConstCore
 
 /--
 Given a list of names produced by `resolveGlobalConst`, throw an error if the list does not contain
diff --git a/src/Lean/Server/CodeActions/Attr.lean b/src/Lean/Server/CodeActions/Attr.lean
index a751d7f56b..231751893d 100644
--- a/src/Lean/Server/CodeActions/Attr.lean
+++ b/src/Lean/Server/CodeActions/Attr.lean
@@ -121,7 +121,7 @@ builtin_initialize
       unless kind == AttributeKind.global do
         throwError "invalid attribute 'command_code_action', must be global"
       let `(attr| command_code_action $args*) := stx | return
-      let args ← args.mapM resolveGlobalConstNoOverloadWithInfo
+      let args ← args.mapM realizeGlobalConstNoOverloadWithInfo
       if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
       modifyEnv (cmdCodeActionExt.addEntry · (⟨decl, args⟩, ← mkCommandCodeAction decl))
   }
@@ -144,7 +144,7 @@ builtin_initialize
         throwError "invalid attribute 'command_code_action', must be global"
       let `(attr| builtin_command_code_action $args*) := stx |
         throwError "unexpected 'command_code_action' attribute syntax"
-      let args ← args.mapM resolveGlobalConstNoOverloadWithInfo
+      let args ← args.mapM realizeGlobalConstNoOverloadWithInfo
       if (IR.getSorryDep (← getEnv) decl).isSome then return -- ignore in progress definitions
       addBuiltin decl args
   }
diff --git a/tests/lean/run/matchEqs.lean b/tests/lean/run/matchEqs.lean
index ab9f46048a..2e06c51335 100644
--- a/tests/lean/run/matchEqs.lean
+++ b/tests/lean/run/matchEqs.lean
@@ -5,7 +5,7 @@ open Lean.Elab
 open Lean.Elab.Command
 
 @[command_elab test] def elabTest : CommandElab := fun stx => do
-  let id ← resolveGlobalConstNoOverloadWithInfo stx[1]
+  let id ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo stx[1]
   liftTermElabM do
     IO.println (repr (← Lean.Meta.Match.getEquationsFor id))
   return ()
diff --git a/tests/lean/run/matchEqsBug.lean b/tests/lean/run/matchEqsBug.lean
index 44884f6f99..a1cfd39fca 100644
--- a/tests/lean/run/matchEqsBug.lean
+++ b/tests/lean/run/matchEqsBug.lean
@@ -5,7 +5,7 @@ open Lean.Elab
 open Lean.Elab.Command
 
 @[command_elab test] def elabTest : CommandElab := fun stx => do
-  let id ← resolveGlobalConstNoOverloadWithInfo stx[1]
+  let id ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo stx[1]
   liftTermElabM do
     IO.println (repr (← Lean.Meta.Match.getEquationsFor id))
   return ()
diff --git a/tests/lean/run/printEqns.lean b/tests/lean/run/printEqns.lean
index 887c6ad555..baa2801b8d 100644
--- a/tests/lean/run/printEqns.lean
+++ b/tests/lean/run/printEqns.lean
@@ -1,7 +1,7 @@
 /--
 info: equations:
-private theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
-private theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
+theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
+theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
   List.append (a :: l) x = a :: List.append l x
 -/
 #guard_msgs in
@@ -9,8 +9,8 @@ private theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α)
 
 /--
 info: equations:
-private theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
-private theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
+theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
+theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
   List.append (a :: l) x = a :: List.append l x
 -/
 #guard_msgs in
@@ -23,9 +23,9 @@ private theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α)
 
 /--
 info: equations:
-private theorem ack.eq_1 : ∀ (x : Nat), ack 0 x = x + 1
-private theorem ack.eq_2 : ∀ (x_2 : Nat), ack (Nat.succ x_2) 0 = ack x_2 1
-private theorem ack.eq_3 : ∀ (x_2 y : Nat), ack (Nat.succ x_2) (Nat.succ y) = ack x_2 (ack (x_2 + 1) y)
+theorem ack.eq_1 : ∀ (x : Nat), ack 0 x = x + 1
+theorem ack.eq_2 : ∀ (x_2 : Nat), ack (Nat.succ x_2) 0 = ack x_2 1
+theorem ack.eq_3 : ∀ (x_2 y : Nat), ack (Nat.succ x_2) (Nat.succ y) = ack x_2 (ack (x_2 + 1) y)
 -/
 #guard_msgs in
 #print eqns ack
diff --git a/tests/lean/run/reserved.lean b/tests/lean/run/reserved.lean
new file mode 100644
index 0000000000..f190b5baa3
--- /dev/null
+++ b/tests/lean/run/reserved.lean
@@ -0,0 +1,90 @@
+-- `g.def` is not reserved yet
+theorem g.def : 1 + x = x + 1 := Nat.add_comm ..
+
+/--
+error: failed to declare `g` because `g.def` has already been declared
+-/
+#guard_msgs (error) in
+def g (x : Nat) := x + 1
+
+def f (x : Nat) := x + 1
+
+/--
+error: 'f.def' is a reserved name
+-/
+#guard_msgs (error) in
+theorem f.def : f x = x + 1 := rfl
+
+/--
+error: 'f.eq_1' is a reserved name
+-/
+#guard_msgs (error) in
+theorem f.eq_1 : f x = x + 1 := rfl
+
+def f.eq_2_ := 10 -- Should be ok
+
+/-- info: f.eq_1 (x : Nat) : f x = x + 1 -/
+#guard_msgs in
+#check f.eq_1
+
+/-- error: unknown identifier 'f.eq_2' -/
+#guard_msgs (error) in
+#check f.eq_2
+
+/-- info: f.def (x : Nat) : f x = x + 1 -/
+#guard_msgs in
+#check f.def
+
+def fact : Nat → Nat
+  | 0 => 1
+  | n+1 => (n+1) * fact n
+
+/--
+info: fact.def :
+  ∀ (x : Nat),
+    fact x =
+      match x with
+      | 0 => 1
+      | Nat.succ n => (n + 1) * fact n
+-/
+#guard_msgs in
+#check fact.def
+
+/-- info: fact.eq_1 : fact 0 = 1 -/
+#guard_msgs in
+#check fact.eq_1
+
+/-- info: fact.eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n -/
+#guard_msgs in
+#check fact.eq_2
+
+/-- error: unknown identifier 'fact.eq_3' -/
+#guard_msgs (error) in
+#check fact.eq_3
+
+def fact' : Nat → Nat
+  | 0 => 1
+  | n+1 => (n+1) * fact' n
+
+example : fact' 0 + fact' 0 = 2 := by
+  simp [fact'.eq_1]
+
+example : fact' 0 + fact' 1 = 2 := by
+  rw [fact'.eq_1]
+  guard_target =ₛ 1 + fact' 1 = 2
+  rw [fact'.eq_2]
+  guard_target =ₛ 1 + (0+1) * fact' 0 = 2
+  rw [fact'.eq_1]
+
+example : fact' 0 + fact' 1 = 2 := by
+  rw [fact'.def, fact'.def]; simp
+  guard_target =ₛ 1 + fact' 0 = 2
+  rw [fact'.def]
+  guard_target =
+    (1 + fact.match_1 (fun _ => Nat) 0 (fun _ => 1) fun n => (n + 1) * fact' n) = 2
+  simp
+
+theorem bla : 0 = 0 := rfl
+
+def bla.def := 1 -- should work since `bla` is a theorem
+def bla.eq_1 := 2 -- should work since `bla` is a theorem