# Zulip Chat Archive

## Stream: general

### Topic: to_additive and pow

#### Floris van Doorn (Jun 02 2021 at 20:02):

We don't use `@[to_additive]`

on definitions/lemmas involving `pow`

(`a ^ n`

).

Am I correct in believing that the only reason that we don't do that is that the additive version `smul`

(`n • a`

) has the arguments switched?

If so, I'll try to teach `@[to_additive]`

to switch these arguments.

#### Patrick Massot (Jun 02 2021 at 20:05):

That would be very nice if there is no hidden bad consequence.

#### Sebastien Gouezel (Jun 02 2021 at 20:06):

Yes, I think that's the only reason.

#### Eric Wieser (Jun 02 2021 at 21:21):

It's maybe complicated by the fact that smul has an additive counterpart, vadd.

#### Eric Wieser (Jun 02 2021 at 21:21):

But I guess that probably isn't used much for nat.

#### Mario Carneiro (Jun 03 2021 at 03:42):

I think the main reason is that `to_additive`

gets confused about theorems involving addition/multiplication on `nat`

#### Damiano Testa (Jun 03 2021 at 06:26):

How often is `to_additive`

used to actually convert something about multiplication on `nat`

to something about addition on `nat`

? If it is not so much (and is easy to implement) maybe it makes sense to prevent `to_additive`

to ever convert `nat.[something]`

to `nat.[something_else]`

?

#### Mario Carneiro (Jun 03 2021 at 06:27):

that's definitely the intent, but it is techically difficult to achieve, because `to_additive`

is roughly just doing a find and replace of `add`

for `mul`

#### Mario Carneiro (Jun 03 2021 at 06:29):

It's not that it sees `nat.mul`

and turns it into `nat.add`

, it sees `has_mul.mul nat nat.has_mul`

and turns it into `has_add.add nat nat.has_mul`

(because `has_mul.mul -> has_add.add`

is among the rewrites but not `nat.has_add -> nat.has_mul`

which we don't want anyway), resulting in a type error

#### Damiano Testa (Jun 03 2021 at 06:30):

Ok, thanks for the explanation! I had been looking at the `to_additive`

code, but cannot make much progress in understanding the mechanics of it.

What you wrote already explains it better than I had understood!

#### Damiano Testa (Jun 03 2021 at 06:33):

I will say one more thing and will likely shut up afterwards, since I am not really sure that I can contribute much.

The failing examples that I have seen could have been solved by replacing some (explicit or implicit) `n + 1`

to a `n.succ`

. Could it be made so that `to_additive`

first replaces all `+ 1`

(on `nat`

) to `.succ`

and then does its magic?

#### Floris van Doorn (Jun 03 2021 at 08:04):

Mario Carneiro said:

I think the main reason is that

`to_additive`

gets confused about theorems involving addition/multiplication on`nat`

Yes, I've noticed that now as well, and I'm keeping this on hold until the other PR is merged. The first tests are very promising though.

Last updated: Aug 03 2023 at 10:10 UTC