Stream: math-comp users

Topic: ✔ all_ssreflect: Focusing on sub-goal


view this post on Zulip Julin Shaji (Feb 18 2024 at 06:34):

Hi.

If there are multiple proof goals with all_ssreflect imported,
focusing on one sub-goal with - / + / * doesn't make other goals
disappear temporarily.

Whereas it does disappear if all_ssreflect is not imported.

Is it how it should be? Or could it be that I got something configured
wrong?

view this post on Zulip Julin Shaji (Feb 18 2024 at 06:37):

For example, with just ssreflect:

Require Import ssreflect.

Goal forall (a: bool + bool), bool.
move => H.
case H.
-
(*
1 subgoal
(1 unfocused at this level)

H : bool + bool

========================= (1 / 1)

bool -> bool
*)

and with all_ssreflect:

From mathcomp Require Import all_ssreflect.

Goal forall (a: bool + bool), bool.
move => H.
case H.
-
(*
2 subgoals

H : bool + bool

========================= (1 / 2)

bool -> bool

========================= (2 / 2)

bool -> bool
*)

view this post on Zulip Reynald Affeldt (Feb 18 2024 at 07:34):

This is the intended behavior.

view this post on Zulip Julin Shaji (Feb 18 2024 at 08:00):

Why was that made the default behaviour? I mean, that would mean even when we want to focus on a particular case, all the other goals will cause some clutter, right?
I guess this behaviour is just for mathcomp?

view this post on Zulip Reynald Affeldt (Feb 18 2024 at 08:45):

I mean, that would mean even when we want to focus on a particular case, all the other goals will cause some clutter, right?

I don't know. As a user, I find it informative to see the other goals and I prefer it this way but that certainly depend on your application.
It looks like you can recover the Coq bullets with the following command
https://coq.inria.fr/doc/V8.10.0/refman/proof-engine/proof-handling.html#set-bullet-behavior
You can maybe also use the command Focusto focus while using MathComp bullets:
https://coq.inria.fr/doc/V8.9.1/refman/proof-engine/proof-handling.html#coq:cmd.focus

view this post on Zulip Julin Shaji (Feb 18 2024 at 09:42):

Thanks!
Hadn't known about Set Bullet Behavior.

It looks like use of Focus is discouraged though.

Got this warning upon using it:

The Focus command is deprecated; use bullets or focusing brackets instead
[deprecated-focus,deprecated-since-8.8,deprecated,default]

What does focusing bracket mean here?

view this post on Zulip Julin Shaji (Feb 18 2024 at 09:44):

Oh.. I guess those brackets are just { and }.

view this post on Zulip Notification Bot (Feb 18 2024 at 09:45):

Julin Shaji has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (Feb 18 2024 at 10:50):

there's also 2:{ if you want to focus on goal 2 etc


Last updated: Jul 15 2024 at 21:02 UTC