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.

ink

def to_additive_ignore_args : Lean.ParserDescr

The to_additive_ignore_args attribute.

Equations

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

ink

def to_additive_relevant_arg : Lean.ParserDescr

The to_additive_relevant_arg attribute.

Equations

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

ink

def to_additive_reorder : Lean.ParserDescr

The to_additive_reorder attribute.

Equations

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

ink

def to_additive_change_numeral : Lean.ParserDescr

The to_additive_change_numeral attribute.

Equations

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

ink

def toAdditiveAttrOption : Lean.ParserDescr

An attr := ... option for to_additive.

Equations

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

ink

def toAdditiveReorderOption : Lean.ParserDescr

An reorder := ... option for to_additive.

Equations

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

ink

def toAdditiveParenthesizedOption : Lean.ParserDescr

Options to to_additive.

Equations

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

ink

def toAdditiveOption : Lean.ParserDescr

Options to to_additive.

Equations

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

ink

def toAdditiveRest : Lean.ParserDescr

Remaining arguments of to_additive.

Equations

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

ink

def to_additive : Lean.ParserDescr

The to_additive attribute.

Equations

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

ink

def attrTo_additive?_ : Lean.ParserDescr

The to_additive attribute.

Equations

• attrTo_additive?_ = Lean.ParserDescr.node `attrTo_additive?_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "to_additive?" false) toAdditiveRest)

ink

def endCapitalNames : Lean.RBMap String (List String) compare

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

• endCapitalNames = Lean.RBMap.ofList [("LE", [""]), ("LT", [""]), ("WF", [""]), ("Coe", ["TC", "T", "HTCT"])]

ink

partial def String.splitCase (s : String) (i₀ : optParam String.Pos 0) (r : optParam (List String) []) : 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"].

ink

opaque ToAdditive.linter.toAdditiveReorder : Lean.Option Bool

Linter to check that the reorder attribute is not given manually

ink

opaque ToAdditive.linter.existingAttributeWarning : Lean.Option Bool

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

ink

opaque ToAdditive.linter.toAdditiveGenerateName : Lean.Option Bool

Linter to check that the reorder attribute is not given manually

ink

opaque ToAdditive.linter.toAdditiveExisting : Lean.Option Bool

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

ink

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.

ink

opaque ToAdditive.reorderAttr : Lean.NameMapExtension (List ℕ)

An attribute that stores all the declarations that needs their arguments reordered when applying @[to_additive]. Currently, we only support swapping consecutive arguments. The list of the natural numbers contains the positions of the first of the two arguments to be swapped. If the first two arguments are swapped, the first two universe variables are also swapped. Example: @[to_additive_reorder 1 4] swaps the first two arguments and the arguments in positions 4 and 5.

ink

opaque ToAdditive.relevantArgAttr : Lean.NameMapExtension ℕ

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: adding @[to_additive_reorder] with an equal or smaller number than the number in this attribute is currently not supported.

ink

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

ink

opaque ToAdditive.translations : Lean.NameMapExtension Lean.Name

Maps multiplicative names to their additive counterparts.

ink

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.NameMap.find? (Lean.SimplePersistentEnvExtension.getState ToAdditive.translations env)

ink

def ToAdditive.insertTranslation (src : Lean.Name) (tgt : Lean.Name) (failIfExists : optParam 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.

ink

structure ToAdditive.Config : Type

• View the trace of the to_additive procedure. Equivalent to set_option trace.to_additive true.

  trace : Bool

• The name of the target (the additive declaration).

  tgt : Lean.Name

• An optional doc string.

  doc : Option String

• If allowAutoName is false (default) then @[to_additive] will check whether the given name can be auto-generated.

  allowAutoName : Bool

• The arguments that should be reordered by to_additive

  reorder : List ℕ

• The attributes which we want to give to both the multiplicative and additive versions. For certain attributes (such as simp and simps) this will also add generated lemmas to the translation dictionary.

  attrs : Array 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.

  ref : Lean.Syntax

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

  existing : Option Bool

Config is the type of the arguments that can be provided to to_additive.

ink

instance ToAdditive.instReprConfig : Repr ToAdditive.Config

Equations

• ToAdditive.instReprConfig = { reprPrec := ToAdditive.reprConfig✝ }

ink

def ToAdditive.additiveTestAux (findTranslation? : Lean.Name → Option Lean.Name) (ignore : Lean.Name → Option (List ℕ)) : Bool → Lean.Expr → Bool

Auxilliary function for additiveTest. The bool argument only matters when applied to exactly a constant.

Equations

• ToAdditive.additiveTestAux findTranslation? ignore = ToAdditive.additiveTestAux.visit findTranslation? ignore

ink

def ToAdditive.additiveTestAux.visit (findTranslation? : Lean.Name → Option Lean.Name) (ignore : Lean.Name → Option (List ℕ)) : Bool → Lean.Expr → Bool

see additiveTestAux

Equations

• One or more equations did not get rendered due to their size.
• ToAdditive.additiveTestAux.visit findTranslation? ignore x (Lean.Expr.const n us) = (x || Option.isSome (findTranslation? n))
• ToAdditive.additiveTestAux.visit findTranslation? ignore x (Lean.Expr.lam binderName binderType t binderInfo) = ToAdditive.additiveTestAux.visit findTranslation? ignore false t
• ToAdditive.additiveTestAux.visit findTranslation? ignore x (Lean.Expr.forallE binderName binderType t binderInfo) = ToAdditive.additiveTestAux.visit findTranslation? ignore false t
• ToAdditive.additiveTestAux.visit findTranslation? ignore x x = true

ink

def ToAdditive.additiveTest (findTranslation? : Lean.Name → Option Lean.Name) (ignore : Lean.Name → Option (List ℕ)) (e : Lean.Expr) : Bool

additiveTest e tests whether the expression e contains no constant nm that is not applied to any arguments, and such that translations.find?[nm] = none. This is used in @[to_additive] for deciding which subexpressions to transform: we only transform constants if additiveTest applied to their first argument returns true. This means we will replace expression applied to e.g. α or α × β× β, but not when applied to e.g. ℕ or ℝ × α× α. We ignore all arguments specified by the ignore NameMap.

Equations

• ToAdditive.additiveTest findTranslation? ignore e = ToAdditive.additiveTestAux findTranslation? ignore false e

ink

def List.swapFirstTwo {α : Type u_1} : List α → List α

Swap the first two elements of a list

Equations

• List.swapFirstTwo x = match x with | [] => [] | [x] => [x] | x :: y :: l => y :: x :: l

ink

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 x = match x with | Lean.Expr.lit (Lean.Literal.natVal 1) => Lean.mkRawNatLit 0 | e => e

ink

def ToAdditive.applyReplacementFun (e : Lean.Expr) : 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.

ink

def ToAdditive.applyReplacementFun.aux (findTranslation? : Lean.Name → Option Lean.Name) (reorderFn : Lean.Name → List ℕ) (ignore : Lean.Name → Option (List ℕ)) (changeNumeral? : Lean.Name → Option (List ℕ)) (isRelevant : Lean.Name → ℕ → Bool) (trace : Bool) : Lean.Expr → Lean.Expr

Implementation of applyReplacementFun.

Equations

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

ink

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.

ink

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.

Equations

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

ink

def ToAdditive.reorderForall (src : Lean.Expr) (reorder : optParam (List ℕ) []) : 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.

ink

def ToAdditive.reorderLambda (src : Lean.Expr) (reorder : optParam (List ℕ) []) : 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.

ink

def ToAdditive.updateDecl (tgt : Lean.Name) (srcDecl : Lean.ConstantInfo) (reorder : optParam (List ℕ) []) : 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.

ink

def ToAdditive.findTargetName (env : Lean.Environment) (src : Lean.Name) (pre : Lean.Name) (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.

ink

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

Returns a NameSet of all auxiliary constants in e that might have been generated when adding pre to the environment. Examples include pre.match_5, Mathlib.MyFile._auxLemma.3 and _private.Mathlib.MyFile.someOtherNamespace.someOtherDeclaration._eq_2. The last two examples may or may not have been generated by this declaration. The last example may or may not be the equation lemma of a declaration with the @[to_additive] attribute. We will only translate it has the @[to_additive] attribute.

Equations

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

ink

partial def ToAdditive.transformDeclAux (cfg : ToAdditive.Config) (pre : Lean.Name) (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.

ink

def ToAdditive.copyInstanceAttribute (src : Lean.Name) (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.

ink

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

ink

def ToAdditive.warnAttr {β : Type} {α : Type} [inst : Inhabited β] (stx : Lean.Syntax) (attr : Lean.SimpleScopedEnvExtension α β) (f : β → Lean.Name → Bool) (thisAttr : Lean.Name) (attrName : Lean.Name) (src : Lean.Name) (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.warnExt stx attr.ext (fun x x_1 => f (List.head! x.stateStack).state x_1) thisAttr attrName src tgt

ink

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

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

Equations

• ToAdditive.warnParametricAttr stx attr thisAttr attrName src tgt = ToAdditive.warnExt stx attr.ext (fun x x_1 => Lean.NameMap.contains x x_1) thisAttr attrName src tgt

ink

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

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

Equations

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

ink

def ToAdditive.firstMultiplicativeArg (nm : Lean.Name) : Lean.MetaM ℕ

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.

ink

partial def ToAdditive.capitalizeLikeAux (s : String) (i : optParam String.Pos 0) (p : String) : String

Helper for capitalizeLike.

ink

def ToAdditive.capitalizeLike (r : String) (s : String) : String

Capitalizes s char-by-char like r. If s is longer, it leaves the tail untouched.

Equations

• ToAdditive.capitalizeLike r s = ToAdditive.capitalizeLikeAux r 0 s

ink

def ToAdditive.capitalizeFirstLike (s : String) : List String → List String

Capitalize First element of a list like s. Note that we need to capitalize multiple characters in some cases, in examples like HMul or hAdd.

Equations

• ToAdditive.capitalizeFirstLike s x = match x with | x :: r => ToAdditive.capitalizeLike s x :: r | [] => []

ink

def ToAdditive.nameDict : String → List String

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.

Equations

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

ink

def ToAdditive.applyNameDict : List String → List String

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

Equations

• ToAdditive.applyNameDict (x_1 :: r) = ToAdditive.capitalizeFirstLike x_1 (ToAdditive.nameDict (String.toLower x_1)) ++ ToAdditive.applyNameDict r
• ToAdditive.applyNameDict [] = []

ink

def ToAdditive.fixAbbreviation : List String → List String

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.

ink

def ToAdditive.guessName : String → String

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

• ToAdditive.guessName = String.mapTokens (Char.ofNat 39) fun s => String.join (ToAdditive.fixAbbreviation (ToAdditive.applyNameDict (String.splitCase s 0)))

ink

def ToAdditive.targetName (cfg : ToAdditive.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.

ink

def ToAdditive.proceedFieldsAux (src : Lean.Name) (tgt : Lean.Name) (f : Lean.Name → Lean.CoreM (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 src.a_i to tgt.b_i.

Equations

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

ink

def ToAdditive.proceedFields (src : Lean.Name) (tgt : Lean.Name) : 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.

ink

def ToAdditive.elabToAdditive : Lean.Syntax → Lean.CoreM ToAdditive.Config

Elaboration of the configuration options for to_additive.

Equations

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

ink

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

Apply attributes to the multiplicative and additive declarations.

ink

partial def ToAdditive.copyMetaData (cfg : ToAdditive.Config) (src : Lean.Name) (tgt : Lean.Name) : Lean.CoreM (Array Lean.Name)

Copies equation lemmas and attributes from src to tgt

ink

partial def ToAdditive.transformDecl (cfg : ToAdditive.Config) (src : Lean.Name) (tgt : Lean.Name) : 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].

ink

partial def ToAdditive.addToAdditiveAttr (src : Lean.Name) (cfg : ToAdditive.Config) (kind : optParam 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.