USING-COMPUTED-HINTS-3.html -- ACL2 Version 3.1

USING-COMPUTED-HINTS-3

Hints as a Function of the Goal (not its Name)

Major Section:  MISCELLANEOUS

Sometimes it is desirable to supply a hint whenever a certain term arises in a conjecture. For example, suppose we have proved

(defthm all-swaps-have-the-property
   (the-property (swap x))
   :rule-classes nil)

and suppose that whenever (SWAP A) occurs in a goal, we wish to add the additional hypothesis that (THE-PROPERTY (SWAP A)). Note that this is equivalent supplying the hint

(if test
    '(:use (:instance all-swaps-have-the-property (x A)))
    nil)

where test answers the question ``does the clause contain (SWAP A)?'' That question can be asked with (occur-lst '(SWAP A) clause). Briefly, occur-lst takes the representation of a translated term, x, and a list of translated terms, y, and determines whether x occurs as a subterm of any term in y. (By ``subterm'' here we mean proper or improper, e.g., the subterms of (CAR X) are X and (CAR X).)

Thus, the computed hint:

(if (occur-lst '(swap a) clause)
    '(:use (:instance all-swaps-have-the-property (x A)))
    nil)

will add the hypothesis (THE-PROPERTY (SWAP A)) to every goal containing (SWAP A) -- except the children of goals to which the hypothesis was added.

A COMMON MISTAKE users are likely to make is to forget that they are dealing with translated terms. For example, suppose we wished to look for (SWAP (LIST 1 A)) with occur-lst. We would never find it with

(occur-lst '(SWAP (LIST 1 A)) clause)

because that presentation of the term contains macros and other abbreviations. By using :trans (see trans) we can obtain the translation of the target term. Then we can look for it with:

(occur-lst '(SWAP (CONS '1 (CONS A 'NIL))) clause)

Note in particular that you must

* eliminate all macros and
* explicitly quote all constants.

We recommend using :trans to obtain the translated form of the terms in which you are interested, before programming your hints.

An alternative is to use the expression (prettyify-clause clause nil nil) in your hint to convert the current goal clause into the s-expression that is actually printed. For example, the clause

((NOT (CONSP X)) (SYMBOLP Y) (EQUAL (CONS '1 (CAR X)) Y))

``prettyifies'' to

(IMPLIES (AND (CONSP X)
              (NOT (SYMBOLP Y)))
         (EQUAL (CONS 1 (CAR X)) Y))

which is what you would see printed by ACL2 when the goal clause is that shown.

However, if you choose to convert your clauses to prettyified form, you will have to write your own explorers (like our occur-lst), because all of the ACL2 term processing utilities work on translated and/or clausal forms. This should not be taken as a terrible burden. You will, at least, gain the benefit of knowing what you are really looking for, because your explorers will be looking at exactly the s-expressions you see at your terminal. And you won't have to wade through our still undocumented term/clause utilities. The approach will slow things down a little, since you will be paying the price of independently consing up the prettyified term.

We make one more note on this example. We said above that the computed hint:

(if (occur-lst '(swap a) clause)
    '(:use (:instance all-swaps-have-the-property (x A)))
    nil)

will add the hypothesis (THE-PROPERTY (SWAP A)) to every goal containing (SWAP A) -- except the children of goals to which the hypothesis was added.

It bears noting that the subgoals produced by induction and top-level forcing round goals are not children. For example, suppose the hint above fires on "Subgoal 3" and produces, say, "Subgoal 3'". Then the hint will not fire on "Subgoal 3'" even though it (still) contains (SWAP A) because "Subgoal 3'" is a child of a goal on which the hint fired.

But now suppose that "Subgoal 3'" is pushed for induction. Then the goals created by that induction, i.e., the base case and induction step, are not considered children of "Subgoal 3'". All of the original hints are available.

Alternatively, suppose that "Subgoal 3' is proved but forces some other subgoal, "[1]Subgoal 1" which is attacked in Forcing Round 1. That top-level forced subgoal is not a child. All the original hints are available to it. Thus, if it contains (SWAP A), the hint will fire and supply the hypothesis, producing "[1]Subgoal 1'". This may be unnecessary, as the hypothesis might already be present in "[1]Subgoal 1". In this case, no harm is done. The hint won't fire on "[1]Subgoal 1" because it is a child of "[1]Subgoal 1" and the hint fired on that.