Nil-goal
How to proceed when the prover generates a goal of NIL
Failed proofs generally conclude with lists of key
checkpoints. (See set-gag-mode or introduction-to-key-checkpoints for an introduction to the notion of ``key
checkpoint''.) These lists may sometimes be annotated as follows.
[NOTE: A goal of NIL was generated. See :DOC nil-goal.]
This documentation topic gives some ideas about how to think about
the situation described by that message, that is: some goal has reduced to
NIL.
Suppose that you see the above NOTE. If you look at the proof log, you
will see a message saying that a goal of NIL has been generated. This
may indicate that the original goal is not a theorem, since most of the
prover's activity is typically to replace a goal by an equivalent conjunction
of its child subgoals. However, if some ancestor of the NIL goal has
undergone a process other than simplification or destructor elimination
— that is, fertilization (heuristic use of equalities), generalization,
or elimination of irrelevance — then it is quite possible that the
prover got to the NIL goal by replacing a goal by a stronger (and perhaps
false) conjunction of child subgoals.
Let's dig a bit deeper by considering two cases for production of a
NIL subgoal. First consider the case that the subgoal is a key
checkpoint at the top level or under a top-level induction — that is, a
key checkpoint listed in the proof summary. In that case, the original
conjecture is very likely not a theorem. Otherwise, if you are using gag-mode (which is the case by default), then you may need to issue the
command :pso (``Print Saved Output'') to see whether the goal was
strengthened from one that was originally a theorem; but here is what may be a
better idea. Instead, it may be best to focus on the key checkpoints printed
in the summary to see if they suggest useful rewrite rules to
prove.
If some NIL subgoal is under a key checkpoint at the top level or
under a top-level induction, then as discussed above, the original conjecture
is probably not a theorem. Therefore, in that case, ACL2 always prints a
NIL subgoal first in a list of checkpoints printed in the summary,
so that a NIL subgoal comes quickly to your attention.
