fix(transform_decl): fix namespace bug (#8733)

* The problem was that when writing `@[to_additive] def foo ...` every declaration used in `foo` in namespace `foo` would be additivized without changing the last part of the name. This behavior was intended to translate automatically generated declarations like `foo._proof_1`. However, if `foo` contains a non-internal declaration `foo.bar` and `add_foo.bar` didn't exist yet, it would also create a declaration `add_foo.bar` additivizing `foo.bar`.
* This PR changes the behavior: if `foo.bar` has the `@[to_additive]` attribute (potentially with a custom additive name), then we won't create a second additive version of `foo.bar`, and succeed normally. However, if `foo.bar` doesn't have the `@[to_additive]` attribute, then we fail with a nice error message. We could potentially support this behavior, but it doesn't seem that worthwhile and it would require changing a couple low-level definitions that `@[to_additive]` uses (e.g. by replacing `name.map_prefix` so that it only maps prefixes if the name is `internal`).
* So far this didn't happen in the library yet. There are currently 5 non-internal declarations `foo.bar` that are used in `foo` where `foo` has the `@[to_additive]` attribute, but all of these declarations were already had an additive version `add_foo.bar`.
* These 5 declarations are `[Mon.has_limits.limit_cone, Mon.has_limits.limit_cone_is_limit, con_gen.rel, magma.free_semigroup.r, localization.r]`
* This fixes the error in #8707 and resolves the Zulip thread https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238707.20linter.20weirdness
* I also added some documentation / comments to the function `transform_decl_with_prefix_fun_aux`, made it non-private, and rewrote some steps.

Author: fpvandoorn

src/tactic/transform_decl.lean

@@ -44,30 +44,43 @@ meta def additive_test (f : name → option name) (replace_all : bool) (ignore :
   (e : expr) : bool :=
 if replace_all then tt else additive_test_aux f ignore ff e
 
-private meta def transform_decl_with_prefix_fun_aux (f : name → option name)
+/-- transform the declaration `src` and all declarations `pre._proof_i` occurring in `src`
+using the dictionary `f`.
+`replace_all`, `trace`, `ignore` and `reorder` are configuration options.
+`pre` is the declaration that got the `@[to_additive]` attribute and `tgt_pre` is the target of this
+declaration. -/
+meta def transform_decl_with_prefix_fun_aux (f : name → option name)
   (replace_all trace : bool) (ignore reorder : name_map $ list ℕ) (pre tgt_pre : name)
   (attrs : list name) : name → command :=
 λ src,
 do
+  -- if this declaration is not `pre` or an internal declaration, we do nothing.
+  tt ← return (src = pre ∨ src.is_internal : bool) |
+    if (f src).is_some then skip else fail!("@[to_additive] failed.
+The declaration {pre} depends on the declaration {src} which is in the namespace {pre}, but " ++
+"does not have the `@[to_additive]` attribute. This is not supported. Workaround: move {src} to " ++
+"a different namespace."),
+  env ← get_env,
+  -- we find the additive name of `src`
   let tgt := src.map_prefix (λ n, if n = pre then some tgt_pre else none),
-  (get_decl tgt >> skip) <|>
-  do
-    decl ← get_decl src,
-    (decl.type.list_names_with_prefix pre).mfold () (λ n _, transform_decl_with_prefix_fun_aux n),
-    (decl.value.list_names_with_prefix pre).mfold () (λ n _, transform_decl_with_prefix_fun_aux n),
-    is_protected ← is_protected_decl src,
-    env ← get_env,
-    let decl :=
-      decl.update_with_fun env (name.map_prefix f) (additive_test f replace_all ignore) reorder tgt,
-    pp_decl ← pp decl,
-    when trace $ trace!"[to_additive] > generating\n{pp_decl}",
-    decorate_error (format!"@[to_additive] failed. Type mismatch in additive declaration.
+  -- we skip if we already transformed this declaration before
+  ff ← return $ env.contains tgt | skip,
+  decl ← get_decl src,
+  -- we first transform all the declarations of the form `pre._proof_i`
+  (decl.type.list_names_with_prefix pre).mfold () (λ n _, transform_decl_with_prefix_fun_aux n),
+  (decl.value.list_names_with_prefix pre).mfold () (λ n _, transform_decl_with_prefix_fun_aux n),
+  -- we transform `decl` using `f` and the configuration options.
+  let decl :=
+    decl.update_with_fun env (name.map_prefix f) (additive_test f replace_all ignore) reorder tgt,
+  pp_decl ← pp decl,
+  when trace $ trace!"[to_additive] > generating\n{pp_decl}",
+  decorate_error (format!"@[to_additive] failed. Type mismatch in additive declaration.
 For help, see the docstring of `to_additive.attr`, section `Troubleshooting`.
 Failed to add declaration\n{pp_decl}
 
-Nested error message:\n").to_string $ -- empty line is intentional
-      if is_protected then add_protected_decl decl else add_decl decl,
-    attrs.mmap' (λ n, copy_attribute n src tgt)
+Nested error message:\n").to_string $ -- the empty line is intentional
+    if env.is_protected src then add_protected_decl decl else add_decl decl,
+  attrs.mmap' $ λ n, copy_attribute n src tgt
 
 /--
 Make a new copy of a declaration,

test/to_additive.lean

@@ -58,3 +58,22 @@ let t := d.type.eta_expand env reorder,
 let decl := declaration.defn `barr6 d.univ_params t e d.reducibility_hints d.is_trusted,
 add_decl decl,
 skip
+
+/-! Test the namespace bug (#8733). This code should *not* generate a lemma
+  `add_some_def.in_namespace`. -/
+def some_def.in_namespace : bool := ff
+
+def some_def {α : Type*} [has_mul α] (x : α) : α :=
+if some_def.in_namespace then x * x else x
+
+-- cannot apply `@[to_additive]` to `some_def` if `some_def.in_namespace` doesn't have the attribute
+run_cmd do
+  dict ← to_additive.aux_attr.get_cache,
+  success_if_fail
+    (transform_decl_with_prefix_dict dict ff tt mk_name_map mk_name_map `some_def `add_some_def []),
+  skip
+
+attribute [to_additive some_other_name] some_def.in_namespace
+attribute [to_additive add_some_def] some_def
+
+run_cmd success_if_fail (get_decl `add_some_def.in_namespace)