@[to_additive] 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.
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
(but this would require having something similar to the
rb_lmap from Lean 3).
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].
#eval "InvHMulLEConjugate₂SMul_ne_top".splitCase yields
["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"].
An attribute that tells
@[to_additive] that certain arguments of this definition are not
involved when using
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 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
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
ℕ × α
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
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 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).
n₁ ... are the positions of the numeral arguments (starting counting from 1).
- 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
@[to_additive]will check whether the given name can be auto-generated.
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 certain attributes (such as
simps) this will also add generated lemmas to the translation dictionary.
- ref : Lean.Syntax
Syntaxelement corresponding to the original multiplicative declaration (or the
to_additiveattribute if it is added later), which we need for adding definition ranges.
An optional flag stating whether the additive declaration already exists. If this flag is set but wrong about whether the additive declaration exists,
to_additivewill raise a linter error. Note: the linter will never raise an error for inductive types and structures.
Implementation function for
We cache previous applications of the function, using the same method that
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
and we're not remembering the cache between these calls.
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
additiveTest applied to their first argument returns
This means we will replace expression applied to e.g.
α × β, but not when applied to
ℝ × α.
We ignore all arguments specified by the
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
test argis false. However, if
fis in the dictionary
relevant, then the argument
relevant.find fis tested, instead of the first argument.
It will also reorder arguments of certain functions, using
g x₁ x₂ x₃ ... xₙ becomes
g x₂ x₁ x₃ ... xₙ if
reorderFn g = some .
NameSet of all auxiliary constants in
e that might have been generated
pre to the environment.
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
attribute. We will only translate it has the
transform the declaration
src and all declarations
pre._proof_i occurring in
using the transforms dictionary.
reorder are configuration options.
pre is the declaration that got the
@[to_additive] attribute and
tgt_pre is the target of this
Warn the user when the multiplicative declaration has an attribute.
Warn the user when the multiplicative declaration has a simple scoped attribute.
runAndAdditivize names desc t runs
t on all elements of
and adds translations between the generated lemmas (the output of
names must be non-empty.
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.
Prod.Group returns 1, and
Pi.One returns 2.
Note: we only consider the first argument of each type-class.
[Pow A N] is a multiplicative type-class on
A, not on
Dictionary used by
guessName to autogenerate names.
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.
Turn each element to lower-case, apply the
capitalize the output like the input.
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
Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and
the body using the
This is used to implement
addToAdditiveAttr src cfg adds a
@[to_additive] attribute to
src with configuration
See the attribute implementation for more details.
It returns an array with names of additive declarations (usually 1, but more if there are nested