One Hint to Every Top-Level Goal in a Forcing Round
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
(if test '(:use lemma42) nil),
where
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
So one acceptable
(member-equal id '(((1) (3) . 0) ((1) (2) . 0) ((1) (1) . 0)))
or you could use
(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
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
(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