spaceloop (Apr 29 2021 at 12:14): 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 -> _ -> _).
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.
Théo Zimmermann (Apr 29 2021 at 12:21):See https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.match-goal
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.
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?
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...
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 *)
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?
spaceloop (Apr 29 2021 at 15:00):This last solution already suits my purposes nicely, thanks Theo.
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.
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.
Théo Zimmermann (Apr 29 2021 at 15:09):Oh right, I wrote this too fast and didn't test it enough.
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.
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
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).
I don't know if there's a simpler solution.
Théo Zimmermann (Apr 29 2021 at 15:22):No, actually this is still wrong.
Théo Zimmermann (Apr 29 2021 at 15:25):I don't know how to test that n is exactly m + 1.
Théo Zimmermann (Apr 29 2021 at 15:25):I guess in Ltac2 this would be trivial.
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 *)).
the idea is that you set the evar to tt the first time you encounter the goal
Last updated: Apr 18 2024 at 19:02 UTC