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 simp
and 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 stringbased 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'
toadd_comm'
,CommSemigroup
toAddCommSemigroup
,x * y
tox + y
andy * x
toy + x
, andCommSemigroup.mul_comm'
toAddCommSemigroup.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 isNat
, an identifier not applied to any arguments.@Mul.mul (α × β) x y
will change to+
. It's first argument contains only the identifierProd
, but this is applied to arguments,α
andβ
.@Mul.mul (α × Int) x y
will not change to+
, since its first argument containsInt
.
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 positionn
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 typeclass, but argumentn
does.  If an identifier has attribute
@[to_additive_ignore_args n1 n2 ...]
then all the arguments in positionsn1
,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 formTop.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 typeFoo
.  If the fixed type occurs inside the
k
th argument of a declarationd
, and thek
th argument is not connected to the multiplicative structure ond
, consider adding attribute[to_additive_ignore_args k]
tod
. 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 ofd
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 typeclass,@[to_additive]
should have automatically added the attribute@[to_additive_relevant_arg]
to the declaration. You can test this by running the following (whered
is the full name of the declaration):
The expected output isopen Lean in run_cmd logInfo m!"{ToAdditive.relevantArgAttr.find? (← getEnv) `d}"
n
where then
th (0indexed) argument ofd
is a type (family) with a multiplicative structure on it.none
means0
. If you get a different output (or a failure), you could add the attribute@[to_additive_relevant_arg n]
manually, wheren
is an (1indexed) 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 tox ^ n
, but it is convenient thatMonoid.npow
has this argument order, since it matchesAddMonoid.nsmul n x
.  If this is not possible, add
(reorder := ...)
argument toto_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 aname
argument, then the new name is autogenerated. First, it takes the longest prefix of the source name that is already known toto_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 theQuotientGroup
namespace will be created in theQuotientAddGroup
namespaces. 
If
@[to_additive]
is called with aname
argumentnew_name
/without a dot/, thento_additive
updates the prefix as described above, then replaces the last part of the name withnew_name
. 
If
@[to_additive]
is called with aname
argumentNewNamespace.new_name
/with a dot/, thento_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 lowercase letter followed by an uppercase letter.
 If multiple strings have the same prefix, they should be grouped by prefix
 In this case, the second list should be prefixfree (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
 One or more equations did not get rendered due to their size.
Instances For
This function takes a String and splits it into separate parts based on the following (naming conventions)[https://github.com/leanprovercommunity/mathlib4/wiki#namingconvention].
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 allornothing 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 welltested.
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
isfalse
(default) then@[to_additive]
will check whether the given name can be autogenerated. 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 certain attributes (such as
simp
andsimps
) this will also add generated lemmas to the translation dictionary.  ref : Lean.Syntax
The
Syntax
element corresponding to the original multiplicative declaration (or theto_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 the same method that Expr.find?
uses,
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.
Equations
 ToAdditive.additiveTestUnsafe findTranslation? ignore e = Id.run (StateT.run' (ToAdditive.additiveTestUnsafe.visit findTranslation? ignore e) Lean.mkPtrSet)
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
 ToAdditive.changeNumeral x = match x with  Lean.Expr.lit (Lean.Literal.natVal 1) => Lean.mkRawNatLit 0  e => e
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, iff
is in the dictionaryrelevant
, then the argumentrelevant.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 pibinders. 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 lambdabinders. 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
, 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.
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
 One or more equations did not get rendered due to their size.
Instances For
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 nonempty.
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 typeclass 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 typeclass.
E.g. [Pow A N]
is a multiplicative typeclass 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
charbychar 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 = match x with  x :: r => ToAdditive.capitalizeLike s x :: r  [] => []
Instances For
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 lowercase,
2nd element should be capitalized properly.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Turn each element to lowercase, 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 [] = []
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 wordbyword translation rules.
 Fix up abbreviations that are not wordbyword translations, like "addComm" or "Nonneg".
Equations
 ToAdditive.guessName = String.mapTokens ''' fun (s : String) => String.join (ToAdditive.fixAbbreviation (ToAdditive.applyNameDict (String.splitCase s 0)))
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.
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.