Is there a way to "flatten" the list of subgoal generated by a tactic?

For instance, `tac1 ; tac2`

will apply `tac2`

to *each* subgoal `g1`

, `g2`

, ... ,`gn`

generated by `tac1`

.

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 `list nat`

:

```
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)
```

where `C1`

, `C2`

, ... , `Cn`

are the constructors of `I`

and `exists vector xi`

stands for a list of existential for the parameters of `Ci`

.

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 `revert`

, `intro`

and `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 `x`

.

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 `left`

for `C1`

(1st subgoal producec `destruct x`

), `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 `inductive`

s 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: Jun 24 2024 at 13:02 UTC