Kinds of goals closed by rw/simp only/simp

Stream: lean4

[Sebastian Ullrich]

We taught our students the tactics mentioned in the title among others today, and there was some confusion over which tactic closes which kind of goal implicitly. Intuitively we might think "rw is weaker than simp only is weaker than simp", but this is not true in that regard:

• rw uses "cheap refl" in the end, that is, try (withReducible rfl)
• simp only tries True.intro
• simp also tries True.intro only, but since there is a refl-like [simp] theorem, it can close as much as rw

If we want to present rw as a "manual simp", in particular as a safe non-terminal tactic, it seems like it should not have this automatic final step. What do you think? Would it be bothersome in your experience to add an extra rfl below a terminal rw?

[Markus Himmel]

Maybe one could have rwr which is like Lean 3 rwa except that it does rfl instead of assumption?

[Sebastian Ullrich]

But rfl is so much shorter to write out than asssumption... :)

[Sebastien Gouezel]

I think Kevin disabled the rfl at the end of a rewrite in his number theory game because his students could not understand what was going on. I agree that it is reasonable.

[Patrick Massot]

Sebastian, is the refl tactic renamed rfl in Lean4?

[Patrick Massot]

(I just want to be sure we're talking about the same thing).

[Sebastian Ullrich]

Ah, yes, it is. This one is not extensible (yet).

[Kevin Buzzard]

Lean 3's refl tactic also closes P <-> P goals, which Lean 4's rfl doesn't. I disabled cheap rfl after rw in NNG not because I was against it, but because I made an active decision not to talk about definitional equality, so x + 0 = x isn't refl in the eyes of the user (in fact we get occasional bug reports complaining that refl closes this when it shouldn't). I really like cheap refl after rw when I'm actually coding, but I would be just as happy to have rwr doing this (in fact perhaps rwr could try harder with refl if we go down this route, because I sometimes have to do rw, refl in Lean 3).

[Mario Carneiro]

I don't think rw should lose the "cheap refl" at the end, or that it should be renamed to rwr. But changing it to not do the cheap refl for educational purposes, like Kevin's NNG rw, seems fine

[Sebastian Ullrich]

@Mario Carneiro I'm not sure I fully understood you, do you mean a different rw should be used in teaching?

[Mario Carneiro]

yes, that's what NNG does

[Mario Carneiro]

once you think the students are comfortable with rw enough that having implicit extra behavior isn't too magical you can take off the training wheels

[Mario Carneiro]

In fact I think the general technique of using curated and possibly simplified versions of lean tactics for the purposes of teaching is a very good idea. Lean is really complicated if you have to tackle all of it at once

[Sebastian Ullrich]

Yes, but ideally I would hope that can be achieved by simply not introducing the advanced tactics, or advances versions such as pattern intro, in the beginning. I still think a clear "power hierarchy" of rw/simp only/simp would be a good design beneficial to both beginners and advanced users.

[Mario Carneiro]

In that case, perhaps simp only should support cheap rfl

[Mario Carneiro]

it is a bit annoying to have to add eq_self_iff_true anyway

[Mario Carneiro]

which has become more visible in mathlib since we started squeezing our simps

[Sebastian Ullrich]

Yes, that would also work. I think it would be fine for education.

[Johan Commelin]

We could have simp ONLY!! [foo, bar] for the very restrictive version (-;
In case someone really doesn't want eq_self_iff_true by default.

[Sebastian Ullrich]

image.png

[Kevin Buzzard]

We noticed that people were confused by rw not closing refl goals in NNG and then when they switched to real Lean suddenly it was, and at the time this was flagged as a potential downside of my rw hack. However NNG came from about a year of experimenting on mathematics undergraduates (this was the original version, and I watched a lot of people working through that stuff) and finding out what worked best for them, and the approach of hiding definitional equality seemed to win out.

The other hack in NNG tactics was that induction in goals like 0 + x = x would give you base case goals like 0 + zero = zero which again was unsurprisingly found confusing, so there was a lot of rewriting nat.zero to 0 behind the scenes.

[Sebastian Ullrich]

@Kevin Buzzard Just to make sure we're on the same page, note that Lean 4's "cheap refl" would not close x + 0 = x since Nat.add is not reducible

[Mario Carneiro]

Lean 3's doesn't either btw

[Mario Carneiro]

example (x : ℕ) : x + 0 = x := by rw [] -- fail

[Jasmin Blanchette]

Sebastian Ullrich said:

Would it be bothersome in your experience to add an extra rfl below a terminal rw?

For what it's worth, the corresponding tactic in Isabelle/HOL, subst, does not automatically call rfl, and that never seemed to bother anybody.

[Kevin Buzzard]

It surely closes 0 + 0 = 0, maybe that's what I was remembering

[Mario Carneiro]

so it does, that's odd

[Kevin Buzzard]

rw add_zero -- "huh"?

[Mario Carneiro]

I think it would be cool if rw used cheap (or even not cheap) refl at the end, if it is the last tactic in the branch. I don't know if the tactic parsing framework is able to determine this though

[Kevin Buzzard]

I remember now, even rw add_zero doesn't close x + 0 = x in NNG, that's the behaviour I wanted. People are so confused by rw, they can't tell the difference between it and apply, like some maths students can't tell the difference between $\implies$ and $=$ when they come to university, the terms are kind of used vaguely at school and sometimes interchangeably. [I am now reminded of a stroppy letter I wrote to my daughter's teacher when she was about 8]

[Mario Carneiro]

I think apply is a vague word in mathematics though, it means "use this theorem somehow"

[Mario Carneiro]

lean's interpretation of apply is a bit too constrained

[Sebastian Ullrich]

Mario Carneiro said:

I think it would be cool if rw used cheap (or even not cheap) refl at the end, if it is the last tactic in the branch. I don't know if the tactic parsing framework is able to determine this though

This sounds easy when you only consider branches, but much harder if you also want to propagate a sensible "terminal" flag through combinators. I believe the result would be more confusing than the status quo. A separate tactic name would be a cleaner solution.

[Mario Carneiro]

Indeed, I think it doesn't match the tactic architecture itself. If the number of goals returned by the tactic was enforced in the type system, like in HOL, then it would make more sense

[Marc Huisinga]

I don't think of rw as a terminal tactic, so I'd be in favor of it not closing cheap rfl goals. Is an extra rfl at the end really that inconvenient?

[Marc Huisinga]

Then again, I can see that it might be slightly annoying if then almost every proof case ends with rfl, which I guess some might consider as noise.

[Johan Commelin]

I really like by rw [lem1, lem2] in calc blocks, short and easy and fits on the same line as the calculation step.

[Johan Commelin]

If it becomes by rw [lem1, lem2]; rfl those 5 extra chars will cause line overflow in some cases

[Johan Commelin]

I wouldn't mind avoiding that

[Marc Huisinga]

Johan Commelin said:

I really like by rw [lem1, lem2] in calc blocks, short and easy and fits on the same line as the calculation step.

This seems like something that calc in particular could add, right?

[Johan Commelin]

Aah, I see. It wouldn't be very uniform though

[Gabriel Ebner]

It's not just calc block though, there are lots of lemmas like lemma foo : a = b := by rw [one, two, three]. Requiring rfl at the end is really cumbersome.

[Sebastian Ullrich]

@Johan Commelin Another aspect to consider, if a) simp was much cheaper in general, and b) squeezing it into simp only was only a Code Action away, do you think you would use rw as often as today? Because I believe Isabelle users would probably default to simp in these cases.

[Sebastian Ullrich]

It will be interesting to see how important/effective squeezing will be in Lean 4 in general. The discrimination trees fundamentally change the whole scalability issue.

[Gabriel Ebner]

rw does a lot of things that simp doesn't: 1) it rewrites in the specified order (which is important if you go against the grain), 1b) it rewrites only once, 2) it can open extra subgoals.

[Mario Carneiro]

simp only is also important for maintaining predictability/robustness in the face of new additions to the simp set

[Gabriel Ebner]

(Type-theory issues aside where rw works but simp doesn't.)

[Mario Carneiro]

(this is summarized in the "no nonterminal simp" rule)

[Sebastian Ullrich]

Oh, nonterminal simps should definitely be squeezed of course

[Sebastian Ullrich]

@Gabriel Ebner Do you have a feeling for how often these features are used in terminal rws? Also not sure off the top of my mind if Lean 4 simp can actually open new goals.

[Mario Carneiro]

I find rw generally easier to control than simp, for the reasons gabriel mentioned

[Mario Carneiro]

but I don't think there is a significant prejudice for one over the other where they both apply

[Gabriel Ebner]

Opening new goals typically does not happen with non-terminal rws. But still, having to write by rw Nat.sub_add_cancel; rfl; ... is cumbersome and noisy.

[Mario Carneiro]

I wouldn't mind having rwr for rewrite and then not-cheap refl, but I generally dislike tactics whose only purpose is to be two tactics in a row

[Sebastian Ullrich]

Probably terrible idea: instead of having tactics speculatively close goals, use an extensible set of tactics at done (which is implicit at the end of a "terminal" tactic block) to do so instead. Then at least you really don't pay for the feature unless you use it.

[Mario Carneiro]

is this like my suggestion about doing it only for the last tactic in a block? How is the position detected / communicated?

[Gabriel Ebner]

Sebastian Ullrich said:

Also not sure off the top of my mind if Lean 4 simp can actually open new goals.

This doesn't seem to work, even if I explicitly name the metavariable:

axiom Nat.sub_add_cancel {m n : Nat} (h : m ≤ n) : n - m + m = n

example (h : m < 10) : 10 - m + m = 10 := by
  rw Nat.sub_add_cancel
  exact Nat.leOfLt h

example (h : m < 10) : 10 - m + m = 10 := by
  simp only [Nat.sub_add_cancel ?m]
  -- simp makes no progress here
  exact Nat.leOfLt h

[Sebastian Ullrich]

Mario Carneiro said:

is this like my suggestion about doing it only for the last tactic in a block? How is the position detected / communicated?

The block itself would do it, not the last tactic. Which is simpler and more robust (we only call the tactic set when we know we would otherwise fail with "unsolved goals" anyway), but means the last tactic can't influence what to try.

[Mario Carneiro]

ha, so we will see proofs by example : true := by?

[Sebastian Ullrich]

Only if we allow that syntactically :)

[Sebastian Ullrich]

As I said, it's probably a terrible idea

[Gabriel Ebner]

I could get behind writing {} instead of {refl}.

[Mario Carneiro]

Having things that run on close isn't that unusual, it's supported in lean 3 as well, although it is only actually used in custom tactic blocks like smt_tactic

[Johan Commelin]

Mario Carneiro said:

ha, so we will see proofs by example : true := by?

How is this worse than example : false -> true.?

[Mario Carneiro]

Did I mean to suggest I disliked the pattern? It's fine, just a bit odd

[Mario Carneiro]

in fact, since example : false -> true. doesn't work anymore in lean 4 I will have to find a new favorite and that one looks like a candidate

[Sebastien Gouezel]

Having tactics run on the end of a proof is standard in Isabelle, and very convenient to close all remaining trivial goals.

[Sebastian Ullrich]

@Sebastien Gouezel If you don't specify an explicit one after qed, it uses assumption only, no?

[Sebastien Gouezel]

Yes, I think so -- but qed (auto) is a very standard idiom.

[Sebastian Ullrich]

Since there is no token at the end of a proof block anymore anyway, we can add qed as a macro for allGoals in Lean 4 :grinning_face_with_smiling_eyes:

[Mac]

Just to throw in my own two cents: I like the idea of rwr. I do have qualms with auto-closing "trivial' goals at the end of a proof without some kind of marker (such as a qed) that you are doing so though. My design philosophy is to minimize implicit magic as much as possible.

[Jeremy Avigad]

IIRC, SSReflect has a simple done tactic that you can invoke in places by writing //. So for example you can write

  rewrite foo bar baz //

and the done would be invoked at the //. Again IIRC, it was a try tactic, so there was no harm if it failed. rewrite would sometimes open up new subgoals (with conditional rewrites), and this was a way you could close them off and then keep going after the //.

(Georges Gonthier was a master of optimizing the number of things that can be accomplished with a single 80-character line of SSReflect code.)

[Jeremy Avigad]

Docs:
https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#an-extended-rewrite-tactic
https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#simplification-items