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: Sep 26 2023 at 12:02 UTC