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

The `to_additive_ignore_args`

attribute.

## Equations

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

The `to_additive_relevant_arg`

attribute.

## Equations

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

The `to_additive_reorder`

attribute.

## Equations

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

The `to_additive_change_numeral`

attribute.

## Equations

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

An `attr := ...`

option for `to_additive`

.

## Equations

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

An `reorder := ...`

option for `to_additive`

.

## Equations

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

Options to `to_additive`

.

## Equations

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

Options to `to_additive`

.

## Equations

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

Remaining arguments of `to_additive`

.

## Equations

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

The `to_additive`

attribute.

## Equations

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

The `to_additive`

attribute.

## Equations

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

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 a 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"])]

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 reorder 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]`

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

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

View the trace of the to_additive procedure. Equivalent to

`set_option trace.to_additive true`

.trace : BoolThe name of the target (the additive declaration).

tgt : Lean.NameAn optional doc string.

If

`allowAutoName`

is`false`

(default) then`@[to_additive]`

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

`to_additive`

The attributes which we want to give to both the multiplicative and additive versions. For certain attributes (such as

`simp`

and`simps`

) this will also add generated lemmas to the translation dictionary.attrs : Array Lean.SyntaxThe

`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.ref : Lean.SyntaxAn 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.

`Config`

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

.

## Instances For

## Equations

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

Auxilliary function for `additiveTest`

. The bool argument *only* matters when applied
to exactly a constant.

## Equations

- ToAdditive.additiveTestAux findTranslation? ignore = ToAdditive.additiveTestAux.visit findTranslation? ignore

see `additiveTestAux`

## Equations

- One or more equations did not get rendered due to their size.
- ToAdditive.additiveTestAux.visit findTranslation? ignore x (Lean.Expr.const n us) = (x || Option.isSome (findTranslation? n))
- ToAdditive.additiveTestAux.visit findTranslation? ignore x (Lean.Expr.lam binderName binderType t binderInfo) = ToAdditive.additiveTestAux.visit findTranslation? ignore false t
- ToAdditive.additiveTestAux.visit findTranslation? ignore x (Lean.Expr.forallE binderName binderType t binderInfo) = ToAdditive.additiveTestAux.visit findTranslation? ignore false t
- ToAdditive.additiveTestAux.visit findTranslation? ignore x x = true

`additiveTest e`

tests whether the expression `e`

contains no 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.additiveTestAux findTranslation? ignore false e

Change the numeral `nat_lit 1`

to the numeral `nat_lit 0`

.
Leave all other expressions unchanged.

## Equations

- ToAdditive.changeNumeral x = match x with | Lean.Expr.lit (Lean.Literal.natVal 1) => Lean.mkRawNatLit 0 | e => e

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

Implementation of `applyReplacementFun`

.

## Equations

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

Eta expands `e`

at most `n`

times.

## Equations

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

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.

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.

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.

Find the target name of `pre`

and all created auxiliary declarations.

## Equations

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

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`

, `Mathlib.MyFile._auxLemma.3`

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

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

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.

Warn the user when the multiplicative declaration has an attribute.

## Equations

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

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

## Equations

- ToAdditive.warnAttr stx attr f thisAttr attrName src tgt = ToAdditive.warnExt stx attr.ext (fun x x_1 => f (List.head! x.stateStack).state x_1) thisAttr attrName src tgt

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 x x_1 => Lean.NameMap.contains x x_1) thisAttr attrName src tgt

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

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.

Helper for `capitalizeLike`

.

Capitalizes `s`

char-by-char like `r`

. If `s`

is longer, it leaves the tail untouched.

## Equations

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 = match x with | x :: r => ToAdditive.capitalizeLike s x :: r | [] => []

Dictionary used by `guessName`

to autogenerate names.

Note: `guessName`

capitalizes first element of the output according to
capitalization of the input. Input and first element should therefore be lower-case,
2nd element should be capitalized properly.

## Equations

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

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 (String.toLower x_1)) ++ ToAdditive.applyNameDict r
- ToAdditive.applyNameDict [] = []

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`

.

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 (Char.ofNat 39) fun s => String.join (ToAdditive.fixAbbreviation (ToAdditive.applyNameDict (String.splitCase s 0)))

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.

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.

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.

Elaboration of the configuration options for `to_additive`

.

## Equations

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

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.