Coverage-problems
Proving the coverage obligation in GL-based proofs.
In order to prove a theorem using GL, one must show that the
symbolic objects chosen to represent the inputs are sufficiently general to
cover the entire set of interest. See shape-specs for a more in-depth
discussion. The def-gl-thm and def-gl-param-thm events as well
as the gl-hint hints all provide some degree of automation for coverage
proofs; often this is enough to satisfy the coverage obligation without further
user interaction. Here we discuss how to debug coverage proofs that do not
succeed.
First, it is probably important to be able to re-run a coverage proof easily
without also re-running the associated symbolic execution, which may be quite
time-consuming. To do this, in either the def-gl-thm or def-gl-param-thm forms, add the keyword argument :TEST-SIDE-GOALS T.
This form will then try to prove the coverage obligation in exactly the manner
it would do during the real proof, but it will not attempt to prove the theorem
itself, and will not record a new ACL2 theorem even if the proof is
successful.
During proof output, GL prints a message "Now proving coverage" when it
begins the coverage proof. The initial goal of a coverage proof will also have
a hypothesis (GL::GL-CP-HINT 'GL::COVERAGE); this hypothesis is logically
meaningless, but a useful indicator of the beginning of a coverage proof.
When GL's usual set of heuristics is used, a coverage proof proceeds as
follows. The initial goal is as follows:
(implies <theorem-hyps>
(gl::shape-spec-obj-in-range
<list-of-input-bindings>
<list-of-input-variables>))
The coverage heuristics proceed by repeatedly opening up the
GL::SHAPE-SPEC-OBJ-IN-RANGE function. This effectively splits the proof
into cases for each component of each variable; for example, if one variable's
shape specifier binding is a cons of two :G-INTEGER forms, then its CAR and CDR
will be considered separately. Eventually, this results in several subgoals,
each with conjunction of requirements for some component of some input.
During this process of opening the GL::SHAPE-SPEC-OBJ-IN-RANGE
conclusion, the coverage heuristics also examine and manipulate the hypotheses.
When the conclusion is focused on a certain input variable or component of that
variable, and some hypothesis does not mention that variable, that hypothesis
will be dropped so as to speed up the proof. If a hypothesis does mention that
variable, it may be expanded (if it is not a primitive) so as to try and gain
more information about that variable. This is a useful heuristic because often
the hypotheses consist of a conjunction of predicates about different input
variables or components of input variables, and some of these predicates are
often themselves defined as conjunctions of predicates about subcomponents.
However, sometimes this expansion goes too far. In many cases, some
conjuncts from the hypothesis have nothing to do with the coverage obligation.
In these cases, the :DO-NOT-EXPAND keyword argument to DEF-GL-THM and
DEF-GL-PARAM-THM may be used. This argument should evaluate to a list of
function symbols; the coverage heuristic is then prohibited from expanding any
of these functions.
For efficiency, the set of rules used in coverage proofs is very restricted.
Because of this, you may see in the proof output a goal which should be
obvious, but is not proven because the necessary rule is not included. The
keyword argument :COV-THEORY-ADD may be used to enable certain additional
rules that are not included. The set of rules that are used is defined in the
ruleset GL::SHAPE-SPEC-OBJ-IN-RANGE-OPEN, which can be listed using
(get-ruleset 'gl::shape-spec-obj-in-range-open (w state)).
The default heuristics for coverage proofs may not always be useful.
Therefore, the user may also supplement or replace the coverage heuristics with
arbitrary computed hints. The keyword argument :COV-HINTS gives a list of
computed hint forms which, according to the value of the keyword argument
:COV-HINTS-POSITION, either replaces or supplements the default hints.
:COV-HINTS-POSITION may be either :REPLACE, in which case the
defaults are not used at all; :FIRST, in which case the user-provided
:COV-HINTS are tried first and the defaults afterward, or the default,
:LAST, in which case the default coverage heuristic is tried before the
user-provided hints.
Note that subgoal names will be different between a :TEST-SIDE-GOALS
and an actual attempt at proving the theorem. Therefore, it is best not to
write computed hints that depend on the ID variable.
