Try this: ring_nf

Stream: mathlib4

[Dan Velleman]

Sometimes the ring tactic succeeds, but it puts a message saying Try this: ring_nf in the Infoview. What's the reason for this? Is Lean telling me that for some reason I should have used ring_nf rather than ring? If so, why?

[Heather Macbeth]

ring consists of trying two tactics, ring1 and ring_nf. If it succeeds without error, that means ring1 worked. If it succeeds with the blue underline and "try this", that means that ring1 failed but ring_nf worked.

[Heather Macbeth]

So changing to ring_nf according to its suggestion will avoid the wasted work of trying ring1 and having it fail.

[Jireh Loreaux]

The point is that ring is supposed to be a "finishing tactic".

[Heather Macbeth]

ring1 (the "true" ring) only closes equality goals.

ring_nf (the nf is for "normal form") will normalize, without necessarily closing the goal. It also has the useful feature that it normalizes inside function applications, so for example it would solve f (1 + a) = f (a + 1).

[Heather Macbeth]

Anyway, @Dan Velleman is probably interested in teaching applications, and I actually think the difference is not worth stressing in this case. I just tell my students to use it freely and ignore the blue underline -- I wish there were an option I could set to turn it off.

[Mario Carneiro]

the option is macro_rules | `(tactic| ring) => `(tactic| ring_nf)

[Heather Macbeth]

Nice!

[Scott Morrison]

But we can add an explicit option if that is nicer to beginners, too!

[Mario Carneiro]

we could make it a pseudo-linter warning

[Scott Morrison]

Note that there are some places in the library where it seems ring_nf works as a finishing tactic by ring fails. (I just saw these in Quandle.lean, for example.)

[Scott Morrison]

I think maybe ring_nf is getting by with weaker typeclasses than ring?

[Mario Carneiro]

yes, there are some cases where that is true, Heather gave f (1 + a) = f (a + 1) as an example above

[Mario Carneiro]

I don't think it's a weaker typeclasses thing, they have the same backend

[Scott Morrison]

The example I had in mind was here, where

x y z: Dihedral n
⊢ 2 * x - (2 * y - z) = 2 * (2 * x - y) - (2 * x - z)

needs ring_nf (which closes the goal), rather than ring.

[Mario Carneiro]

what instances are on Dihedral?

[Mario Carneiro]

looking at the code I don't see any instances at all, in which case I don't see how you can prove anything. Maybe these are actually - and * on ZMod instead of Dihedral?

[Mario Carneiro]

in any case this is cursed code which is abusing ring_nf and non-canonical instances