More to_additive issues

Stream: mathlib4

[Richard Osborn]

While porting Algebra.Regular.Basic (mathlib4#758), to_additive has not been finding the correct translations. I can fix most of the problems by giving an explicit name for the additive version of IsLeftRegular and IsRightRegular, but roughly 9 theorems still fail. Should those be duplicated manually for now or is there an easy fix to to_additive? I'm not really sure how to debug such things.

[Damiano Testa]

Hi, I think that I was the author of the file. When I added the to_additive conversion, I also added a dictionary entry to to_additive to convert regular to add_regular and the left/right variants. I cannot see now how to do a similar change for the mathlib4 version of to_additive, but hopefully this explains why the attribute does not find the right name.

[Damiano Testa]

I'm on mobile, so I cannot help much, but these are the mathlib lines that I added:

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/to_additive.lean#L226-L229

[Jireh Loreaux]

Side note: @Richard Osborn just FYI: you marked Algebra.Regular.Basic with a Yes on the port status wiki. The Yes is reserved for PRs that have already been merged, and marking it too early could cause issues. It's not a big deal, I've already fixed it, I'm just informing.