Stream: Coq users

Topic: ✔ How to get rid of duplicate goals


view this post on Zulip 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?.

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Notification Bot (Oct 12 2022 at 11:49):

walker has marked this topic as resolved.

view this post on Zulip 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

view this post on Zulip 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: Jan 27 2023 at 02:04 UTC