feat(to_additive): support (attr := reassoc) (#38994)

This PR uses `registerGeneratingAttr`, so that `to_additive (attr := reassoc)` also tags the `_assoc` lemma with `to_additive`.

This interacts awkwarly with `to_dual (attr := reassoc)`, because in that case, the `reassoc` attribute is responsible for handling the `to_dual` attribute. This is solved by adding a check so that we only insert a new translation if it doesn't already exist (e.g. because `reassoc` could have added it).

Author: JovanGerb

Mathlib/CategoryTheory/Monoidal/Mod.lean

@@ -147,9 +147,6 @@ alias IsMod_Hom.smul_hom := IsModHom.smul_hom
 
 attribute [to_additive existing (attr := reassoc (attr := simp))] IsModHom.smul_hom
 
-set_option linter.existingAttributeWarning false in
-attribute [to_additive existing] IsModHom.smul_hom_assoc
-
 variable {M N O : D} [ModObj A M] [ModObj A N] [ModObj A O]
 
 @[to_additive]

Mathlib/CategoryTheory/Monoidal/Mon.lean

@@ -103,10 +103,7 @@ variable {M X Y : C} [MonObj M]
 @[inherit_doc] scoped notation "η" => MonObj.one
 @[inherit_doc] scoped notation "η[" M "]" => MonObj.one (X := M)
 
-attribute [reassoc (attr := simp)] one_mul mul_one mul_assoc
-attribute [reassoc (attr := simp)] AddMonObj.zero_add AddMonObj.add_zero AddMonObj.add_assoc
-set_option linter.existingAttributeWarning false in
-attribute [to_additive existing] one_mul_assoc mul_one_assoc mul_assoc_assoc
+attribute [to_additive existing (attr := reassoc (attr := simp))] one_mul mul_one mul_assoc
 
 /-- Transfer `MonObj` along an isomorphism. -/
 -- Note: The simps lemmas are not tagged simp because their `#discr_tree_simp_key` are too generic.

Mathlib/Tactic/CategoryTheory/Reassoc.lean

@@ -138,14 +138,11 @@ def reassocExpr' (pf : Expr) : TermElabM Expr := do
         Term.registerSyntheticMVarWithCurrRef inst (.typeClass none)
   return e
 
-initialize registerBuiltinAttribute {
-  name := `reassoc
-  descr := ""
-  applicationTime := .afterCompilation
-  add := fun src ref kind => match ref with
+private def reassocImpl (src : Name) (ref : Syntax) (kind : AttributeKind) : AttrM Name :=
+  match ref with
   | `(attr| reassoc $[$toDual:toDualOpt]? $optAttr) => MetaM.run' do
-    if (kind != AttributeKind.global) then
-      throwError "`reassoc` can only be used as a global attribute"
+    unless kind == AttributeKind.global do
+      throwAttrMustBeGlobal `reassoc kind
     let toDual := toDual.isSome || (Translate.findTranslation? (← getEnv) ToDual.data src).isSome
     let tgt := src.appendAfter "_assoc"
     addRelatedDecl src tgt ref optAttr fun value levels => do
@@ -157,7 +154,17 @@ initialize registerBuiltinAttribute {
     if toDual then
       liftCommandElabM <| Command.elabCommand <| ←
         `(command| attribute [to_dual none] $(mkIdent tgt))
-  | _ => throwUnsupportedSyntax }
+    return tgt
+  | _ => throwUnsupportedSyntax
+
+initialize
+  registerGeneratingAttr `reassoc ((#[·]) <$> reassocImpl · · ·)
+  registerBuiltinAttribute {
+    name := `reassoc
+    descr := ""
+    applicationTime := .afterCompilation
+    add := (discard <| reassocImpl · · ·)
+    }
 
 /--
 `reassoc_of% t`, where `t` is

Mathlib/Tactic/Translate/Core.lean

@@ -883,17 +883,20 @@ def warnParametricAttr {β : Type} [Inhabited β] (stx : Syntax) (attr : Paramet
 /-- `translateLemmas names argInfo desc t` runs `t` on all elements of `names`
 and adds translations between the generated lemmas (the output of `t`).
 `names` must be non-empty. -/
-def translateLemmas {m : Type → Type} [Monad m] [MonadError m] [MonadLiftT CoreM m]
+def translateLemmas
     (t : TranslateData) (names : Array Name) (reorder : Reorder) (relevantArg : RelevantArg)
-    (desc : String) (ref : Syntax) (runAttr : Name → m (Array Name)) : m Unit := do
+    (desc : String) (ref : Syntax) (runAttr : Name → CoreM (Array Name)) : CoreM Unit := do
   let auxLemmas ← names.mapM runAttr
   let nLemmas := auxLemmas[0]!.size
   for nm in names, lemmas in auxLemmas do
     unless lemmas.size == nLemmas do
       throwError "{names[0]!} and {nm} do not generate the same number of {desc}."
   for srcLemmas in auxLemmas, tgtLemmas in auxLemmas.eraseIdx! 0 do
     for srcLemma in srcLemmas, tgtLemma in tgtLemmas do
-      insertTranslation t srcLemma tgtLemma reorder relevantArg ref
+      -- Only add a translation if one doesn't already exist.
+      -- This happens if `srcLemma` is the `_assoc` lemma from `to_dual (attr := reassoc)`.
+      if (findTranslation? (← getEnv) t srcLemma).isNone then
+        insertTranslation t srcLemma tgtLemma reorder relevantArg ref
 
 /-- Return the provided target name or autogenerate one if one was not provided. -/
 def targetName (t : TranslateData) (cfg : Config) (src : Name) : CoreM Name := do