mathlib3 documentation

tactic.to_additive

Transport multiplicative to additive #

This file defines an attribute to_additive that can be used to automatically transport theorems and definitions (but not inductive types and structures) from a multiplicative theory to an additive theory.

Usage information is contained in the doc string of to_additive.attr.

Missing features #

Temporarily change the has_reflect instance for name.

An auxiliary attribute used to store the names of the additive versions of declarations that have been processed by to_additive.

An attribute that tells @[to_additive] that certain arguments of this definition are not involved when using @[to_additive]. This helps the heuristic of @[to_additive] by also transforming definitions if or another fixed type occurs as one of these arguments.

An attribute that is automatically added to declarations tagged with @[to_additive], if needed.

This attribute tells which argument is the type where this declaration uses the multiplicative structure. If there are multiple argument, we typically tag the first one. If this argument contains a fixed type, this declaration will note be additivized. See the Heuristics section of to_additive.attr for more details.

If a declaration is not tagged, it is presumed that the first argument is relevant. @[to_additive] uses the function to_additive.first_multiplicative_arg to automatically tag declarations. It is ok to update it manually if the automatic tagging made an error.

Implementation note: we only allow exactly 1 relevant argument, even though some declarations (like prod.group) have multiple arguments with a multiplicative structure on it. The reason is that whether we additivize a declaration is an all-or-nothing decision, and if we will not be able to additivize declarations that (e.g.) talk about multiplication on ℕ × α anyway.

Warning: adding @[to_additive_reorder] with an equal or smaller number than the number in this attribute is currently not supported.

An attribute that stores all the declarations that needs their arguments reordered when applying @[to_additive]. Currently, we only support swapping consecutive arguments. The list of the natural numbers contains the positions of the first of the two arguments to be swapped. If the first two arguments are swapped, the first two universe variables are also swapped. Example: @[to_additive_reorder 1 4] swaps the first two arguments and the arguments in positions 4 and 5.

Find the first argument of nm that has a multiplicative type-class on it. Returns 1 if there are no types with a multiplicative class as arguments. E.g. prod.group returns 1, and pi.has_one returns 2.

meta def to_additive.map_namespace (src tgt : name) :

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.

value_type is the type of the arguments that can be provided to to_additive. to_additive.parser parses the provided arguments:

  • replace_all: replace all multiplicative declarations, do not use the heuristic.
  • trace: output the generated additive declaration.
  • tgt : name: the name of the target (the additive declaration).
  • doc: an optional doc string.
  • if allow_auto_name is ff (default) then @[to_additive] will check whether the given name can be auto-generated.
Instances for to_additive.value_type

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.

meta def to_additive.target_name (src tgt : name) (dict : name_map name) (allow_auto_name : bool) :

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

the parser for the arguments to to_additive.

meta def to_additive.proceed_fields (env : environment) (src tgt : name) (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.

@[protected]

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:

@[to_additive add_foo]
theorem foo := sorry

An existing documentation string will not be automatically used, so if the theorem or definition has a doc string, a doc string for the additive version should be passed explicitly to to_additive.

/-- Multiplication is commutative -/
@[to_additive "Addition is commutative"]
theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm

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.

If the declaration to be transported has attributes which need to be copied to the additive version, then to_additive should come last:

@[simp, to_additive] lemma mul_one' {G : Type*} [group G] (x : G) : x * 1 = x := mul_one x

The following attributes are supported and should be applied correctly by to_additive to the new additivized declaration, if they were present on the original one:

reducible, _refl_lemma, simp, norm_cast, instance, refl, symm, trans, elab_as_eliminator, no_rsimp,
continuity, ext, ematch, measurability, alias, _ext_core, _ext_lemma_core, nolint

The exception to this rule is the simps attribute, which should come after to_additive:

@[to_additive, simps]
instance {M N} [has_mul M] [has_mul N] : has_mul (M × N) := λ p q, p.1 * q.1, p.2 * q.2⟩⟩

Additionally the mono attribute is not handled by to_additive and should be applied afterwards to both the original and additivized lemma.

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'.

Heuristics #

to_additive uses heuristics to determine whether a particular identifier has to be mapped to its additive version. The basic heuristic is

  • Only map an identifier to its additive version if its first argument doesn't contain any unapplied identifiers.

Examples:

  • @has_mul.mul ℕ n m (i.e. (n * m : ℕ)) will not change to +, since its first argument is , an identifier not applied to any arguments.
  • @has_mul.mul (α × β) x y will change to +. It's first argument contains only the identifier prod, but this is applied to arguments, α and β.
  • @has_mul.mul (α × ℤ) x y will not change to +, since its first argument contains .

The reasoning behind the heuristic is that the first argument is the type which is "additivized", and this usually doesn't make sense if this is on a fixed type.

There are some exceptions to this heuristic:

  • Identifiers that have the @[to_additive] attribute are ignored. For example, multiplication in ↥Semigroup is replaced by addition in ↥AddSemigroup.
  • If an identifier d has attribute @[to_additive_relevant_arg n] then the argument in position n is checked for a fixed type, instead of checking the first argument. @[to_additive] will automatically add the attribute @[to_additive_relevant_arg n] to a declaration when the first argument has no multiplicative type-class, but argument n does.
  • If an identifier has attribute @[to_additive_ignore_args n1 n2 ...] then all the arguments in positions n1, n2, ... will not be checked for unapplied identifiers (start counting from 1). For example, cont_mdiff_map has attribute @[to_additive_ignore_args 21], which means that its 21st argument (n : ℕ∞) can contain (usually in the form has_top.top ℕ ...) and still be additivized. So @has_mul.mul (C^∞⟮I, N; I', G⟯) _ f g will be additivized.

Troubleshooting #

If @[to_additive] fails because the additive declaration raises a type mismatch, there are various things you can try. The first thing to do is to figure out what @[to_additive] did wrong by looking at the type mismatch error.

  • Option 1: It additivized a declaration d that should remain multiplicative. Solution:
    • Make sure the first argument of d is a type with a multiplicative structure. If not, can you reorder the (implicit) arguments of d so that the first argument becomes a type with a multiplicative structure (and not some indexing type)? The reason is that @[to_additive] doesn't additivize declarations if their first argument contains fixed types like or . See section Heuristics. If the first argument is not the argument with a multiplicative type-class, @[to_additive] should have automatically added the attribute @[to_additive_relevant_arg] to the declaration. You can test this by running the following (where d is the full name of the declaration):
        run_cmd to_additive.relevant_arg_attr.get_param `d >>= tactic.trace
      
      The expected output is n where the n-th argument of d is a type (family) with a multiplicative structure on it. If you get a different output (or a failure), you could add the attribute @[to_additive_relevant_arg n] manually, where n is an argument with a multiplicative structure.
  • Option 2: It didn't additivize a declaration that should be additivized. This happened because the heuristic applied, and the first argument contains a fixed type, like or . Solutions:
    • If the fixed type has an additive counterpart (like ↥Semigroup), give it the @[to_additive] attribute.
    • If the fixed type occurs inside the k-th argument of a declaration d, and the k-th argument is not connected to the multiplicative structure on d, consider adding attribute [to_additive_ignore_args k] to d.
    • If you want to disable the heuristic and replace all multiplicative identifiers with their additive counterpart, use @[to_additive!].
  • Option 3: Arguments / universe levels are incorrectly ordered in the additive version. This likely only happens when the multiplicative declaration involves pow/^. Solutions:
    • Ensure that the order of arguments of all relevant declarations are the same for the multiplicative and additive version. This might mean that arguments have an "unnatural" order (e.g. monoid.npow n x corresponds to x ^ n, but it is convenient that monoid.npow has this argument order, since it matches add_monoid.nsmul n x.
    • If this is not possible, add the [to_additive_reorder k] to the multiplicative declaration to indicate that the k-th and (k+1)-st arguments are reordered in the additive version.

If neither of these solutions work, and to_additive is unable to automatically generate the additive version of a declaration, manually write and prove the additive version. Often the proof of a lemma/theorem can just be the multiplicative version of the lemma applied to multiplicative G. Afterwards, 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.

In addition to transporting the “main” declaration, to_additive transports its equational lemmas and tags them as equational lemmas for the new declaration, attributes present on the original equational lemmas are also transferred first (notably _refl_lemma).

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. The ancestor attribute must come before the to_additive attribute, and it is essential that the order of the base structures passed to ancestor matches between the multiplicative and additive versions of the structure.

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 case to_additive double checks that the new name differs from the original one.

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:

@[to_additive add_foo]
theorem foo := sorry

An existing documentation string will not be automatically used, so if the theorem or definition has a doc string, a doc string for the additive version should be passed explicitly to to_additive.

/-- Multiplication is commutative -/
@[to_additive "Addition is commutative"]
theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm

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.

If the declaration to be transported has attributes which need to be copied to the additive version, then to_additive should come last:

@[simp, to_additive] lemma mul_one' {G : Type*} [group G] (x : G) : x * 1 = x := mul_one x

The following attributes are supported and should be applied correctly by to_additive to the new additivized declaration, if they were present on the original one:

reducible, _refl_lemma, simp, norm_cast, instance, refl, symm, trans, elab_as_eliminator, no_rsimp,
continuity, ext, ematch, measurability, alias, _ext_core, _ext_lemma_core, nolint

The exception to this rule is the simps attribute, which should come after to_additive:

@[to_additive, simps]
instance {M N} [has_mul M] [has_mul N] : has_mul (M × N) := λ p q, p.1 * q.1, p.2 * q.2⟩⟩

Additionally the mono attribute is not handled by to_additive and should be applied afterwards to both the original and additivized lemma.

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'.

Heuristics #

to_additive uses heuristics to determine whether a particular identifier has to be mapped to its additive version. The basic heuristic is

  • Only map an identifier to its additive version if its first argument doesn't contain any unapplied identifiers.

Examples:

  • @has_mul.mul ℕ n m (i.e. (n * m : ℕ)) will not change to +, since its first argument is , an identifier not applied to any arguments.
  • @has_mul.mul (α × β) x y will change to +. It's first argument contains only the identifier prod, but this is applied to arguments, α and β.
  • @has_mul.mul (α × ℤ) x y will not change to +, since its first argument contains .

The reasoning behind the heuristic is that the first argument is the type which is "additivized", and this usually doesn't make sense if this is on a fixed type.

There are some exceptions to this heuristic:

  • Identifiers that have the @[to_additive] attribute are ignored. For example, multiplication in ↥Semigroup is replaced by addition in ↥AddSemigroup.
  • If an identifier d has attribute @[to_additive_relevant_arg n] then the argument in position n is checked for a fixed type, instead of checking the first argument. @[to_additive] will automatically add the attribute @[to_additive_relevant_arg n] to a declaration when the first argument has no multiplicative type-class, but argument n does.
  • If an identifier has attribute @[to_additive_ignore_args n1 n2 ...] then all the arguments in positions n1, n2, ... will not be checked for unapplied identifiers (start counting from 1). For example, cont_mdiff_map has attribute @[to_additive_ignore_args 21], which means that its 21st argument (n : ℕ∞) can contain (usually in the form has_top.top ℕ ...) and still be additivized. So @has_mul.mul (C^∞⟮I, N; I', G⟯) _ f g will be additivized.

Troubleshooting #

If @[to_additive] fails because the additive declaration raises a type mismatch, there are various things you can try. The first thing to do is to figure out what @[to_additive] did wrong by looking at the type mismatch error.

  • Option 1: It additivized a declaration d that should remain multiplicative. Solution:
    • Make sure the first argument of d is a type with a multiplicative structure. If not, can you reorder the (implicit) arguments of d so that the first argument becomes a type with a multiplicative structure (and not some indexing type)? The reason is that @[to_additive] doesn't additivize declarations if their first argument contains fixed types like or . See section Heuristics. If the first argument is not the argument with a multiplicative type-class, @[to_additive] should have automatically added the attribute @[to_additive_relevant_arg] to the declaration. You can test this by running the following (where d is the full name of the declaration):
        run_cmd to_additive.relevant_arg_attr.get_param `d >>= tactic.trace
      
      The expected output is n where the n-th argument of d is a type (family) with a multiplicative structure on it. If you get a different output (or a failure), you could add the attribute @[to_additive_relevant_arg n] manually, where n is an argument with a multiplicative structure.
  • Option 2: It didn't additivize a declaration that should be additivized. This happened because the heuristic applied, and the first argument contains a fixed type, like or . Solutions:
    • If the fixed type has an additive counterpart (like ↥Semigroup), give it the @[to_additive] attribute.
    • If the fixed type occurs inside the k-th argument of a declaration d, and the k-th argument is not connected to the multiplicative structure on d, consider adding attribute [to_additive_ignore_args k] to d.
    • If you want to disable the heuristic and replace all multiplicative identifiers with their additive counterpart, use @[to_additive!].
  • Option 3: Arguments / universe levels are incorrectly ordered in the additive version. This likely only happens when the multiplicative declaration involves pow/^. Solutions:
    • Ensure that the order of arguments of all relevant declarations are the same for the multiplicative and additive version. This might mean that arguments have an "unnatural" order (e.g. monoid.npow n x corresponds to x ^ n, but it is convenient that monoid.npow has this argument order, since it matches add_monoid.nsmul n x.
    • If this is not possible, add the [to_additive_reorder k] to the multiplicative declaration to indicate that the k-th and (k+1)-st arguments are reordered in the additive version.

If neither of these solutions work, and to_additive is unable to automatically generate the additive version of a declaration, manually write and prove the additive version. Often the proof of a lemma/theorem can just be the multiplicative version of the lemma applied to multiplicative G. Afterwards, 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.

In addition to transporting the “main” declaration, to_additive transports its equational lemmas and tags them as equational lemmas for the new declaration, attributes present on the original equational lemmas are also transferred first (notably _refl_lemma).

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. The ancestor attribute must come before the to_additive attribute, and it is essential that the order of the base structures passed to ancestor matches between the multiplicative and additive versions of the structure.

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 case to_additive double checks that the new name differs from the original one.

A linter that checks that multiplicative and additive lemmas have both doc strings if one of them has one