to_additive and fixed types

Stream: general

[Floris van Doorn]

@[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]

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]

Could we instead mark exactly which types to additivize with M : add_target Type where add_target is just id?

[Floris van Doorn]

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]

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]

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]

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]

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]

what does the ! mean?

[Sebastien Gouezel]

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

[Scott Morrison]

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

[Mario Carneiro]

I think it should be the default if at all possible

[Mario Carneiro]

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

[Mario Carneiro]

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

[Floris van Doorn]

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]

@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]

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

[Mario Carneiro]

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

[Floris van Doorn]

yes: src#smooth_map.has_mul

[Floris van Doorn]

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]

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]

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]

since it will also get involved in theorems

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Floris van Doorn]

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]

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]

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]

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]

I think the same mechanism would work there

[Floris van Doorn]

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

[Yaël Dillies]

to_additive tries turning σ⁻¹ into -σ where σ : equiv.perm ι. Any chance we might extend your fix, @Floris van Doorn ?

[Floris van Doorn]

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]

equiv.perm.prod_comp in #11344

[Kevin Buzzard]

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]

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]

@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]

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]

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