Documentation

Mathlib.Tactic.ToAdditive.Frontend

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

In the mul_comm' example above, to_additive maps:

Heuristics #

to_additive uses heuristics to determine whether a particular identifier has to be mapped to its additive version. The basic heuristic is

Examples:

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:

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.

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 #

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

                      A set of strings of names that end in a capital letter.

                      • If the string contains a lowercase letter, the string should be split between the first occurrence of a lower-case letter followed by an upper-case letter.
                      • If multiple strings have the same prefix, they should be grouped by prefix
                      • In this case, the second list should be prefix-free (no element can be a prefix of a later element)

                      Todo: automate the translation from String to an element in this RBMap (but this would require having something similar to the rb_lmap from Lean 3).

                      Equations
                      Instances For
                        partial def String.splitCase (s : String) (i₀ : optParam String.Pos 0) (r : optParam (List String) []) :

                        This function takes a String and splits it into separate parts based on the following (naming conventions)[https://github.com/leanprover-community/mathlib4/wiki#naming-convention].

                        E.g. #eval "InvHMulLEConjugate₂SMul_ne_top".splitCase yields ["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"].

                        Linter to check that the reorder attribute is not given manually

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

                        Linter to check that the 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 all-or-nothing 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 well-tested.

                        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

                          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

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

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

                            • 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 : Option Bool

                              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
                              unsafe def ToAdditive.additiveTestUnsafe (findTranslation? : Lean.NameOption Lean.Name) (ignore : Lean.NameOption (List )) (e : Lean.Expr) :

                              Implementation function for additiveTest. 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.

                              Instances For
                                def ToAdditive.additiveTest (findTranslation? : Lean.NameOption Lean.Name) (ignore : Lean.NameOption (List )) (e : Lean.Expr) :

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

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

                                    Equations
                                    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, 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 (findTranslation? : Lean.NameOption Lean.Name) (reorderFn : Lean.NameList (List )) (ignore : Lean.NameOption (List )) (changeNumeral? : Lean.NameOption (List )) (relevantArg : Lean.Name) (trace : Bool) :

                                        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

                                            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.

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

                                              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

                                                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

                                                  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 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
                                                      Instances For

                                                        It's just the same as Lean.Meta.setInlineAttribute but with type CoreM Unit.

                                                        TODO (lean4#4965): make Lean.Meta.setInlineAttribute a CoreM Unit and remove this definition.

                                                        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
                                                            def ToAdditive.warnExt {σ : Type} {α : Type} {β : Type} [Inhabited σ] (stx : Lean.Syntax) (ext : Lean.PersistentEnvExtension α β σ) (f : σLean.NameBool) (thisAttr : Lean.Name) (attrName : Lean.Name) (src : Lean.Name) (tgt : Lean.Name) :

                                                            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} {β : Type} [Inhabited β] (stx : Lean.Syntax) (attr : Lean.SimpleScopedEnvExtension α β) (f : βLean.NameBool) (thisAttr : Lean.Name) (attrName : Lean.Name) (src : Lean.Name) (tgt : Lean.Name) :

                                                              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
                                                                def ToAdditive.warnParametricAttr {β : Type} (stx : Lean.Syntax) (attr : Lean.ParametricAttribute β) (thisAttr : Lean.Name) (attrName : Lean.Name) (src : Lean.Name) (tgt : Lean.Name) :

                                                                Warn the user when the multiplicative declaration has a parametric attribute.

                                                                Equations
                                                                Instances For

                                                                  additivizeLemmas names desc t runs t on all elements of names and adds translations between the generated lemmas (the output of t). names must be non-empty.

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

                                                                    Find the first argument of nm that has a multiplicative type-class on it. Returns 1 if there are no types with a multiplicative class as arguments. E.g. Prod.Group returns 1, and Pi.One returns 2. Note: we only consider the first argument of each type-class. E.g. [Pow A N] is a multiplicative type-class on A, not on N.

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

                                                                      Capitalizes s char-by-char 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
                                                                        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 lower-case, 2nd element should be capitalized properly.

                                                                          Instances For

                                                                            Turn each element to lower-case, apply the nameDict and capitalize the output like the input.

                                                                            Equations
                                                                            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:

                                                                                1. Split according to capitalisation rule and at _.
                                                                                2. Apply word-by-word translation rules.
                                                                                3. Fix up abbreviations that are not word-by-word translations, like "addComm" or "Nonneg".
                                                                                Equations
                                                                                Instances For

                                                                                  Return the provided target name or autogenerate one if one was not provided.

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