Commit 2021-06-29 21:36 2c749b12

feat(algebra/to_additive): do not additivize operations on constant types (#7792)

• Fixes #4210
• Adds a heuristic to @[to_additive] that decides which multiplicative identifiers to replace with their additive counterparts.
• See Zulip thread or documentation for the precise heuristic.
• We tag some types with @[to_additive], so that they are handled correctly by the heurstic. These types pempty, empty, unit and punit.
• We make the following change to enable to above bullet point: you are allowed to translate a declaration to itself, only if you write its name again as argument of the attribute (if you don't specify an argument we want to raise an error, since that likely is a mistake).
• Because of this heuristic, all declarations with the @[to_additive] attribute should have a type with a multiplicative structure on it as its first argument. The first argument should not be an arbitrary indexing type. This means that in finset.prod and finprod we reorder the first two (implicit) arguments, so that the first argument is the codomain of the function.
• This will eliminate many (but not all) type mismatches generated by @[to_additive].
• This heuristic doesn't catch all cases: for example, the declaration could have two type arguments with multiplicative structure, and the second one is ℕ, but the first one is a variable.