rotate

Stream: mathlib4

[Arthur Paulino]

I just found out that we already have rotate_left n and rotate_right n tactics. Should I open a PR removing the rotate_goals tactic?

[Arthur Paulino]

Feel free to close it: https://github.com/leanprover-community/mathlib4/pull/185

[Johan Commelin]

Would rotate_up and rotate_down be more intuitive? The goal state displays the goals in a vertical list...

[Arthur Paulino]

But then we'd have it changed in the core code, right?

[Mario Carneiro]

the polarity was also not what I expected: mathlib rotate n, which moves the nth goal to the front and rotates everything else around that, is rotate_left n in lean 4

[Arthur Paulino]

What do you mean by "the polarity was also not what I expected"?

[Mario Carneiro]

I had guessed that rotate_right did that

[Mario Carneiro]

in hindsight, and especially if you think about the goals laid out in a left-to-right list, it makes sense, but I agree with Johan that the directionality here is a bit confused

[Mario Carneiro]

maybe rotate n and rotate -n is a better idea after all

[Gabriel Ebner]

FWIW, I would expect rotate_right to rotate in clockwise direction.

[Arthur Paulino]

pull_goals and push_goals might be a bit more explicit

[Gabriel Ebner]

Looking through mathlib3, most occurrences of swap n are followed by exact or { ... }.

I think it would make more sense to add case n => ... instead of adding all kinds of obscure goal permutations. (We already have pick_goal, this is enough to get any permutation that you want. :smirk:)

[Arthur Paulino]

for case n => ... we have on_goal n => ..., which doesn't restrict the incoming tactics to close the goal

[Stuart Presnell]

Perhaps rotate_to n, which suggests rotating the carousel of goals to the nth entry (and for negative values we count from the end of the list)?

[Johan Commelin]

I think on_goal is all I would need.

[Gabriel Ebner]

which doesn't restrict the incoming tactics to close the goal

This restriction is often desired though. Even adding just a macro which expands case $n => $seq to on_goal $n => { $seq } seems useful.

[Johan Commelin]

If it could take a list of goals that would be a nice cherry.

[Stuart Presnell]

I'm less keen on _left, _down, etc. since they depend on the particular on-screen representation of the list of goals.

[Johan Commelin]

I sometimes want something between all_goals and on_goal.

[Arthur Paulino]

@Gabriel Ebner why is the restriction desired?

[Johan Commelin]

It makes proof scripts more robust. As proof author you promise "the next block will close this goal". So when the proof breaks 7 months later, it's easier to figure out where to tweak things.

[Johan Commelin]

Instead of suddenly staring at a 57 line long script that has 5 open goals left at the end.

[Gabriel Ebner]

Because that makes tactics proofs more reliable. That is, whenever you see case ... => ... you can be certain that the case closes that goal. Lean 4 can even continue executing the proof if the case fails, because it's clear how the goals need to look afterwards.

[Sebastian Ullrich]

Modulo instantiation of metavariables :) ...

[Arthur Paulino]

Got it, thanks!

[Eric Rodriguez]

I would love to have something that let me focus some specific goals and close them all automatically. I think that is a fantastic idea

[Arthur Paulino]

Eric Rodriguez said:

I would love to have something that let me focus some specific goals and close them all automatically. I think that is a fantastic idea

Something like on_goals [1, 2, 3] => try this; try that; etc?

[Johan Commelin]

If you can implement etc, that would be major!! :wink:

[Mario Carneiro]

Arthur Paulino said:

Eric Rodriguez said:

I would love to have something that let me focus some specific goals and close them all automatically. I think that is a fantastic idea

Something like on_goals [1, 2, 3] => try this; try that; etc?

lol, I swear mathlib4#187 was invented independently

[Mario Carneiro]

Gabriel Ebner said:

Looking through mathlib3, most occurrences of swap n are followed by exact or { ... }.

I think it would make more sense to add case n => ... instead of adding all kinds of obscure goal permutations. (We already have pick_goal, this is enough to get any permutation that you want. :smirk:)

Heh, great minds think alike: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60swap.60.20semantics.20tactics.20names/near/270789014

[Mario Carneiro]

To summarize the on_goals PR: It adds two new tactics: on_goal is generalized to multiple goals as in on_goal 1 3 5 => simp will apply simp to goals 1,3,5 and place the resulting subgoals back where it found them, and on_goals 1 3 5 => tac will apply tac to a state consisting of goals 1,3,5, and then placing the resulting goals at the front and all the unselected goals at the end

[Mario Carneiro]

so on_goals 1 3 5 => skip will move goals 1 3 5 to the front

[Arthur Paulino]

[This thread no longer matches it title btw]
That difference in behavior is not clear to me just by looking at their names though. I would expect on_goals to behave just like on_goal, but accepting multiple goals. And then focus_goals would be the one that brings the goals up in the queue (if this is a helpful behavior)

[Mario Carneiro]

Lean 4 can even continue executing the proof if the case fails, because it's clear how the goals need to look afterwards.

How does this mechanism work anyways? In lean 3 any failure is fatal, and if you are calling setGoals later in the tactic I don't see how you can recover if an embedded tactic fails

[Mario Carneiro]

It's true that the names are not very different, but it's not the only tactic like that: intro vs intros both introduce multiple variables but intros keeps going after it has introduced the named ones

[Arthur Paulino]

But "goals" is the plural of "goal". And "intros" is... just "intro" + "s"

[Mario Carneiro]

no, intros is definitely the plural of intro

[Johan Commelin]

Could on_goals work in place, and pick_goals move things to the front?

[Arthur Paulino]

Ah, oops (english not my mother tongue)

[Mario Carneiro]

I think it is best not to go overboard with disambiguating names because it's supposed to be a language in the linguistic sense. You have to learn the words but the brevity pays off in the long run

[Mario Carneiro]

There is a balance to be sure, you don't want it to be impossible to learn, but it is most important that it is not misleading, it's okay if it's vague

[Gabriel Ebner]

Mario Carneiro said:

Lean 4 can even continue executing the proof if the case fails, because it's clear how the goals need to look afterwards.

How does this mechanism work anyways? In lean 3 any failure is fatal, and if you are calling setGoals later in the tactic I don't see how you can recover if an embedded tactic fails

I think case foo => tac does the equivalent of case foo => { tac } <|> sorry.

[Julian Berman]

Is intros staying in Lean 4?

[Mario Carneiro]

yes

[Arthur Paulino]

Maybe on_goals and on_goals' work better because their difference is very small

[Mario Carneiro]

like I said, lean 4 has intro and intros and they are different

[Gabriel Ebner]

Mario Carneiro said:

so on_goals 1 3 5 => skip will move goals 1 3 5 to the front

This is super subtle and easy to overlook. How about we have pick_goal 1 2 3 => tac for the one that moves multiple goals to the front?

[Mario Carneiro]

my mnemonic is: on_goal runs your tactic on 1 goal (multiple times), on_goals runs on many goals

[Gabriel Ebner]

How does on_goal execute the tactic multiple times? From what I can tell, the only difference between on_goal and on_goals is how the goals are permuted afterwards.

[Mario Carneiro]

to be fair on_goals ns => skip is like running a program for its side effects, we should have a macro for that particular use case to make the side effect more central

[Arthur Paulino]

Mario Carneiro said:

my mnemonic is: on_goal runs your tactic on 1 goal (multiple times), on_goals runs on many goals

But that's not what the code is doing, right? on_goal is accepting multiple goals on your PR

[Mario Carneiro]

on_goal is like all_goals, it runs the tactic in a focused state on each goal

[Mario Carneiro]

If you do on_goal 1 2 => simp, first simp will run on goal 1, then simp will run on goal 2. If you do on_goals 1 2 => simp then simp will run on goals 1 and 2 together (and it will ignore goal 2 like most tactics run in a multi-goal state)

[Mario Carneiro]

by 1 goal I mean that simp sees a tactic state with 1 goal in it

[Mario Carneiro]

The test has a use of on_goals 2 4 => swap which permutes [1, 2, 3, 4, 5] into [4, 2, 1, 3, 5]

[Gabriel Ebner]

So on_goal 3 5 8 => simp is like on_goals 3 5 8 => all_goals simp modulo goal permutation? This is yet one more reason it should get a visibly different name.

[Johan Commelin]

The way I understand it is that those two are not the same. (Sorry, I missed that there was no s in the first on_goal. Which I guess exactly makes Gabriel's point.)

[Mario Carneiro]

Yes. I originally wanted to implement one in terms of the other but it's not possible for on_goals to have the goal order preservation thing

[Mario Carneiro]

I think on_goal is likely to be much more useful than on_goals

[Johan Commelin]

Also, I would intuitively expect on_goals 3 5 8 => simp to be the same as on_goals 3 5 8 => all_goals simp.

[Mario Carneiro]

it's rare to need to work with multi-goal states directly, but these are goal permutation tactics, that's the point

[Mario Carneiro]

@Johan Commelin on_goal satisfies that

[Johan Commelin]

I think we need more to stress the difference then just this s.

[Mario Carneiro]

with_goals?

[Mario Carneiro]

for on_goals

[Johan Commelin]

Right, on_goal does, but on_goals doesn't. Which is exactly why you wrote on_goals. I get that now. But it took me a while.

[Johan Commelin]

on_goals {3,5,8} => simp?

[Johan Commelin]

To emphasize that you run the tactic once a the "set" of those 3 goals.

[Mario Carneiro]

heh, if you write that then I'm going to generalize it

[Johan Commelin]

Yeah, that's part of the hint (-;

[Johan Commelin]

Is it clear that on_goals can not place the goals back in the place where they came from?

[Johan Commelin]

on_goal 3 5 8 would just be on_goals {3} {5} {8}.

[Mario Carneiro]

"where they came from" is not well defined if they came from a set {3, 5, 8}

[Mario Carneiro]

if you get two goals out, where would they go? the first one replaces 3, the second 5, ...?

[Johan Commelin]

yeah, fair enough.

[Mario Carneiro]

Plus, I'm not even sure that's a useful behavior most of the time

[Arthur Paulino]

If the user is not attacking the first goal, I don't think there's a clear intent to bring subgoals to the front

[Mario Carneiro]

I think the majority of the time that's always what you want to do

[Mario Carneiro]

on_goal is the only exception I know to that

[Mario Carneiro]

everything happens at the head of the list

[Gabriel Ebner]

If we're letting the user select a goal, it would be nice if you could also use tags in addition to numbers. That is on_goal 3 zero => simp only.

[Mario Carneiro]

wait, do we have non-closing case?

[Mario Carneiro]

I guess it's fine in the on_goal syntax to support tags

[Arthur Paulino]

What is a tag in this context?

[Gabriel Ebner]

No, I don't think we have non-closing case. We also don't have an unstructured case (which just moves the goal to the front and renames the variables).

[Gabriel Ebner]

Arthur Paulino said:

What is a tag in this context?

The succ i ih in case succ i ih => tac.

[Mario Carneiro]

lean 3 has multiple word tags, are those possible?

[Gabriel Ebner]

I think so, but I can't remember the syntax.

[Mario Carneiro]

Maybe we should consider how to port the lean 3 case tactic that is sitting in Syntax.lean

[Mario Carneiro]

Hm, I think I can see a decent grammar for on_goal, by example:

on_goal 1, zero, succ x ih, {3 a, -1 b c} => ...

[Arthur Paulino]

Regarding mathlib#187 I wanna suggest a mix of some ideas I saw here:
What if instead of on_goal and on_goals we had on_goals and with_goals?
with_goals being the one that brings unsolved goals to the front

My rationale is that "on" reminds me of something that happens as in place as possible

[Mario Carneiro]

this grammar could also be used for variations on what to do with the goal, like case

[Mario Carneiro]

In the grammar above you wouldn't need with_goals: on_goal 1 2 3 => becomes on_goal 1, 2, 3 => and with_goals 1 2 3 => becomes on_goal {1, 2, 3} =>

[Johan Commelin]

@Mario Carneiro With you on_goal example, will you just move everything to the front? Or are the singleton goal-sets working "in-place"?

[Mario Carneiro]

If you use braces, you get with_goals behavior: the set gets pulled to the front

[Mario Carneiro]

anything not in braces stays where it is

[Mario Carneiro]

so on_goal {3} => is also useful if you don't want it to stay where it is

[Arthur Paulino]

Ah, then you can mix for instance on_goal 3 {5, 7} and subgoals from 5 and 7 would get pulled up?

[Mario Carneiro]

yes

[Arthur Paulino]

Okay that's a neat solution IMO

[Mario Carneiro]

if the goals were [1,2,3,4,5,6,7] before then after they would be [57',1,2,3',4,6]

[Johan Commelin]

What is the behaviour of on_goal {2,3} {2,3} => skip? On goal list [1,2,3].

[Mario Carneiro]

[2,3,2,3,1]

[Mario Carneiro]

yes you can copy goals

[Johan Commelin]

Ok, so the second {2,3} doesn't operate on the result of the first {2,3} => simp.

[Johan Commelin]

Of course these are weird edge cases that don't show up in practice (I hope).

[Mario Carneiro]

No, but by the time you get around to them they might be solved already

[Mario Carneiro]

if you do something other than skip then the second invocation probably won't see them at all

[Arthur Paulino]

Isn't it safer if you take a snapshot and iterate on that instead of unfolding as it goes?

[Mario Carneiro]

I do

[Arthur Paulino]

(I probably made no sense)

[Mario Carneiro]

All goal indexes refer to the goal state at the start, not after half of the tactics have run

[Mario Carneiro]

but goals can "expire" due to other goals getting worked on

[Mario Carneiro]

especially if you copied a goal

[Mario Carneiro]

I'm sure you've seen this in lean 3 when you apply something and it produces a bunch of metavariables and then you equate two things and all the metavariable goals disappear

[Arthur Paulino]

I suspect we've reached a thin line between play and actual need, but I'm enjoying to see the power of Lean metaprogramming in action

[Arthur Paulino]

Also I'm learning a lot from this process of empowering and cleaning up mathlib3 tactics (and it barely started for me)

[Mario Carneiro]

Of course no one will use all of those features simultaneously. But it is useful to have an orthogonal mechanism, here goal selection, in a way that applies to multiple tactics, since it makes skills transferrable

[Arthur Paulino]

Yeah, how many times have I wanted something like on_goal 1 2 => intros...

[Yaël Dillies]

Where is the tactic rotate gone? I found it very practical for proof building.

[Adam Topaz]

import Mathlib

open Lean Elab Tactic

example (p q : Prop) : p ∧ q := by
  constructor
  run_tac do
    let goals ← getGoals
    setGoals <| goals.rotate 3
  sorry
  sorry

[Adam Topaz]

Sorry, I didn't actually read this thread before posting.

[Kyle Miller]

The tactic is now called rotate_left and rotate_right

[Yaël Dillies]

Ah great!

[Yaël Dillies]

@Martin Dvořák, another one for your cheatsheet :point_up:

[Martin Dvořák]

May I kick apply? out in order to make space for rotate_left on the bottom of the page?
https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf

[Yaël Dillies]

Make it two pages? Reduce the font size?

[Martin Dvořák]

Then I'd rather make two versions. Let's move this discussion here:
https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/Lean4.20cheatsheet

[Patrick Massot]

Martin Dvořák said:

May I kick apply? out in order to make space for rotate_left on the bottom of the page?
https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf

I think apply? is infinitely more important than rotate_left.

[Alex J. Best]

Why are you worried about page sizes anyway? Surely this is a digital document that nobody is actually printing

[Patrick Massot]

The layout is based on a document that I ask my students to physically have with them when I'm teaching this. And I print it for them.

[Alex J. Best]

Ok, thats interesting, do they have laptops at the same time?

[Alex J. Best]

Also how come simp isn't on the list?

[Alex J. Best]

I'd kick convert_to out in favour of that any day

[Martin Dvořák]

Can we please continue the discussion about priorities for the cheatsheet in the respective thread?
The missing simp is a mistake and I want to address it.

[Eric Rodriguez]

Where is the thread?

[Damiano Testa]

I also like the pick_goal tactic. Maybe we need a pick_thread now?

[Martin Dvořák]

Eric Rodriguez said:

Where is the thread?

https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/Lean4.20cheatsheet