rename abel1 -> abel, abel -> abel_nf

Stream: general

[Scott Morrison]

By analogy with ring and ring_nf, since the term ordering in abel is slightly arbitrary, I wonder if we should promote abel1 (which closes equality goals) to abel as the main tactic, then have abel_nf as the tactic that rewrites into normal forms.

[Mario Carneiro]

Isn't there a ring1 as well?

[Mario Carneiro]

Ah, ring in mathlib is just a wrapper around ring1 with a fallback to use ring_nf and complain that you didn't call it directly

[Scott Morrison]

Ah, okay, so actually to make them parallel, we would leave abel1 alone, move abel to abel_nf, and add a new abel

[Scott Morrison]

Mostly I'm just curious how much we actually need abel (rather than abel1).

[Mario Carneiro]

ring_nf has basically exactly the same issues as abel_nf

[Mario Carneiro]

but it gets a surprising amount of use

[Mario Carneiro]

I originally added it only for debugging purposes

[Scott Morrison]

So far I'm failing to find places in mathlib where abel1 isn't enough. People are apparently good about using it correctly. :-)

[Scott Morrison]

Oooh, I found a non-terminal use, in algebra/star/chsh.lean, and it's my fault. :-)