Guard-simplification
Levels of simplification for guard proof obligations
ACL2 provides several features for obtaining the proof obligations
generated for guard verification. Each of these features can be
invoked with an argument that controls the level of simplification to be
applied before returning those proof obligations. This topic examines those
simplification levels. It starts by splitting the features into two groups;
then continues by explaining the three levels of simplification; and finally,
makes the key point that one group allows the top two levels of simplification
and the other group allows the bottom two levels.
These features can be partitioned into two groups, which we reference below
as the ``AT'' and ``AFTER'' groups, as follows. These
correspond respectively to the two groups discussed in the documentation
topic, guard-formula-utilities, for capturing formulas produced either
during guard verification or when a :guard-theorem is supplied for a
:use hint.
- Simplification AT guard-verification time:
- Simplification AFTER guard-verification time:
Each feature above has an argument (possibly optional) that controls the
level of simplification. Each such argument can take any of three values, as
follows. But NOTE: T and :LIMITED are the only legal values
for the “AT” (first) group, and :LIMITED and NIL are the
only legal values for the “AFTER'' (second) group.
- T:
Full simplification, which is the default behavior for verify-guards
- :LIMITED:
Reduced simplification, skipping simplifications that depend on the set of
currently enabled rules
- NIL:
No simplification
The key point of this topic is the following specification of the values
allowed for the simplification argument, for the features in each group. For
features in the AT group, T and :LIMITED are the legal
values. For features in the AFTER group, :LIMITED and NIL
are the legal levels. Let's see why this is reasonable and discuss whether
the missing value for each group might be allowed in the future.
First consider the AFTER group. A :guard-theorem
:use hint obtains the guard theorem proved for a previously
guard-verified function. The current-theory at the time of that
:use hint may be very different from what it was at guard-verification
time. Thus, when processing that hint it would be misleading to allow the
current theory to participate in simplification that produces the guard
theorem, since the result could be very different from the guard theorem
generated during the earlier guard verification. That is why the value T
is not allowed for the simplification argument of a :guard-theorem hint. Instead, the default is :LIMITED. The gthm
utility provides a way to show the formula that would be provided by a
:guard-theorem lemma instance, so gthm also disallows T, and
its default is also :LIMITED. Note that the utility verify-guards-formula is more appropriate than gthm to view the formula
to be proved if one is about to verify guards for a function. (If gthm
were to be used for that purpose too, then T might be allowed as a
simplification argument; but that could lead to confusion, in particular about
the default.)
Now consider the AT group, which relates to guard verification.
T is a reasonable default: it is generally useful to maximize
simplification while generating the guard theorem before attempting its proof.
But one may prefer more control, by avoiding simplification until the proof is
attempted. :LIMITED has proved to be a good compromise: it limits
simplification to basic operations, in particular avoiding goals that are
subsumed by other goals or are instances of trivial built-in-clause
rules. If the need arises to support NIL as a simplification value,
perhaps ACL2 will change to support that.
