The Coq mailing list

[Nicolas Magaud <magaud AT unistra.fr>]

Dear Club,

I sometimes use the goal selector “par:" to take advantage of task 
parallelism in proving the subgoals at stake.

Upon completion of the proof, I want to write a Ltac tactic to prove the 
whole goal in one go. In this case, I can not use the “par:” construction 
anymore.

Attached is a small example (example.v) where I would like to do : 
“intros p q; destruct p; destruct q; par:solve [left;reflexivity | 
right;discriminate]” to take advantage of parallel computations. Here the 
data-type has 20 constructors, but in the real world, I face goals where the 
inductive type has around 50/100 constructors and more than 3 variables are 
involved in the statement, which is not a decidability property any more.

Of course, I can decompose in 2 steps : 

intros p q; destruct p; destruct q.
par:solve [left;reflexivity | right;discriminate].

but what I would like to do is to have a Ltac definition for this sequence of 
tactics : 

Ltac mysolve := let p := fresh in let q:= fresh in intros p q; destruct p; 
destruct q; par:solve [left;reflexivity | right;discriminate].

Such a definition is rejected because of the par: construct occurrence. If I 
remove “par:”, it works fine but subgoals are not proved in parallel anymore.

Is there a  way to use the par goal selector inside a sequence of tactics in 
order to take advantage of the available parallelism ?

Thanks in advance,

Nicolas Magaud

Attachment: example_par.v
Description: Binary data