refactor(Tactic/Translate): document name translation a bit more (#39988)

I found the code a bit hard to read: the following commits each improve the code slightly.
Also add a test exercising the "name matches the auto-generated name" code path.
#39962 will tweak the naming algorithm slightly.

Co-authored-by: damiano <adomani@gmail.com>

Author: grunweg

Mathlib/Tactic/Translate/Core.lean

@@ -310,8 +310,9 @@ structure Config : Type where
   /-- View the trace of the translation procedure.
   Equivalent to `set_option trace.translate true`. -/
   trace : Bool := false
-  /-- The given name of the target. -/
-  tgt : Name := Name.anonymous
+  /-- The given name of the target: an anonymous name means no explicit name was provided,
+  and the translate tactic auto-generates a name instead -/
+  target : Name := Name.anonymous
   /-- An optional doc string. -/
   doc : Option String := .none
   /-- If `allowAutoName` is `false` (default) then
@@ -911,39 +912,42 @@ def translateLemmas
 /-- Return the provided target name or autogenerate one if one was not provided. -/
 def targetName (t : TranslateData) (cfg : Config) (src : Name) : CoreM Name := do
   if cfg.self then
-    if cfg.tgt != .anonymous then
-      logWarning m!"`{t.attrName} self` ignores the provided name {cfg.tgt}"
+    if cfg.target != .anonymous then
+      logWarning m!"`{t.attrName} self` ignores the provided name {cfg.target}"
     return src
   if cfg.none then
-    if cfg.tgt != .anonymous then
-      logWarning m!"`{t.attrName} private` ignores the provided name {cfg.tgt}"
+    if cfg.target != .anonymous then
+      logWarning m!"`{t.attrName} private` ignores the provided name {cfg.target}"
     return ← withDeclNameForAuxNaming src do
       mkAuxDeclName <| .mkSimple ("_" ++ t.attrName.toString)
   -- When re-tagging an existing translation, simply return that existing translation.
   if cfg.existing then
-    if cfg.tgt == .anonymous then
+    if cfg.target == .anonymous then
       if let some tgt := findTranslationName? (← getEnv) t src then
         return tgt
   let .str pre s := src | throwError "{t.attrName}: can't transport {src}"
   trace[translate_detail] "The name {s} splits as {open GuessName in s.splitCase}"
-  let tgt_auto := GuessName.guessName (t.guessNameExt.getState (← getEnv)) s
-  let depth := cfg.tgt.getNumParts
-  let pre := translateNamespace (← getEnv) pre
-  let (pre1, pre2) := pre.splitAt (depth - 1)
-  let res := if cfg.tgt == .anonymous then pre.str tgt_auto else pre1 ++ cfg.tgt
-  if res == src then
+  -- Auto-generated name of the resulting declaration, without prior namespace components.
+  let translatedName := GuessName.guessName (t.guessNameExt.getState (← getEnv)) s
+  let translatedNamespace := translateNamespace (← getEnv) pre
+  let autoGeneratedName := translatedNamespace.str translatedName
+  -- Heuristic: if a new name is manually provided which has fewer components than `src`,
+  -- prepend the first components from `src` to create a translated name of the same depth.
+  let resultingName := if cfg.target == .anonymous then autoGeneratedName else
+    (translatedNamespace.splitAt (cfg.target.getNumParts - 1)).1 ++ cfg.target
+  if resultingName == src then
     throwError "{t.attrName}: the generated translated name equals the original name '{src}'.\n\
     If this is intentional, use the `@[{t.attrName} self]` syntax.\n\
     Otherwise, check that your declaration name is correct \
     (if your declaration is an instance, try naming it)\n\
     or provide a translated name using the `@[{t.attrName} my_add_name]` syntax."
-  if cfg.tgt == pre2.str tgt_auto && !cfg.allowAutoName then
+  if cfg.target != .anonymous && autoGeneratedName == resultingName && !cfg.allowAutoName then
     Linter.logLintIf linter.translateGenerateName cfg.ref m!"\
       `{t.attrName}` correctly autogenerated target name for {src}.\n\
-      You may remove the explicit argument {cfg.tgt}."
-  if cfg.tgt != .anonymous then
-    trace[translate_detail] "The automatically generated name would be {pre.str tgt_auto}"
-  return res
+      You may remove the explicit argument {cfg.target}."
+  if cfg.target != .anonymous then
+    trace[translate_detail] "The automatically generated name would be {autoGeneratedName}"
+  return resultingName
 where
   translateNamespace (env : Environment) (n : Name) : Name :=
     let n' := Name.mapPrefix (findTranslationName? env t) n
@@ -1132,7 +1136,7 @@ def elabTranslationAttr (declName : Name) (stx : Syntax) : CoreM Config := do
       | _ => throwUnsupportedSyntax
     return {
       trace := !stx[1].isNone
-      tgt := match tgt with | some tgt => tgt.getId | _ => Name.anonymous
+      target := match tgt with | some tgt => tgt.getId | _ => Name.anonymous
       doc, attrs, reorder?, relevantArg?, dontTranslate, existing, self, none, rename,
       ref := match tgt with | some tgt => tgt.raw | _ => stx[0] }
   | _ => throwUnsupportedSyntax

Mathlib/Tactic/Translate/TagUnfoldBoundary.lean

@@ -76,7 +76,7 @@ def elabInsertCastAux (declName : Name) (castKind : CastKind) (stx : Term) (t :
   let newName ← mkAuxDeclName ((t.attrName.appendBefore "_").appendAfter "_cast")
   addDecl newName newType newValue
   -- Now add the translation attribute to relate the two new declarations
-  _ ← addTranslationAttr t name { tgt := newName, existing := true, ref := .missing }
+  _ ← addTranslationAttr t name { target := newName, existing := true, ref := .missing }
   return (name, newName)
 where
   unfoldLHS? : CastKind → Expr → OptionT TermElabM Expr

MathlibTest/Attribute/ToAdditive/Basic.lean

@@ -35,6 +35,16 @@ lemma Foo.Bar.baz'' (g h : G) : g * h = h * g := mul_comm g h
 /-- info: Bar.Bars.Stars.Bazzz.b.{u_1} {G : Type u_1} [AddCommGroup G] (g h : G) : g + h = h + g -/
 #guard_msgs in #check Bar.Bars.Stars.Bazzz.b
 
+/--
+warning: `to_additive` correctly autogenerated target name for CommGroup.foo.
+You may remove the explicit argument AddCommGroup.foo.
+
+Note: This linter can be disabled with `set_option linter.translateGenerateName false`
+-/
+#guard_msgs in
+@[to_additive AddCommGroup.foo]
+lemma _root_.CommGroup.foo {g h : G} : g * h = h * g := mul_comm g h
+
 end
 
 @[to_additive bar0]