## Stream: general

#### 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.

#### 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: Dec 20 2023 at 11:08 UTC