Zulip Chat Archive

Stream: new members

Topic: How to read goal states efficiently?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 06 2020 at 06:08):

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

view this post on Zulip 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

view this post on Zulip Floris van Doorn (Jul 06 2020 at 16:47):

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

view this post on Zulip 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

view this post on Zulip Chris M (Jul 07 2020 at 04:01):

@Floris van Doorn Thanks that workaround works for me.

Is this considered a bug?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Jul 07 2020 at 05:06):

I added your first report to lean#201


Last updated: May 18 2021 at 16:25 UTC