Stream: Coq users

Topic: sequentializing or treating differently subgoals (ltac).

Pierre Vial (Dec 11 2020 at 11:05):

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?

Théo Winterhalter (Dec 11 2020 at 11:20):

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.

Théo Winterhalter (Dec 11 2020 at 11:21):

But I guess that's not what you want…

Théo Winterhalter (Dec 11 2020 at 11:22):

Can you give us a goal your right tactic would solve?

Pierre Vial (Dec 11 2020 at 12:52):

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 Iand 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.

Théo Winterhalter (Dec 11 2020 at 13:44):

To be honest I don't know if it's possible to do this the smart way.

Théo Winterhalter (Dec 11 2020 at 13:49):

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.

Pierre-Marie Pédrot (Dec 11 2020 at 14:02):

You could accumulate a trace as a Coq term (e.g. a list of booleans) and replay that maybe?

Théo Winterhalter (Dec 11 2020 at 14:04):

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.

Pierre Vial (Dec 11 2020 at 14:06):

@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

Pierre-Marie Pédrot (Dec 11 2020 at 14:08):

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?

Pierre-Marie Pédrot (Dec 11 2020 at 14:08):

(Even in vanilla Ltac1 there are horrible tricks to get the index of a constructor)

Théo Winterhalter (Dec 11 2020 at 14:17):

Ah I see, I did not take into account that you indeed had some information.

Théo Winterhalter (Dec 11 2020 at 14:18):

But I Pierre is using MetaCoq as well, then just getting it from there might be the best.

Pierre Vial (Dec 11 2020 at 14:54):

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 ?

Théo Winterhalter (Dec 11 2020 at 15:01):

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: Apr 20 2024 at 12:02 UTC