Removable-runes
Compute runes to disable
Example Form:
(removable-runes (defun proper-cons-nest-p (x)
(declare (xargs :guard (pseudo-termp x)))
(cond ((symbolp x) nil)
((fquotep x) (true-listp (cadr x)))
((eq (ffn-symb x) 'cons)
(proper-cons-nest-p (fargn x 2)))
(t nil)))
:verbose-p :minimal)
General Form:
(removable-runes event-form
:verbose-p v ; default = :normal
:multiplier m ; default = 1)
)
where event-form is an embeddable event (see events); v is
nil, :minimal, :normal, or t; and m is a positive
rational number. The value returned is an error-triple (mv erp
runes state), where erp is typically nil and runes is a list
of runes that can be disabled for the indicated event-form;
moreover, if the multiplier m is less than 1, then the event is admitted
with fewer prover steps. (See set-prover-step-limit for a discussion
of prover steps.) For example, if the list of runes returned for an event
form is ((:definition f1) (:rewrite thm1)), then the proof of that event
form was performed successfully — and, for the default m = 1, with
no more prover steps — if we first evaluate the event
(in-theory (disable (:definition f1) (:rewrite thm1))).
For a related utility, see minimal-runes.
WARNING: It is generally best to avoid using :in-theory hints in the form you supply to removable-runes or its related utility,
minimal-runes. We explain why below, after describing how the tool
works.
We now describe the two keyword arguments in turn, and in doing so, we
explain how the tool works.
The :verbose-p argument controls the level of output. We begin by
describing the default behavior. The output for the default value
:verbose-p = :normal is broken into sections for successive ``rounds''.
Each section appears as follows, other than the initial section, which only
lists the steps for the original proof attempt.
New steps: [steps]
Old steps: [steps] (Initially: [steps])
Time: [time]
Removed: [rune]
Removable:
[list of runes]
Used:
[list of runes]
[progress line]
The ``New Steps'' field has the number of prover steps taken by that
round's proof attempt. The ``Old Steps'', ``Time'',
``Removed'', ``Removable'', and ``Used'' fields state the
following, respectively: the number of prover steps for the previous round and
for the initial round (but this line is omitted for the initial round); the
time taken for the new event (by default, the run time; see get-internal-time); the rune that was newly disabled for the current round;
the list of runes disabled after the current round, which extends the previous
round's Removable field with that newly disabled rune; and the list of
runes used automatically in the proof for the current round. For all but the
initial round, the event was admitted in the previous round after disabling
the Removable runes (with an in-theory event), resulting in a set
S of runes reported for that event. The progress line shows attempts in
the current round to decrease the number of steps by disabling one rune from
S per attempt, using '.' for a failed such attempt and '+' for
a success. Each such rune is chosen from the list of runes reported for the
previous round.
If :verbose-p = :minimal, then the output will be as described above
except that the Removable and Used fields are omitted. If
:verbose-p = nil, then there is no output. Finally, if :verbose-p =
t, then all the fields are printed, but in addition you will see the usual
output for each attempt, each (except for the initial event) preceded by the
corresponding in-theory event.
We now say a bit more about the tool's algorithm as we describe the
:multiplier argument, which is 1 by default but can also be any positive
rational number. Recall that each round is an attempt to find a rune to
disable: specifically, one that provides the fewest number of resulting prover
steps. The multiplier provides a bound on the number of prover steps: if
s0 is the number of steps for the preceding (or initial) round, then the
number of steps for the next round is not allowed to exceed (floor (* m s0)
1), where m is the value of the :multiplier keyword. If this
bound reaches 0 (which can only happen if m < 1, the algorithm
terminates.
As promised above, we now explain why it is generally best to avoid using
:in-theory hints in the form you supply to
removable-runes or its related utility, minimal-runes. To see why,
consider the following example. First evaluate:
(include-book "tools/removable-runes" :dir :system)
(defund foo (x) (cons x x))
Notice that foo is now disabled; see defund. The
following example may seem surprising; an explanation is below.
ACL2 !>(removable-runes
(thm (equal (foo x) (cons x x))
:hints (("Goal" :in-theory (enable foo)))))
-
New steps: 15 (initial attempt)
Time: 0.00
Used: ((:DEFINITION FOO))
+
New steps: 15
Old steps: 15 (Initially: 15)
Time: 0.00
Removed: (:DEFINITION FOO)
Removable:
((:DEFINITION FOO))
Used:
((:DEFINITION FOO))
((:DEFINITION FOO))
ACL2 !>
The result is that the definition of foo is removable, i.e., can be
disabled; yet clearly that definition is needed for the proof! To understand
this possibly surprising result, understand that removable-runes precedes
each proof attempt by globally disabling the candidate set of removable runes.
So in essence the proof attempt when attempting to disable the definition of
foo is really as follows.
(progn (in-theory (disable foo))
(thm (equal (foo x) (cons x x))
:hints (("Goal" :in-theory (enable foo)))))
Obviously the hint takes precedence over the initial in-theory event,
which is why the proof succeeds. The moral of the story is this: avoid
:in-theory hints when using removable-runes or its companion tool,
minimal-runes. Instead, you could do this, for example:
(in-theory (enable foo))
(removable-runes
(thm (equal (foo x) (cons x x))))
Finally, we expand on a point made above. When a rune is chosen to add to
the evolving list of disables, the corresponding proof attempt might actually
involve runes that were not present in any earlier proof attempt. Any new
such runes are then considered for disabling in later rounds.
