Multiplicative variant of the `abel` tactic

Stream: mathlib4

[Robin Carlier]

It looks like there is no tactic like abel for handling computations in commutative multiplicative group/monoids, so I tried to see if I could get a duplicate version of abel called abel_multhat would do the same thing in the multiplicative notations, and the resulting file (also containing the abel tactic) looks like this. As I’m completely new to metaprogramming, there is an awful lot of code duplication and this is basically just a copy of the code of abel with a few modifications here and there.

Would this be too much code duplication to be considered PR-able?

[Johan Commelin]

I thought there were already two PR attempting this...

[Johan Commelin]

One of them is #13233

[Johan Commelin]

The other is #13442...

[Johan Commelin]

We should really get this tactic. But I don't have the meta skills to make this converge

[Robin Carlier]

Oh, I wasn’t aware of these PR. I guess I’ll just wait until one of these get merged. #13233 seems to take the exact same approach that I did anyway. Thanks for digging them up!

[Kim Morrison]

Could we arrange that abel does both?

[Damiano Testa]

I would think that it should be possible, although there might be some choice about what to do when the target involves an expression in a ring, with both additions and multiplications.

[Damiano Testa]

Maybe, defaulting to addition is reasonable and an abel! could also normalize summands?

[Robin Carlier]

When trying to code it, I considered that and thought that defaulting to addition + an optional config option to force the multiplicative mode would be reasonable, but I lack the meta skills to do this kind of things.

[Damiano Testa]

I wonder whether we can leverage to_additive to take care of most of the fluff and simply add a small plug at the end of it all that decides whether it should run add_abel or mul_abel.

[Damiano Testa]

I scanned through the abel file and here is a potential approach:

• write a Syntax-toSyntax conversion that does what to_additive does, but only for the very limited scope of what abel needs;
• multiplicativize everything in abel for which it makes sense to do so and elaborate each definition and the Syntax-converted one;
• extend Context to also keep track of whether the operation is addition or multiplication;
• extend the switch that decides whether you are facing an AddGroup or an AddMonoid, to also allow Group and Monoid;
• put everything together.

None of the steps above looks hard, probably, when you actually start doing it, you will realize that there was more involved, but I think that it should be all relatively straightforward.

Any opinions on this?

[Eric Wieser]

Kim Morrison said:

Could we arrange that abel does both?

Or at least, have mabel and abel call the same underlying TacticM with different configuration