## Stream: Coq users

### Topic: ✔ How to get rid of duplicate goals

#### walker (Oct 12 2022 at 11:41):

There is a certain rewrite lemma that I had to use with repeat, and I generates goals that looks like this:

``````2/5
is_lc n = true
(3/5)
x ∉ {[x0]}
(4/5)
is_lc n = true
(5/5)
x ∉ {[x0]}
``````

Is there a way to get rid of the duplicate goals without having to reprove them or without a previous assert + auto?.

#### Théo Zimmermann (Oct 12 2022 at 11:46):

Short answer is no. You can either use `assert` or apply the same tactics to all of them with goal selectors.

#### Théo Zimmermann (Oct 12 2022 at 11:47):

Maybe one could find tricks to merge duplicate goals using existential variables though (I have never tried that).
E.g., using `refine ?[my_goal]` on one of them, then `eexact ?my_goal` on the rest of them (using goal selectors)?

#### walker (Oct 12 2022 at 11:49):

alright, they were not hard to prove anyways, but asserts always feel confusing for me (when reading proofs) so Idon't want to use it.

I just selected the goals and solved them maually.

#### Notification Bot (Oct 12 2022 at 11:49):

walker has marked this topic as resolved.

#### Gaëtan Gilbert (Oct 12 2022 at 12:02):

it's possible to merge goals in ltac2

``````Require Import Ltac2.Ltac2.
Import Ltac2.Constr.

Ltac2 never () := Control.throw Assertion_failure.

Goal (0 = 0 -> 0 = 0 -> False) -> False.
Proof.
intros H;apply H.
all:
let newgoal := { contents := None } in
Control.enter (fun () =>
match newgoal.(contents) with
| None =>
Control.refine (fun () =>
let goal := Control.goal () in
(* NB: we can't get the evar for the current goal so we have to make a new one *)
match Unsafe.kind open_constr:(_ : \$goal) with
| Unsafe.Cast v _ _ =>
newgoal.(contents) := Some v;
v
| _ => never ()
end)
| Some v => Control.refine (fun () => v)
end).
(* 1 goal 0 = 0 *)
reflexivity.
Show Proof. (* fun H => H eq_refl eq_refl *)
Qed.
``````

I think in Ltac1 it's impossible

#### Enrico Tassi (Oct 12 2022 at 12:18):

Deduplicating goals is in fact the example I use in Coq-Elpi's tutorial to explain multi goal tactics:
https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_tactic.html#multi-goal-tactics

Last updated: Jun 18 2024 at 10:02 UTC