# Ad hoc asynchronicity

**URL:** <https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079>\
**Category:** Developing the Rocq Prover\
**Created:** [October 13, 2020, 6:03am UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079 "2020-10-13T06:03:00Z")\
**Posts on this page:** 11\
**Page:** 1

<div class="post-metadata">

**Author:** ![mrhaandi](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mrhaandi/32/379_2.png) [@mrhaandi](https://discourse.rocq-prover.org/u/mrhaandi)\
**Post date:** [October 13, 2020, 6:03am UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/1 "2020-10-13T06:03:00Z")

</div>

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.

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

```auto
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](https://github.com/coq/coq/issues/9550)

---

<div class="post-metadata">

**Author:** ![yforster](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yforster/32/30_2.png) [@yforster](https://discourse.rocq-prover.org/u/yforster)\
**Post date:** [October 14, 2020, 7:36am UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/2 "2020-10-14T07:36:39Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [October 23, 2020, 1:07pm UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/3 "2020-10-23T13:07:18Z")

</div>

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](https://github.com/coq/coq/wiki/Coq-Users-and-Developers-Workshop-2020) (which will happen online from Nov 30th to Dec 4th).

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [October 23, 2020, 3:14pm UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/4 "2020-10-23T15:14:13Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![yforster](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yforster/32/30_2.png) [@yforster](https://discourse.rocq-prover.org/u/yforster)\
**Post date:** [October 23, 2020, 3:51pm UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/5 "2020-10-23T15:51:17Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [October 23, 2020, 3:58pm UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/6 "2020-10-23T15:58:54Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![yforster](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yforster/32/30_2.png) [@yforster](https://discourse.rocq-prover.org/u/yforster)\
**Post date:** [October 23, 2020, 4:13pm UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/7 "2020-10-23T16:13:47Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [October 23, 2020, 4:25pm UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/8 "2020-10-23T16:25:12Z")

</div>

> [@yforster](#):
>
> You’re suggesting to alter the semantics of `abstract` to match what Andrej suggested for a new `async` tactical?

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:

```coq
Lemma foo_subproof: goal.
Proof. t. Qed.

```

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [October 23, 2020, 4:45pm UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/9 "2020-10-23T16:45:50Z")

</div>

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

I think it does change if backtracking is involved.  
Consider

```coq
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?

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [October 23, 2020, 5:01pm UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/10 "2020-10-23T17:01:33Z")

</div>

> [@SkySkimmer](#):
>
> I think it does change if backtracking is involved.

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

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [October 23, 2020, 7:44pm UTC](https://discourse.rocq-prover.org/t/ad-hoc-asynchronicity/1079/11 "2020-10-23T19:44:09Z")

</div>

> [@yforster](#):
>
> @Zimmi48 is it easy to assess which one is easier for a not-so-experienced participant of the CUDW?

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.