to_additive documentation

Stream: new members

[Damiano Testa]

I am going to quit for today: here is what I have so far: let me know if you think that something is wrong! I am still planning to add stuff, but probably not today!

The to_additive attribute.

Two of the most common operations are addition (+) and multiplication (+). Often,
you would like to state and prove an additive and a multiplicative version of the same
result. For instance, the two lemmas

lemma one_mul {M : Type*} [monoid M] (m : M) : (1 : M) * m = m

and

lemma zero_add {M : Type*} [add_monoid M] (m : M) : (0 : M) + m = m

are "equal", but of course, actually different. The to_additive attribute helps you by
converting the statement and proof of the multiplicative version to a statement and
proof of the additive version. The attribute also guesses the name for the corresponding
additive lemma, but you can override this.

Here is an example of how the syntax works.

@[to_additive]
lemma one_mul_new {M : Type*} [monoid M] (m : M) : (1 : M) * m = m :=
one_mul _

generates the explicit lemma one_mul_new. It also generated the lemma zero_add_new,
as you can see by typing #check @zero_add_new. If, for some reason, you do not like
the auto-generated name, you can overrule it by saying

@[to_additive my_better_name]
lemma one_mul_newer {M : Type*} [monoid M] (m : M) : (1 : M) * m = m :=
one_mul _

again, checking the ghost lemma by #check @my_better_name.

You can combine the to_additive attribute with other attributes, for instance with simp.
For instance,

@[to_additive, simp] -- autogenerates `zero_add_new`,
-- only `one_mul_new` has the `simp` attribute
lemma one_mul_new {M : Type*} [monoid M] (m : M) : (1 : M) * m = m :=
one_mul _

auto-generates the additive version and gives the simp attribute to the multiplicative verion.
If you want the additive version to also acquire the simp attribute, you simply exchange the
order of the attributes:

@[simp, to_additive] -- autogenerates `zero_add_new`,
-- both `one_mul_new` and `zero_add_new` have the `simp` attribute
lemma one_mul_new {M : Type*} [monoid M] (m : M) : (1 : M) * m = m :=
one_mul _

To check the attributes, simply type #print zero_add_new and at the very beginning,
Lean will tell you which attributes the lemma zero_add_new has.

You cannot use to_additive with structures: if you want two structures, one additive and
one multiplicative, than you need to constructed separately.

However, you can use the to_additive attribute also for def and theorem. In the case of
def, the linter requires a doc-string for all def, including the autogenerated ones.

Here is an example of how to achieve this.
[example]

[Kevin:
You should write some to_additive doc before you forget everything. The basic things are: (1) basic usage (it makes an additive version of a multiplicative lemma) (2) add the attribute after simp if you want the simp to apply to the additive version (3) for structures (rather than theorems) you have to make the structure yourself and then tag it later (your confusion about adding the attribute at the same time or afterwards) (4) link to the "dictionary" which auto-generates things like theorem names (5) how to override docstrings e.g. with add_decl_doc (see for example line 279 of submonoid.basic, I linked to the file above) (6) the gotcha with g^n vs n smul g and how it breaks everything.

/-- multiplicative docstring -/
@[to_additive "additive docstring"] def gi : galois_insertion...

and the "choose another name rather than the auto-generated one" trick e.g.

@[to_additive ordered_add_comm_group.add_lt_add_left]
lemma ordered_comm_group.mul_lt_mul_left' (a b : α) (h : a < b) (c : α) : c * a < c * b :=

(remove the prime, because there will be some ring version which doesn't have an additive counterpart)]

[Yakov:
The final aspect is tagging something with to_additive "out of band", that is, via an attribute ... line like at

@[simp] lemma order_of_one : order_of (1 : α) = 1 :=
begin
apply le_antisymm,
{ exact order_of_le_of_pow_eq_one (nat.one_pos) (pow_one 1) },
{ exact nat.succ_le_of_lt ( order_of_pos' ⟨1, ⟨nat.one_pos, pow_one 1⟩⟩) }
end

@[simp] lemma add_order_of_zero : add_order_of (0 : H) = 1 :=
by simp [← order_of_of_add_eq_add_order_of]

attribute [to_additive add_order_of_zero] order_of_one]

[Damiano Testa]

Here is a version that is closer to final:

The to_additive attribute.

Basic usage:

Automation for converting multiplicative to additive

Lemmas, theorems, definitions

Two of the most common operations are addition (+) and multiplication (+). Often,
you would like to state and prove an additive and a multiplicative version of the same
result. For instance, the two lemmas

lemma one_mul {M : Type*} [monoid M] (m : M) : (1 : M) * m = m

and

lemma zero_add {M : Type*} [add_monoid M] (m : M) : (0 : M) + m = m

are "equal", but of course, actually different. The to_additive attribute helps you by
converting the statement and proof of the multiplicative version to a statement and
proof of the additive version. The attribute also guesses the name for the corresponding
additive lemma, but you can override this.

Here is an example of how the syntax works.

@[to_additive]
lemma one_mul_new {M : Type*} [monoid M] (m : M) : (1 : M) * m = m :=
one_mul _

generates the explicit lemma one_mul_new. It also generated the lemma zero_add_new,
as you can see by typing #check @zero_add_new. If, for some reason, you do not like
the auto-generated name, you can overrule it by saying

@[to_additive my_better_name]
lemma one_mul_newer {M : Type*} [monoid M] (m : M) : (1 : M) * m = m :=
one_mul _

again, checking the ghost lemma by #check @my_better_name.

Further attributes

You can combine the to_additive attribute with other attributes, for instance with simp.
For instance,

@[to_additive, simp] -- autogenerates `zero_add_new`,
-- only `one_mul_new` has the `simp` attribute
lemma one_mul_new {M : Type*} [monoid M] (m : M) : (1 : M) * m = m :=
one_mul _

auto-generates the additive version and gives the simp attribute to the multiplicative verion.
If you want the additive version to also acquire the simp attribute, you simply exchange the
order of the attributes:

@[simp, to_additive] -- autogenerates `zero_add_new`,
-- both `one_mul_new` and `zero_add_new` have the `simp` attribute
lemma one_mul_new {M : Type*} [monoid M] (m : M) : (1 : M) * m = m :=
one_mul _

To check the attributes, simply type #print zero_add_new and at the very beginning,
Lean will tell you which attributes the lemma zero_add_new has.

Warning.
You cannot use to_additive with structures: if you want two structures, one additive and
one multiplicative, than you need to constructed separately.

to_additive and doc strings

However, you can use the to_additive attribute also for def and theorem. In the case of
def, the linter requires a doc-string for all def, including the autogenerated ones.

Here is an example of how to achieve this.
variables {G : Type*} [has_mul G]

/-- left_mul_one g denotes left multiplication by g -/
@[to_additive "left_add_zero g denotes left addition by g"]
def left_mul_one : G → G → G := λ g : G, λ x : G, g * x

#check @left_mul_one
#check @left_add_zero

In VSCode, hovering over the names of the lemmas in the #check [...] lines, shows the two
doc strings.

An alternative is to use add_decl_doc.

/-- A truly trivial multiplicative lemma. -/
@[to_additive]
lemma simple_mul {M : Type*} [monoid M] : true := sorry

/-- And the truly trivial additive doc string. -/
add_decl_doc add_submonoid.dense_induction

#check @simple_mul
#check @simple_add

Structures

As we mentioned above, the @[to_additive] attribute cannot be used directly on a structure
(or on a class). However, after you made the two separate multiplicative and additive
structures, you can add the tag afterwards. Here is an example.

These are the definitions of a comm_semigroup and of an add_comm_semigroup:

/-- A commutative semigroup is a type with an associative commutative `(*)`. -/
@[protect_proj, ancestor semigroup]
class comm_semigroup (G : Type u) extends semigroup G :=
(mul_comm : ∀ a b : G, a * b = b * a)

/-- A commutative additive semigroup is a type with an associative commutative `(+)`. -/
@[protect_proj, ancestor add_semigroup]
class add_comm_semigroup (G : Type u) extends add_semigroup G :=
(add_comm : ∀ a b : G, a + b = b + a)
attribute [to_additive] comm_semigroup

Notice the line attribute [to_additive] comm_semigroup, following the two definitions.
You can add the attribute anywhere after the two definitions. If you want to overrule
the auto-generated name, you can use the syntax

attribute [to_additive my_special_additive_name] comm_semigroup

Issues

Sometimes, the wonderful automation crumbles. In trying to define a ℕ-semimodule structure
on an abelian (multiplicative/additive) group, it would be useful to be able to apply to_additive.
Unfortunately, this is, at the moment, not implemented. The reason is simple.

The ℕ-action on an abelian multiplicative group G is via iterated multiplication,
that is, via exponentiation:
n ∈ ℕ acts on g ∈ G via n ↦ g ^ n.

The ℕ-action on an abelian additive group A is via iterated addition, that is
(s)multiplication:
n ∈ ℕ acts on a ∈ A via n ↦ n • a.

These two actions are on different sides and the to_additive attribute is not flexible
enough to see through this. Sadly, for the moment, you will have to duplicate all the lemmas
relating to additive/multiplicative actions.

[Damiano Testa]

@Kevin Buzzard I did not understand your comment
(4) link to the "dictionary" which auto-generates things like theorem names

[Damiano Testa]

Also, if people are happy with this, where should I put it?

[Eric Wieser]

We have some docs already at attr#to_additive

[Eric Wieser]

So I guess merging what you wrote with that is the way to go

[Julian Külshammer]

I think it is worth mentioning the example you had in your draft that another issue is that sometimes you have 1s you don't want to translate to 0s, like in order_of (1:R)=1. This will fail, if I read the error message correctly, because it tries to translate both 1s to 0s, but the one on the RHS shouldn't be translated.

[Julian Külshammer]

I think what Kevin meant with (4) was some list which names get translated, like mul - > add, one - > zero, etc (I don't actually know how long that list is)