Closing after `rw`, `conv`: `eq_refl` instead of `rfl`

Stream: lean4

[Joachim Breitner]

The tactics rw and conv, besides rewriting the goal, also try to close “trivial” goals.

Right now, rw uses try with_reducible rfl, and conv uses try rfl.

(Reminder: rfl is a macro that tries multiple tactics, including eq_refl, which is essentially exact Eq.rfl, and
apply_rfl, which uses @[refl] to solve goals in other relations, like Perm xs xs).

I think this can be refined:

• It seems more predictable if the rewriting-like tactics rw and conv consider the same goals “trivial”.

• I’d argue that it’s not natural for conv or rw to solve non-Eq-goals like Perm xs xs – conv or rw have nothing to do with Perm, so why should it tryexact Perm.rfl, but not other ways to close “trivial” goals (e.g. assumption). So these tactics should maybe use eq_refl instead of rfl, and when necessary the user has to close the goal explicitly with rfl or exact Perm.rfl.

• It may be ill-advised to run try eq_refl (or try rfl) in tactics without with_reducible. It may take a lot of unfolding until it is clear that a goal isn’t reflexive. This is probably why rw uses with_reducible, so conv should probably too. In the cases where this currently doesn't close the goal, the user will have to follow conv with an explicit rfl, but maybe that’s ok, given that something “nontrivial” happens then?

I did an experiment in conv changing try refl to try eq_refl, and the fallout in mathlib was okish. I had to add a few exact Iff.rfl aftewards, but only few other relations (Perm, Associated.refl, le_rfl), and for the latter at least I find it preferable to have that as a separate step.

I’m less sure about exact Iff.rfl. Given that rw can rewrite with Iff as well, it seems natural that it would consider Iff P P a trivial goal. And by the first point above, then also conv should do so. Maybe here the pragmatic thing is to let eq_refl (and thus MVarId.refl) handle Iff in the same built-in manner. This comes at little extra cost.

How does this sound? What did I miss?

Pinging @Mario Carneiro and @Scott Morrison , since this is related to a few disjoint threads of conversation.

[Damiano Testa]

My personal view is that more automation is an improvement. So, I am not too thrilled about weakening tactics that currently do their job well. In case this is something that is desirable for other reasons, would it still be possible to access the current behaviour via something like rw!?

For a point of comparison, notice that rewrite is essentially non-existent in mathlib and I wonder whether the "new" rw would also be similarly non-existent.

[Damiano Testa]

So, casting this more positively: bring on the same strong rfl for both rw and conv!

[Yaël Dillies]

Joachim Breitner said:

• I’d argue that it’s not natural for conv or rw to solve non-Eq-goals like Perm xs xs – conv or rw have nothing to do with Perm, so why should it tryexact Perm.rfl, but not other ways to close “trivial” goals (e.g. assumption). So these tactics should maybe use eq_refl instead of rfl, and when necessary the user has to close the goal explicitly with rfl or exact Perm.rfl.

I think it's very natural to the extent that on paper a sequence of rewriting ends when the LHS and RHS are the same.

[Joachim Breitner]

I understand that point of view. But if the stance is “more automation is better”, wouldn't you then simply expect every tactic to implicitly run try trivial in the end? So why rfl and not something else?

[Yaël Dillies]

... because that's what closes goals of the form LHS ~ RHS when LHS and RHS are the same?

[Yaël Dillies]

On paper, you don't say "and now we are done because the LHS and RHS are the same", but you do say "and now we are done by assumption".

[Damiano Testa]

Joachim Breitner said:

I understand that point of view. But if the stance is “more automation is better”, wouldn't you then simply expect every tactic to implicitly run try trivial in the end? So why rfl and not something else?

I thought that the limitation to "trying every tactic all the times" was mostly an issue of slowing down. I personally would be very happy if automation could tell me quickly "I can take over from here!".

[Damiano Testa]

Thus, I view it as a delicate balance between having a good response time and a good automation. After all, with most trivial lemmas, I normally try aesop first, just in case... if Lean did that in the background, that would be awesome!

[Damiano Testa]

Maybe it could be an option that you can switch on/off, something like set_option fancyRw true and then you get the current behaviour and otherwise you use the better-performing, but less conclusive weaker rw?

[Damiano Testa]

Btw, in Lean 3 there was a misuse of simpa that meant that simp; rfl could be replaced by simpa: I know that Mario did not like this, but those who knew about this "bug" used it liberally... until they were caught out!

This is to say: I suspect that in mathlib, a trend is to try to avoid seeing rfls as much as possible.

[Siddhartha Gadgil]

Damiano Testa said:

Thus, I view it as a delicate balance between having a good response time and a good automation. After all, with most trivial lemmas, I normally try aesop first, just in case... if Lean did that in the background, that would be awesome!

Bumping this one last time: there is a PR for Lean (with Mathlib) to do this in the background and this has been open for months.

Assuming this dies again, in a few days I will try to make a minimal dependency repo so users can use it with/without Mathlib and also while developing in Mathlib (I hope).

[Patrick Massot]

I think it’s difficult to have this discussion without any information about the actual speed difference.

[Joachim Breitner]

I admit for me the appeal isn’t (just) performance, but predictability and orthogonal building blocks – why should conv even close a goal at all. But I do understand that having to writing rfl is tedious and pragmatically it’s nice if you don’t have to.

I’ll run a speed center run to see if using eq_refl instead of rfl shows up. But I doubt it, it’s not that much on a hot path. I am worried a bit more if a user might run into a situation where try rfl blows up because it unfolds things it shouldn’t, and then they can’t use conv anymore. (I guess they can work around it with with_reducible conv…).

I might not have peeked into this rabbit hole if there was a single commonly accepted tactic for “do trivial things we don’t want to see”, and that tactic was used by rw and conv etc. consistently (maybe trivial was intended to be this, although it seems too expensive to run unconditionally and opportunistically). Or is there a good reason that rw and conv each try a different tactic that I missed?

[Damiano Testa]

For me, the main motivation is that, very often, rfl, by rfl, exact rfl, trivial, tauto, aesop are all a replacement for something that on paper is "and we are done" (or, better, "and now we are really done").

[Kyle Miller]

I think it makes sense doing a light trivial at the ends of tactics to close the goal in obvious cases for tactics that cannot close goals themselves, and closing in a predictable way.

A full trivial is not very predictable, since it depends on the local context. The tactic should look at just the thing that was rewritten to see if it can close the goal.

I looked at simp and dsimp as well to see how they close goals when operating on the target.

1. simp checks to see if the goal is True, and if so, closes it with True.intro.
2. dsimp (1) does the True check and (2) it does its own "try with_reducible exact rfl"

The simp tactic doesn't need to do (2) since reflexivity of Eq is already a simp lemma.

When simp and dsimp act on hypotheses, instead they both simply look for False and if so close the goal using False.elim.

[Kyle Miller]

I think rw should, like simp and dsimp, also close goals if the result after rewriting is a True or False, depending on whether it's in the target or a hypothesis.

[Joachim Breitner]

So trivial isn’t trivial enough :-)

[Kyle Miller]

I also think it makes sense for rw (and perhaps dsimp too!) to be aware of other reflexive relations and be able to close those. Think about rewriting x + x ≤ 2 * x to 2 * x ≤ 2 * x. Should I really need to do rfl after this?

[Joachim Breitner]

Would you want apply or refine to also do this try really_trivial? Or by what criteria do we decide which tactics should and which shouldn’t close trivial goals?

[Kyle Miller]

Those tactics should always have a tactic coming after them, so I don't think you'd expect them to finish automatically.

[Kyle Miller]

The theory I'm going by is that with rw you could use it to reduce an expression to True in principle, but there are a few sorts of obvious stopping points where it's not expensive to have the system finish up.

[Kyle Miller]

And also, rw can't close the goal itself.

[Joachim Breitner]

Hmm, simp, rw and conv, by their own, even more so have always a tactic coming, because they just rewrite the goal. The trivial-closing functionality is bolted on and independent of their core functionality, so I don’t yet see how they are different from other tactics.

[Kyle Miller]

apply and refine can close the goal themselves

[Kyle Miller]

Speaking of conv, I think of that being more in the "simp family" since it's a way for the user to apply the congruence lemmas that simp uses to navigate into expressions. If it's like an interactive simp, then it's justified having it close the goal like simp/dsimp. A full try rfl is way too much without any reducibility restriction, I think.

[Joachim Breitner]

Ok, then I misunderstood “Those tactics should always have a tactic coming after them”.

Maybe the point is that apply and refine are more low-level and closer to “constructing proof terms”, so more automation would be strange here.

[Damiano Testa]

To take this to an extreme, I would be surprised by closing a goal with refine ?_.

[Kyle Miller]

There are two things I'm saying about apply and refine:

1. They're able to close the goal themselves, unlike rw
2. Generally, you use refine to set up specific goal states. It would be very confusing if any of your ?_'s did not appear afterwards. For apply, there's more leeway for auto-closing goals, and it might be appreciated, so long as it's not for any explicit ?_s

[Joachim Breitner]

A full try rfl is way too much without any reducibility restriction, I think.

Ok, sounds like it would be worth to at least change try rfl to try with_reducible rfl, to make it behave more like rw and dsimp.

[Damiano Testa]

Speaking of unexpected behaviour, this is a valid proof:

example (a b : Nat) (h : a = 0) : b = b := by
  rw [] at h

[Damiano Testa]

(I wonder whether the form rw at would find my support for not try any form of rfl after itself.)

[Kyle Miller]

I think the way rw does a blanket with_reducible rfl is not great. Ideally, it would only look at the thing being rewritten and use that to close the goal. There's no rewrite going on here, so I suppose it wouldn't even look at h

[Kyle Miller]

Your idea makes sense. If there's no at clause, or if |- doesn't appear in the at clause, then don't do with_reducible rfl.

[Ruben Van de Velde]

I like it a lot, perhaps just because I'm used to it. But agree that it only makes sense when rewriting the goal

[Kyle Miller]

If there is an at clause, then it could also try using False.elim on each mentioned hypothesis.

[Damiano Testa]

Yes, I can get behind the try rfl only when the goal is involved in the rw.

[Damiano Testa]

Honestly, I would be curious to know where in Mathlib there are rw at [not the goal] that actually close the goal.

[Kyle Miller]

Ruben Van de Velde said:

I like it a lot, perhaps just because I'm used to it. But agree that it only makes sense when rewriting the goal

Could you clarify if you're disagreeing with anything here? Are you saying you like how rw closes the goal even if you didn't operate on the goal? (And if so, why you wouldn't do rfl instead?)

[Ruben Van de Velde]

I like that it tries (weak) rfl when operating on the goal

[Kyle Miller]

Ok, I thought "it" might have been Damiano's example.

[Damiano Testa]

I think that very few people would find rw [] at h as an idiomatic way of doing rfl.

[Kyle Miller]

One more tactic to think about is rwa, which intentionally does assumption at the end (one of the tactics that trivial tries).

There's a bit of a bug since rwa does rw and then assumption, so it's possible to have it apply to the wrong goal. I guess rwa should focus on the main goal first?

[Mario Carneiro]

Damiano Testa said:

I think that very few people would find rw [] at h as an idiomatic way of doing rfl.

Note, this is something we can lint

[Mario Carneiro]

I much prefer it when tactics have regular behavior, even if that behavior is silly sometimes, and we use linters to catch the case where silly behavior is exploited directly

[Damiano Testa]

In fact, I would say that rw [] (at ...)? should be disallowed, just like "simp made no progress".

[Mario Carneiro]

I don't agree, it means you can't just split a rw into pieces anymore

[Damiano Testa]

You can if the pieces perform at least one rw...

[Mario Carneiro]

I'm very glad it wasn't syntactically disallowed like so many other "1 or more"'s in lean

[Mario Carneiro]

because it is often the first step in deciding what to rewrite with

[Mario Carneiro]

and I don't want the goal to be obscured at that point by a silly error I don't care about

[Damiano Testa]

Ah, I am happy that it is syntactically allowed, but it should still trigger some warning in final code.

[Mario Carneiro]

again, linters

[Damiano Testa]

If the unused tactic linter were faster, that could be a job for it...

[Damiano Testa]

And then, also the "simp made no progress" would be caught by a linter.

[Mario Carneiro]

that one is a bit different, there would be fallout from that change (as there was when changing it to fail in the first place) because it affects tactic control flow

[Mario Carneiro]

but it would be nice to have a linter if you have a try simp (or even try tac in general) block which always fails and hence does nothing

[Mario Carneiro]

but I guess your linter would also pick that up?

[Damiano Testa]

Yes, those "unused try ..." get caught.

[Damiano Testa]

Basically, any time that the goals do not change, the linter tells you.

[Damiano Testa]

("Change" is conservative, in that it picks up on non pp-differences, since it looks at the mctx before and after each tactic application)

[Joachim Breitner]

Joachim Breitner said:

I’ll run a speed center run to see if using eq_refl instead of rfl shows up. But I doubt it, it’s not that much on a hot path. ```
I still can’t really read these reports, but looks like there isn’t much happening with that change:
http://speed.lean-fro.org/mathlib4/compare/15cb8470-fe7e-433b-b297-f5fd49de63a1/to/58cf4f76-662f-46e2-8f38-68d0457b2d89

[Floris van Doorn]

Btw: I am very much in favor of weakening conv's behavior to only apply reflexivity reducibly. Personally I think we shouldn't match things up to semireducible transparency if there is a reasonable chance that it will fail (in a proof script that itself works).

[Joachim Breitner]

Thanks, good to know. That’ll also make conv match rw’s behaviour. I’ll try that today (https://github.com/leanprover/lean4/pull/3763).

[Ruben Van de Velde]

Maybe rfl itself should be weaker and we should have rfl! for the more aggressive one

[Joachim Breitner]

That’s worth exploring. Although for interactive use, rfl is fine, I’d say – you notice when it’s slow, and you usually only leave it in when it works. It’s mostly hidden uses in other tactics, with backtracking, where a possibly slow and failing run can remain and slow everything down.

[Floris van Doorn]

I agree with Joachim: if the user explicitly requests to do something, then we should try harder (i.e. up to semireducibility).

[Joachim Breitner]

Joachim Breitner said:

Thanks, good to know. That’ll also make conv match rw’s behaviour. I’ll try that today (https://github.com/leanprover/lean4/pull/3763).

Here is the impact on mathlib:
https://github.com/leanprover-community/mathlib4/compare/nightly-testing...lean-pr-testing-3763
Nothing surprising, just a bunch of proofs where after conv the goals weren’t syntactically equal, but some amount of reduction was needed. Not unreasonable to require an explicit rfl to say “and now solve by defeq”, I’d say.

Nothing exciting happening in the speedcenter.

With @Floris van Doorn and @Kyle Miller in favor of applying reflexivity only reducibly, unless someone complains, I’ll go ahead with this in a while