Documentation

Mathlib.Tactic.ToAdditive.Frontend

The `@[to_additive]` attribute. #

Implementation of the to_additive attribute. See the docstring of ToAdditive.to_additive for more information

def ToAdditive.to_additive_ignore_args :

Lean.ParserDescr

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.

Equations

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

Instances For

def ToAdditive.to_additive_relevant_arg :

Lean.ParserDescr

This attribute is deprecated. Use to_additive (relevant_arg := ...) instead.

Equations

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

Instances For

def ToAdditive.to_additive_change_numeral :

Lean.ParserDescr

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

Equations

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

Instances For

def ToAdditive.to_additive_dont_translate :

Lean.ParserDescr

The to_additive_dont_translate attribute, used to specify types that should be translated by to_additive, but its operations should remain multiplicative.

Usage notes:

Apply this together with the to_additive attribute.
The name generation of to_additive is not aware that the operations on this type should not be translated, so you generally have to specify the name itself, if the name should remain multiplicative.

Equations

ToAdditive.to_additive_dont_translate = Lean.ParserDescr.node `ToAdditive.to_additive_dont_translate 1024 (Lean.ParserDescr.nonReservedSymbol "to_additive_dont_translate" false)

Instances For

def ToAdditive.toAdditiveAttrOption :

Lean.ParserDescr

An attr := ... option for to_additive.

Equations

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

Instances For

def ToAdditive.toAdditiveReorderOption :

Lean.ParserDescr

reorder := ... reorders the arguments/hypotheses in the generated declaration. It uses 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 used in to_dual to swap the arguments in ≤, < and ⟶. It is also used in to_additive to translate from ^ to •.

Equations

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

Instances For

def ToAdditive.toAdditiveRelevantOption :

Lean.ParserDescr

the relevant_arg := ... option tells which argument is a type where this declaration uses the multiplicative structure. This is inferred automatically using the function findMultiplicativeArg, but it can also be overwritten using this syntax.

If there are multiple arguments with a multiplicative structure, we typically tag the first one. If this argument contains a fixed type, this declaration will not be additivized. See the Heuristics section of the to_additive doc-string for more details.

If a declaration is not tagged, it is presumed that the first argument is relevant.

To indicate that there is no relevant argument, set it to a number that is out of bounds, i.e. larger than the number of arguments, e.g. (relevant_arg := 100).

Implementation note: we only allow exactly 1 relevant argument, even though some declarations (like Prod.instGroup) 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 we will not be able to additivize declarations that (e.g.) talk about multiplication on ℕ × α anyway.

Equations

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

Instances For

def ToAdditive.toAdditiveDontTranslateOption :

Lean.ParserDescr

dont_translate := ... takes a list of type variables (separated by spaces) that should not be considered for translation. For example in

lemma foo {α β : Type} [Group α] [Group β] (a : α) (b : β) : a * a⁻¹ = 1 ↔ b * b⁻¹ = 1

we can choose to only additivize α by writing to_additive (dont_translate := β).

Equations

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

Instances For

def ToAdditive.toAdditiveOption :

Lean.ParserDescr

Options to to_additive.

Equations

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

Instances For

def ToAdditive.toAdditiveNameHint :

Lean.ParserDescr

An existing or self name hint for to_additive.

Equations

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

Instances For

def ToAdditive.toAdditiveRest :

Lean.ParserDescr

Remaining arguments of to_additive.

Equations

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

Instances For

def ToAdditive.to_additive :

Lean.ParserDescr

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 to_additive existing syntax to use an existing additive declaration, instead of automatically generating it.

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. The dictionary is ToAdditive.nameDict and can be found in the Tactic.ToAdditive.GuessName file. If you introduce a new name which should be translated by to_additive you should add the translation to this dictionary.

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. You can turn this behavior off by also adding the @[to_additive_dont_translate] attribute.
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 (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 self] 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 ℕ)
- If none of the arguments have a multiplicative structure, then the heuristic should not apply at all. This can be achieved by setting relevant_arg out of bounds, e.g. (relevant_arg := 100).
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 (relevant_arg := ...) to the declaration. You can test this by running the following (where d is the full name of the declaration):
```
  open Lean in run_cmd logInfo m!"{ToAdditive.relevantArgAttr.find? (← getEnv) `d}"
```
  The expected output is 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.
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.

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

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.
You can add a namespace translation using the following command:
```
run_meta ToAdditive.insertTranslation `QuotientGroup `QuotientAddGroup
```
Later uses of @[to_additive] on declarations in the QuotientGroup namespace will be created in the QuotientAddGroup namespace. This is not necessary if there is already a declaration with name QuotientGroup.
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.

Equations

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

Instances For

def ToAdditive.attrTo_additive?_ :

Lean.ParserDescr

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 to_additive existing syntax to use an existing additive declaration, instead of automatically generating it.

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. The dictionary is ToAdditive.nameDict and can be found in the Tactic.ToAdditive.GuessName file. If you introduce a new name which should be translated by to_additive you should add the translation to this dictionary.

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. You can turn this behavior off by also adding the @[to_additive_dont_translate] attribute.
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 (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 self] 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 ℕ)
- If none of the arguments have a multiplicative structure, then the heuristic should not apply at all. This can be achieved by setting relevant_arg out of bounds, e.g. (relevant_arg := 100).
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 (relevant_arg := ...) to the declaration. You can test this by running the following (where d is the full name of the declaration):
```
  open Lean in run_cmd logInfo m!"{ToAdditive.relevantArgAttr.find? (← getEnv) `d}"
```
  The expected output is 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.
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.

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

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.
You can add a namespace translation using the following command:
```
run_meta ToAdditive.insertTranslation `QuotientGroup `QuotientAddGroup
```
Later uses of @[to_additive] on declarations in the QuotientGroup namespace will be created in the QuotientAddGroup namespace. This is not necessary if there is already a declaration with name QuotientGroup.
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.

Equations

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

Instances For

opaque ToAdditive.linter.existingAttributeWarning :

Lean.Option Bool

Linter, mostly used by @[to_additive], that checks that the source declaration doesn't have certain attributes

opaque ToAdditive.linter.toAdditiveGenerateName :

Lean.Option Bool

Linter to check that the to_additive attribute is not given manually

opaque ToAdditive.linter.toAdditiveExisting :

Lean.Option Bool

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

opaque ToAdditive.linter.toAdditiveRelevantArg :

Lean.Option Bool

Linter to check that the relevant_arg attribute is not given manually

opaque ToAdditive.ignoreArgsAttr :

Lean.NameMapExtension (List ℕ)

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.

opaque ToAdditive.reorderAttr :

Lean.NameMapExtension (List (List ℕ))

An extension that stores all the declarations that need their arguments reordered when applying @[to_additive]. It is applied using the to_additive (reorder := ...) syntax.

opaque ToAdditive.relevantArgAttr :

Lean.NameMapExtension ℕ

This attribute is deprecated. Use to_additive (relevant_arg := ...) instead.

opaque ToAdditive.dontTranslateAttr :

Lean.NameMapExtension Unit

The to_additive_dont_translate attribute, used to specify types that should be translated by to_additive, but its operations should remain multiplicative.

Usage notes:

Apply this together with the to_additive attribute.
The name generation of to_additive is not aware that the operations on this type should not be translated, so you generally have to specify the name itself, if the name should remain multiplicative.

opaque ToAdditive.changeNumeralAttr :

Lean.NameMapExtension (List ℕ)

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

opaque ToAdditive.translations :

Lean.NameMapExtension Lean.Name

Maps multiplicative names to their additive counterparts.

def ToAdditive.findTranslation? (env : Lean.Environment) :

Lean.Name → Option Lean.Name

Get the multiplicative → additive translation for the given name.

Equations

ToAdditive.findTranslation? env = (Lean.SimplePersistentEnvExtension.getState ToAdditive.translations env).find?

Instances For

def ToAdditive.findPrefixTranslation (env : Lean.Environment) (nm : Lean.Name) :

Get the multiplicative → additive translation for the given name, falling back to translating a prefix of the name if the full name can't be translated. This allows translating automatically generated declarations such as IsRegular.casesOn.

Equations

ToAdditive.findPrefixTranslation env nm = Lean.Name.mapPrefix (ToAdditive.findTranslation? env) nm

Instances For

def ToAdditive.insertTranslation (src tgt : Lean.Name) (failIfExists : Bool := true) :

Lean.CoreM Unit

Add a (multiplicative → additive) name translation to the translations map.

Equations

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

Instances For

structure ToAdditive.ArgInfo :

ArgInfo stores information about how a constant should be translated.

reorder : List (List ℕ)
The arguments that should be reordered by to_additive, using cycle notation.
relevantArg : ℕ
The argument used to determine whether this constant should be translated.

Instances For

def ToAdditive.insertTranslationAndInfo (src tgt : Lean.Name) (argInfo : ArgInfo) (failIfExists : Bool := true) :

Lean.CoreM Unit

Add a name translation to the translations map and add the argInfo information to src.

Equations

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

Instances For

structure ToAdditive.Config :

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).
doc : Option String
An optional doc string.
allowAutoName : Bool
If allowAutoName is false (default) then @[to_additive] will check whether the given name can be auto-generated.
reorder : List (List ℕ)
The arguments that should be reordered by to_additive, using cycle notation.
relevantArg? : Option ℕ
The argument used to determine whether this constant should be translated.
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.
dontTranslate : List Lean.Ident
A list of type variables that should not be translated by to_additive.
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.
existing : Bool
An optional flag stating that the additive declaration already exists. If this flag is 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.
self : Bool
An optional flag stating that the target of the translation is the target itself. This can be used to reorder arguments, such as in attribute [to_dual self (reorder := 3 4)] LE.le. It can also be used to give a hint to additiveTest, such as in attribute [to_additive self] Unit. If self := true, we should also have existing := true.

Instances For

instance ToAdditive.instReprConfig :

Equations

ToAdditive.instReprConfig = { reprPrec := ToAdditive.instReprConfig.repr }

def ToAdditive.instReprConfig.repr :

Config → ℕ → Std.Format

Equations

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

Instances For

def ToAdditive.etaExpandN (n : ℕ) (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Eta expands e at most n times.

Equations

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

Instances For

def ToAdditive.expand (e : Lean.Expr) :

Lean.MetaM Lean.Expr

e.expand eta-expands all expressions that have as head a constant n in reorder. They are expanded until they are applied to one more argument than the maximum in reorder.find n. It also expands all kernel projections that have as head a constant n in reorder.

Equations

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

Instances For

unsafe def ToAdditive.additiveTestUnsafe (env : Lean.Environment) (e : Lean.Expr) (dontTranslate : Array Lean.FVarId) :

Option (Lean.Name ⊕ Lean.FVarId)

Implementation function for additiveTest. Failure means that in that subexpression there is no constant that blocks e from being translated. 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 ifs 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 env e dontTranslate = (StateT.run' (ToAdditive.additiveTestUnsafe.visit env dontTranslate e) Lean.mkPtrSet).run

Instances For

unsafe def ToAdditive.additiveTestUnsafe.visit (env : Lean.Environment) (dontTranslate : Array Lean.FVarId) (e : Lean.Expr) (inApp : Bool := false) :

OptionT (StateM (Lean.PtrSet Lean.Expr)) (Lean.Name ⊕ Lean.FVarId)

Equations

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

Instances For

def ToAdditive.additiveTest (env : Lean.Environment) (e : Lean.Expr) (dontTranslate : Array Lean.FVarId := #[]) :

Option (Lean.Name ⊕ Lean.FVarId)

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 relevant 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 env e dontTranslate = ToAdditive.additiveTest.unsafe_impl_3 env e dontTranslate

Instances For

def List.swapFirstTwo {α : Type u_1} :

List α → List α

Swap the first two elements of a list

Equations

[].swapFirstTwo = []
[x_1].swapFirstTwo = [x_1]
(x_1 :: y :: l).swapFirstTwo = y :: x_1 :: l

Instances For

def ToAdditive.changeNumeral :

Lean.Expr → Lean.Expr

Change the numeral nat_lit 1 to the numeral nat_lit 0. Leave all other expressions unchanged.

Equations

ToAdditive.changeNumeral (Lean.Expr.lit (Lean.Literal.natVal 1)) = Lean.mkRawNatLit 0
ToAdditive.changeNumeral x✝ = x✝

Instances For

def ToAdditive.applyReplacementFun (e : Lean.Expr) (dontTranslate : Array Lean.FVarId := #[]) :

Lean.MetaM Lean.Expr

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

def ToAdditive.applyReplacementFun.aux (dontTranslate : Array Lean.FVarId) (env : Lean.Environment) (trace : Bool) :

Lean.Expr → Lean.Expr

Implementation of applyReplacementFun.

Equations

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

Instances For

def ToAdditive.renameBinderNames (src : Lean.Expr) :

Rename binder names in pi type.

Equations

ToAdditive.renameBinderNames src = src.mapForallBinderNames fun (x : Lean.Name) => match x with | p.str s => p.str (ToAdditive.guessName s) | n => n

Instances For

def ToAdditive.reorderForall (reorder : List (List ℕ)) (src : Lean.Expr) :

Lean.MetaM Lean.Expr

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

def ToAdditive.reorderLambda (reorder : List (List ℕ)) (src : Lean.Expr) :

Lean.MetaM Lean.Expr

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

def ToAdditive.applyReplacementForall (dontTranslate : List ℕ) (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Run applyReplacementFun on an expression ∀ x₁ .. xₙ, e, making sure not to translate type-classes on xᵢ if i is in dontTranslate.

Equations

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

Instances For

def ToAdditive.applyReplacementLambda (dontTranslate : List ℕ) (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Run applyReplacementFun on an expression fun x₁ .. xₙ ↦ e, making sure not to translate type-classes on xᵢ if i is in dontTranslate.

Equations

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

Instances For

def ToAdditive.declUnfoldAuxLemmas (decl : Lean.ConstantInfo) :

Lean.MetaM Lean.ConstantInfo

Unfold auxlemmas in the type and value.

Equations

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

Instances For

def ToAdditive.getDontTranslates (given : List Lean.Ident) (type : Lean.Expr) :

Lean.MetaM (List ℕ)

Given a list of variable local identifiers that shouldn't be translated, determine the arguments that shouldn't be translated.

TODO: Currently, this function doesn't deduce any dont_translate types from type. In the future we would like that the presence of MonoidAlgebra k G will automatically flag k as a type to not be translated.

Equations

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

Instances For

def ToAdditive.updateDecl (tgt : Lean.Name) (srcDecl : Lean.ConstantInfo) (reorder : List (List ℕ)) (dont : List Lean.Ident) :

Lean.MetaM Lean.ConstantInfo

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

def ToAdditive.declAbstractNestedProofs (decl : Lean.ConstantInfo) :

Lean.MetaM Lean.ConstantInfo

Abstracts the nested proofs in the value of decl if it is a def.

Equations

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

Instances For

def ToAdditive.findTargetName (env : Lean.Environment) (src pre tgt_pre : Lean.Name) :

Lean.CoreM Lean.Name

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

def ToAdditive.findAuxDecls (e : Lean.Expr) (pre : Lean.Name) :

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 if it has the @[to_additive] attribute.

Note that this function would return proof_nnn aux lemmas if we hadn't unfolded them in declUnfoldAuxLemmas.

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

partial def ToAdditive.transformDeclAux (cfg : Config) (pre tgt_pre : Lean.Name) :

Lean.Name → Lean.CoreM Unit

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.

def ToAdditive.copyInstanceAttribute (src tgt : Lean.Name) :

Lean.CoreM Unit

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

def ToAdditive.warnAttrCore (stx : Lean.Syntax) (f : Lean.Environment → Lean.Name → Bool) (thisAttr attrName src tgt : Lean.Name) :

Lean.CoreM Unit

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

def ToAdditive.warnAttr {α β : Type} [Inhabited β] (stx : Lean.Syntax) (attr : Lean.SimpleScopedEnvExtension α β) (f : β → Lean.Name → Bool) (thisAttr attrName src tgt : Lean.Name) :

Lean.CoreM Unit

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

Equations

ToAdditive.warnAttr stx attr f thisAttr attrName src tgt = ToAdditive.warnAttrCore stx (fun (x : Lean.Environment) => f (Lean.ScopedEnvExtension.getState attr x)) thisAttr attrName src tgt

Instances For

def ToAdditive.warnParametricAttr {β : Type} [Inhabited β] (stx : Lean.Syntax) (attr : Lean.ParametricAttribute β) (thisAttr attrName src tgt : Lean.Name) :

Lean.CoreM Unit

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

def ToAdditive.additivizeLemmas {m : Type → Type} [Monad m] [Lean.MonadError m] [MonadLiftT Lean.CoreM m] (names : Array Lean.Name) (argInfo : ArgInfo) (desc : String) (t : Lean.Name → m (Array Lean.Name)) :

additivizeLemmas names argInfo 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

def ToAdditive.findMultiplicativeArg (nm : Lean.Name) :

Find the argument of nm that appears in the first multiplicative (type-class) argument. Returns 1 if there are no types with a multiplicative class as arguments. E.g. Prod.instGroup returns 1, and Pi.instOne returns 2. Note: we only consider the relevant argument ((relevant_arg := ...)) 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

def ToAdditive.targetName (cfg : Config) (src : Lean.Name) :

Lean.CoreM Lean.Name

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

def ToAdditive.proceedFieldsAux (src tgt : Lean.Name) (argInfo : ArgInfo) (f : Lean.Name → Array Lean.Name) :

Lean.CoreM Unit

if f src = #[a_1, ..., a_n] and f tgt = #[b_1, ... b_n] then proceedFieldsAux src tgt f will insert translations from a_i to b_i.

Equations

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

Instances For

def ToAdditive.proceedFields (src tgt : Lean.Name) (argInfo : ArgInfo) :

Lean.CoreM Unit

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

def ToAdditive.elabToAdditive :

Lean.Syntax → Lean.CoreM Config

Elaboration of the configuration options for to_additive.

Equations

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

Instances For

partial def ToAdditive.applyAttributes (stx : Lean.Syntax) (rawAttrs : Array Lean.Syntax) (thisAttr src tgt : Lean.Name) (argInfo : ArgInfo) :

Lean.Elab.TermElabM (Array Lean.Name)

Apply attributes to the multiplicative and additive declarations.

partial def ToAdditive.copyMetaData (cfg : Config) (src tgt : Lean.Name) (argInfo : ArgInfo) :

Lean.CoreM (Array Lean.Name)

Copies equation lemmas and attributes from src to tgt

partial def ToAdditive.transformDecl (cfg : Config) (src tgt : Lean.Name) (argInfo : ArgInfo := { }) :

Lean.CoreM (Array Lean.Name)

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

def ToAdditive.checkExistingType (src tgt : Lean.Name) (reorder : List (List ℕ)) (dont : List Lean.Ident) :

Lean.MetaM Unit

Verify that the type of given srcDecl translates to that of tgtDecl.

Equations

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

Instances For

partial def ToAdditive.addToAdditiveAttr (src : Lean.Name) (cfg : Config) (kind : Lean.AttributeKind := Lean.AttributeKind.global) :

Lean.AttrM (Array Lean.Name)

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.