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):

yes: src#smooth_map.has_mul

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