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
First, we describe the ACL2 ``waterfall''. Then, we describe how hints are handled by 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
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
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
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
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
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
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
When a hint is selected, the list of hint settings is updated so that for
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 (
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
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 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
Again, more examples may be found in the community book
Also see override-hints for an advanced feature that allows modification of the hint selected for a goal.