Is there a way to "flatten" the list of subgoal generated by a tactic?
tac1 ; tac2 will apply
tac2 to each subgoal
g2, ... ,
gn generated by
I'm trying to do the following: applying
right once to
g1, twice to
g2 and so on.
One possibility would be applying a tactic
tac2' working not on each subgoal
gi but on the sequence of all obligations generated by
g1 ... gn. Is there a way to do so?
Another possibility would be applying a tactic
tac2'' on each
gi which actually takes
i as a parameter. Is this also possible?
So you are having troubles that the tactic is working on a tree of goals and not a list?
If this is inside a proof (and not in the definition of some tactic), you can use goal selectors.
tac1. all: tac2. (* Applies tac2 to all goals that are selected at the moment, so all goals if you did not use bullets *) 1,4: tac3. (* Only to the first and fourth goals *) 1-3: tac4. (* To goals 1, 2 and 3 *)
The idea is that Coq automatically flattens the goals once a tactic is finished evaluating.
But I guess that's not what you want…
Can you give us a goal your
right tactic would solve?
Yes, indeed, I'm trying to do this while defining a tactic and the number of subgoals may vary.
Using metacoq, I do have a tactic that, given a datatype
I, gives me the statement that every inhabitant of
I is produced by a constructor, e.g. for
forall (x : list nat), x = [ ] \/ (exists (x0 : nat ) (lx1 : list nat), x = x0 :: x1
In general, I'll have statements of the form
forall (x : I), (exists vector x1, x = C1( 1)) \/ exists vector x2, x = C2 x2) \/ ... \/ (exists vector xn, x = Cn xn)
C2, ... ,
Cn are the constructors of
exists vector xi stands for a list of existential for the parameters of
I'm trying to prove this statement automatically.
What I'm currently doing is introducing then destructing
x. I also have a tactic using one of your recent answers (thanks !), based on
exists to automatically solve a goal (without disjunctions) of the form
exists vector xi, Ci (xi) = C(yi) where
yi is a vector of variables obtained by destructing
But to apply this last tactic, I must first select one of the element of the disjunction: actually, in
i-th subgoal, I'm must select the
i-th element of the disjunction.
To obtain the full tactic, I should do
C1(1st subgoal producec
left. right. for the 2nd one,
left. left. right. for the third and ...
right. ... right. for the last one.
To be honest I don't know if it's possible to do this the smart way.
From Coq Require Import List Utf8. Import ListNotations. Ltac bar := match goal with | |- _ \/ _ => left ; bar | |- _ \/ _ => right ; bar | |- exists x, _ => eexists ; bar | |- _ => reflexivity end. Lemma foo : ∀ (x : list nat), x =  ∨ (∃ (x0 : nat) (lx1 : list nat), x = x0 :: lx1). Proof. intro x. destruct x ; bar. Qed.
This works by doing backtracking.
You could accumulate a trace as a Coq term (e.g. a list of booleans) and replay that maybe?
But how can you do something different in each goal? It seems you need to carry around the info of the goal you are in.
@Théo Winterhalter by just modifying a bit your code, I made it work, thanks ! But in practice, I should not need backtracking so I'm curious about @Pierre-Marie Pédrot 's idea
I believe that even in Ltac1 you can extract your constructor from the goal. With MetaCoq you can probably turn that into an index, and then run a Ltac1 that performs the corresponding sequence of left / right from that?
(Even in vanilla Ltac1 there are horrible tricks to get the index of a constructor)
Ah I see, I did not take into account that you indeed had some information.
But I Pierre is using MetaCoq as well, then just getting it from there might be the best.
Yes, I thought of that, but if I wanted to have simpler test (i.e. whitout digging to much inside
inductives of MetaCoq), but in fine, it's what I will do.
@Pierre-Marie Pédrot Would you have an example of such a trick ?
You don't have to dig inside the inductive, I think if you look at the constructor, it comes with an integer telling you which one it is.
Last updated: Jan 31 2023 at 14:03 UTC