To indicate where a hint is to be used
Examples: "Goal" "goal" "Subgoal *1/3''" "subgoal *1/3''" "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
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
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
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.
("Subgoal *1/14.2'" :use ...)
This might surprise you because the system appears to do nothing to
But what if you want to give an
("Subgoal *1/14.2'" :induct ...).
When the above hint is activated the
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
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)))
(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)))