to_additive and smul

Stream: mathlib4

[Scott Morrison]

I haven't looked into this closely, but I'm hoping e.g. @Floris van Doorn may be able to give a quick answer here.

There are some missing to_additive attributes in Mathlib/Algebra/Group/Defs.lean, e.g.

-- TODO restore @[to_additive zsmul_eq_smul]
@[simp]
theorem zpow_eq_pow (n : ℤ) (x : G) : DivInvMonoid.zpow n x = x ^ n :=
  rfl

These attributes don't work, I think because of the switched order of arguments. What is the status of this? Do we need more support from to_additive? Or are there just some attributes missing elsewhere?

[Mario Carneiro]

This required an extension in to_additive, I recall it used to not work in mathlib either

[Floris van Doorn]

In mathlib3 it seems to work. Maybe @Edward Ayers can give an overview of the missing features / known bugs in @[to_additive]. I haven't watched it closely after he took over.

[Edward Ayers]

All of the features of to_additive from the lean3 version should be present (if not correct) in mathlib4. So we have all the attributes like to_additive_reorder and so on that are needed for the fiddly cases like pow → smul. I can't debug Scott's example above but there should be an attribute that can be added to help, maybe to Pow.

But there are going to be bugs because the rules for converting are quite subtle. There are also some issues with how number literals work that needed to be modified. I am also worried that it won't work right for heterogeneous versions of the operators. I got it working on most of a ported lean3 unit test file and the basic group theory lemmas that were in mathlib4 at the time, with the hope that more bugs would arise as people use it.

Relevant PR: https://github.com/leanprover-community/mathlib4/pull/234