to_additive clashes

Stream: general

[Johan Commelin]

While porting, we are discovering that several multiplicative statements are being mapped to the same additive statement.
I don't know how to modify to_additive, but I think it should error when a decl already exists.
And then we pass a +force flag to make it shut up, so that the following still works

def some_mul_thing : foobar := baz

def some_add_thing : fooquux := bumsdings

attribute [to_additive +force some_add_thing] some_mul_thing

[Reid Barton]

Maybe something more self-explanatory e.g. [to_additive as_existing some_add_thing]

[Floris van Doorn]

Additivizing a declaration to an additive declaration that already exists is quite common: sometimes @[to_additive] is not good enough to translate the declaration automatically (this happens basically with all lemmas that involve powers that should be translated to smul).

In rare cases it's even useful to have multiple multiplicative declarations that map to the same additive declaration (so one of the to_additive calls will then refer to an existing declaration. I responded in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20align.20failures/near/323303372 why this is sometimes useful.

I agree that it might be good to have a syntax for the cases where the additive declaration already exists. I think this can be a Lean 4-only thing? It's easy to implement if we decide on a syntax.

[Floris van Doorn]

(I actually want to implement something similar for simps where in some cases it will run in "expensive mode", which can be slow in certain cases. I want to add a token like simps! that runs in expensive mode.)

[Yaël Dillies]

to_additive!?

[Floris van Doorn]

to_additive! used to have another meaning that nobody ever used and wasn't very useful (it was to disable the heuristics, but they turn out to be pretty good - !4#1504). So to_additive! is available. However, ! tends to mean "try harder", which isn't really the case here. I think I'll do to_additive existing, unless someone has a better suggestion.

[Floris van Doorn]

(Duplicated message deleted)

[Floris van Doorn]

Implemented in !4#1881 (see last commit, everything else is from the dependencies)