HINTS-AND-THE-WATERFALL

how hints fit into the ACL2 proof waterfall
Major Section:  MISCELLANEOUS

Below we describe the flow of an ACL2 proof attempt, with special attention to how hints are applied during a proof. For most ACL2 users, only one point is important to take away from this documentation topic: you may specify hints during a proof (see hints; perhaps also see computed-hints and see default-hints), and they can be expected to behave intuitively. See the-method for a summary of how to interact with the ACL2 prover; see introduction-to-the-theorem-prover for a more detailed tutorial; and see hints for an introduction to ACL2 hints, including detailed documentation for specific hint types.

The remainder of this topic serves as a reference in case one needs a deeper understanding of the workings of ACL2's handling of hints. Also, for examples of the sophisticated use of hints, primarily for experts, see distributed book books/hints/basic-tests.lisp.

First, we describe the ACL2 ``waterfall'', which handles each goal either by replacing it with a list (possibly empty) of child goals, or else by putting the goal into a ``pool'' for later proof by induction. Then, we describe how hints are handled by the waterfall.

The Waterfall.

Each goal considered by the ACL2 prover passes through a series of proof processes, called the ``waterfall processes'', as stored in the constant *preprocess-clause-ledge*. The top process applies top-level hints, including :use hints; the next is a lightweight ``preprocess'' simplifier for ``simple'' rules (see simple); the next is the main ACL2 simplifier; and finally ACL2 attempts (in this order) destructor elimination, fertilization (heuristic use of equalities), generalization, and elimination of irrelevance. Each process may ``hit'', creating zero or more child goals that are each then handled at the top of the waterfall; or it may ``miss'', in which case the next process in the above sequence is considered. If all processes miss, then a ``push'' process defers the goal until it is later considered for proof by induction. When all goals have been thus handled, the goal most recently pushed for proof by induction is considered, and the process repeats.

We next describe the two additional ways in which control can be returned to the top of the waterfall.

When the simplification process is attempted unsuccessfully for a goal, the goal is deemed to have ``settled down''. In this case, and if no ancestor of the goal has settled down, then the ``settled-down'' process is deemed to have ``hit'' on the goal, the effect being that the goal makes a new pass through all the waterfall processes. (Other processes can then notice that settling down has occurred and modify their heuristics accordingly.) For example, if "Goal" simplifies to "Subgoal 2" (among others), and "Subgoal 2" simplifies to "Subgoal 2.3" (among others), which in turn is not further simplified, then the ``settled-down'' process hits on "Subgoal 2.3" but not on any of its children, their children, and so on.

When simplification has missed (and thus the goal has settled down), the next proof process is normally destructor elimination. However, if a computed hint is suitable (in a sense described below; also see computed-hints, especially the discussion of stable-under-simplificationp), then that hint is selected as control is returned to the top of the waterfall. A subtlety is that in this case, if the most recent hit had been from settling down, then the prover ``changes its mind'' and considers that the goal has not yet settled down after all as it continues through the waterfall.

Each time a goal is considered at the top of the waterfall, then before passing through the proof processes as described above, ACL2 searches for a relevant hint to select unless it has already been provided a hint in the ``stable-under-simplificationp'' case mentioned above. We turn now to a more thorough discussion of how hints are selected and applied.

The handling of hints.

In the discussion below we will ignore forcing rounds, as each forcing round is simply treated as a new proof attempt that uses the list of hints provided at the start of the proof.

When the theorem prover is called by thm or events such as defthm, defun, and verify-guards, it gathers up the hints that have been supplied, often provided as a :hints argument, but for example using a :guard-hints argument for guard verification proofs. (ACL2(r) users (see real) may also employ :std-hints.) It then appends these to the front of the list of default hints (see default-hints). The resulting list becomes the initial value of the list of ``pending hints'', one of two critical lists maintained by the theorem prover to manage hints. The other critical list is a list of ``hint settings''; the two lists are maintained as follows.

When a goal is first considered, a hint is selected from the list of pending hints if any is found to apply, as described below. If a hint is selected, then it takes effect and is removed from the pending hints. Except: if the selected hint is a computed hint with value t specified for :computed-hint-replacement, then it is not removed; and if that value is a list of hints, then that list is appended to the front of the list of pending hints after the selected hint is removed (also see computed-hints). The selected hint is also used to update the hint settings, as described below.

The list of hint settings associates hint keywords with values. It is passed from the current goal to its children (and hence the children's children, and so on), though modified by hints selected from pending hints, as described below. This list is maintained so that when a goal is pushed for proof by induction, the hint settings are applied at the start of the proof by induction. Note that the list of hint settings is not re-applied to descendents of a goal in the current waterfall; a hint is applied only when it is selected (and also perhaps later as just described, through the stored hint settings at the start of a proof by induction). For example, if the hint selected for "Subgoal 3" includes :in-theory (enable foo), then the hint settings are correspondingly updated when processing "Subgoal 3", and they persist at subgoals such as "Subgoal 3.2" and "Subgoal 3.2.1" (unless overriden by hints on those goals); but the theory specifying foo is not re-installed at every such subgoal.

When a hint is selected, the list of hint settings is updated so that for each keyword :kwd and associated value val from the hint, :kwd is associated with val in the hint settings, discarding any previous association of :kwd with a value in the hint settings. Except, certain ``top-level'' hints are never saved in the hint settings: :use, :cases, :by, :bdd, :or, and :clause-processor.

For example, suppose that we specify the following hints, with no default hints.

(("Goal" :expand ((bar x y)))
 ("Subgoal 3" :in-theory (enable foo)))
These hints then become the initial list of pending hints. When the proof attempt begins, the prover encounters the top-level goal ("Goal") and pulls the "Goal" hint from the pending hints, so that the list of hint settings contains a value only for keyword :expand. This hint setting will remain for all children of the top-level goal as well, and their children, and so on, and will be inherited by induction -- in other words, it will remain throughout the entire proof. Now consider what happens when the proof reaches "Subgoal 3". At this point there is only one pending hint, which is in fact attached to that subgoal. Therefore, this hint is pulled from the pending hints (leaving that list empty), and the hint settings are extended by associating the :in-theory keyword with the theory represented by (enable foo). That theory is immediately installed until the prover finishes addressing "Subgoal 3", its children, their children, and so on; and until that completion is reached, the :in-theory keyword remains associated with the (enable foo) in the hint settings, although of course there is no re-installation of the theory at any ensuing child goal. When finally "Subgoal 3" and its descendents have been completed and the prover is about to consider "Subgoal 2", the :in-theory association is removed from the hint settings and the global theory is re-installed. However, the list of pending hints remains empty.

It remains to describe how a hint is selected for a goal. When a goal is first considered (hence at the top of the waterfall), the list of pending hints is scanned, in order, until one of the hints is suitable for the goal. An explicit hint (goal-name :kwd1 val1 ... :kwdn valn) is suitable if goal-name is the name of the current goal and there is at least one keyword. A computed hint is suitable if it evaluates to a non-nil value. As indicated earlier in this documentation topic, an exception occurs when a computed hint is selected after simplification fails (the ``stable-under-simplificationp'' case): in that case, the goal returns to the top of the waterfall with that hint as the selected hint, and no additional search for a hint to select is made at that time.

The following slightly tricky example illustrates handling of hints.

ACL2 !>(set-default-hints '(("Goal" :do-not '(preprocess))))
 (("Goal" :DO-NOT '(PREPROCESS)))
ACL2 !>(thm (equal (append (append x y) z) (append x y z))
            :hints (("Goal" :in-theory (disable car-cons))))

ACL2 Warning [Hints] in ( THM ...):  The goal-spec "Goal" is explicitly
associated with more than one hint.  All but the first of these hints
may be ignored.  If you intended to give all of these hints, combine
them into a single hint of the form ("Goal" :kwd1 val1 :kwd2 val2 ...).
See :DOC hints-and-the-waterfall.

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

[Note:  A hint was supplied for our processing of the goal above. 
Thanks!]

Name the formula above *1.

The warning above is printed because "Goal" is associated with two pending hints: one given by the set-default-hints call and one supplied by the :hints keyword of the thm form. The :in-theory hint is selected because user-supplied hints are ahead of default hints in the list of pending hints; we then get the first ``Note'' above. The goal progresses through the waterfall without any proof process applying to the goal; in particular, it cannot be further simplified. After the simplification process, a ``settled-down'' process applies, as discussed above, immediately causing another trip through the waterfall. Since the :in-theory hint was earlier removed from the list of pending hints when it was applied, the default (:do-not) hint is now the only pending hint. That hint is applied, resulting in the second ``Note'' above.

Again, more examples may be found in the distributed book books/hints/basic-tests.lisp. A particularly tricky but informative example in that book is the one related to nonlinearp-default-hint.

Also see override-hints for an advanced feature that allows modification of the hint selected for a goal.