fix(src/tactic/alias): Teach get_alias_target about alias f ↔ a b (…

…#13742)

the `get_alias_target` function in `alias.lean` is used by the
`to_additive` command to add the “Alias of …” docstring when creating an
additive version of an existing alias (this was #13330).

But `get_alias_target` did not work for `alias f ↔ a b`. This fixes it
by extending the `alias_attr` map to not just store whether a defintion
is an alias, but also what it is an alias of. Much more principled than
trying to reconstruct the alias target from the RHS of the alias
definition.

Note that `alias` currently says “Alias of `foo_iff`” even though it’s
really an alias of `foo_iff.mp`. This is an existing bug, not fixed in
this PR – the effect is just that this “bug” will uniformly apply to
additive lemmas as well.

Hopefully will get rid of plenty of nolint.txt entries, and create
better docs.

Also improve the test file for the linter significantly.

src/algebra/parity.lean

@@ -53,13 +53,11 @@ by simp [is_square, pow_two]
 
 alias is_square_iff_exists_sq ↔ is_square.exists_sq is_square_of_exists_sq
 
-attribute [to_additive even.exists_two_nsmul] is_square.exists_sq
-/-- Alias of the forwards direction of `even_iff_exists_two_nsmul`. -/
-add_decl_doc even.exists_two_nsmul
+attribute [to_additive even.exists_two_nsmul "Alias of the forwards direction of
+`even_iff_exists_two_nsmul`."] is_square.exists_sq
 
-attribute [to_additive even_of_exists_two_nsmul] is_square_of_exists_sq
-/-- Alias of the backwards direction of `even_iff_exists_two_nsmul`. -/
-add_decl_doc even_of_exists_two_nsmul
+attribute [to_additive even_of_exists_two_nsmul "Alias of the backwards direction of
+`even_iff_exists_two_nsmul`."] is_square_of_exists_sq
 
 @[simp, to_additive]
 lemma is_square_one [mul_one_class α] : is_square (1 : α) := ⟨1, (mul_one _).symm⟩

src/tactic/alias.lean

@@ -46,7 +46,7 @@ open lean.parser tactic interactive
 
 namespace tactic.alias
 
-@[user_attribute] meta def alias_attr : user_attribute :=
+@[user_attribute] meta def alias_attr : user_attribute unit name :=
 { name := `alias, descr := "This definition is an alias of another.", parser := failed }
 
 meta def alias_direct (d : declaration) (doc : string) (al : name) : tactic unit :=
@@ -59,7 +59,7 @@ do updateex_env $ λ env,
     declaration.thm al ls t $ task.pure $ expr.const n (level.param <$> ls)
   | _ := undefined
   end),
-  alias_attr.set al () tt,
+  alias_attr.set al d.to_name tt,
   add_doc_string al doc
 
 meta def mk_iff_mp_app (iffmp : name) : expr → (ℕ → expr) → tactic expr
@@ -74,7 +74,7 @@ meta def alias_iff (d : declaration) (doc : string) (al : name) (iffmp : name) :
   v ← mk_iff_mp_app iffmp t (λ_, expr.const d.to_name (level.param <$> ls)),
   t' ← infer_type v,
   updateex_env $ λ env, env.add (declaration.thm al ls t' $ task.pure v),
-  alias_attr.set al () tt,
+  alias_attr.set al d.to_name tt,
   add_doc_string al doc
 
 meta def make_left_right : name → tactic (name × name)
@@ -156,12 +156,7 @@ meta def get_lambda_body : expr → expr
 
 meta def get_alias_target (n : name) : tactic (option name) :=
 do tt ← has_attribute' `alias n | pure none,
-  d ← get_decl n,
-  let (head, args) := (get_lambda_body d.value).get_app_fn_args,
-  let head := if head.is_constant_of `iff.mp ∨ head.is_constant_of `iff.mpr then
-    expr.get_app_fn (head.ith_arg 2)
-  else head,
-  guardb $ head.is_constant,
-  pure $ head.const_name
+   v ← alias_attr.get_param n,
+   pure $ some v
 
 end tactic.alias

test/lint_to_additive_doc.lean

@@ -1,61 +1,62 @@
 import algebra.group.to_additive
 import tactic.alias
 
+/-- Test assertion helpers -/
+meta def assert_ok (n : name) := do
+  decl ← tactic.get_decl n,
+  some msg ← linter.to_additive_doc.test decl | pure (),
+  fail! "Linting {n} complained unexpectedly:\n{msg}"
+
+meta def assert_complain (n : name) := do
+  decl ← tactic.get_decl n,
+  none ← linter.to_additive_doc.test decl | pure (),
+  fail! "Linting {n} succeeded unexpectedly"
+
 /-- Docstring -/
 @[to_additive add_foo]
 def foo (α : Type*) [has_one α] : α := 1
 
+run_cmd assert_complain ``foo
+run_cmd assert_ok ``add_foo
+
 @[to_additive add_bar "docstring"]
 def bar (α : Type*) [has_one α] : α := 1
 
+run_cmd assert_complain ``bar
+run_cmd assert_ok ``add_bar
+
 /-- Docstring -/
 @[to_additive add_baz "docstring"]
 def baz (α : Type*) [has_one α] : α := 1
 
+run_cmd assert_ok ``baz
+run_cmd assert_ok ``add_baz
+
 @[to_additive add_quux]
 def quux (α : Type*) [has_one α] : α := 1
 
-def no_to_additive (α : Type*) [has_one α] : α := 1
+run_cmd assert_ok ``quux
+run_cmd assert_ok ``add_quux
+
+def without_to_additive (α : Type*) [has_one α] : α := 1
+
+run_cmd assert_ok ``without_to_additive
 
 -- Aliases always have docstrings, so we do not want to complain if their
 -- additive version do not
 alias quux <- quux_alias
 attribute [to_additive add_quux_alias] quux_alias
 
+run_cmd assert_ok ``quux_alias
+run_cmd assert_ok ``add_quux_alias
+
+-- Same for iff aliases
+def a_one_iff_b_one (α : Type*) [has_one α] (a b : α) (h : a = b) : (a = 1) ↔ (b = 1) := by {subst h}
+alias a_one_iff_b_one ↔ b_one_of_a_one a_one_of_b_one
+attribute [to_additive] a_one_iff_b_one
+attribute [to_additive] b_one_of_a_one
+attribute [to_additive] a_one_of_b_one
 
-open tactic
-run_cmd do
-  decl ← get_decl ``foo,
-  res ← linter.to_additive_doc.test decl,
-  -- linter complains
-  guard $ res.is_some
-
-run_cmd do
-  decl ← get_decl ``bar,
-  res ← linter.to_additive_doc.test decl,
-  -- linter complains
-  guard $ res.is_some
-
-run_cmd do
-  decl ← get_decl ``baz,
-  res ← linter.to_additive_doc.test decl,
-  -- linter is happy
-  guard $ res.is_none
-
-run_cmd do
-  decl ← get_decl ``quux,
-  res ← linter.to_additive_doc.test decl,
-  -- linter is happy
-  guard $ res.is_none
-
-run_cmd do
-  decl ← get_decl ``no_to_additive,
-  res ← linter.to_additive_doc.test decl,
-  -- linter is happy
-  guard $ res.is_none
-
-run_cmd do
-  decl ← get_decl ``quux_alias,
-  res ← linter.to_additive_doc.test decl,
-  -- linter is happy
-  guard $ res.is_none
+run_cmd assert_ok ``a_one_iff_b_one
+run_cmd assert_ok ``a_one_of_b_one
+run_cmd assert_ok ``b_one_of_a_one