test in a computed hint of the form (if test '(:key1 val1 ...) nil).
Major Section: MISCELLANEOUS
Suppose the main proof completes with a forcing round on three
subgoals, "[1]Subgoal 3", "[1]Subgoal 2", and "[1]Subgoal 1".
Suppose you wish to :use lemma42 in all top-level goals of the
first forcing round. This can be done supplying the hint
(if test '(:use lemma42) nil),where
test is an expression that returns
t when ID is one of the clause ids in question.
goal-spec (parse-clause-id goal-spec)
"[1]Subgoal 3" ((1) (3) . 0)
"[1]Subgoal 2" ((1) (2) . 0)
"[1]Subgoal 1" ((1) (1) . 0)
Recall (see clause-identifier) that parse-clause-id maps
from a goal spec to a clause id, so you can use that function on the
goal specs printed in the failed proof attempt to determine the
clause ids in question.
So one acceptable test is
(member-equal id '(((1) (3) . 0)
((1) (2) . 0)
((1) (1) . 0)))
or you could use parse-clause-id in your computed hint if you
don't want to see clause ids in your script:
(or (equal id (parse-clause-id "[1]Subgoal 3"))
(equal id (parse-clause-id "[1]Subgoal 2"))
(equal id (parse-clause-id "[1]Subgoal 1")))
or you could use the inverse function (see clause-identifier):
(member-equal (string-for-tilde-@-clause-id-phrase id)
'("[1]Subgoal 3"
"[1]Subgoal 2"
"[1]Subgoal 1"))
Recall that what we've shown above are the tests to use in the
computed hint. The hint itself is (if test '(:use lemma42) nil)
or something equivalent like (and test '(:use lemma42)).
The three tests above are all equivalent. They suffer from the problem of requiring the explicit enumeration of all the goal specs in the first forcing round. A change in the script might cause more forced subgoals and the ones other than those enumerated would not be given the hint.
You could write a test that recognizes all first round top-level
subgoals no matter how many there are. Just think of the
programming problem: how do I recognize all the clause id's of the
form ((1) (n) . 0)? Often you can come to this formulation of
the problem by using parse-clause-id on a few of the candidate
goal-specs to see the common structure. A suitable test in this
case is:
(and (equal (car id) '(1)) ; forcing round 1, top-level (pre-induction)
(equal (len (cadr id)) 1) ; Subgoal n (not Subgoal n.i ...)
(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 (by default) 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.
In particular, the following test supplies the hint to every top-level goal of the first forcing round:
(equal (car id) '(1))You might worry that it would also supply the hint to the subgoal produced by the hint -- the cases we ruled out by the ``overkill'' above. But that doesn't happen since the hint is unavailable to the children. You could even write:
(equal (car (car id)) 1)which would supply the hint to every goal of the form "[1]Subgoal ..." and again, because we see and fire on the top-level goals first, we will not fire on, say, "[1]Subgoal *1.3/2", i.e., the id '((1 1 3) (2) . 0) even though the test recognizes that id.
Finally, the following test supplies the hint to every top-level goal of every forcing round (except the 0th, which is the ``gist'' of the proof, not ``really'' a forcing round):
(not (equal (car (car id)) 0))
Recall again that in all the examples above we have exhibited the
test in a computed hint of the form (if test '(:key1 val1 ...) nil).