Design of tactics that create side goals

Stream: lean4

[Kyle Miller]

I've been thinking about the way in which rewrite adds side goals due to conditional rewrites to the goal list, and this is a good moment in Lean's development to reflect on the design.

The short version of this message is that I think it would be an improvement if tactics followed the rule "primary goals should be pushed to the front, side goals should be appended to the end".

Background

Recall that if you have a conditional rewrite theorem thm : p -> a = b, then when you do rewrite [thm] with a goal list g1, g2, g3, you get g1', gp, g2, g3, where gp is the goal for condition p. That is, the main goal is modified and the side goals are inserted just after the main goal.

This has the nice property that rewrite [thm1, thm2] is equivalent to rewrite [thm]; rewrite [thm2]. (Note that this is why I'm talking about rewrite instead of rw. It's possible for rw [thm] to close the main goal!)

However, a less-nice property is that rewrite [thm1, thm2] results in g1', gp2, gp1, g2, g3. The side goals are in reverse order with respect to the rewrite order. It's possible to modify the rewrite tactic so that it collects side goals across a full rewrite sequence and then inserts them in the correct order, but then we lose the equivalence between rewrite [thm1, thm2] and rewrite [thm]; rewrite [thm2].

If rewrite were to append side goals to the end of the goal list instead, the equivalence would be preserved and the side goals would appear in the natural order; the running example would result in g1', g2, g3, gp1, gp2.

Considerations

1. For many projects the difference between inserting side goals vs appending side goals doesn't matter — a common tactic-writing style is to disallow using tactics like rewrite on tactic states with more than one goal (you're expected to focus first). The adaptation cost would be to shuffle around proof blocks for side goals.
2. This isn't like constructor or cases, which create new "primary" goals. We're interested in what to do about side goals. Presumably they are lesser in importance and you want to get to them at the end, or otherwise use case ... => to select one and operate on it immediately. (Note about constructor/apply: in some modes you may want to have non-prop "value" goals that appear in the types of other goals to be appended to the end. These are like side goals, perhaps.)
3. The current behavior keeps related goals contiguous, and appending to the end would disrupt that. I would like to hear if anyone relies on this property. This should not affect projects that adhere to the tactic proof discipline mentioned in 1. (Possibly tactic infotree analysis tools may be affected.)
4. I'm considering adding the syntax rewrite [...thms...] by ...tactics.... The idea is that the by block would capture the side goals, to create structured proofs with rewrite. You may think that this would make inserting vs appending an irrelevant point, but appending would mean that side goals appear in the same order, whether or not you use a by clause.

[Kyle Miller]

Some questions

• Would "primary goals should be pushed to the front, side goals should be appended to the end" be a good general rule? Are there exceptions?
• Ignoring by clauses, would it lead to better or worse proof structures?
• Are there tactics where what constitutes a side goal is too ambiguous to be actionable? For example, some tactics create new goals from ?_ placeholders in terms. For rewrite, these are effectively side goals, but for refine these are the primary goals.
• Perhaps what constitutes a side goal needs some configurability? One case study is apply, which by default puts any goals from placeholders after the new primary goals. You can get different goal orders depending on if you write apply thm or apply thm ?_!

I'm interested to hear any other thoughts about this proposed change as well.

[Ruben Van de Velde]

I do have a slight aesthetic aversion to the "unstructured" way that rw deals with side goals; it seems to fit in less well in lean 4 than lean 3. I think I'd generally prefer something like your (4) as the preferred solution.

Side note: it's even more fun when you use rw, in the sense that you can have rw [a, b, c]; rw [d, e, f] which looks like you could merge them, but the first one closes the main goal and the second one deals with a side goal from b

[Kyle Miller]

Yeah, having a good story for "structured rw" in (4) is the main motivation for this question about what to do about the unstructured case. I think it would be rather awkward if you'd need to change the order of tac1 and tac2 depending on whether or not you're using the by clause:

rw [a, b, c] by
  · tac1
  · tac2

(I'm assuming that everyone agrees it would be unacceptable for the by clause goals to come in reverse order!)

[Thomas Murrills]

It would be nice if there were some general way to organize and address side goals specifically, possibly by having some extra (optional) organizing information for goals in the tactic state in addition to the goal list; I’m not sure that order within the goal list alone is sufficient to capture the notion of side goals.

(If that’s on the table, it might also be worth thinking about what tracked information would be necessary to allow deferred goals, as per past discussions, since these could possibly have a common solution.)

[Thomas Murrills]

A past relevant discussion: discussion about possible syntax for addressing side goals, which itself refers to this message

[Kyle Miller]

Let's not explore deferring goals here. It's a fun route to go down, but it's surprisingly complicated, and it's not clear that it would improve the user experience.

If you want, you can look into Rocq's "shelved goal" system. It adds nontrivial complexity to describing the operations of tactics, and to needing to maintain the shelf through your tactic proof.

[Damiano Testa]

In my experience, most of the time, side goals already appear in a very natural order (I follow pretty strictly the "only one active goal at a time"). I very rarely have to rely on apply ... ?_ ... or fapply to massage the order in which side goals are naturally created.

[Damiano Testa]

The main exception for me are indeed long rw chains: their side-goals become tricky to identify.

[Damiano Testa]

I would be very much in favour of keeping side goals in creation order and having them after all the current goals is also a good choice (and maintains the "goals in creation order", which I think is a good default).

[Sébastien Gouëzel]

I would prefer if side goals came first, and the main goal remains last (speaking about the only relevant mathlib situation, i.e., there is a single main goal before the rewrite). The reason is that, in this way, the side goal can be dealt with right away, with bullets, and then you can resume the main argument, unbulleted. Something like

  ... this is quite a long proof
  rw [a, b]
  · one or two lines to deal with side goal of a
  · one or two lines to deal with side goal of b
  resume main proof, still going on for quite long, with a bunch of other rewrites

If the side goals were appended to the end, long proofs would become unreadable with a bunch of goals at the end completely unrelated to what came just before. I would probably use rotate_left to move them in this kind of situation

[Aaron Liu]

I never use rw with leaving side goals, so this is a non-problem for me

[Kyle Miller]

@Sébastien Gouëzel Do I understand correctly that (1) moving the goals to the end would enable rotate_left, which is not currently possible with the current behavior where side goals are inserted right after the main goal, and that (2) you're answering this from the perspective of "what if rw doesn't get by clauses"? Would you not write it in the following way?

  ... this is quite a long proof
  rw [a, b] by
    · one or two lines to deal with side goal of a
    · one or two lines to deal with side goal of b
  resume main proof, still going on for quite long, with a bunch of other rewrites

[Damiano Testa]

Could the behaviour be governed by a sideGoalsFirst option? I would probably prefer side-goals in creation order, and whether or not they appear after the current main goal or after all currently in scope goals is what the option decides.

[Damiano Testa]

Kyle Miller said:

  ... this is quite a long proof
  rw [a, b] by
    · one or two lines to deal with side goal of a
    · one or two lines to deal with side goal of b
  resume main proof, still going on for quite long, with a bunch of other rewrites

For me, this is really great, btw!

[Sébastien Gouëzel]

It is currently possible in mathlib to use rotate_left, because there is one single main goal. In this respect, your suggestion does not make a difference. What I am saying is that, if we are changing the rw behavior, we could also consider putting side goals to the front because, to me, it would be an even better behavior. by would be fine for this, but if it's not needed that's even better.

[Thomas Murrills]

Just to clarify, would the expectation be that each tactic which creates side goals is expected to re-implement the trailing by syntax? I.e., we don't want a generic combinator or something for handling side goals?

[Michael Rothgang]

This situation Sébastien describes is also common for me, both in analysis proofs (e.g. manipulating ENNReal quantities) but also (iirc) in differential geometry. The idiom rw [foo, bar, baz] <;> try assumption specifically to deal with such side goals is somewhat common.

[Kyle Miller]

@Sébastien Gouëzel It's worth mentioning that putting side goals at the front breaks the equivalence between rewrite [a, b, c] and rewrite [a]; rewrite [b]; rewrite [c]. That would also be a very significant breakage; pretty much every proof with a conditional rewrite would need adaptation. I expect that my proposed change has a much smaller impact, at least for mathlib with it's one-main-goal discipline.

There's reason for by beyond convenience. It gives you a way to act on all produced side goals at once, without needing to figure out how to differentiate the side goals from the main goal. You can do rw [a, b, c] by all_goals assumption and be sure that there are no side goals remaining. In comparison, rw [a, b, c] <;> try assumption can lead to strange states when proofs break.

[Kyle Miller]

@Thomas Murrills Yes, at least for now. If a generic solution appears one day, we can switch to it (and probably automate the adaptations too). I want to avoid making the tactic metaprogramming API even more complicated without having a lot of evidence for what a general solution ought to be.

[Michael Rothgang]

reason for by beyond convenience

That sounds like a useful property to have!

[Sébastien Gouëzel]

@Kyle Miller, yes, the suggestion of bringing side goals to the front is maybe something that could be explored if we were starting from scratch, but with the existing code base the refactor would probably be a nightmare for a pretty mild gain, contrary to your suggestion. Your proposal with the by looks like a good intermediate ground!

[Thomas Murrills]

Kyle Miller said:

Thomas Murrills Yes, at least for now.

Makes sense! I'll also clarify my message and mention that I don't necessarily believe strongly that we should have a side-goal combinator; I just wasn't sure what the scope of this discussion was. :)

(It's possible, after all, that the best approach for other tactics is just to provide a convenient, standard API for those who want to implement trailing by syntax; it's also possible that creating a more generic underlying infrastructure here could be worth it for other, indirect benefits it might enable, like the ability to better organize and display goals in the infoview according to their "role". It’s definitely not clear at the moment.)

[Chris Henson]

@Kyle Miller I think your statement:

Perhaps what constitutes a side goal needs some configurability?

is potentially valuable. Especially with trying to use grind more lately, I find myself spending more time than I'd like structuring proofs in a way that I can finish with all_goals grind, which can be awkward depending on where something like refine places a goal. If a new best practice is decided upon for working with side goals, I think the docs for grind in the reference manual is one good place to mention it.