Major Section: INTRODUCTION-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-nthcdrare disabled. That local theory remains the one in use for all descendent subgoals generated from the one named, until and unless one of those descendent subgoals has an
:in-theoryhint associated with it. There are many kinds of hints besides
:in-theoryand 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
(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 descendents. 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
Goalis the global current theory minus
rule1, while the theory mentioned for its descendent,
Subgoal *1/3.2'', is the global current theory minus
rule2. In particular, if both
rule2are enabled in the global current theory, then
rule1is 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 descendents 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
: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.