ring vs ring_nf

Stream: mathlib4

[Patrick Massot]

I think I still don't understand the semantic distinction between ring and ring_nf. Why is Lean complaining in

import Mathlib.Tactic.Ring

example (a b : ℤ) (f : ℤ → ℤ) : f (a*b) = f (b*a) := by ring

I understand that Lean complains because ring1 fails and ring_nf doesn't. But why do we need to bother the user with that?

[Scott Morrison]

The idea here is that in this situation ring is doing some amount of failed work to close the goal, which is then thrown away and we start over again with ring_nf. So potentially this replacement is a speed-up.

[Scott Morrison]

I agree it is annoying to be hassling the user about this.

[Scott Morrison]

A possible compromise could be to count heartbeats, and not bother telling the user anything if ring failed fast anyway. But that is starting to get messy.

[Mario Carneiro]

It's not an equality in rings, I think it is important to fail to set the expectations for what this tactic is supposed to do

[Patrick Massot]

The why does ring_nf succeeds?

[Kevin Buzzard]

Yeah I guess one could argue that making ring do this is "mission creep"

[Mario Carneiro]

ring is not a kitchen sink tactic and I will try to prevent it from becoming one

[Mario Carneiro]

ring_nf does normalization of commutative ring subexpressions

[Scott Morrison]

This is not to say we can't add a kitchen sink wrapper, for teaching and demo purposes. by its_just_rearranging_from_here.

[Mario Carneiro]

roughly, you can think of ring_nf as simp [ring], if that was a thing you could do

[Mario Carneiro]

Scott Morrison said:

This is not to say we can't add a kitchen sink wrapper, for teaching and demo purposes. by its_just_rearranging_from_here.

Or even for general use, e.g. as a plugin for tidy

[Scott Morrison]

Maybe even call it algebra, and have it delegate out to ring, group, noncomm_group, abel, linarith.

[Scott Morrison]

Not sure whether it should default to silence or printing a Try this, with the other alternative behind a ! or a ?.

[Patrick Massot]

Writing Try this behind a ? seems more natural.

[Heather Macbeth]

Note:

import Mathlib.Tactic.Ring

-- `ring1` normalizes exponents, the mathlib3 `ring_exp`
example : 2 ^ (a + 3) = 8 * 2 ^ a := by ring1

-- `ring_nf` normalizes ring expressions inside function applications, even iterated at multiple levels
example (f g : ℕ → ℕ) : g (f (2 ^ a * 2 ^ 3) + 3) = g (3 + f (8 * 2 ^ a)) := by ring_nf

[deleted bad example]

[Heather Macbeth]

For a really useful normalization tactic,it would be nice to figure out a principled combination of ring1's ability to normalize exponents and ring_nf's ability to normalize all levels of commutative ring expressions involved.

[Heather Macbeth]

Actually, scratch that, I think ring_nf also deals with exponents -- I didn't test my example properly. Sorry for underestimating you, ring_nf!