Tactic wishlist: Abel

Stream: metaprogramming / tactics

[Sam Ezeh]

The tactic wishlist has an entry for supporting muliplicative structures in the abel tactic, could I work on this? https://github.com/leanprover-community/mathlib4/issues/10361

[Kyle Miller]

I think so.

Do you have a plan for how to support multiplicative structures? I would suggest making a new tactic that takes an equation for multiplicative structures and converts it into one for additive structures (using docs#Additive) and then making another tactic, maybe call it mabel, that applies this new tactic and then runs abel. The goal here is (1) to make small composable tactics that could be useful on their own and (2) to re-use abel without needing to re-implement any of its functionality, which makes maintenance much easier.

[Kevin Buzzard]

I think that the name of the tactic alone is a great reason for working on this. I'm still disappointed that we don't have ratify.

[Sam Ezeh]

Kyle Miller said:

Do you have a plan for how to support multiplicative structures?

My initial idea was to build on the abel tactic directly by updating the parser and adding the normalisation rules for the multiplicative case. I think your idea is much more sensible

[Yury G. Kudryashov]

Kevin Buzzard said:

I think that the name of the tactic alone is a great reason for working on this. I'm still disappointed that we don't have ratify.

You can easily declare an alias for rify (AFAIR, we have it).

[Sam Ezeh]

https://github.com/leanprover-community/mathlib4/pull/13442 I wrote this draft this morning

[Sam Ezeh]

I need to support the mabel at h syntax but I don't know how to do this.

syntax (name := to_additive) "to_additive" (location)? : tactic

results in unknown parser declaration/category/alias 'location'