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 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.
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:
add_comm_prefix x s
returns "comm_" ++ s
if x = tt
and s
otherwise.
Dictionary used by to_additive.guess_name
to autogenerate names.
the parser for the arguments to to_additive
.
Add the aux_attr
attribute to the structure fields of src
so that future uses of to_additive
will map them to the corresponding tgt
fields.
The attribute to_additive
can be used to automatically transport theorems
and definitions (but not inductive types and structures) from a multiplicative
theory to an additive theory.
To use this attribute, just write:
@[to_additive]
theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm
This code will generate a theorem named add_comm'
. It is also
possible to manually specify the name of the new declaration, and
provide a documentation string:
@[to_additive add_foo "add_foo doc string"]
/ foo doc string /
theorem foo := sorry
The transport tries to do the right thing in most cases using several heuristics described below. However, in some cases it fails, and requires manual intervention.
If the declaration to be transported has attributes which need to be
copied to the additive version, then to_additive
should come last:
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⟩⟩
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'
,comm_semigroup
toadd_comm_semigroup
,x * y
tox + y
andy * x
toy + x
, andcomm_semigroup.mul_comm'
toadd_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 identifierprod
, 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 two exceptions in 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 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,times_cont_mdiff_map
has attribute@[to_additive_ignore_args 21]
, which means that its 21st argument(n : with_top ℕ)
can containℕ
(usually in the formhas_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. Solutions: 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. This is not possible ifd
is something likepi.has_one
orprod.group
, where the second argument (also) has a multiplicative structure.  Sometimes only the proof of a lemma/theorem uses these problematic declarations. In some cases you can rewrite the proof a little bit to work around these declarations.
 Make sure the first argument of
 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 declarationd
, and thek
th argument is not connected to the multiplicative structure ond
, consider adding attribute[to_additive_ignore_args k]
tod
.  If you want to disable the heuristic and replace all multiplicative
identifiers with their additive counterpart, use
@[to_additive!]
.
 If the fixed type has an additive counterpart (like
 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 matchesadd_monoid.nsmul n x
.  If this is not possible, add the
[to_additive_reorder k]
to the multiplicative declaration to indicate that thek
th and(k+1)
st arguments are reordered in the additive version.
 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
.
After transporting the “main” declaration, to_additive
transports
its equational lemmas.
Structure fields and constructors #
If src
is a structure, then to_additive
automatically adds
structure fields to its mapping, and similarly for constructors of
inductive types.
For new structures this means that to_additive
automatically handles
coercions, and for old structures it does the same, if ancestry
information is present in @[ancestor]
attributes. 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 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. 
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 thequotient_group
namespace will be created in thequotient_add_group
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
argumentnew_namespace.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.