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?.
Short answer is no. You can either use assert
or apply the same tactics to all of them with goal selectors.
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)?
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.
walker has marked this topic as resolved.
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
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: Oct 13 2024 at 01:02 UTC