How to read goal states efficiently?

Stream: new members

[Chris M]

I'm confused about how the goal state is displayed depending on the position of the cursor. Consider these two pieces of code:
If I holw my cursor after apply le_antisymm,, I only see one goal state:

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm, --If I hold my cursor here, I can see one goal state: x ⊓ y ⊓ z ≤ x ⊓ (y ⊓ z).
    repeat {apply le_inf};
    {infs}
end

But in the following, I see two goal states:

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm, --If I hold my cursor here, I can see two goal states: x ⊓ y ⊓ z ≤ x ⊓ (y ⊓ z), and x ⊓ (y ⊓ z) ≤ x ⊓ y ⊓ z.
end

In practice, in order to get clariy on what's going on, I find myself cntrl-xing later parts of a proof to see the fully goal state, and then pasting them back. This seems like it wasn't the intended way to use this.

How do people do this normally?

[Scott Morrison]

I guess one not-so-great answer is that I don't write repeat or use ; until I have the whole proof working --- I switch to using those only when golfing.

[Scott Morrison]

Both of them make it harder to understand the intermediate tactic states.

[Floris van Doorn]

I don't remember this being a problem before. Was this always the behavior?
Here is a #mwe:

import order.lattice

variables {α : Type*} [lattice α] {x y z : α}
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm,
    apply le_inf; sorry,
end

[Floris van Doorn]

Ok, I just tested, and this was already the behavior of 3.5.1

[Floris van Doorn]

My workaround, which is probably a bit more useful than Scott's:
Whenever you create 2+ subgoals, you can put each subgoal individually in braces: { ... }. This also happens to be a good style, adopted in mathlib.

import order.lattice

variables {α : Type*} [lattice α] {x y z : α}
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm, -- you see both subgoals here
    { apply le_inf; sorry },
    { }
end

[Chris M]

@Floris van Doorn Thanks that workaround works for me.

Is this considered a bug?

[Chris M]

Also, in this code, I see both subgoals if I use , but only the first if I use ;

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm, --I can see both subgoals if I hover here.
    {repeat {apply le_inf};
    {infs}}
end
example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm; --but only the first if I hover here
    {repeat {apply le_inf};
    {infs}}
end

[Johan Commelin]

Yup, that's a known limitation of ;. I'm not sure how hard it would be to fix it.

[Chris M]

I'm actually unsure what the general rule is: when you put a cursor at a location, what goal does it show?
For example:

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
begin
    apply le_antisymm;
    {repeat {apply le_inf --If I put my cursor here, what goal is it showing? The goal that apply le_inf is working on in the first chain of the repeat, or something like that?
    };
    {infs}}
end

[Floris van Doorn]

I would consider your first post a bug.

Your last post is a known limitation. ; is not really a tactic separator, since it combines multiple tactics into a single one, so Lean doesn't quite know to display in the middle of that.
And as your last example shows: it is not even clear what you want to show at every point in the proof. I think it tries to show the goal the first time it reaches that spot, or something.

[Alex J. Best]

Its always been the first from my experience. You can use the command trace_state which will print the state every time its run, this way you can see all the goals at some point.

[Floris van Doorn]

Ah, the fact that it shows the first goal after ; at all is pretty recent: lean#239. I already thought that it was showing garbage before (to be more precise: I think it showed the state before your tactic containing the ;). Your question about showing all goals after ; is already mentioned in lean#201.

[Floris van Doorn]

I added your first report to lean#201