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.
