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
community 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 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.
