to_additive on AddMonoidWithOne

Stream: mathlib4

[Chris Birkbeck]

I'm having trouble with the following to_additive, which I think should work since I can prove the additive version with the same proof (as seen below):

@[to_additive]
theorem pnat_multipliable_iff_multipliable_succ' {α R : Type*} [AddMonoidWithOne R]
 [TopologicalSpace α] [CommMonoid α] {f : R → α} :
    Multipliable (fun x : ℕ+ => f x) ↔ Multipliable fun x : ℕ => f (x + 1) := by
  convert Equiv.pnatEquivNat.symm.multipliable_iff.symm
  simp

theorem pnat_summable_iff_summable_succ' {α R : Type*} [AddMonoidWithOne R]
[TopologicalSpace α] [AddCommMonoid α]
    {f : R → α} : Summable (fun x : ℕ+ => f x) ↔ Summable fun x : ℕ => f (x + 1) := by
  convert Equiv.pnatEquivNat.symm.summable_iff.symm
  simp

The to_additive is giving the following error, which I'm not sure how to fix:

Aplication type mismatch: In the application
  @Zero.toOfNat0 R inst✝².toOne
the argument
  inst✝².toOne
has type
  One R : Type u_11
but is expected to have type
  Zero R : Type u_11

[Chris Birkbeck]

#27841

[Aaron Liu]

You don't lose any generality if you take f : ℕ → α instead

[Aaron Liu]

so drop the AddMonoidWithOne

[Aaron Liu]

hmm

[Aaron Liu]

I guess you end up with f ↑(x + 1) on the rhs instead of f (↑x + 1)

[Aaron Liu]

now I'm not sure anymore

[Chris Birkbeck]

yeah the coercions become annoying which is why I want this version.

[Bryan Gin-ge Chen]

Just from the error message it looks like to_additive isn't translating One to Zero. I seem to recall there was some issue with those typeclasses, maybe @Jovan Gerbscheid can explain?

[Weiyi Wang]

or perhaps it is translating 1 to 0 when it shouldn't in this case?

[Chris Birkbeck]

Yeah I don't think it should be trying to translate it and there is something in the documentation about this for multiplicative instances, but I can't seem to get it to ignore R when doing this.

[Jovan Gerbscheid]

Yes, this is a known limitation of to_additive. The heuristics are smart enough to see that 1 : ℕ should not be translated to 0 : ℕ, but it still tries to translate 1 : R to 0 : R, because it doesn't take into account that the R has an AddMonoidWithOne instance. For example, a consequence of this is that the theory of AddMonoidAlgebra and MonoidAlgebra are duplicated in the same file, instead of using to_additive.

I think there are two ways in which this problem might be solved (in a hypothetical future fix).

1. introduce the syntax @[to_additive (dont_translate := R) to tell to_additive to not translate multiplicative things relating to R.
2. in addition to the above, let to_additive infer from AddMonoidWithOne R that R should not be translated. This would involve tagging all instances that are multiplicative and additive, such as Ring, Field and AddMonoidWithOne.

[Chris Birkbeck]

@[to_additive (dont_translate := R)] doesnt seem to work, it says: unexpected identifier; expected 'attr' or 'reorder'

[Chris Birkbeck]

also how/where do I tag the instances in your second point?

[Etienne Marion]

These are potential solutions, but they have not been implemented.

[Chris Birkbeck]

oh sorry I misread!

[Jovan Gerbscheid]

I've though about this a bit more, and I think we can add the following heuristic:
For any to_additive constant, let the nth argument be the first multiplicative argument (there is already code that looks for this, related to to_additive_relevant_arg). Then when translating this constant, we check if anything in the nth argument has been tranlated. If not, we also don't translate this constant.

In the original example, One.toOfNat was translated to Zero.toOfNat, but its argument inst.toOne was not translated. Hence this heuristic would fix that, so that neither gets translated. Hopefully this will also make MonoidAlgebra work with to_additive.

I won't be able to work on this for a week now so if anyone wants to try, feel free to.

cc @Floris van Doorn

[Floris van Doorn]

Jovan Gerbscheid said:

I've though about this a bit more, and I think we can add the following heuristic:
For any to_additive constant, let the nth argument be the first multiplicative argument (there is already code that looks for this, related to to_additive_relevant_arg). Then when translating this constant, we check if anything in the nth argument has been tranlated. If not, we also don't translate this constant.

In the original example, One.toOfNat was translated to Zero.toOfNat, but its argument inst.toOne was not translated. Hence this heuristic would fix that, so that neither gets translated. Hopefully this will also make MonoidAlgebra work with to_additive.

I don't understand what you mean here. Can you expand it more?
Usually the "first multiplicative argument" is a type argument, which is often a variable, and so often nothing gets translated in this argument.

If you mean "look at the type-class argument(s), and see whether anything in that gets translated", that might be an interesting idea. But the basic thing doesn't work. E.g. if we have something which uses the instance CommMonoid.toMonoid (CommRing.toCommMonoid inst) then to_additive will currently translate this to the (type-incorrect) AddCommMonoid.toAddMonoid (CommRing.toCommMonoid inst), so we also have to block that translation.

This gets complicated, but it might actually work. When we translate foo a1 a2 ... an, we first translate all arguments. Then we take (all?) the type-class arguments on the first multiplicative argument, and see if their translation changed anything. Then we translate foo to its additive version only if

1. the current heuristic says we can change it
2. the type-class arguments either changed or is a variable.

Note: the recursive call of the translation might have to return a boolean stating "I have changed my subexpression", or more accurately "the above test passed", since for lemmas with to_additive self, the test can pass and we can replace foo with its additive version, without actually changing the term.

[Jovan Gerbscheid]

Yes, that is what I meant, looking at the multiplicative type class argument. We could look at multiple type class arguments, but I don't think that would gain us more than just looking at the first one. In the algorithm that determines the to_additive_relevant_arg, it first finds the first argument whose type gets translated (i.e. the type class argument), and then if the first argument of that is a variable, then that is the relevant multiplicative argument.

And indeed a good way to do this is to have the recursive call return a Bool to say whether anything has been tranlated in there. I hadn't thought of the case of the argument being a variable, that case should indeed also be tranlated.

[Jovan Gerbscheid]

I've made #28591 that implements the above heuristic, and I've been able to use @[to_additive] on almost everything in Algebra.MonoidAlgebra.Defs :tada:

[Chris Birkbeck]

Oh great! thanks so much for doing this!

[Jovan Gerbscheid]

I've encountered some limitations of my current approach, so I'm considering to instead do something closer to my original suggestion in this thread. For example:

• Figuring out whether an instance has changed isn't always as easy as it seems. There can be an instance of type Mul (MonoidAlgebra _ _) which gets translated into an instance of type Mul (AddMonoidAlgebra). My heuristic would pick this up as that it was changed, but since it is still a Mul instance, in should count as unchanged.
• Some functions, like MulOpposite, don't have an instance argument, so my heuristic doesn't work here.
• The following instance failed to be translated by my version of to_additive:

instance isScalarTower [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S]
  [IsScalarTower R S k] : IsScalarTower R S (MonoidAlgebra k G) :=
Finsupp.isScalarTower G k

The problem is that although it knows to not translate k because it is a semiring, it still thinks that it should translate SMul R S

[Yaël Dillies]

In your example, R appears along with k in IsScalarTower R S k. Since k isn't additivisable, this means that R isn't either

[Yaël Dillies]

That's the only constraint I could find

[Jovan Gerbscheid]

Yes, but the issue is that at that point to_additive has already additivized SMul R S

[Yaël Dillies]

I seriously doubt to_additive can be implemented with a single-pass algorithm

[Jovan Gerbscheid]

My new idea, which is essentially what I had suggested at the start of this thread, is to have a way to tell to_additive which type arguments should not be translated. Then to_additive should treat these local variables the same way as it does constants marked with to_additive_dont_translate.

And I would like it to infer these arguments automatically when possible, so that most of the time you can just write @[to_additive]. And in edge cases like my example above you might need to write [to_additive (dont_translate := R S)] (maybe the logic could be beefed up to do this automatically as well)

[Jovan Gerbscheid]

By only looking at the type arguments, we can still fully support MulOpposite.

[Jovan Gerbscheid]

btw, from the above PR, I've split out a small (general) fix: #28625

[Jovan Gerbscheid]

I have now implemented (half of) my alternative fix at #28637. It implements the (dont_translate := ...) syntax, but doesn't implement any heuristics for figuring out the values automatically. Although I haven't yet tested this for MonoidAlgebra.

[Jovan Gerbscheid]

@Yaël Dillies, another option is that you do both at the same time: refactor MonoidAlgebra while also switching it to use to_additive. You don't need the (dont_translate := ...) heuristic to get started with this. It would just be nice to have. And this would be a good test case for #28637

[Yaël Dillies]

Oh god, that's probably a bad idea review-wise

[Yaël Dillies]

Why do it simultaneously? Is the reason that I'm redefining MonoidAlgebra R M as AddMonoidAlgebra R (Multiplicative M)?

[Jovan Gerbscheid]

No, I just though it could be more efficient

[Jovan Gerbscheid]

In #28637, I have now to_additive-ized MonoidAlgebra, to show that it works, inserting (dont_translate := k) whenever necessary. So, it is ready for review (and I'd be happy to split off the MonoidAlgebra part into a separate PR).

Some issues with additivizing showed up when the MonoidAlgebra and AddMonoidAlgebra theorems don't have the same shape. In particular MonoidAlgebra.of : G →* MonoidAlgebra k G is annoying, as its additive version is Multiplicative G →* AddMonoidAlgebra k G. We may want to consider making it into just a function G → MonoidAlgebra k G.

Additionally AddMonoidAlgebra.opRingEquiv isn't actually the additivization of MonoidAlgebra.opRingEquiv, which is a bit annoying. But it seems that both versions are genuinely being used.