Introduction-to-hints
How to provide hints to the theorem prover
We assume you've read introduction-to-rewrite-rules-part-1,
introduction-to-key-checkpoints, and introduction-to-the-database.
You may give the theorem prover a hint that is specific to a particular
subgoal generated during a proof attempt. Of course, you learn the name of
the subgoal by inspecting the key checkpoints or other proof output. You are
not expected to anticipate the need for hints at specific subgoals; instead,
you usually deduce that a hint is required because the subgoals is not proved
but you see that existing rules and context make it provable.
The most common hint is to enable and/or disable a particular rule on some
particular subgoal.
(defthm name
formula
:hints (("Subgoal *1/3.2''" :in-theory (disable nth-nthcdr))))
The hint above tells the rewriter that just before it begins to work on
Subgoal *1/3.2'' it should switch to a local theory in which all of the
rules generated from the event nth-nthcdr are disabled. That local
theory remains the one in use for all descendant subgoals generated from the
one named, until and unless one of those descendant subgoals has an
:in-theory hint associated with it. There are many kinds of hints
besides :in-theory and in general, after each subgoal name, you can give
various forms of advice and list various adjustments you wish to make to the
context in which the prover is operating when it begins addressing the subgoal
named.
The top-level goal is always named Goal. Thus
(defthm name
formula
:hints (("Goal" ...hints1...)
("Subgoal *1/3.2''" ...hints2...)))
has the effect of using hints1 for the top-level goal and all of its
children throughout the entire proof, except for Subgoal *1/3.2'' and its
children, where hints2 is used instead.
There are a few hints which ``take effect'' exactly on the subgoal to which
they are attached and are not inherited by their descendents.
Here is an incomplete list of some of the more common hints; we note the
ones that do not pass on their effects to their descendants. We recommend
that you not follow the advanced links (marked ``'')
below until you have read the entire tutorial.
See in-theory for how to enable and/or disable rules. The new
theory is computed by a ``theory expression'' (see theories )
such as (disable nth-nthcdr) and typically makes adjustments such as
additions or deletions to the global current theory. All the relevant new
theories are computed before the proof begins. Thus, in
(defthm name
formula
:hints (("Goal" :in-theory (disable rule1))
("Subgoal *1/3.2''" (disable rule2))))
the theory mentioned for Goal is the global current theory minus
rule1, while the theory mentioned for its descendant, Subgoal
*1/3.2'', is the global current theory minus rule2. In particular, if
both rule1 and rule2 are enabled in the global current theory, then
rule1 is enabled during the processing of Subgoal *1/3.2'' because
it was not removed explicitly there.
See use for how to force the theorem prover to
take note of particular instances of particular theorems; in particular, the
instances are created and added as hypotheses to the subgoal in question. The
hint is not inherited by the descendants of the subgoal (since the formula
being proved has been modified by the hint). If the rule you are using (with
a :use hint) is an enabled rewrite rule, it might interfere with the
added hypothesis — by rewriting itself to T — and thus often
you will both :use ... and :in-theory (disable ...).
See expand for how to tell the theorem prover to expand one or
more function calls whenever encountered.
See cases for how to force the theorem prover to do a case
split to prove the subgoal under each of an exhaustive list of cases given in
the hint. This hint takes action specifically at the named subgoal and is not
passed down to its children.
See induct for how to tell the theorem prover to go
immediately into induction for the subgoal in question, and to use the
induction scheme suggested by the hint rather than the one suggested by the
terms in the subgoal itself. This hint is not inherited by its
descendents.
See hints for a complete list of all hints, and see hints-and-the-waterfall for a more thorough description of how the effects
of hints at a subgoal are inherited by the descendents.
If you are reading this as part of the tutorial introduction to the theorem
prover, use your browser's Back Button now to return to introduction-to-the-theorem-prover.
