limiting the effect of [to_additive]

Stream: mathlib4

[Javier Burroni]

Hello,

I noticed that some of the theorems regarding BigOperators and intervals are limited to intervals of ℕ (and thus cannot be used, for example, with ℕ⁺).

It seems that the root cause of this is the to_additive attribute.
Take, for instance, prod_Ico_succ_top:

This version works perfectly:

theorem prod_Ico_succ_top [AddCommMonoid α] [LinearOrder α] [LocallyFiniteOrder α] [One α]
    [SuccAddOrder α] [NoMaxOrder α] {a b : α} (hab : a ≤ b) (f : α → M) :
    (∏ k ∈ Ico a (b+1), f k) = (∏ k ∈ Ico a b, f k) * f b := by
  rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]

But once we introduce the @[to_additive] attribute, we encounter an error:

@[to_additive] failed. Type mismatch in additive declaration. For help, see the docstring of `to_additive.attr`, section `Troubleshooting`. Failed to add declaration
Finset.sum_Ico_succ_top:
Application type mismatch: In the application
  @SuccAddOrder α instDistribLatticeOfLinearOrder.toSemilatticeInf.toPreorder
    inst✝⁵.toAddCommSemigroup.toAddCommMagma.toAdd inst✝²
the argument
  inst✝²
has type
  Zero α : Type u_1
but is expected to have type
  One α : Type u_1

Clearly, what's happening is that the attribute is transforming everything into additive notation (converting the One to Zero).

My question is: Is it possible to limit the action of to_additive to the type M?

[Floris van Doorn]

No, this is unfortunately a limitation of the current implementation of to_additive.

[Floris van Doorn]

Of course, to_additive shouldn't restrict Mathlib in this way, but in this case, it probably means stating/proving both the multiplicative and the additive version

[Aaron Liu]

From the section Troubleshooting of the to_additive docstring:

• Option 2: It additivized a declaration d that should remain multiplicative. Solution:
  • Make sure the first argument of d is a type with a multiplicative structure. If not, can you
    reorder the (implicit) arguments of d so that the first argument becomes a type with a
    multiplicative structure (and not some indexing type)?
    The reason is that @[to_additive] doesn't additivize declarations if their first argument
    contains fixed types like ℕ or ℝ. See section Heuristics.
    If the first argument is not the argument with a multiplicative type-class, @[to_additive]
    should have automatically added the attribute @[to_additive_relevant_arg] to the declaration.
    You can test this by running the following (where d is the full name of the declaration):
    open Lean in run_cmd logInfo m!"{ToAdditive.relevantArgAttr.find? (← getEnv) `d}"
    The expected output is n where the n-th (0-indexed) argument of d is a type (family)
    with a multiplicative structure on it. none means 0.
    If you get a different output (or a failure), you could add the attribute
    @[to_additive_relevant_arg n] manually, where n is an (1-indexed) argument with a
    multiplicative structure.

I don't really understand what it's saying here.

[Javier Burroni]

Thank you!
I was going to ask if it was okay to add both versions to Mathlib to remove these specific limitations. From your response, I assume it is.

[Floris van Doorn]

I'm surprised we don't have an open issue for this yet. Fixing to_additive to support this would mean improving the to_additive heuristic to not translate ring-like structure. This is probably doable, but might be hard. I just added it as the last point of #1074

[Javier Burroni]

As suggested, I tried to state/prove both versions and then connect them:

omit [CommMonoid M] in
theorem sum_Ico_succ_top [AddCommMonoid M] [LinearOrder α] [Add α] [One α] [LocallyFiniteOrder α]
    [SuccAddOrder α] [NoMaxOrder α] {a b : α} (hab : a ≤ b) (f : α → M) :
    (∑ k ∈ Ico a (b + 1), f k) = (∑ k ∈ Ico a b, f k) + f b := by
  rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, sum_insert right_notMem_Ico, add_comm]

theorem prod_Ico_succ_top [LinearOrder α] [Add α] [One α] [LocallyFiniteOrder α] [SuccAddOrder α]
    [NoMaxOrder α] {a b : α} (hab : a ≤ b) (f : α → M) :
    (∏ k ∈ Ico a (b + 1), f k) = (∏ k ∈ Ico a b, f k) * f b := by
  rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]

attribute [to_additive sum_Ico_succ_top] prod_Ico_succ_top

However, the last line produces an error because to_additive is checking that the generated version matches the expected one:

`to_additive` validation failed: expected
  ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder α] [inst_2 : Add α] [inst_3 : Zero α]
    [inst_4 : LocallyFiniteOrder α] [SuccAddOrder α] [NoMaxOrder α] {a b : α},
    a ≤ b → ∀ (f : α → M), ∑ k ∈ Ico a (b + 0), f k = ∑ k ∈ Ico a b, f k + f b
but 'Finset.sum_Ico_succ_top' has type
  ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder α] [inst_2 : Add α] [inst_3 : One α]
    [inst_4 : LocallyFiniteOrder α] [SuccAddOrder α] [NoMaxOrder α] {a b : α},
    a ≤ b → ∀ (f : α → M), ∑ k ∈ Ico a (b + 1), f k = ∑ k ∈ Ico a b, f k + f b

Looking at the code for addToAdditiveAttr, it seems I cannot add a version that does not conform to what to_additive would generate.

Do I have any option?

[Floris van Doorn]

This check was added relatively recently in #24401 by @Jovan Gerbscheid.
You can still add both lemmas and do not connect them via to_additive.

The to_additive connection could potentially be helpful though: if we use prod_Ico_succ_top (α := ℕ) in a proof somewhere, then to_additive should be able to correctly translate that to sum_Ico_succ_top (α := ℕ) if the translation is in the dictionary, even though the lemma cannot be translated in general. What are your thoughts on this @Jovan Gerbscheid?

[Jovan Gerbscheid]

Hmm, so the situation is that the lemma can be translated under the assumption that α is a fixed type and M is a changing type. This example might be enough motivation to have my check not be strictly enforced, i.e. being able to turn it off using something like set_option linter.to_additive.check false. But on the other hand, we really want to_additive to just understand this. This would mean that we would have to tell it in some way that α is fixed.

Note that conversely, we have to tell to_additive that Unit is not a fixed type, i.e. its multiplication does get translated to an addition.

[Floris van Doorn]

(EDITED): We're already doing what you say about Unit, via this line:
https://github.com/leanprover-community/mathlib4/blob/860d21962a6ace996c34b44e9e9668eee7c61753/Mathlib/Tactic/ToAdditive.lean#L15
This is telling to_additive to translate multiplication to addition on Unit.

[Floris van Doorn]

EDIT: I misread your last sentence. We are already doing that.

[Floris van Doorn]

I agree that it would be better to just improve the heuristic, but it's not easy.
One option would be to somehow keep track of all the variables that have some additive structure (I think checking for Add or Zero should be sufficient in 99% of cases) and treat those variables as constants (i.e. do not additivize operations on them). This information has to be cached to have the hope to make this performant.

[Jovan Gerbscheid]

@Javier Burroni in the meantime, I've implemented the dont_translate feature, so you can do

import Mathlib

variable {α G M : Type*}

namespace Finset

variable [CommMonoid M] {s₂ s₁ s : Finset α} {a : α} {g f : α → M}

@[to_additive (dont_translate := α)]
theorem prod_Ico_succ_top' [AddCommMonoid α] [LinearOrder α] [LocallyFiniteOrder α] [One α]
    [SuccAddOrder α] [NoMaxOrder α] {a b : α} (hab : a ≤ b) (f : α → M) :
    (∏ k ∈ Ico a (b+1), f k) = (∏ k ∈ Ico a b, f k) * f b := by
  rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]