Stream: Coq users

Topic: Focus based on type


view this post on Zulip spaceloop (Apr 29 2021 at 12:14):

Hi, is it possible to focus/select goals based on their type? I'd like to work on all the goals of for example (bool -> _ -> _).

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 12:20):

You probably need to use the match goal with Ltac construct (combined with the all: goal selector) then.

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 12:21):

See https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.match-goal

view this post on Zulip spaceloop (Apr 29 2021 at 13:17):

Thanks! This simple example works:

Goal (bool -> nat) * nat.
  constructor.

  all: try match goal with
  | |- bool -> _ => intros; exact 2
  end.

  all: try match goal with
  | |- nat => exact 3
  end.
Qed.

view this post on Zulip spaceloop (Apr 29 2021 at 13:17):

However, it requires me to write a single tactic expression on the RHS of the match. Is there a way to focus the goals that match? Such that I can continue developing the proof for those goals interactively?

view this post on Zulip Kenji Maillard (Apr 29 2021 at 13:51):

Here is one way to filter out the goals that you do not want to consider immediately:

Goal (bool -> nat) * nat.
Proof.
  split.

  (* filtering out all goals that do not match _ -> _ *)
  all: match goal with | |- (_ -> _) => idtac | |- _ => shelve end.

  (* only one goal left *)
  intros ; exact 2.

  (* Recover **all** the goals on the shelve *)
  Unshelve.
  exact 3.
Qed.

That's far from perfect though...

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 14:05):

spaceloop said:

However, it requires me to write a single tactic expression on the RHS of the match. Is there a way to focus the goals that match? Such that I can continue developing the proof for those goals interactively?

You can't focus (with bullets or focusing brackets) on multiple goals at once. However, if you are looking for a single goal what you could do would be to move the goal you want to focus on in the first position and then focus with brackets:

Goal (bool -> nat) * nat.
  constructor.

  all: unshelve (try match goal with
  | |- nat => shelve
  end). (* puts nat goal first *)
  { (* focus on nat goal *)

view this post on Zulip spaceloop (Apr 29 2021 at 15:00):

Thanks both for pointing me at the shelve/unshelve tactics! Suppose I know there is only one goal of a certain type, is it then possible to focus on that one and fail otherwise?

view this post on Zulip spaceloop (Apr 29 2021 at 15:00):

This last solution already suits my purposes nicely, thanks Theo.

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 15:02):

You can add the line:

  | _ => fail 2

before the end to make the tactic fail if the goal doesn't exist.

view this post on Zulip spaceloop (Apr 29 2021 at 15:08):

That fails when there is a goal that does not match, presumably because of the all selector.

Goal (bool -> nat) * nat.
split.

  all: unshelve (try match goal with
  | |- nat=> shelve
  | _ => fail 2
  end).

Tactic failure.

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 15:09):

Oh right, I wrote this too fast and didn't test it enough.

view this post on Zulip spaceloop (Apr 29 2021 at 15:10):

Ideally I'd have a tactic that succeeds when there is exactly one goal that matches the given type (0 or > 1 would fail), and then focus on that one.

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 15:12):

OK, this is probably doable with numgoals: https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.numgoals

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 15:21):

Here is what I managed to do:

  all: unshelve (let n := numgoals in try match goal with
  | |- nat => let n := numgoals in tryif guard n = 1 then shelve else idtac
  end; let m := numgoals in guard n > m).

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 15:21):

I don't know if there's a simpler solution.

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 15:22):

No, actually this is still wrong.

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 15:25):

I don't know how to test that n is exactly m + 1.

view this post on Zulip Théo Zimmermann (Apr 29 2021 at 15:25):

I guess in Ltac2 this would be trivial.

view this post on Zulip Gaëtan Gilbert (Apr 29 2021 at 15:41):

maybe with a dummy evar, like

all: unshelve (let c := open_constr(_ : unit) in try match goal with
| |- nat => tryif constr_eq c tt then (* more than 1 *) else (unify c tt; shelve)
end; tryif constr_eq c tt then (* exactly 1 *) else (* 0 *)).

view this post on Zulip Gaëtan Gilbert (Apr 29 2021 at 15:42):

the idea is that you set the evar to tt the first time you encounter the goal


Last updated: Jan 29 2023 at 01:02 UTC