This file defines an attribute to_additive that can be used to automatically transport theorems and definitions (but not inductive types and structures) from multiplicative theory to additive theory.
To use this attribute, just write
@[to_additive]
theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm
This code will generate a theorem named add_comm'. It is also possible to manually specify the name of the new declaration, and provide a documentation string.
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.
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.
After transporting the “main” declaration, to_additive transports its equational lemmas.
If src is a structure, then to_additive automatically adds structure fields to its mapping, and similarly for constructors of inductive types.
For new structures this means that to_additive automatically handles coercions, and for old structures it does the same, if ancestry information is present in @[ancestor] attributes.
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.
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 new_namespace.new_name /with a dot/, then to_additive uses this new name as is.
As a safety check, in the first two cases to_additive double checks that the new name differs from the original one.
Automatically transport structures and other inductive types.
Handle protected attribute. Currently all new definitions are public.
For structures, automatically generate theorems like group α ↔ add_group (additive α).
Mapping of prefixes that do not correspond to any definition, see quotient_group.
Rewrite rules for the last part of the name that work in more cases. E.g., we can replace monoid with add_monoid etc.