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, and see hints for an introduction to ACL2 hints and detailed documentation for specific hint types.
The remainder of this topic serves as a references 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 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 consulted when a goal is pushed for later proof by
induction, at which time the hint settings are stored so that when the
induction proof begins, it begins with those hint settings. Note that the
list of hint settings is not re-applied to descendents of a goal; a hint is
applied only when it is selected. 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 hints are chosen 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 is 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
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 hints to consider; 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. At that point
the :in-theory hint had previously been removed when it was applied,
leaving the default (:do-not) hint as the only applicable hint. That
hint is indeed 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.