feat: using non-private equational theorem names

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,

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.
 -/
 def resolveGlobalName (n : Name) : MacroM (List (Prod Name (List String))) := do
   (← getMethods).resolveGlobalName n

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 -/
 

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

src/Lean/Elab/BuiltinCommand.lean

@@ -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 <| resolveGlobalConstNoOverloadWithInfo id
     unless ((← getEnv).getModuleIdxFor? declName).isNone do
       throwError "invalid 'add_decl_doc', declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then

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"

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
+         resolveGlobalConst' ident
        catch _ =>
          let name := ident.getId.eraseMacroScopes
          if (← Simp.isBuiltinSimproc name) then

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 resolveGlobalConstNoOverloadWithInfo
      for cls in classes, args? in argss? do
        try
-         let className ← resolveGlobalConstNoOverloadWithInfo cls
+         let className ← liftCoreM <| resolveGlobalConstNoOverloadWithInfo cls
          withRef cls do
            if declNames.size == 1 && args?.isNone then
              if (← tryApplyDefHandler className declNames[0]!) then
@@ -118,7 +118,7 @@ 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 := #[]

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 ← resolveGlobalConstNoOverloadWithInfo stx[1]
     Meta.mkInjectiveTheorems declName
 
 end Lean.Elab.Command

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
 
@@ -283,27 +284,24 @@ def addConstInfo [MonadEnv m] [MonadError m]
 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 resolveGlobalConstNoOverloadWithInfo (id : Syntax) (expectedType? : Option Expr := none) : CoreM Name := do
+  let n ← resolveGlobalConstNoOverload' 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
+def resolveGlobalConstWithInfos (id : Syntax) (expectedType? : Option Expr := none) : CoreM (List Name) := do
+  let ns ← resolveGlobalConst' 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
+def resolveGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name × List String)) := do
+  let ns ← resolveGlobalName' id
   if (← getInfoState).enabled then
     for (n, _) in ns do
       addConstInfo ref n

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 ← resolveGlobalConstNoOverload' classNameStx
           withRef classNameStx do
             unless (← processDefDeriving className header.declName) do
               throwError "failed to synthesize instance '{className}' for '{header.declName}'"

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -370,9 +370,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

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]!

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -107,7 +107,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

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 <| resolveGlobalConstWithInfos 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 <| resolveGlobalConstWithInfos 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 <| resolveGlobalConstWithInfos id
   cs.forM printEqnsOf
 
 end Lean.Elab.Command

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

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 => resolveGlobalConstNoOverloadWithInfo stx
   let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) declNames.contains
   changeLhs lhsNew
 

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 => resolveGlobalConstNoOverloadWithInfo stx
   let loc := expandOptLocation stx[2]
   withLocation loc (deltaLocalDecl declNames) (deltaTarget declNames)
     (throwTacticEx `delta · m!"did not delta reduce {declNames}")

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 (← resolveGlobalConstNoOverload' id)
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.NormCast

src/Lean/Elab/Tactic/Rewrite.lean

@@ -51,7 +51,7 @@ 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 resolveGlobalConstNoOverload' 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}'"

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 (← resolveGlobalConst' id)) catch _ => pure none
             if let some declNames := declNames? then
               let declName ← ensureNonAmbiguous id declNames
               if (← Simp.isSimproc declName) then

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 ← resolveGlobalConstNoOverload' 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 ← resolveGlobalConstNoOverload' declName
     let dsimp ← checkSimprocType declName
     let keys ← elabSimprocKeys pattern
     let registerProcName := if dsimp then ``registerBuiltinDSimproc else ``registerBuiltinSimproc

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)

src/Lean/Meta/Eqns.lean

@@ -4,46 +4,65 @@ 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  `name` is of the form `f.def` and `f.eq_<idx>` where `f` is a safe definition.
+-/
+def isEqnReservedName (env : Environment) (name : Name) : Bool :=
+  match name with
+  | .str p s =>
+    if s == "def" then
+      env.isSafeDefinition p
+    else if "eq_".isPrefixOf s && (s.drop 3).isNat then
+      env.isSafeDefinition p
+    else
+      false
+  | _ => false
+
+/--
+Ensures that `f.def` and `f.eq_<idx>` are reserved names if `f` is a safe definition.
+-/
+builtin_initialize registerReservedNamePredicate isEqnReservedName
 
 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)
@@ -60,15 +79,15 @@ 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,9 +112,9 @@ 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.
+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
@@ -117,29 +136,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
@@ -161,4 +180,11 @@ def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) :
       return some eqThm
    return none
 
+builtin_initialize
+  registerReservedNameAction fun name => do
+    if isEqnReservedName (← getEnv) name then
+      throwError "Eqn action is WIP"
+    else
+      return false
+
 end Lean.Meta

src/Lean/ReservedNameAction.lean

@@ -0,0 +1,79 @@
+/-
+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.
+The result is `true` if a handler for the given reserved name was found.
+Note that the handler can throw an exception.
+-/
+def executeReservedNameAction (name : Name) : CoreM Bool := do
+  for act in (← reservedNameActionsRef.get) do
+    if (← act name) then
+      return true
+  return false
+
+/--
+Similar to `resolveGlobalName`, but also executes reserved name actions.
+-/
+def resolveGlobalName' (id : Name) : CoreM (List (Name × List String)) := do
+  let cs ← resolveGlobalName id
+  for (c, _) in cs do
+    unless (← getEnv).contains c do
+      if (← executeReservedNameAction c) then
+        unless (← getEnv).contains c do
+          throwError "'{id}' is a reserved name, but reserved name code generator failed"
+      else
+        throwError "'{id}' is a reserved name, but none of the installed reserved name code generators is applicable"
+  return cs
+
+/--
+Similar to `resolveGlobalConstCore`, but also executes reserved name actions.
+-/
+def resolveGlobalConstCore' (n : Name) : CoreM (List Name) := do
+  let cs ← resolveGlobalName' n
+  filterFieldList n cs
+
+/--
+Similar to `resolveGlobalConstNoOverloadCore`, but also executes reserved name actions.
+-/
+def resolveGlobalConstNoOverloadCore' (n : Name) : CoreM Name := do
+  ensureNoOverload n (← resolveGlobalConstCore' n)
+
+/--
+Similar to `resolveGlobalConst`, but also executes reserved name actions.
+-/
+def resolveGlobalConst' (stx : Syntax) : CoreM (List Name) :=
+  preprocessSyntaxAndResolve stx resolveGlobalConstCore'
+
+/--
+Similar to `resolveGlobalConstNoOverload`, but also executes reserved name actions.
+-/
+def resolveGlobalConstNoOverload' (id : Syntax) : CoreM Name := do
+  ensureNonAmbiguous id (← resolveGlobalConst' id)
+
+end Lean

src/Lean/ResolveName.lean

@@ -10,6 +10,36 @@ 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 model, we just check the
+registered predicates, but do not trigger actions associated with them. For example,
+give a definition `foo`, we have the reserved name `foo.def` associated with it, and
+an action for creating a theorem that states that `foo` is equal to its definition.
+-/
+
+/-- 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 reserved name 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 +143,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 +164,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 +220,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 +273,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 +331,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

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 <| resolveGlobalConstNoOverloadWithInfo stx[1]
   liftTermElabM do
     IO.println (repr (← Lean.Meta.Match.getEquationsFor id))
   return ()

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 <| resolveGlobalConstNoOverloadWithInfo stx[1]
   liftTermElabM do
     IO.println (repr (← Lean.Meta.Match.getEquationsFor id))
   return ()

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