doc(algebra/group/to_additive): add doc strings and tactic doc entry (#…

…3055)

src/algebra/group/to_additive.lean

@@ -11,63 +11,9 @@ import tactic.algebra
 
 This file defines an attribute `to_additive` that can be used to
 automatically transport theorems and definitions (but not inductive
-types and structures) from multiplicative theory to additive theory.
+types and structures) from a multiplicative theory to an additive theory.
 
-To use this attribute, just write
-
-```
-@[to_additive]
-theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm
-```
-
-This code will generate a theorem named `add_comm'`.  It is also
-possible to manually specify the name of the new declaration, and
-provide a documentation string.
-
-The transport tries to do the right thing in most cases using several
-heuristics described below.  However, in some cases it fails, and
-requires manual intervention.
-
-## Implementation notes
-### Handling of hidden definitions
-
-Before transporting the “main” declaration `src`, `to_additive` first
-scans its type and value for names starting with `src`, and transports
-them. This includes auxiliary definitions like `src._match_1`,
-`src._proof_1`.
-
-After transporting the “main” declaration, `to_additive` transports
-its equational lemmas.
-
-### Structure fields and constructors
-
-If `src` is a structure, then `to_additive` automatically adds
-structure fields to its mapping, and similarly for constructors of
-inductive types.
-
-For new structures this means that `to_additive` automatically handles
-coercions, and for old structures it does the same, if ancestry
-information is present in `@[ancestor]` attributes.
-
-### Name generation
-
-* If `@[to_additive]` is called without a `name` argument, then the
-  new name is autogenerated.  First, it takes the longest prefix of
-  the source name that is already known to `to_additive`, and replaces
-  this prefix with its additive counterpart. Second, it takes the last
-  part of the name (i.e., after the last dot), and replaces common
-  name parts (“mul”, “one”, “inv”, “prod”) with their additive versions.
-
-* If `@[to_additive]` is called with a `name` argument `new_name`
-  /without a dot/, then `to_additive` updates the prefix as described
-  above, then replaces the last part of the name with `new_name`.
-
-* If `@[to_additive]` is called with a `name` argument
-  `new_namespace.new_name` /with a dot/, then `to_additive` uses this
-  new name as is.
-
-As a safety check, in the first two cases `to_additive` double checks
-that the new name differs from the original one.
+Usage information is contained in the doc string of `to_additive.attr`.
 
 ### Missing features
 
@@ -83,6 +29,8 @@ that the new name differs from the original one.
 namespace to_additive
 open tactic exceptional
 
+/-- An auxiliary attribute used to store the names of the additive versions of declarations
+that have been processed by `to_additive`. -/
 @[user_attribute]
 meta def aux_attr : user_attribute (name_map name) name :=
 { name      := `to_additive_aux,
@@ -98,14 +46,28 @@ meta def aux_attr : user_attribute (name_map name) name :=
                   mk_name_map, []⟩,
   parser    := lean.parser.ident }
 
+/-- A command that can be used to have future uses of `to_additive` change the `src` namespace
+to the `tgt` namespace.
+
+For example:
+```
+run_cmd to_additive.map_namespace `quotient_group `quotient_add_group
+```
+
+Later uses of `to_additive` on declarations in the `quotient_group` namespace will be created
+in the `quotient_add_group` namespaces.
+-/
 meta def map_namespace (src tgt : name) : command :=
 do let n := src.mk_string "_to_additive",
    let decl := declaration.thm n [] `(unit) (pure (reflect ())),
    add_decl decl,
    aux_attr.set n tgt tt
 
+/-- `value_type` is the type of the arguments that can be provided to `to_additive`.
+`to_additive.parser` parses the provided arguments into `name` for the target and an
+optional doc string. -/
 @[derive has_reflect, derive inhabited]
-structure value_type := (tgt : name) (doc : option string)
+structure value_type : Type := (tgt : name) (doc : option string)
 
 /-- Dictionary used by `to_additive.guess_name` to autogenerate names. -/
 meta def tr : list string → list string
@@ -127,6 +89,7 @@ string.map_tokens ''' $
 λ s, string.intercalate (string.singleton '_') $
 tr (s.split_on '_')
 
+/-- Return the provided target name or autogenerate one if one was not provided. -/
 meta def target_name (src tgt : name) (dict : name_map name) : tactic name :=
 (if tgt.get_prefix ≠ name.anonymous -- `tgt` is a full name
  then pure tgt
@@ -146,6 +109,7 @@ meta def target_name (src tgt : name) (dict : name_map name) : tactic name :=
   then fail ("to_additive: can't transport " ++ src.to_string ++ " to itself")
   else pure res)
 
+/-- the parser for the arguments to `to_additive` -/
 meta def parser : lean.parser value_type :=
 do
   tgt ← optional lean.parser.ident,
@@ -167,6 +131,8 @@ do
     λ names, guard (names.fst = names.snd) <|>
       aux_attr.set (src.append names.fst) (tgt.append names.snd) tt prio
 
+/-- Add the `aux_attr` attribute to the structure fields of `src`
+so that future uses of `to_additive` will map them to the corresponding `tgt` fields. -/
 meta def proceed_fields (env : environment) (src tgt : name) (prio : ℕ) : command :=
 let aux := proceed_fields_aux src tgt prio in
 do
@@ -181,6 +147,105 @@ aux (λ n, (env.constructors_of n).mmap $
                 | _ := fail "Bad constructor name"
                 end)
 
+/--
+The attribute `to_additive` can be used to automatically transport theorems
+and definitions (but not inductive types and structures) from a multiplicative
+theory to an additive theory.
+
+To use this attribute, just write:
+
+```
+@[to_additive]
+theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm
+```
+
+This code will generate a theorem named `add_comm'`.  It is also
+possible to manually specify the name of the new declaration, and
+provide a documentation string:
+
+```
+@[to_additive add_foo "add_foo doc string"]
+/-- foo doc string -/
+theorem foo := sorry
+```
+
+The transport tries to do the right thing in most cases using several
+heuristics described below.  However, in some cases it fails, and
+requires manual intervention.
+
+## Implementation notes
+
+The transport process generally works by taking all the names of
+identifiers appearing in the name, type, and body of a declaration and
+creating a new declaration by mapping those names to additive versions
+using a simple string-based dictionary and also using all declarations
+that have previously been labeled with `to_additive`.
+
+In the `mul_comm'` example above, `to_additive` maps:
+* `mul_comm'` to `add_comm'`,
+* `comm_semigroup` to `add_comm_semigroup`,
+* `x * y` to `x + y` and `y * x` to `y + x`, and
+* `comm_semigroup.mul_comm'` to `add_comm_semigroup.add_comm'`.
+
+Even when `to_additive` is unable to automatically generate the additive
+version of a declaration, it can be useful to apply the attribute manually:
+
+```
+attribute [to_additive foo_add_bar] foo_bar
+```
+
+This will allow future uses of `to_additive` to recognize that
+`foo_bar` should be replaced with `foo_add_bar`.
+
+### Handling of hidden definitions
+
+Before transporting the “main” declaration `src`, `to_additive` first
+scans its type and value for names starting with `src`, and transports
+them. This includes auxiliary definitions like `src._match_1`,
+`src._proof_1`.
+
+After transporting the “main” declaration, `to_additive` transports
+its equational lemmas.
+
+### Structure fields and constructors
+
+If `src` is a structure, then `to_additive` automatically adds
+structure fields to its mapping, and similarly for constructors of
+inductive types.
+
+For new structures this means that `to_additive` automatically handles
+coercions, and for old structures it does the same, if ancestry
+information is present in `@[ancestor]` attributes.
+
+### Name generation
+
+* If `@[to_additive]` is called without a `name` argument, then the
+  new name is autogenerated.  First, it takes the longest prefix of
+  the source name that is already known to `to_additive`, and replaces
+  this prefix with its additive counterpart. Second, it takes the last
+  part of the name (i.e., after the last dot), and replaces common
+  name parts (“mul”, “one”, “inv”, “prod”) with their additive versions.
+
+* Namespaces can be transformed using `map_namespace`. For example:
+  ```
+  run_cmd to_additive.map_namespace `quotient_group `quotient_add_group
+  ```
+
+  Later uses of `to_additive` on declarations in the `quotient_group`
+  namespace will be created in the `quotient_add_group` namespaces.
+
+* If `@[to_additive]` is called with a `name` argument `new_name`
+  /without a dot/, then `to_additive` updates the prefix as described
+  above, then replaces the last part of the name with `new_name`.
+
+* If `@[to_additive]` is called with a `name` argument
+  `new_namespace.new_name` /with a dot/, then `to_additive` uses this
+  new name as is.
+
+As a safety check, in the first two cases `to_additive` double checks
+that the new name differs from the original one.
+
+-/
 @[user_attribute]
 protected meta def attr : user_attribute unit value_type :=
 { name      := `to_additive,
@@ -203,6 +268,13 @@ protected meta def attr : user_attribute unit value_type :=
       | some doc := add_doc_string tgt doc
       | none := skip
       end }
+
+add_tactic_doc
+{ name                     := "to_additive",
+  category                 := doc_category.attr,
+  decl_names               := [`to_additive.attr],
+  tags                     := ["transport", "environment", "lemma derivation"] }
+
 end to_additive
 
 /- map operations -/