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 -> _ -> _).
You probably need to use the match goal with
Ltac construct (combined with the all:
goal selector) then.
See https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.match-goal
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?
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...
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?
This last solution already suits my purposes nicely, thanks Theo.
You can add the line:
| _ => fail 2
before the end
to make the tactic fail if the goal doesn't exist.
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.
Oh right, I wrote this too fast and didn't test it enough.
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.
OK, this is probably doable with numgoals
: https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.numgoals
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.
No, actually this is still wrong.
I don't know how to test that n is exactly m + 1.
I guess in Ltac2 this would be trivial.
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: Oct 13 2024 at 01:02 UTC