		Search-engine friendly clone of the ACL2 documentation.

Goal-spec

To indicate where a hint is to be used

Examples:
"Goal"
"goal"
"Subgoal *1/3''"
"subgoal *1/3''"
"[2]Subgoal *1/3''"

When hints are given to the theorem prover, a goal-spec is provided to specify the goal to which the hints are to be applied. The hints provided are carried along innocuously until the named goal arises. When it arises, the hints are ``activated'' for that goal and its descendents.

A legal goal specification may be extracted from the theorem prover's output. Certain lines clearly label formulas, as in

Subgoal *1/3.2'
(IMPLIES ... ...)

and these lines all give rise to goal specifications. In general, these lines all start either with ``Goal'' or ``Subgoal'' or else with those words preceded by a number in square brackets, as in

[1]Subgoal *1/3.2'
(IMPLIES ... ...).

A goal specification may be obtained by deleting any surrounding whitespace from such a line and embedding the text in string quotation marks. Thus

"[1]Subgoal *1/3.2'"

is the goal specifier for the goal above.

As noted, a hint is applied to a goal when the hint's goal specification matches the name ACL2 assigns to the goal. The matching algorithm is case-insensitive. Thus, alternative goal specifications for the goal above are "[1]subgoal *1/3.2'" and "[1]SUBGOAL *1/3.2'". The matching algorithm does not tolerate non-case discrepancies. Thus, "[1]Subgoal*1/3.2'" and " [1]Subgoal *1/3.2'" are unacceptable.

Sometimes a formula is given two names, e.g.,

Subgoal *1/14.2'
(IMPLIES ...
         ...)
Name the formula above *1.1.

It is the first name (the one that starts with ``Goal'' or ``Subgoal'') and not the second which constitutes a legal goal-spec. Roughly speaking, when the system prints the line containing the goal specification, it activates any hints that are attached to that goal-spec. Consider the example above. Suppose Subgoal *1/14.2' could be proved by using a certain lemma instance. Then the appropriate entry in the hints would be:

("Subgoal *1/14.2'" :use ...)

This might surprise you because the system appears to do nothing to *1/14.2' besides push it for a subsequent induction. But actually between the time the system printed the goal-spec line and the time it decides to push the goal, you can think of the system as trying everything it has. So a use hint activated when Subgoal *1/14.2' arises is just what you want.

But what if you want to give an :induct hint? By the time induction is tried, the formula has been given the name *1.1. Well, this is one you just have to remember:

("Subgoal *1/14.2'" :induct ...).

When the above hint is activated the :induct directive short-circuits the rest of the processing and sends immediately the formula into the pool of goals to prove by induction. The induct hint is attached to the formula in the pool and when the time comes to turn our attention to that goal, the induct advice is followed.

You can probably figure out the naming conventions for goals after seeing some examples in prover output. Let's discuss the use of the character ' for a suffix. If a goal has a single subgoal then a prime is added; e.g., if "Subgoal 3.2" has a single subgoal then it is named "Subgoal 3.2'" rather than "Subgoal 3.2.1". If in turn that goal has a single subgoal, it is named "Subgoal 3.2''"; and so on. When four or more primes would be generated, say, n primes, then the suffix is "'n'"; e.g., continuing the preceding example we get "Subgoal 3.2'''", "Subgoal 3.2'4'", "Subgoal 3.2'5'", and so on. If any of these generates at least two subgoals then any ``prime'' suffix is dropped; for example, if "Subgoal 3.2'5'" has two subgoals then they are named "Subgoal 3.2.2" and "Subgoal 3.2.1".

We conclude by emphasizing a point made above, that a hint is applied to a goal when the hint's goal specification matches the name ACL2 assigns to the goal. If there is no such match, then the hint is ignored. Consider the following example.

(thm (equal (append (append x y) z) (append x y z))
     :hints (("Subgoal *1/" :in-theory nil)))

Normally, :in-theory hints are inherited by subgoals (see hints-and-the-waterfall), so you might expect that the empty theory is used in Subgoal *1/2 and Subgoal *1/1. But in fact, since there is no subgoal printed that is labeled Subgoal *1/, the above :in-theory hint is ignored. The above example is in contrast to the following, where the hint makes the proof fail, because there really is a Subgoal *1/ in the proof this time.

(thm (implies (and (not (endp x)) (not (endp (cdr x))))
              (equal (append (append x y) z) (append x y z)))
     :hints (("Subgoal *1/" :in-theory nil)))

Subtopics

Clause-identifier: The internal form of a goal-spec