With-auto-termination
Re-use an existing termination proof automatically.
NOTE: THIS UTILITY HAS BEEN LARGELY SUPERSEDED BY
defunt. See defunt.
The following (admittedly, contrived) example shows how to use this
utility. First define:
(defund my-dec (x) (1- x))
(defun my-max (x y)
(declare (xargs :measure (+ (nfix x) (nfix y))
:hints (("Goal" :in-theory (enable my-dec)))))
(cond ((zp x) y)
((zp y) x)
(t (1+ (my-max (my-dec x) (my-dec y))))))
Now consider the following definition. Its recursion pattern resembles
that of the function above: we recur on the application of my-dec to the
two arguments, assuming both arguments are positive integers.
ACL2 !>(with-auto-termination
(defun my-sum (a b)
(cond ((and (posp a) (posp b))
(+ 2 (my-sum (my-dec a) (my-dec b))))
((zp b) a)
(t b))))
MY-SUM
ACL2 !>
We see that the function has been successfully admitted, since the function
name is returned and there is no error message. How did this happen? We can
evaluate :pe my-sum to see the resulting event, but an
alternative, before submitting the form above, is to ask just to show the
event, without evaluating it, using :show :event:
ACL2 !>:u
L 3:x(DEFUN MY-MAX (X Y) ...)
ACL2 !>(with-auto-termination
(defun my-sum (a b)
(cond ((and (posp a) (posp b))
(+ 2 (my-sum (my-dec a) (my-dec b))))
((zp b) a)
(t b)))
:show :event)
(DEFUN
MY-SUM (A B)
(DECLARE
(XARGS :MEASURE (BINARY-+ (NFIX A) (NFIX B))
:HINTS (("Goal" :USE (:INSTANCE (:TERMINATION-THEOREM MY-MAX)
(Y B)
(X A))
:IN-THEORY (THEORY 'AUTO-TERMINATION-THEORY)))))
(COND ((AND (POSP A) (POSP B))
(+ 2 (MY-SUM (MY-DEC A) (MY-DEC B))))
((ZP B) A)
(T B)))
ACL2 !>
We see that ACL2 found a function in the logical world whose
termination argument justifies the termination of my-sum — namely,
the function my-max. Then a suitable :measure and
:hints were generated in order to admit the new event.
General Form:
(with-auto-termination
form
:theory th ; default (theory 'auto-termination-theory)
:expand ex ; default nil
:show s ; default nil
:verbose v ; default :minimal
)
where form is a call of defun or defund, and keyword
arguments, which are not evaluated, have the defaults shown above. If this
event is successful, then the input definition is modified by adding a
generated declare form, which provides a :measure and :hints
that take advantage of the termination-theorem for an existing function
that was admitted without skipping proofs (see skip-proofs and set-ld-skip-proofs). The hints include a :use hint for that
earlier termination-theorem, as well as an :in-theory hint and possibly
an :expand hint, as discussed below. But before adding the new
declare form, any :measure and :hints are removed from the
input form.
We now describe the keyword arguments.
- :theory and :expand — These are probably only necessary in
the case of defining a reflexive function (one with a recursive call within a
recursive call, such as (f (f x))). These are passed along as
:in-theory and expand hints, respectively, on
"Goal" in the generated declare form. A convenient special value
for :theory is :current, which is equivalent to supplying the value
(current-theory :here).
- :show — If this is nil then ACL2 will attempt to admit the
resulting definition. Otherwise, :show should be either :event or
:dcl, in which case an error-triple is returned without changing
the ACL2 world. If :show is :event, then the resulting value
will be the generated definition, while if :show is :dcl, then the
resulting value will be just the generated declare form.
- :verbose — By default, if a declare form is successfully
generated, then the resulting event will be processed without output from the
prover. To see output from the prover, use :verbose t. To avoid even
the little messages about ``Searching'' and ``Reusing'', use :verbose
nil.
See community book kestrel/utilities/auto-termination-tests.lisp for more
examples.
