# Zulip Chat Archive

## Stream: general

### Topic: to_additive and fixed types

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

`@[to_additive]`

doesn't work well with fixed types, like `nat`

, `real`

, `ennreal`

, ...

This is described in issue #4210, but here is a quick example:

```
lemma prod_flip {n : ℕ} (f : ℕ → β) :
∏ r in range (n + 1), f (n - r) = ∏ k in range (n + 1), f k
```

If you try to `@[to_additive]`

this, it tries to replace the `(1 : nat)`

into `(0 : nat)`

: definitely not intended.

In #7792 I'm trying to fix it. First I used the following heuristic:

Only replace a multiplicative constant (like

`has_mul.mul`

) by its additive version if its first argument doesn't contain any unapplied "constants" (definitions, inductives, etc.)

The first argument is (usually) the type with the multiplicative structure, so if that contains `nat`

, `real`

, ..., we don't additivize it, and same if we work on `ℕ × ℕ`

. We do want to allow constants applied to arguments, like `prod A B`

, `monoid_hom A B`

, etc.

After some testing, I needed to relax this a little further. Some types, like `Monoid`

have an additive counterpart (`AddMonoid`

), and `@[to_additive]`

works fine for them. So I relaxed the rule to

Only replace a multiplicative constant by its additive version if its first argument doesn't contain any unapplied constants that don't have the

`@[to_additive]`

attribute.

This works well for 90%+ of the library. I could fix a couple of workarounds we used, where we didn't use `@[to_additive]`

on lemmas (like `prod_flip`

above).

However, I'm running into issues in `geometry.manifold.algebra.smooth_functions`

. The reason is that here we're working addition and multiplication on `C^∞⟮I, N; I', G⟯`

. The problem is that this `∞`

lives in `with_top nat`

, which means that the type we're working with involves `nat`

. This means that the heuristic in this PR fails, but the old version did work.

Now I can think of two solutions:

- Try to find a better heuristic that covers this case correctly
- Give options to
`@[to_additive]`

that tell it which heuristic to use (like`@[to_additive!]`

).

I'm leaning towards the second option, since I don't think we can find a heuristic that covers all cases.

Thoughts?

#### Kevin Buzzard (Jun 02 2021 at 20:39):

My far more limited experience with to_additive makes me want to agree with you that it will be hard to find a heuristic that covers all cases.

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

Could we instead mark exactly which types to additivize with `M : add_target Type`

where add_target is just `id`

?

#### Floris van Doorn (Jun 02 2021 at 21:34):

Interesting, but there might be some issues with that suggestion...

Where do you propose to stick these `add_target`

? For `prod_flip`

, does `β`

have type `add_target Type`

?

If I have a lemma that uses multiplication on `α × β`

, how does `add_target`

tell us whether I need to turn this into addition?

Also, inferring types of subterms in the middle of an `@[to_additive]`

could be tricky...

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

I do not know a better heuristic, but I also ran into a similar problem recently. It is analogous to Floris' example above: to keep all the examples in the same place, this is what it was.

```
import algebra.group.defs
variables {β : Type*} [mul_one_class β]
@[to_additive]
lemma npow_rec_one (a : β) : npow_rec 2 a = a * a := congr_arg _ (mul_one _)
-- red squiggle under 2:
/- type mismatch at application
0
term
nat.has_one
has type
has_one ℕ
but is expected to have type
has_zero ℕ
-/
```

#### Sebastien Gouezel (Jun 03 2021 at 07:20):

What about an attribute `always_do_to_additive_`

that we would put on types such as `C^∞⟮I, N; I', G⟯`

, and saying: when there is this attribute, `to_additive`

should not bother checking the type for something like `nat`

inside, and just do its thing?

#### Sebastien Gouezel (Jun 03 2021 at 07:22):

The heuristic would become:

Only replace a multiplicative constant by its additive version if its first argument is a type with the

`always_do_to_additive`

attribute, or doesn't contain any unapplied constants that don't have the @[to_additive] attribute.

#### Sebastien Gouezel (Jun 03 2021 at 07:44):

I see that you've already implemented the `to_additive!`

version in #7792, and that it works fine. So please ignore my comment, your solution is perfect!

#### Mario Carneiro (Jun 03 2021 at 07:45):

what does the `!`

mean?

#### Sebastien Gouezel (Jun 03 2021 at 07:48):

It means "try to be clever" (i.e., notice when some things should not be additivized, like `1 : ℕ`

).

#### Scott Morrison (Jun 03 2021 at 07:49):

I think it's insufficiently obvious, and some explicit option name is worth the extra typing here.

#### Mario Carneiro (Jun 03 2021 at 07:52):

I think it should be the default if at all possible

#### Mario Carneiro (Jun 03 2021 at 07:53):

I guess it's an option because it sometimes does the wrong thing?

#### Mario Carneiro (Jun 03 2021 at 07:54):

I don't really understand @Floris van Doorn's problem example

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

I'm not yet sure if what I'm doing in #7792 is good yet, since now the "dumb" option is the default one. I actually like @Sebastien Gouezel 's suggestion quite well, and might make that the default one (and the "dumb" option as a fallback).

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

@Mario Carneiro In the PR if `@[to_additive]`

sees something like `@has_mul.mul A _ x y`

then it looks whether `A`

contains any occurrence of `nat`

(or another fixed type), and if so, it will not replace the `mul`

by `add`

. This heuristic works well almost everywhere, except when `A`

is `C^∞⟮I, N; I', G⟯`

, because there is a `nat`

hidden in there, but we still want to turn the `mul`

into the `add`

.

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

Oh, we *want* that to go from mul to add?

#### Mario Carneiro (Jun 03 2021 at 08:04):

Surely we can't just deal with the add and mul structures on that type in the same way

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

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

I think we can, it's the same as `prod`

, just more complicated. And it has an additional argument that happens to contain `nat`

.

#### Sebastien Gouezel (Jun 03 2021 at 08:05):

You have Lie groups for which the notation is multiplicative, and other Lie groups (vector spaces, or tori) for which the notation is additive. And you want `to_additive`

to work in this context.

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

I would like to have some annotation that says that the `∞`

argument in `C^∞⟮I, N; I', G⟯`

is a "fixed parameter" and to_additive should not dig into it, but I suspect that might not be enough

#### Mario Carneiro (Jun 03 2021 at 08:07):

since it will also get involved in theorems

#### Mario Carneiro (Jun 03 2021 at 08:10):

I think, for the heuristic as described, it would suffice for the "first argument" to be modifiable to "argument n" where n is specified by the constant. That way we can just set it for this C function

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

That sounds like a more refined version of Sebastien's proposal: instead of always accepting `C^∞⟮I, N; I', G⟯`

we will just look in some (but not other) arguments.

And yeah, you may be right that we need to tag a whole bunch of definitions (and lemmas?) with this information...

#### Mario Carneiro (Jun 03 2021 at 08:11):

If it defaults to argument 1, it sounds like this example is the only one that needs tagging

#### Mario Carneiro (Jun 03 2021 at 08:12):

since all the lemmas are explicitly about C infinity, they don't have a fixed parameter in the first position

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

Mario Carneiro said:

I think, for the heuristic as described, it would suffice for the "first argument" to be modifiable to "argument n" where n is specified by the constant. That way we can just set it for this C function

I don't see what you mean:

We have `@has_mul.mul (C^∞⟮I, N; I', G⟯) _ x y`

, and so we look into the first argument of `has_mul.mul`

whether it contains `nat`

anywhere. This is the type `C^∞⟮I, N; I', G⟯`

. We don't look at argument numbers within this type (currently).

#### Mario Carneiro (Jun 03 2021 at 08:20):

I see. In that case, I think C needs an annotation that says "please don't look into argument 1 when asking whether there are constants in applications of me"

#### Mario Carneiro (Jun 03 2021 at 08:21):

I think this best matches the use case here, where we want to treat `C^∞`

as a sort of composite constructor no different than `prod`

#### Eric Wieser (Jun 03 2021 at 08:29):

A more challenging task for `to_additive`

might be `add_monoid_algebra`

vs `monoid_algebra`

, where only one of the two type-arguments is additive-ized

#### Mario Carneiro (Jun 03 2021 at 08:32):

I think the same mechanism would work there

#### Floris van Doorn (Jun 11 2021 at 04:35):

Ok, I implemented Mario's suggestion in #7792 and it works well.

#### Yaël Dillies (Jan 17 2022 at 08:18):

`to_additive`

tries turning `σ⁻¹`

into `-σ`

where `σ : equiv.perm ι`

. Any chance we might extend your fix, @Floris van Doorn ?

#### Floris van Doorn (Jan 17 2022 at 12:14):

Can you post/link some examples of multiplicative declarations involving `perm`

that you want to be additivized?

Are there *any* multiplicative operations on `perm`

that can be additivized? (I guess not.)

If the rule is "treat `perm`

like `ℕ`

or `ℝ`

and never additivize operations on this type, then this is easy to support.

#### Yaël Dillies (Jan 17 2022 at 12:42):

`equiv.perm.prod_comp`

in #11344

#### Kevin Buzzard (Jan 17 2022 at 13:11):

I guess an informal rule of thumb would be "if multiplication is not commutative in general, mathematicians are unlikely to want to additivise it", but this might not be helpful here.

#### Yaël Dillies (May 02 2022 at 19:32):

`to_additive`

troubles again, but this time with `ℕ`

:fear:

```
import order.filter.pointwise
-- just to avoid the `ℕ`-action diamond, unrelated to the present problem
local attribute [-instance] filter.has_scalar_filter
namespace filter
variables {α : Type*}
-- works fine
lemma nsmul_top' [add_monoid α] : ∀ {n : ℕ}, n ≠ 0 → n • (⊤ : filter α) = ⊤
| 0 := λ h, (h rfl).elim
| 1 := λ _, one_nsmul (⊤ : filter α)
| (n + 2) := λ _, by { rw [succ_nsmul, nsmul_top n.succ_ne_zero, top_add_top] }
-- works fine
lemma top_pow' [monoid α] : ∀ {n : ℕ}, n ≠ 0 → (⊤ : filter α) ^ n = ⊤
| 0 := λ h, (h rfl).elim
| 1 := λ _, pow_one _
| (n + 2) := λ _, by { rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top] }
-- `to_additive` tries to additize `ℕ`
/-
type mismatch at application
0
term
.nat.has_one
has type
has_one ℕ
but is expected to have type
has_zero .ℕ
-/
@[to_additive nsmul_top''] lemma top_pow'' [monoid α] : ∀ {n : ℕ}, n ≠ 0 → (⊤ : filter α) ^ n = ⊤
| 0 := λ h, (h rfl).elim
| 1 := λ _, pow_one _
| (n + 2) := λ _, by { rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top] }
end filter
```

#### Yaël Dillies (May 02 2022 at 19:38):

@Floris van Doorn said:

If the rule is "treat

`perm`

like`ℕ`

or`ℝ`

and never additivize operations on this type", then this is easy to support.

Did you ever implement this in the end, Floris?

#### Floris van Doorn (May 02 2022 at 20:38):

No, I didn't implement that, and probably it's better to implement it directly in the Lean 4 version of to_additive.

#### Floris van Doorn (May 02 2022 at 20:53):

Your new error probably has something to do with some annotations the equation compiler is adding that interferes with the heuristics of `to_additive`

.

Last updated: Dec 20 2023 at 11:08 UTC