fix: use private names for theorems that are created on demand

closes #1006

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -164,10 +164,6 @@ structure EqnsExtState where
 builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
   registerEnvExtension (pure {})
 
-/-- Create a "unique" base name for equations and splitter -/
-def mkBaseNameFor (env : Environment) (declName : Name) : Name :=
-  Lean.mkBaseNameFor env declName `_eq_1 `_eqns
-
 /-- Try to close goal using `rfl` with smart unfolding turned off. -/
 def tryURefl (mvarId : MVarId) : MetaM Bool :=
   withOptions (smartUnfolding.set . false) do
@@ -250,7 +246,7 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
 def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {} {} do
   let env ← getEnv
   withOptions (tactic.hygienic.set . false) do
-    let baseName := Lean.mkBaseNameFor env declName `_unfold `_unfold
+    let baseName := mkPrivateName env 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

@@ -55,7 +55,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 := Eqns.mkBaseNameFor (← getEnv) info.declName
+  let baseName := mkPrivateName (← getEnv) info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]

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

@@ -58,7 +58,7 @@ where
 
 def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set . false) do
-  let baseName := Eqns.mkBaseNameFor (← getEnv) declName
+  let baseName := mkPrivateName (← getEnv) declName
   let eqnTypes ← withNewMCtxDepth <| lambdaTelescope info.value fun xs body => do
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body

src/Lean/Environment.lean

@@ -787,23 +787,4 @@ instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
   getEnv    := liftM (getEnv : m Environment)
   modifyEnv := fun f => liftM (modifyEnv f : m Unit)
 
-/--
-  If `env` does not contain a declaration with name `declName ++ elemSuffix`, then return `declName`.
-  Otherwise, find the smallest positive `Nat` `i` such that `declName ++ suffix.appendIndexAfter i ++ elemSuffix` is not
-  the name of a declaration in the given environment.
--/
-partial def mkBaseNameFor (env : Environment) (declName : Name) (elemSuffix : Name) (suffix : Name) : Name :=
-  if !env.contains (declName ++ elemSuffix) then
-    declName
-  else
-    go 1
-where
-  go (idx : Nat) : Name :=
-    let baseName := declName ++ suffix.appendIndexAfter idx
-    if !env.contains (baseName ++ elemSuffix) then
-      baseName
-    else
-      go (idx + 1)
-
-
 end Lean

src/Lean/Meta/Match/MatchEqs.lean

@@ -69,10 +69,6 @@ builtin_initialize matchEqnsExt : EnvExtension MatchEqnsExtState ←
 private def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Unit :=
   modifyEnv fun env => matchEqnsExt.modifyState env fun s => { s with map := s.map.insert matchDeclName matchEqns }
 
-/-- Create a "unique" base name for conditional equations and splitter -/
-private def mkBaseNameFor (env : Environment) (matchDeclName : Name) : Name :=
-  Lean.mkBaseNameFor env matchDeclName `splitter `_matchEqns
-
 def unfoldNamedPattern (e : Expr) : MetaM Expr := do
   let visit (e : Expr) : MetaM TransformStep := do
     if e.isAppOfArity ``namedPattern 4 then
@@ -383,7 +379,7 @@ where
   Create conditional equations and splitter for the given match auxiliary declaration. -/
 private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
   withConfig (fun c => { c with etaStruct := false }) do
-  let baseName := mkBaseNameFor (← getEnv) matchDeclName
+  let baseName := mkPrivateName (← getEnv) matchDeclName
   let constInfo ← getConstInfo matchDeclName
   let us := constInfo.levelParams.map mkLevelParam
   let some matchInfo ← getMatcherInfo? matchDeclName | throwError "'{matchDeclName}' is not a matcher function"

tests/lean/run/matchEqsBug.lean

@@ -29,6 +29,6 @@ test% f.match_1
 def g.match_1.splitter := 4
 
 test% g.match_1
-#check g.match_1._matchEqns_1.eq_1
-#check g.match_1._matchEqns_1.eq_2
-#check g.match_1._matchEqns_1.splitter
+#check g.match_1.eq_1
+#check g.match_1.eq_2
+#check g.match_1.splitter

tests/lean/structuralEqns.lean.expected.out

@@ -1,4 +1,4 @@
-(some foo._unfold)
+(some _private.structuralEqns.0.foo._unfold)
 foo._unfold : ∀ (xs ys zs : List Nat),
   foo xs ys zs =
     match (xs, ys) with