|
|
|---|
|
|
|
|---|
Consequences of how parallelized proofs of subgoals are pushed for induction
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
The following discussion, concerning the naming of subgoals pushed for proof by induction and the timeliness of aborting when two or more goals are pushed for proof by induction, only applies when waterfall parallelism is enabled (see set-waterfall-parallelism).
When two sibling subgoals (e.g. 4.5 and 4.6) both push goals to be proved by induction (e.g., 4.6 pushes *1 and 4.5 pushes *2), a name is assigned to the second pushed subgoal (e.g., *2) as if the first push hasn't happened (e.g., *2 is mistakenly called *1). In such a case, we say what the name _could_ be. The following non-theorem illustrates how this works.
(set-waterfall-parallelism :full) (thm (equal (append (car (cons x x)) y z) (append x x y)))
There is another consequence of the way the parallelized waterfall pushes
subgoals for proof by induction. Without waterfall parallelism enabled, ACL2
sometimes decides to abort instead of pushing a goal for later proof by
induction, preferring instead to induct on the original conjecture. But with
waterfall parallelism enabled, the prover no longer necessarily immediately
aborts to prove the original conjecture. Suppose for example that sibling
subgoals, Subgoal 4.6 and Subgoal 4.5, each push a subgoal for induction. If
the waterfall is performing the proof of each of these subgoals in parallel,
the proof will no longer abort immediately after the second push occurs, that
is at Subgoal 4.5. As a result, the prover will continue through Subgoal 4.4,
Subgoal 4.3, and beyond. It is not until the results of combining the proof
results of Subgoal 4.6 with the results from the remaining sibling subgoals
(4.5, 4.4, and so on), that the proof attempt will abort and revert to prove
the original conjecture by induction. This example illustrates behavior that
is rather like the case that