Examples illustrating `simplify-defun`.

See simplify-defun for relevant background. The examples
below are deliberately simple, in order to make clear how `simplify-defun` behaves with various keyword arguments.

We start with the following basic example.

(defun bar (x) (declare (xargs :measure (nfix x))) (if (zp x) 0 (+ 1 1 (bar (+ -1 x))))) (include-book "kestrel/apt/simplify" :dir :system) (simplify-defun bar :new-name bar-simp :thm-name bar-simplified :new-enable nil :thm-enable t)

ACL2 responds to this call of

(DEFUND BAR-SIMP (X) (DECLARE (XARGS :GUARD T :MEASURE (NFIX X) :VERIFY-GUARDS NIL ; would be T if BAR were guard-verified :HINTS (("Goal" :USE (:TERMINATION-THEOREM BAR)) '(:IN-THEORY (DISABLE* BAR (:E BAR) (:T BAR)))))) (IF (ZP X) 0 (+ 2 (BAR-SIMP (+ -1 X)))))

Notice that the guard and measure are the same as for

Adding

To see the full expansion produced by the call of

(ENCAPSULATE NIL ... ; helpful stuff local to the encapsulate (DEFUND BAR-SIMP (X) ...) ; as shown above (LOCAL ; helper events, not shown here ...) (DEFTHM BAR-SIMPLIFIED ; the value of keyword argument :thm-name (EQUAL (BAR X) (BAR-SIMP X)) :HINTS ...))

On the other hand, if you want less output, not more, use

ACL2 !>(simplify-defun bar :new-name bar-simp :thm-name bar-simplified :new-enable nil :thm-enable t :print nil) T ACL2 !>:pe bar-simp d 3:x(SIMPLIFY-DEFUN BAR :NEW-NAME ...) >L d (DEFUN BAR-SIMP (X) (DECLARE (XARGS :GUARD T :MEASURE (NFIX X) :VERIFY-GUARDS NIL :HINTS (("Goal" :USE (:TERMINATION-THEOREM BAR))))) (IF (ZP X) 0 (+ 2 (BAR-SIMP (+ -1 X))))) ACL2 !>

Notice the calls of `defund` and `defthm`, which respect
keyword arguments supplied to

The following trivial example illustrates the use of assumptions.

(defun foo (x) (ifix x)) (simplify-defun foo :assumptions ((integerp x)))

If you want to evaluate the

(simplify-defun foo :assumptions (:eval '((integerp x))))

Here is the result (either way). Notice that since we did not specify

(DEFUN FOO$1 (X) (DECLARE (XARGS :GUARD T :VERIFY-GUARDS NIL)) X)

Notice that the body was simplified under the given assumption that

The

(defun foo (x) (declare (xargs :guard (true-listp x))) (if (consp x) (foo (cdr x)) x))

In this example we specify

(show-simplify-defun foo :assumptions :guard :hints (:assumptions-preserved ; the sole applicability condition (("Goal" :in-theory (e/d (append) (union-eq))))))

The command above generates the following key lemma. Note that the local
function

(DEFTHM FOO-HYPS-PRESERVED-FOR-FOO-LEMMA (FLET ((FOO-HYPS (X) (DECLARE (IGNORABLE X)) (TRUE-LISTP X))) (IMPLIES (AND (FOO-HYPS X) (CONSP X)) (FOO-HYPS (CDR X)))) :HINTS (("Goal" :IN-THEORY (E/D (APPEND) (UNION-EQ))) '(:USE (:GUARD-THEOREM FOO))) :RULE-CLASSES NIL)

Since the original body is

The examples above all pertain to simplifying the body of a definition. The following example shows how to simplify the guard and/or measure of a definition.

ACL2 !>(defun foo (x) (declare (xargs :guard (and (true-listp x) (not (atom x))) :measure (fix (len x)))) (if (consp (cdr x)) (foo (append nil (cdr x))) x)) ... FOO ACL2 !>(simplify-defun foo :simplify-body nil :simplify-guard t :simplify-measure t) (DEFUN FOO$1 (X) (DECLARE (XARGS :GUARD (AND (TRUE-LISTP X) (CONSP X)) :MEASURE (LEN X) :VERIFY-GUARDS T :GUARD-HINTS ... ; uses (:GUARD-THEOREM FOO) :HINTS ... ; uses (:GUARD-THEOREM FOO) )) (IF (CONSP (CDR X)) (FOO$1 (APPEND NIL (CDR X))) X)) ACL2 !>

Clearly the values of both the

Notice that the body has not been simplified, even though ACL2 could easily
simplify

(simplify-defun foo :simplify-body nil :simplify-guard t :simplify-measure t :guard-hints (("Goal" :use car-cons)) :measure-hints (("Goal" :in-theory (enable nth))))

This time our own hints show up in the resulting definition of

:GUARD-HINTS (("Goal" :USE CAR-CONS)) :HINTS (("Goal" :IN-THEORY (ENABLE NTH)))

By default, simplification done on behalf of `defun` form — is
carried out in the current theory (see current-theory). However, the

(defun foo (x) (declare (xargs :guard (natp x))) (car (cons (+ x x) 3))) (defthmd double ; disabled globally (equal (+ x x) (* 2 x))) (simplify-defun foo :theory '(double natp) :simplify-body t ; default :simplify-guard t)

The resulting `defun` form contains simplifications for both the
guard and the body. The rewrite rule

For convenience, *exactly* those two rules.

(DEFUN FOO$1 (X) (DECLARE (XARGS :GUARD (AND (INTEGERP X) (NOT (< X 0))) :VERIFY-GUARDS T :GUARD-HINTS ...)) (* 2 X))

At this point let us mention the one keyword argument not yet mentioned:

:VERIFY-GUARDS NIL

instead of what it has currently, namely the following.

:VERIFY-GUARDS T

Examples above illustrate Boolean values for the

(defun foo (x) x) (defun bar (x) (if x (cons x x) 17)) (defun f (x y z) (cons (if (foo x) (bar x) z) (if (foo x) (foo y) z))) (simplify-defun f :simplify-body (if (foo x) @ z))

In a left-to-right depth-first traversal of the body of *governors* of the subterm, formed from the superior IF-tests. In this
case,

ACL2 !>(simplify-defun f :simplify-body (if (foo x) @ z)) (DEFUN F$1 (X Y Z) (DECLARE (XARGS :GUARD T :VERIFY-GUARDS NIL)) (CONS (IF (FOO X) (CONS X X) Z) (IF (FOO X) (FOO Y) Z))) ACL2 !>

Any variable whose name begins with an atsign (

(simplify-defun f :simplify-body (if (foo a) @ z))

The specified pattern does not match the subterm

(simplify-defun f :simplify-body (if (foo _a) @ z))

For that matter, we can even replace

(simplify-defun f :simplify-body (if (foo _a) @ _b))

Both of the

On the other hand, the following call fails because the variable

(simplify-defun f :simplify-body (if (foo _a) @ _a))

The _-var, `symbol-name`,

(simplify-defun f :simplify-body (if (foo _) @ _))

See simplify-defun (specifically, the section on the

We have seen that the language of patterns allows variables

(simplify-defun f :simplify-body (if (foo _) (:@ _) _))

Let's look at another example of the use of

(defun g (x y) (list (+ (nth 0 x) 3) (* (car (cons y y)) 4) (* (nth 0 x) 5)))

Suppose we want to simplify just the second call of

ACL2 !>(simplify-defun g :simplify-body (* (:@ (nth 0 x)) _)) (DEFUN G$1 (X Y) (DECLARE (XARGS :GUARD T :VERIFY-GUARDS NIL)) (LIST (+ (NTH 0 X) 3) (* (CAR (CONS Y Y)) 4) (* (AND (CONSP X) (CAR X)) 5))) ACL2 !>

Notice that neither of the following alternatives would produce the result above.

; Would simplifythe first occurrence of (nth 0 x) instead: (simplify-defun g :simplify-body (:@ (nth 0 x))) ; Would simplify (car (cons y y)) instead. (simplify-defun g :simplify-body (* @ _))

Here is an example that specifies more than one subterm to be simplified. Consider:

(defun foo (x y) (list (list (list (* 3 (+ 1 (+ 1 x))) (* 3 (+ 1 (+ 1 x))) (* 4 5 (+ 1 (+ 1 y)))))))

Then the indicated pattern below matches the subterm

(list (* 3 (+ 1 (+ 1 x))) (* 3 (+ 1 (+ 1 x))) (* 4 5 (+ 1 (+ 1 y))))

with the @-var

ACL2 !>(simplify-defun foo :simplify-body (list @1 ; equivalently, (:@ _@1) _ (* _ 5 @2))) (DEFUN FOO$1 (X Y) (DECLARE (XARGS :GUARD T :VERIFY-GUARDS NIL)) (LIST (LIST (LIST (+ 6 (* 3 X)) (* 3 (+ 1 (+ 1 X))) (* 4 5 (+ 2 Y)))))) ACL2 !>

Actually, it suffices simply to use only the special @-var,

(simplify-defun foo :simplify-body (list @ _ (* _ 5 @))) (simplify-defun foo :simplify-body (list (:@ _) _ (* _ 5 (:@ _))))

It is also possible to specify simplification inside `let`
and `let*` expressions. Let's look at two examples based on the
following definition.

(defun let-test (x y) (let* ((u (cons x x)) (v (car u))) (car (cons v y))))

First we simplify one of the bindings.

(simplify-defun let-test :simplify-body (:@ (car _)))

The new definition body results from simplifying the binding of

(LET ((V X)) (CAR (CONS V Y)))

This time, let us simplify just the body of the definition. What do you think the result will be? It might surprise you.

(simplify-defun let-test :simplify-body (:@ (car (cons _ _))))

You might have expected that the new body is obtained simply by replacing

X

To see why, consider how

By default, the simplified body is equal to the original body, under the given assumptions (if any). But you may specify that the two bodies should merely be equivalent, with respect to a specified known equivalence relation. Here is an example showing how that works. We start with the following events.

(defun fix-true-listp (lst) (if (consp lst) (cons (car lst) (fix-true-listp (cdr lst))) nil)) (defthm member-fix-true-listp (iff (member a (fix-true-listp lst)) (member a lst))) (defun foo (e x) (member-equal e (fix-true-listp x)))

We would like to eliminate the call of

ACL2 !>(simplify-defun foo :equiv iff) (DEFUN FOO$1 (E X) (DECLARE (XARGS :GUARD T :VERIFY-GUARDS NIL)) (MEMBER-EQUAL E X)) ACL2 !>

If `mutual-recursion`, then every function defined with

(mutual-recursion (defun foo (x) (if (atom x) (+ 1 1) (cons (ffn-symb x) (foo-lst (rest x))))) (defun foo-lst (x) (if (atom x) nil (cons (+ 1 2 (foo (first x))) (foo-lst (rest x)))))) (simplify-defun foo)

The result is the introduction of a new

(MUTUAL-RECURSION (DEFUN FOO$1 (X) (DECLARE (XARGS ...)) (IF (CONSP X) (CONS (CAR X) (FOO-LST$1 (CDR X))) 2)) (DEFUN FOO-LST$1 (X) (DECLARE (XARGS ...)) (IF (CONSP X) (CONS (+ 3 (FOO$1 (CAR X))) (FOO-LST$1 (CDR X))) NIL)))

Moreover, keyword arguments are handled in a special way (except for
*clique* of functions introduced by the

(simplify-defun foo :simplify-body (:map (foo t) (foo-lst nil)))

Then, as specified, only the definition of

(MUTUAL-RECURSION (DEFUN FOO$1 (X) (DECLARE (XARGS ...)) (IF (CONSP X) (CONS (CAR X) (FOO-LST$1 (CDR X))) 2)) (DEFUN FOO-LST$1 (X) (DECLARE (XARGS ...)) (IF (ATOM X) NIL (CONS (+ 1 2 (FOO$1 (FIRST X))) (FOO-LST$1 (REST X))))))