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: Oct 13 2024 at 01:02 UTC