# The `@[to_additive]`

attribute. #

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' {α} [CommSemigroup α] (x y : α) : x * y = y * x := mul_comm x y
```

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' {α} [CommSemigroup α] (x y : α) : x * y = y * x := CommSemigroup.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.

Use the `(reorder := ...)`

syntax to reorder the arguments in the generated additive declaration.
This is specified using cycle notation. For example `(reorder := 1 2, 5 6)`

swaps the first two
arguments with each other and the fifth and the sixth argument and `(reorder := 3 4 5)`

will move
the fifth argument before the third argument. This is mostly useful to translate declarations using
`Pow`

to those using `SMul`

.

Use the `(attr := ...)`

syntax to apply attributes to both the multiplicative and the additive
version:

```
@[to_additive (attr := simp)] lemma mul_one' {G : Type*} [Group G] (x : G) : x * 1 = x := mul_one x
```

For `simps`

this also ensures that some generated lemmas are added to the additive dictionary.
`@[to_additive (attr := to_additive)]`

is a special case, where the `to_additive`

attribute is added to the generated lemma only, to additivize it again.
This is useful for lemmas about `Pow`

to generate both lemmas about `SMul`

and `VAdd`

. Example:

```
@[to_additive (attr := to_additive VAdd_lemma, simp) SMul_lemma]
lemma Pow_lemma ... :=
```

In the above example, the `simp`

is added to all 3 lemmas. All other options to `to_additive`

(like the generated name or `(reorder := ...)`

) are not passed down,
and can be given manually to each individual `to_additive`

call.

## 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'`

,`CommSemigroup`

to`AddCommSemigroup`

,`x * y`

to`x + y`

and`y * x`

to`y + x`

, and`CommSemigroup.mul_comm'`

to`AddCommSemigroup.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:

`@Mul.mul Nat n m`

(i.e.`(n * m : Nat)`

) will not change to`+`

, since its first argument is`Nat`

, an identifier not applied to any arguments.`@Mul.mul (α × β) x y`

will change to`+`

. It's first argument contains only the identifier`Prod`

, but this is applied to arguments,`α`

and`β`

.`@Mul.mul (α × Int) x y`

will not change to`+`

, since its first argument contains`Int`

.

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,`ContMDiffMap`

has attribute`@[to_additive_ignore_args 21]`

, which means that its 21st argument`(n : WithTop ℕ)`

can contain`ℕ`

(usually in the form`Top.top ℕ ...`

) and still be additivized. So`@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: The most common case is that 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`ℝ`

. However, the heuristic misfires on some other declarations. Solutions:- First figure out what the fixed type is in the first argument of the declaration that didn't
get additivized. Note that this fixed type can occur in implicit arguments. If manually finding
it is hard, you can run
`set_option trace.to_additive_detail true`

and search the output for the fragment "contains the fixed type" to find what the fixed type is. - If the fixed type has an additive counterpart (like
`↥Semigroup`

), give it the`@[to_additive]`

attribute. - If the fixed type has nothing to do with algebraic operations (like
`TopCat`

), add the attribute`@[to_additive existing Foo]`

to the fixed type`Foo`

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

. Example:`ContMDiffMap`

ignores the argument`(n : WithTop ℕ)`

- First figure out what the fixed type is in the first argument of the declaration that didn't
get additivized. Note that this fixed type can occur in implicit arguments. If manually finding
it is hard, you can run
- Option 2: 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):

The expected output is`open Lean in run_cmd logInfo m!"{ToAdditive.relevantArgAttr.find? (← getEnv) `d}"`

`n`

where the`n`

-th (0-indexed) argument of`d`

is a type (family) with a multiplicative structure on it.`none`

means`0`

. If you get a different output (or a failure), you could add the attribute`@[to_additive_relevant_arg n]`

manually, where`n`

is an (1-indexed) argument with a multiplicative structure.

- Make sure the first argument of
- 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`AddMonoid.nsmul n x`

. - If this is not possible, add
`(reorder := ...)`

argument to`to_additive`

.

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

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.

### Structure fields and constructors #

If `src`

is a structure, then the additive version has to be already written manually.
In this case `to_additive`

adds all structure fields to its mapping.

### 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.[todo] Namespaces can be transformed using

`map_namespace`

. For example:`run_cmd to_additive.map_namespace `QuotientGroup `QuotientAddGroup`

Later uses of

`to_additive`

on declarations in the`QuotientGroup`

namespace will be created in the`QuotientAddGroup`

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`NewNamespace.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 `to_additive_ignore_args`

attribute.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The `to_additive_relevant_arg`

attribute.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The `to_additive_reorder`

attribute.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The `to_additive_change_numeral`

attribute.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

An `attr := ...`

option for `to_additive`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

A `reorder := ...`

option for `to_additive`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Options to `to_additive`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Options to `to_additive`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Remaining arguments of `to_additive`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The `to_additive`

attribute.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The `to_additive`

attribute.

## Equations

- attrTo_additive?_ = Lean.ParserDescr.node `attrTo_additive?_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "to_additive?" false) toAdditiveRest)

## Instances For

A set of strings of names that end in a capital letter.

- If the string contains a lowercase letter, the string should be split between the first occurrence of a lower-case letter followed by an upper-case letter.
- If multiple strings have the same prefix, they should be grouped by prefix
- In this case, the second list should be prefix-free (no element can be a prefix of a later element)

Todo: automate the translation from `String`

to an element in this `RBMap`

(but this would require having something similar to the `rb_lmap`

from Lean 3).

## Equations

- endCapitalNames = Lean.RBMap.ofList [("LE", [""]), ("LT", [""]), ("WF", [""]), ("Coe", ["TC", "T", "HTCT"])]

## Instances For

This function takes a String and splits it into separate parts based on the following (naming conventions)[https://github.com/leanprover-community/mathlib4/wiki#naming-convention].

E.g. `#eval "InvHMulLEConjugate₂SMul_ne_top".splitCase`

yields
`["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"]`

.

Linter to check that the `reorder`

attribute is not given manually

Linter, mostly used by `@[to_additive]`

, that checks that the source declaration doesn't have
certain attributes

Linter to check that the `to_additive`

attribute is not given manually

Linter to check whether the user correctly specified that the additive declaration already exists

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 stores all the declarations that needs their arguments reordered when
applying `@[to_additive]`

. It is applied automatically by the `(reorder := ...)`

syntax of
`to_additive`

, and should not usually be added manually.

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: interactions between this and the `(reorder := ...)`

argument are not well-tested.

An attribute that stores all the declarations that deal with numeric literals on variable types.

Numeral literals occur in expressions without type information, so in order to decide whether `1`

needs to be changed to `0`

, the context around the numeral is relevant.
Most numerals will be in an `OfNat.ofNat`

application, though tactics can add numeral literals
inside arbitrary functions. By default we assume that we do not change numerals, unless it is
in a function application with the `to_additive_change_numeral`

attribute.

`@[to_additive_change_numeral n₁ ...]`

should be added to all functions that take one or more
numerals as argument that should be changed if `additiveTest`

succeeds on the first argument,
i.e. when the numeral is only translated if the first argument is a variable
(or consists of variables).
The arguments `n₁ ...`

are the positions of the numeral arguments (starting counting from 1).

Maps multiplicative names to their additive counterparts.

Get the multiplicative → additive translation for the given name.

## Equations

## Instances For

`Config`

is the type of the arguments that can be provided to `to_additive`

.

- trace : Bool
View the trace of the to_additive procedure. Equivalent to

`set_option trace.to_additive true`

. - tgt : Lean.Name
The name of the target (the additive declaration).

An optional doc string.

- allowAutoName : Bool
If

`allowAutoName`

is`false`

(default) then`@[to_additive]`

will check whether the given name can be auto-generated. The arguments that should be reordered by

`to_additive`

, using cycle notation.- attrs : Array Lean.Syntax
The attributes which we want to give to both the multiplicative and additive versions. For

`simps`

this will also add generated lemmas to the translation dictionary. - ref : Lean.Syntax
The

`Syntax`

element corresponding to the original multiplicative declaration (or the`to_additive`

attribute if it is added later), which we need for adding definition ranges. An optional flag stating whether the additive declaration already exists. If this flag is set but wrong about whether the additive declaration exists,

`to_additive`

will raise a linter error. Note: the linter will never raise an error for inductive types and structures.

## Instances For

## Equations

- ToAdditive.instReprConfig = { reprPrec := ToAdditive.reprConfig✝ }

Implementation function for `additiveTest`

.
We cache previous applications of the function, using an expression cache using ptr equality
to avoid visiting the same subexpression many times. Note that we only need to cache the
expressions without taking the value of `inApp`

into account, since `inApp`

only matters when
the expression is a constant. However, for this reason we have to make sure that we never
cache constant expressions, so that's why the `if`

s in the implementation are in this order.

Note that this function is still called many times by `applyReplacementFun`

and we're not remembering the cache between these calls.

## Instances For

`additiveTest e`

tests whether the expression `e`

contains a constant
`nm`

that is not applied to any arguments, and such that `translations.find?[nm] = none`

.
This is used in `@[to_additive]`

for deciding which subexpressions to transform: we only transform
constants if `additiveTest`

applied to their first argument returns `true`

.
This means we will replace expression applied to e.g. `α`

or `α × β`

, but not when applied to
e.g. `ℕ`

or `ℝ × α`

.
We ignore all arguments specified by the `ignore`

`NameMap`

.

## Equations

- ToAdditive.additiveTest findTranslation? ignore e = ToAdditive.additiveTest.unsafe_impl_1 findTranslation? ignore e

## Instances For

Change the numeral `nat_lit 1`

to the numeral `nat_lit 0`

.
Leave all other expressions unchanged.

## Equations

## Instances For

`applyReplacementFun e`

replaces the expression `e`

with its additive counterpart.
It translates each identifier (inductive type, defined function etc) in an expression, unless

- The identifier occurs in an application with first argument
`arg`

; and `test arg`

is false. However, if`f`

is in the dictionary`relevant`

, then the argument`relevant.find f`

is tested, instead of the first argument.

It will also reorder arguments of certain functions, using `reorderFn`

:
e.g. `g x₁ x₂ x₃ ... xₙ`

becomes `g x₂ x₁ x₃ ... xₙ`

if `reorderFn g = some [1]`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Implementation of `applyReplacementFun`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Eta expands `e`

at most `n`

times.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Reorder pi-binders. See doc of `reorderAttr`

for the interpretation of the argument

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Reorder lambda-binders. See doc of `reorderAttr`

for the interpretation of the argument

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Run applyReplacementFun on the given `srcDecl`

to make a new declaration with name `tgt`

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Find the target name of `pre`

and all created auxiliary declarations.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Returns a `NameSet`

of all auxiliary constants in `e`

that might have been generated
when adding `pre`

to the environment.
Examples include `pre.match_5`

and
`_private.Mathlib.MyFile.someOtherNamespace.someOtherDeclaration._eq_2`

.
The last two examples may or may not have been generated by this declaration.
The last example may or may not be the equation lemma of a declaration with the `@[to_additive]`

attribute. We will only translate it has the `@[to_additive]`

attribute.

## Equations

- ToAdditive.findAuxDecls e pre = e.foldConsts ∅ fun (n : Lean.Name) (l : Lean.NameSet) => if (n.getPrefix == pre || Lean.isPrivateName n || n.hasMacroScopes) = true then l.insert n else l

## Instances For

It's just the same as `Lean.Meta.setInlineAttribute`

but with type `CoreM Unit`

.

TODO (lean4#4965): make `Lean.Meta.setInlineAttribute`

a `CoreM Unit`

and remove this definition.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

transform the declaration `src`

and all declarations `pre._proof_i`

occurring in `src`

using the transforms dictionary.
`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.

Copy the instance attribute in a `to_additive`

[todo] it seems not to work when the `to_additive`

is added as an attribute later.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Warn the user when the multiplicative declaration has an attribute.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Warn the user when the multiplicative declaration has a simple scoped attribute.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Warn the user when the multiplicative declaration has a parametric attribute.

## Equations

- ToAdditive.warnParametricAttr stx attr thisAttr attrName src tgt = ToAdditive.warnExt stx attr.ext (fun (x1 : Lean.NameMap β) (x2 : Lean.Name) => x1.contains x2) thisAttr attrName src tgt

## Instances For

`additivizeLemmas names desc t`

runs `t`

on all elements of `names`

and adds translations between the generated lemmas (the output of `t`

).
`names`

must be non-empty.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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.One`

returns 2.
Note: we only consider the first argument of each type-class.
E.g. `[Pow A N]`

is a multiplicative type-class on `A`

, not on `N`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Helper for `capitalizeLike`

.

Capitalizes `s`

char-by-char like `r`

. If `s`

is longer, it leaves the tail untouched.

## Equations

## Instances For

Capitalize First element of a list like `s`

.
Note that we need to capitalize multiple characters in some cases,
in examples like `HMul`

or `hAdd`

.

## Equations

- ToAdditive.capitalizeFirstLike s (x_1 :: r) = ToAdditive.capitalizeLike s x_1 :: r
- ToAdditive.capitalizeFirstLike s [] = []

## Instances For

Turn each element to lower-case, apply the `nameDict`

and
capitalize the output like the input.

## Equations

- ToAdditive.applyNameDict (x_1 :: r) = ToAdditive.capitalizeFirstLike x_1 (ToAdditive.nameDict x_1.toLower) ++ ToAdditive.applyNameDict r
- ToAdditive.applyNameDict [] = []

## Instances For

There are a few abbreviations we use. For example "Nonneg" instead of "ZeroLE"
or "addComm" instead of "commAdd".
Note: The input to this function is case sensitive!
Todo: A lot of abbreviations here are manual fixes and there might be room to
improve the naming logic to reduce the size of `fixAbbreviation`

.

## Instances For

Autogenerate additive name. This runs in several steps:

- Split according to capitalisation rule and at
`_`

. - Apply word-by-word translation rules.
- Fix up abbreviations that are not word-by-word translations, like "addComm" or "Nonneg".

## Equations

- ToAdditive.guessName = String.mapTokens ''' fun (s : String) => String.join (ToAdditive.fixAbbreviation (ToAdditive.applyNameDict s.splitCase))

## Instances For

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

## Equations

- One or more equations did not get rendered due to their size.
- ToAdditive.targetName cfg src = Lean.throwError (Lean.toMessageData "to_additive: can't transport " ++ Lean.toMessageData src ++ Lean.toMessageData "")

## Instances For

if `f src = #[a_1, ..., a_n]`

and `f tgt = #[b_1, ... b_n]`

then `proceedFieldsAux src tgt f`

will insert translations from `src.a_i`

to `tgt.b_i`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Add the structure fields of `src`

to the translations dictionary
so that future uses of `to_additive`

will map them to the corresponding `tgt`

fields.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Elaboration of the configuration options for `to_additive`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Apply attributes to the multiplicative and additive declarations.

Copies equation lemmas and attributes from `src`

to `tgt`

Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and
the body using the `translations`

dictionary.
This is used to implement `@[to_additive]`

.

`addToAdditiveAttr src cfg`

adds a `@[to_additive]`

attribute to `src`

with configuration `cfg`

.
See the attribute implementation for more details.
It returns an array with names of additive declarations (usually 1, but more if there are nested
`to_additive`

calls.