## Stream: new members

### Topic: How to read goal states efficiently?

#### Chris M (Jul 06 2020 at 05:06):

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 (Jul 06 2020 at 06:08):

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 (Jul 06 2020 at 06:08):

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

#### Floris van Doorn (Jul 06 2020 at 16:41):

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 (Jul 06 2020 at 16:47):

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

#### Floris van Doorn (Jul 06 2020 at 16:49):

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 (Jul 07 2020 at 04:01):

@Floris van Doorn Thanks that workaround works for me.

Is this considered a bug?

#### Chris M (Jul 07 2020 at 04:49):

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 (Jul 07 2020 at 04:53):

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

#### Chris M (Jul 07 2020 at 04:56):

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 (Jul 07 2020 at 04:58):

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 (Jul 07 2020 at 04:58):

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 (Jul 07 2020 at 05:03):

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.