bug in ring?

Stream: mathlib4

[Jireh Loreaux]

@Mario Carneiro is this a bug in ring, or am I misunderstanding something? The call to ring succeeds and closes the goal, but it asks to try ring_nf. So ring1 fails to close the goal, but ring_nf does? I was under the impression that this shouldn't happen.

import Mathlib -- I'm lazy

example (x y : ℝ) : max x 0 + max y 0 + (-(y + x) + max (y + x) 0) -
    (-x + max x 0 + (-y + max y 0) + max (x + y) 0) = 0 := by
  ring -- Try this: ring_nf
  -- also: no goals

[Mario Carneiro]

this can certainly happen, that's why it makes the suggestion

[Mario Carneiro]

in this case it's because you need to unify the x + y and y + x inside max

[Kevin Buzzard]

This is happening to a student of mine. At the end of the day I am very confused why ring can ever both (a) close a goal and (b) tell the user they should be using another tactic instead. My student's work has 5 blue outputs telling them that they should be using ring_nf for no obvious reason. Both ring and ring_nf close all 5 goals. Is this expected behaviour?

[Ruben Van de Velde]

Are they situation where ring works on a subexpression of the goal, not the entire goal?

[Alex J. Best]

I think this is expected, it is maybe also a hint that you are using ring which is a finishing tactic, in a potentially nonfinishing way.

[Kevin Buzzard]

But ring is closing the goals. It's just moaning anyway.

[Alex J. Best]

That's why I said _potentially_ the difference is whether ring is being asked to prove an equality of rings (which it should finish on every time if the goal is a ring identity). Or just normalize all ring expressions it finds as subexpressions of the goal, which may happen to prove the goal but ring has no guarentee of doing so

[Mario Carneiro]

when ring moans about calling another tactic, it also calls that tactic itself

[Mario Carneiro]

it's just saying "you must have called me by mistake, here I'll call that tactic you meant to say but you may as well call that other tactic yourself"

[Kevin Buzzard]

I am very unclear about why ring is telling me that I should not be using it when it is closing the goal.

[Kevin Buzzard]

Is this situation unique to ring?

[Mario Carneiro]

simpa does this too

[Mario Carneiro]

it's basically a lint

[Mario Carneiro]

polyrith too

[Kevin Buzzard]

So I just tell the student to change to the "non-finishing tactic" ring_nf and ignore the fact that it closes the goal despite the existence of this tactic being precisely because we want a non-finishing ring?

[Mario Carneiro]

nf stands for normal form, not non-finishing

[Mario Carneiro]

it can close goals

[Alex J. Best]

Probably if they want to write a very maintainable proof it should be something like congr; ring. Do you have examples you are thinking of?

[Yaël Dillies]

I thought the point of the normal form version of ring was to use it in non-finishing contexts?

[Mario Carneiro]

it is not necessarily finishing

[Kevin Buzzard]

Right! I get the impression that we're told that ring_nf has a second usage, namely to shut ring up when it closes the goal but randomly complains.

[Mario Carneiro]

ring didn't close the goal, it failed and then called ring_nf which closed the goal

[Kevin Buzzard]

ring closed the goal in the sense that I ran ring and the goal was closed.

[Yaël Dillies]

Okay, but then what is ring_nf if not a subprocess of ring?

[Kevin Buzzard]

I don't see the logic here. If you want ring to fail then why not just let it fail?

[Mario Carneiro]

because otherwise you might not realize (1) that ring_nf exists and (2) it closes your goal

[Kevin Buzzard]

By this logic why don't we have every tactic calling ring_nf if it fails?

[Yaël Dillies]

In my mind, ring is a big machine, calling several (sub)tactics, one of which is ring_nf. Is my mental picture wrong?

[Mario Carneiro]

the version that fails and does not play games with ring_nf is called ring1

[Kevin Buzzard]

Great, so let's redefine rw to be try rw; ring_nf and have a new tactic rw1 which is the old rw.

[Mario Carneiro]

This is just like tidy, the simple to call tactic does a bunch of things, maybe more than you really ought to leave in a completed proof

[Mario Carneiro]

as an aside, rw is already doing a similar thing

[Mario Carneiro]

it calls rfl at the end, and you need rewrite if you don't want the trailing rfl

[Kyle Miller]

That's a bit different though, since rw [] solving a goal by rfl doesn't report any suggestion

[Mario Carneiro]

although it doesn't bug you about the difference since it's using a weak rfl

[Eric Wieser]

@Kevin Buzzard, I think the thing to realize is that ring used to not complain at all, but they we decided "actually, it shouldn't be used on these goals at all". Instead of changing it to fail, which would be very annoying for new users, we changed it to complain and tell them to write something eles which is less annoying.

[Alex J. Best]

Kyle Miller said:

That's a bit different though, since rw [] solving a goal by rfl doesn't report any suggestion

it probably should imo

[Kyle Miller]

Maybe when ring calls ring_nf and it succeeds, it should fail with the helpful suggestion that ring_nf would succeed?

[Kevin Buzzard]

If ring is just like tidy then are you suggesting that it should never occur in any mathlib code and should always be replaced by ring_nf, like tidy should be replaced with the output of tidy??

[Mario Carneiro]

ring could certainly dress its suggestion up in the style of a linter warning

[Kevin Buzzard]

Right now the situation is that ring sometimes happily closes goals with no complaints, and sometimes closes goals with complaints, and sometimes doesn't close goals and complains. I think this makes it unique: none of the other suggestions of "tactics which are like ring" above have such a wide range of possibilities.

[Mario Carneiro]

when ring succeeds, it is basically equivalent to ring1 (and it doesn't waste its time doing something else) so there isn't much value in suggesting ring1 there unless you are interested in using it for control flow

[Eric Wieser]

Mario, is my claim above that this was a backwards-compatibility feature correct?

[Kyle Miller]

Mario Carneiro said:

ring could certainly dress its suggestion up in the style of a linter warning

Why a linter warning and not a full error? It seems like ring's suggestion to use ring_nf is more of a pointer to the user for what to try instead, and it's nice of it to try ring_nf for you ahead of offering the suggestion.

[Mario Carneiro]

@Eric Wieser I believe so

[Mario Carneiro]

I suppose it could be an error, although that's an interesting combination of diagnostics

[Mario Carneiro]

since we have an error on top of an info message on top of an interesting final state

[Mario Carneiro]

(the final state is important because it shows the uncancelled terms)

[Kevin Buzzard]

Kevin Buzzard said:

Right now the situation is that ring sometimes happily closes goals with no complaints, and sometimes closes goals with complaints, and sometimes doesn't close goals and complains. I think this makes it unique: none of the other suggestions of "tactics which are like ring" above have such a wide range of possibilities.

Aah, this is false: simpa also has this property (sometimes it will close the goal and tell the user to use simp instead).

[Kyle Miller]

Yaël Dillies said:

In my mind, ring is a big machine, calling several (sub)tactics, one of which is ring_nf. Is my mental picture wrong?

Yes, that's not how it works. The ring1 tactic is monolithic, and all it does is take both sides of an equality, evaluate them into a normal form, and if both sides are the same, it generates a proof of the original equality. The ring_nf tactic uses the internals of ring1 and simp to evaluate subexpressions into a normal form, where it evaluates the expressions into a normal form to rewrite the expression.

Then this is the ring tactic:

macro (name := ring) "ring" : tactic =>
  `(tactic| first | ring1 | ring_nf; trace "Try this: ring_nf")

[Kyle Miller]

Both ring1 and ring_nf share the ring expression normalizer, but ring_nf has code supporting it that ring1 doesn't have.