INTRODUCTION-TO-HINTS

how to provide hints to the theorem prover 
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-nthcdr are 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-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 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 Goal is 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 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 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 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.