to_additive and pow

Stream: general

[Floris van Doorn]

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]

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

[Sebastien Gouezel]

Yes, I think that's the only reason.

[Eric Wieser]

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

[Eric Wieser]

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

[Mario Carneiro]

I think the main reason is that to_additive gets confused about theorems involving addition/multiplication on nat

[Damiano Testa]

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]

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]

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]

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]

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]

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.