nil
Major Section: MISCELLANEOUS
At the end of a failed proof, one typically sees so-called ``key checkpoints'' (see set-gag-mode). These may 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: some goal has reduced to
nil.Suppose then that you see the above NOTE. If you look back at the proof log,
even with gag-mode enabled, 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 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 -- 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.
At present, if you are using gag-mode (the default) then you will need
to issue the command :pso (``Print Saved Output'') if you want to
see whether the situation above has occurred. However, that might not be
necessary. A good rule of thumb is that if the nil goal is under more
level of induction (e.g., with a prefix ``*i.j'' such as ``Subgoal
*1.1/2.2''), then there is some likelihood that the situation above did
indeed occur, and you can spend your time and energy looking at the key
checkpoints printed in the summary to see if they suggest useful rewrite
rules to prove. On the other hand, if the nil goal is at the top
level (e.g. with a name not starting with ``*'', such as ``Subgoal 3.2''),
then the original conjecture is probably not a theorem. If you do not
quickly see why that is the case, then you might find it useful to issue the
command :pso to see which case reduced to nil, in order to get
insight about how the theorem might be falsified.
