PARALLEL-PUSHING-OF-SUBGOALS-FOR-INDUCTION

consequences of how parallelized proofs of subgoals are pushed for induction
Major Section:  PARALLELISM

This documentation topic relates to the experimental extension of ACL2 supporting parallel evaluation 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 :otf-flg is t, in the sense that the abort does not happen immediately, but also rather like the case that :otf-flg is nil, in the sense that the abort does occur before getting to Subgoal 3.