Documentation

Mathlib.Tactic.ToAdditive.ToAdditive

The @[to_additive] attribute. #

The @[to_additive] attribute is used to translate multiplicative declarations to their additive equivalent. See the docstrings of to_additive for more information.

source
def Mathlib.Tactic.ToAdditive.to_additive_ignore_args :
Lean.ParserDescr

An attribute that tells that certain arguments of this definition are not involved when translating. This helps the translation heuristic 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
    source
    def Mathlib.Tactic.ToAdditive.to_additive_relevant_arg :
    Lean.ParserDescr

    the (relevant_arg := ...) option tells which argument to look at to determine whether to translate this constant. This is inferred automatically using the function findRelevantArg, but it can also be overwritten using this syntax.

    If there are multiple possible arguments, we typically tag the first one. If this argument contains a fixed type, this declaration will not be translated. 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 relevant argument. The reason is that whether we translate a declaration is an all-or-nothing decision, and we will not be able to translate declarations that (e.g.) talk about multiplication on ℕ × α anyway.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Mathlib.Tactic.ToAdditive.to_additive_dont_translate :
      Lean.ParserDescr

      The global dont_translate attribute specifies that operations on the given type should not be translated. This can be either for types that are translated, such as MonoidAlgebra -> AddMonoidAlgebra, or for fixed types, such as Fin n/ZMod n.

      Note: The name generation is not aware that the operations on this type should not be translated, so you generally have to specify a name manually, if some part should not be translated.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Mathlib.Tactic.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:

          insert_to_additive_translation 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
          source
          def Mathlib.Tactic.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:

            insert_to_additive_translation 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
            source
            opaque Mathlib.Tactic.ToAdditive.ignoreArgsAttr :
            Lean.NameMapExtension (List ℕ)

            An attribute that tells that certain arguments of this definition are not involved when translating. This helps the translation heuristic by also transforming definitions if ℕ or another fixed type occurs as one of these arguments.

            source
            opaque Mathlib.Tactic.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.

            source
            opaque Mathlib.Tactic.ToAdditive.linter.toAdditiveRelevantArg :
            Lean.Option Bool

            Linter to check that the relevant_arg attribute is not given manually

            source
            opaque Mathlib.Tactic.ToAdditive.relevantArgAttr :
            Lean.NameMapExtension ℕ

            the (relevant_arg := ...) option tells which argument to look at to determine whether to translate this constant. This is inferred automatically using the function findRelevantArg, but it can also be overwritten using this syntax.

            If there are multiple possible arguments, we typically tag the first one. If this argument contains a fixed type, this declaration will not be translated. 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 relevant argument. The reason is that whether we translate a declaration is an all-or-nothing decision, and we will not be able to translate declarations that (e.g.) talk about multiplication on ℕ × α anyway.

            source
            opaque Mathlib.Tactic.ToAdditive.dontTranslateAttr :
            Lean.NameMapExtension Unit

            The global dont_translate attribute specifies that operations on the given type should not be translated. This can be either for types that are translated, such as MonoidAlgebra -> AddMonoidAlgebra, or for fixed types, such as Fin n/ZMod n.

            Note: The name generation is not aware that the operations on this type should not be translated, so you generally have to specify a name manually, if some part should not be translated.

            source
            opaque Mathlib.Tactic.ToAdditive.translations :
            Lean.NameMapExtension Lean.Name

            Maps multiplicative names to their additive counterparts.

            source
            def Mathlib.Tactic.ToAdditive.nameDict :
            Std.HashMap String (List String)

            Dictionary used by guessName to autogenerate names. This only transforms single name components, unlike abbreviationDict.

            Note: guessName capitalizes the output according to the capitalization of the input. In order for this to work, the input should always start with a lower case letter, and the output should always start with an upper case letter.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Mathlib.Tactic.ToAdditive.abbreviationDict :
              Std.HashMap String String

              We need to fix a few abbreviations after applying nameDict, i.e. replacing ZeroLE by Nonneg. This dictionary contains these fixes. The input should contain entries that is in lowerCamelCase (e.g. ltzero; the initial sequence of capital letters should be lower-cased) and the output should be in UpperCamelCase (e.g. LTZero). When applying the dictionary, we lower-case the output if the input was also given in lower-case.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Mathlib.Tactic.ToAdditive.data :
                Translate.TranslateData

                The bundle of environment extensions for to_additive

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Mathlib.Tactic.ToAdditive.commandInsert_to_additive_translation__ :
                  Lean.ParserDescr

                  insert_to_additive_translation mulName addName inserts the translation mulName ↦ addName into the to_additive dictionary. This is useful for translating namespaces that don't (yet) have a corresponding translated declaration.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For