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 at 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, before pushing a goal for later proof by induction if none of
these proof processes applies to the goal. When all goals have been thus
handled, the goal most recently pushed for proof by induction is considered,
and the process repeats.
When the simplification process is attempted unsuccessfully for a goal, the
goal is deemed to have ``settled down''. If no ancestor of the goal has
settled down, then the ``settled-down'' process is deemed to have ``hit'' on
the goal, the sole effect being that the goal makes a new pass through all
the waterfall processes. 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.
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 key lists maintained by the theorem prover to manage
hints. The other key 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 pending hints after the
selected hint is removed; (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. The primary function of this list is that when a goal is pushed for later proof by induction, 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 children goals; a hint is applied only when it is selected.
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 (at the top of the waterfall), the list of pending hints is
scanned, in order, until one of the hints is suitable 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.
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 a bit misplaced in this slightly tricky example. 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
indicated above, immediately causing another trip through the waterfall. At
that point the :in-theory
hint had already been removed when it applied,
leaving the default (:do-not
) hint as the only applicable hint. That
hint is indeed applied, resulting in the second ``Note'' above.
Also see override-hints for an advanced feature that allows modification of
the hint selected for a goal.