		Search-engine friendly clone of the ACL2 documentation.

Hints

Hints-and-the-waterfall

How hints fit into the ACL2 proof waterfall

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 community book books/hints/basic-tests.lisp.

First, we describe the ACL2 ``waterfall''. Then, we describe how hints are handled by the waterfall.

The Waterfall.

The ACL2 waterfall is the heart of the ACL2 prover. It attempts to prove a given goal and either completes the proof, fails, or produces goals to be proved by induction or forcing rounds. The waterfall comprises a series of steps, such as simplification or generalization, each of which attempts to replace a given goal by zero or more subgoals whose provability implies provability of that goal. Note that every proof by induction starts a new trip through the waterfall, as does every forcing round; and these occur only after all preceding trips through the waterfall are complete. Let us see in more detail how the waterfall works.

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); that is followed by the main ACL2 simplifier and then the “settled-down” process described further below; and finally ACL2 attempts (in this order) destructor elimination, fertilization (heuristic use of equalities), generalization, and elimination of irrelevance. See architecture-of-the-prover for more information on these processes. 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''. This notion of ``settled down'' is handled, as follows, by the next waterfall process after simplification: the ``settled-down'' process. If some ancestor of the goal (possibly the goal itself) has previously settled down, then the ``settled-down'' process is deemed to have missed on the goal. Otherwise it hits 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, suppose that "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 it does not hit not on any of its children or their children (and so on), because each of those has an ancestor, "Subgoal 2.3", that has already been marked as ``settled-down''.

The next proof process after settled-down 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 descendants 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 overridden 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 descendants 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 !>(set-gag-mode nil)
<state>
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, consider
 combining them into a single hint of the form ("Goal" :kwd1 val1 :kwd2
 val2 ...). See :DOC hints and :DOC hints-and-the-waterfall; community
 book books/hints/merge-hint.lisp might also be helpful.

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

 [Note:  A hint was supplied for 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 first 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 community 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.