how to use computed hints



Driving Home the Basics

The common hint

("Subgoal 3.2.1''" :use lemma42)
has the same effect as the computed hint
    '(:use lemma42)
which, of course, is equivalent to
     '(:use lemma42))
which is also equivalent to the computed hint
provided the following defun has first been executed
(defun my-special-hint (id clause world)
  (declare (xargs :mode :program)
           (ignore clause world))
      '(:use lemma42)


(defthm main (big-thm a b c)

(defthm main (big-thm a b c)



One Hint to Every Top-Level Goal in a Forcing Round


(if test '(:use lemma42) nil),



So one acceptable test is

                   ((1) (2) . 0)
                   ((1) (1) . 0)))
              '("[1]Subgoal 3"
                "[1]Subgoal 2"
                "[1]Subgoal 1"))




     (equal (cddr id) 0))      ; no primes

The test above is ``overkill'' because it recognizes precisely the clause ids in question. But recall that once a computed hint is used, it is removed from the hints available to the children of the clause. Thus, we can widen the set of clause ids recognized to include all the children without worrying that the hint will be applied to those children.


(equal (car id) '(1))
(equal (car (car id)) 1)





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

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)))
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)
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) in your hint to convert the current goal clause into the s-expression that is actually printed. For example, the clause

``prettyifies'' to
              (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:


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.


Computing the Hints

So far we have used computed hints only to compute when a fixed set of keys and values are to be used as a hint. But computed hints can, of course, compute the set of keys and values. You might, for example, write a hint that recognizes when a clause ``ought'' to be provable by a :BDD hint and generate the appropriate hint. You might build in a set of useful lemmas and check to see if the clause is proveable :BY one of them. You can keep all function symbols disabled and use computed hints to compute which ones you want to :EXPAND. In general, you can write a theorem prover for use in your hints, provided you can get it do its job by directing our theorem prover.

Suppose for example we wish to find every occurrence of an instance of (SWAP x) and provide the corresponding instance of ALL-SWAPS-HAVE-THE-PROPERTY. Obviously, we must explore the clause looking for instances of (SWAP x) and build the appropriate instances of the lemma. We could do this in many different ways, but below we show a general purpose set of utilities for doing it. The functions are not defined in ACL2 but could be defined as shown.

Our plan is: (1) Find all instances of a given pattern (term) in a clause, obtaining a set of substitutions. (2) Build a set of :instance expressions for a given lemma name and set of substitutions. (3) Generate a :use hint for those instances when instances are found.

The pair of functions below find all instances of a given pattern term in either a term or a list of terms. The functions each return a list of substitutions, each substitution accounting for one of the matches of pat to a subterm. At this level in ACL2 substitutions are lists of pairs of the form (var . term). All terms mentioned here are presumed to be in translated form.

The functions take as their third argument a list of substitutions accumulated to date and add to it the substitutions produced by matching pat to the subterms of the term. We intend this accumulator to be nil initially. If the returned value is nil, then no instances of pat occurred.

(defun find-all-instances (pat term alists)
 (declare (xargs :mode :program))
  (instancep alist)
  (one-way-unify pat term)
  (let ((alists (if instancep (add-to-set-equal alist alists) alists)))
     ((variablep term) alists)
     ((fquotep term) alists)
     ((flambdap (ffn-symb term))
      (find-all-instances pat
                          (lambda-body (ffn-symb term))
                          (find-all-instances-list pat (fargs term) alists)))
     (t (find-all-instances-list pat (fargs term) alists))))))

(defun find-all-instances-list (pat list-of-terms alists) (declare (xargs :mode :program)) (cond ((null list-of-terms) alists) (t (find-all-instances pat (car list-of-terms) (find-all-instances-list pat (cdr list-of-terms) alists))))))

We now turn our attention to converting a list of substitutions into a list of lemma instances, each of the form

(:INSTANCE name (var1 term1) ... (vark termk))
as written in :use hints. In the code shown above, substitutions are lists of pairs of the form (var . term), but in lemma instances we must write ``doublets.'' So here we show how to convert from one to the other:
(defun pairs-to-doublets (alist)
  (declare (xargs :mode :program))
  (cond ((null alist) nil)
        (t (cons (list (caar alist) (cdar alist))
                 (pairs-to-doublets (cdr alist))))))

Now we can make a list of lemma instances:

(defun make-lemma-instances (name alists)
  (declare (xargs :mode :program))
   ((null alists) nil)
   (t (cons (list* :instance name (pairs-to-doublets (car alists)))
            (make-lemma-instances name (cdr alists))))))

Finally, we can package it all together into a hint function. The function takes a pattern, pat, which must be a translated term, the name of a lemma, name, and a clause. If some instances of pat occur in clause, then the corresponding instances of name are :USEd in the computed hint. Otherwise, the hint does not apply.

(defun add-corresponding-instances (pat name clause)
  (declare (xargs :mode :program))
  (let ((alists (find-all-instances-list pat clause nil)))
     ((null alists) nil)
     (t (list :use (make-lemma-instances name alists))))))
The design of this particular hint function makes it important that the variables of the pattern be the variables of the named lemma and that all of the variables we wish to instantiate occur in the pattern. We could, of course, redesign it to allow ``free variables'' or some sort of renaming.

We could now use this hint as shown below:

(defthm ... ...
  :hints ((add-corresponding-instances
           '(SWAP x)
The effect of the hint above is that any time a clause arises in which any instance of (SWAP x) appears, we add the corresponding instance of ALL-SWAPS-HAVE-THE-PROPERTY. So for example, if Subgoal *1/3.5 contains the subterm (SWAP (SWAP A)) then this hint fires and makes the system behave as though the hint:
("Subgoal *1/3.5"
had been present.


Debugging Computed Hints



If you defmacro the macro below you could then write instead:

(defmacro show-hint (hint &optional marker)
   ((and (consp hint)
         (stringp (car hint)))
    `(let ((marker ,marker)
           (ans ,(if (symbolp hint)
                     `(,hint id clause world)
       (if ans
                (if (null marker) 0 1)


Some Final Comments





ACL2 Version Number


ACL2 !>*acl2-version*
"ACL2 Version 1.9"



(defthm version-8
while in version 1.9 you can prove
(defthm version-9


Therefore we adopted the draconian policy that books are certified by a given version of ACL2 and must be recertified to be used in other versions. While there are less draconian solutions to the problems illustrated above, we thought this was the simplest.


an explanation of why ACL2 has an explicit brr mode








ACL2 property lists and the ACL2 logical data base








