Ad hoc asynchronicity

Developing the Coq system
#1

In large, complex proofs it is sometimes difficult to make the overall argument parallel (due to linear Require dependencies). However, it is common practice in individual proofs to see e.g.

apply lemma1; [ auto | firstorder | ].
apply lemma2; [ trivial | auto | ].
rest_of_proof...

In particular, applying lemma1 and lemma2 creates several (here three) subgoals, of which only one (here the third) is particularly interesting and the others can be solved by automation individually (also contain no evars).
More often than not, heavy automation increases compilation time.
Assume in the above auto, firstorder, and rest_of_proof take roughly the same time to compile.

Suggestion (is the following interesting/feasible?):
Introduce a tactical async such that given a tactic t, the tactic async t succeeds immediately (if the goal has no evars) and closes the goal. Simultaneously, a worker is spawned that is responsible to actually close the goal using the tactic t until Qed.

Returning to the above example

apply lemma1; [ async auto | async firstorder | ].
apply lemma2; [ trivial | async auto | ].
rest_of_proof...

would (given at least 4 CPU cores) compile several times faster. I know of par:, which does not seem to fit the above use case.

Before adding another [wish] to the Coq bugtracker, I wanted to know your opinion. Somewhat related: #9550

2 Likes
#2

Would something like

async: [auto | firstorder]

which is applicable if there are exactly two subgoals, and which works like par but runs auto on the first goal and firstorder on the second subgoal also suffice as a first step?

It would be less flexible than what you have in mind, but maybe easier to implement since one can take the implementation of par as starting point.

Maybe @ppedrot (or somebody else, I don’t know who is the expert for things like this) could comment how hard that seems to him, and whether it might make for a nice implementation project for a participant of the upcoming CUDW?

#3

I like your idea. It seems to me that it would be superior to the current par: goal selector indeed. As @yforster mentions, this could be a nice project for the upcoming CUDW (which will happen online from Nov 30th to Dec 4th).

#4

Note that we do not need a new tactic. For all intent and purpose, it already exists, it is called abstract. We just need to convince the IDE to run it asynchronously.

#5

That means destruct H; [abstract nia | abstract lia] runs nia and lia in parallel on the two resulting subgoals during compilation? (I.e. when called in a coqc run?)

Is that documented somewhere?

#6

That is not what I meant. The original post suggests to “introduce a tactical async such that given a tactic t, the tactic async t succeeds immediately (if the goal has no evars) and closes the goal.” What I meant is that abstract already checks that the goal has no evars and closes the goal by filling it with the application of a separate lemma, which is proved using the given tactic.

The thing is, all these steps are done sequentially, but there is no fundamental reason to do so. Closing the goal with the application of the separate lemma does not need the separate lemma to be fully proved already. The latter could be done asynchronously. This is already what happens when the separate lemma is explicitly stated by the user, but not when it is implicitly stated by abstract.

1 Like
#7

Ok, I think I understand: You’re suggesting to alter the semantics of abstract to match what Andrej suggested for a new async tactical?

After thinking a little, I would now say that both the change of the abstract tactic and an implementation of an async: goal selector would be very useful. @Zimmi48 is it easy to assess which one is easier for a not-so-experienced participant of the CUDW?

#8

That is my point. We do not need to change the semantics of abstract. We just need the IDE to verify the following lemma asynchronously, which it would do anyway if the user had written it by hand:

Lemma foo_subproof: goal.
Proof. t. Qed.
#9

We do not need to change the semantics of abstract. We

I think it does change if backtracking is involved.
Consider

Lemma foo : nat * bool.
Proof. split;try abstract exact true; exact 0. Defined.

If you delay the failure how do you get back to exact 0 where needed?

1 Like
#10

Good point. So, there is indeed a change of semantics.

#11

I don’t think I’m the best person to assess the difficulty of doing this, but given the points made by Guillaume, I think it is doable.