linting against "multi-goal proofs"

Stream: mathlib4

[Damiano Testa]

I wrote a simple linter for warning when a proof "should" be structured using ·. You can see some of the effects of the linter in #12338.

The actual linter PR is #12339.

[Damiano Testa]

The main question is: do you find that these changes are an improvement?

[Damiano Testa]

As a disclaimer, there was no explicit bias regarding which proofs to modify: I more of less went from the latest lint warnings and climbed my way up for a while.

[Johan Commelin]

To me, these changes seem a huge net improvement (even if there might be some edge cases).

I also think that new users will be happy to receive some guidance with structuring their goals, as we've seen that it may lead to confusing situations otherwise.

[Joachim Breitner]

I concur. Rocq also has an option that forces strict subgoal handling.

I think I wish that we had syntax that clearly distinguishes the side conditions created by rw from the continuation of the proof (if any), asserts the number of side conditions created, allows me to discharge them first, and continue with the main goal afterwards. Something like

  rw [lem1, lem2] using
    . proof of side condition 1
    . proof of side condition 2
  next step in main proofs

where after using I see only side condition (great for all_goals).

[Damiano Testa]

Joachim, it might be easy to implement a tactic like after tac using ... which delays the "main" goal on which tac is acting until all "side-goals" are solved after using. Note that tac could be a tactic sequence, not just rw.

[Johan Commelin]

Which might allow for things like

rw [lem1, lem2] using all_goals positivity
next step in main proofs

[Richard Osborn]

· apply lt_of_lt_of_le _ h.b_add_w_le_one; (· exact i); (· exact 0) looks ugly to me. This is probably an edge case that can be fixed?

[Yaël Dillies]

I agree with Joachim. In the meantime, can you avoid linting against · focusing on the last goal?

[Yaël Dillies]

Those changes look like noise to me. The other ones look good.

[Damiano Testa]

The linter actually does not complain on the last goal: I added those changes, since I felt that the proof was more "structured".

[Damiano Testa]

Technically, the linter complains when the tactic produces a goal that did not exist before, for some notion of "existed before". When there is a single goal, the linter (usually) says nothing.

[Damiano Testa]

For the side-conversation sparked by Joachim, you can find a quick implementation here.

[Damiano Testa]

Richard Osborn said:

· apply lt_of_lt_of_le _ h.b_add_w_le_one; (· exact i); (· exact 0) looks ugly to me. This is probably an edge case that can be fixed?

Honestly, I find that the culprit of the ugliness is trying to fit multiple tactics in a single line:

· apply lt_of_lt_of_le _ h.b_add_w_le_one
  · exact i
  · exact 0

looks perfectly good to me!

[Damiano Testa]

I simply tried to limit the changes to maintain, as much as possible, the original syntax/structure.

[Damiano Testa]

Yaël, I will revert the formatting of the last goal, since those changes are, in fact, not enforced by the linter. A discussion on whether they should or should not be enforced can happen later.

[Damiano Testa]

Yaël, are you against all focusing of the last goal, or something like

refine xx ?_ ?_
· assumption
· assumption

would be acceptable?

[Thomas Murrills]

Love the structuring! :D I agree that using …; (. tac); … looks worse, though. (I’d actually even go so far as to say we could lint against . in that situation! Not as part of this linter, but just in general. I.e. . should preferably always be line-initial, imo.)

[Yaël Dillies]

No, I think that's an acceptable focusing of the last goal

[Richard Osborn]

Damiano Testa said:

Richard Osborn said:

· apply lt_of_lt_of_le _ h.b_add_w_le_one; (· exact i); (· exact 0) looks ugly to me. This is probably an edge case that can be fixed?

Honestly, I find that the culprit of the ugliness is trying to fit multiple tactics in a single line:

· apply lt_of_lt_of_le _ h.b_add_w_le_one
  · exact i
  · exact 0

looks perfectly good to me!

Or even better: apply lt_of_lt_of_le _ <| h.b_add_w_le_one (i := i) (j := 0). (Maybe this could be linted for?)
But I don't disagree that using multiple lines is often the better choice.

[Mario Carneiro]

Thomas Murrills said:

Love the structuring! :D I agree that using …; (. tac); … looks worse, though. (I’d actually even go so far as to say we could lint against . in that situation! Not as part of this linter, but just in general. I.e. . should preferably always be line-initial, imo.)

You can also use { tac } for this. But the style I've been using for these trailing side goals lately is main <;> [rfl; skip], which works well with the multi-goal linter since even though this doesn't necessarily enforce that the side goal is closed, the multi-goal linter will as long as the next line is not a focus dot

[Mario Carneiro]

But in general I think that in this case there are enough bad options that it is a reason for someone to want to override the linter and write

induction n; rfl
...

anyway, and I'm inclined to make the linter allow this specific pattern (where the offending call rfl is not line-initial)

[Damiano Testa]

I guess that I could make the linter only flag whatever if flags, if it happens as the first tactic on a line.

[Damiano Testa]

Still, I am usually more in favour of adding lines, than compacting proofs.

[Damiano Testa]

I reverted/modified the more controversial changes in #12338 and added a few more files.

[Damiano Testa]

The PR contains a little more than what would be needed to please the linter: there should be about 130 files on which the linter would fail and the PR touches just under 200.

[Damiano Testa]

Is the general consensus that this is going to be merged? Should I finish the adjustments? Would it be better to do them in separate PRs?

[Kim Morrison]

I like this!

[Damiano Testa]

If I may say so myself, I am also very happy about the suggestions from the linter!

[Damiano Testa]

Tomorrow I'll continue with the changes then!

[Richard Osborn]

What are peoples thoughts on

cases n <;> [rfl; simp [Nat.two_mul]]

vs

cases n
· rfl
· simp [Nat.two_mul]

I'm generally against golfing, but I don't mind the former.

[Mario Carneiro]

it isn't against the linter at least

[Kim Morrison]

I think either of these are acceptable. I would write always the later, mostly out of desire to prefer using the "basic" way to say something, when there are multiple syntaxes for the same thing. (And to demonstrate my faith that the enter key is durable. :-)

[Damiano Testa]

#12338 is quite big as a PR and has already received some attention, so I think that it is best to leave it as is and put the new changes in a separate PR (that might eventually be merged into #12338).

[Damiano Testa]

The separate PR is #12361: it is entirely analogous to #12338, it simply touches different files.

[Damiano Testa]

Here is a summary:

• the "multiple goals linter" #12339;
• the first batch of adaptations #12338;
• the second batch of adaptations #12361;
• a draft PR combining the three above, just to keep track of the progress of the linter #12352.

[Johan Commelin]

Thanks for the community reviews on the 1st and 2nd batch! I have bors d+d them, so hopefully they will land in master somewhere today.

There are two more batches that @Damiano Testa prepared:

• #12372
• #12381

Reviews very welcome and appreciated!

[Damiano Testa]

Those PRs have been merged: thank you all very much for your reviews!

I split off the final remaining PR into two:

• #12381
• #12560

These are the last remaining adaptations adding cdots. I imagine that once they are all in, running the linter once more will highlight a few more instances, but there should few of those final touches.

[Damiano Testa]

A further update: the adaptations that were opened at the time of the PR have made it into mathlib: thank you for the reviews!

I expect that there might be some extra stray focusing missing, even though I have tried to keep up with mathlib.

In the meantime, I place the linter close to the bottom of the import hierarchy and am building mathlib against it, to see what more it catches.

[Damiano Testa]

If anyone feels like reviewing the linter, the PR is #12339.

[Damiano Testa]

As far as I can tell, all the suggestions of the linter were either "just correct" (most of the times), or flagged some slight weirdness with a proof (most of the rest of the times). I think that I was never unhappy with its suggestions.

[Damiano Testa]

There may be some extra discussion about how to deal with a workflow like "deal with the main goal now, leave all side-goals for later". However, this would probably also require some further tactic support and seems out of scope for the linter right now.

[Michael Rothgang]

Going over this thread, I see that

• a broad preference for the adaptations made in the other thread
• no outstanding objections to the linter in its current form (some controversial changes around focusing the last goal were reverted)
• some ideas for future tactic extensions, as discussed e.g. here. My impression is that these are not blocking right now.

On the other hand, I hear strong support for this, also from a learnability perspective (making beginning lean users aware of multiple goals being present is probably rather helpful). Is that a good summary; are there any objections to merging the linter? If not, I'll try to review the linter soon.

[Michael Rothgang]

#14939 fixes all current violations of the lint: reviews welcome!