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.

add_comm_prefix x s returns "comm_" ++ s if x = tt and s otherwise.

Dictionary used by to_additive.guess_name to autogenerate names.

Autogenerate target name for to_additive.

Return the provided target name or autogenerate one if one was not provided.

the parser for the arguments to to_additive

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.

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.