# Zulip Chat Archive

## Stream: new members

### Topic: to_additive documentation

#### Damiano Testa (Apr 09 2021 at 16:59):

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 (Apr 09 2021 at 19:18):

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 (Apr 09 2021 at 19:19):

@Kevin Buzzard I did not understand your comment

(4) link to the "dictionary" which auto-generates things like theorem names

#### Damiano Testa (Apr 09 2021 at 19:20):

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

#### Eric Wieser (Apr 09 2021 at 19:42):

We have some docs already at attr#to_additive

#### Eric Wieser (Apr 09 2021 at 19:43):

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

#### Julian Külshammer (Apr 09 2021 at 19:52):

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 (Apr 09 2021 at 19:54):

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)

Last updated: May 17 2021 at 22:15 UTC