Simplify-defun-examples
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.
Example Set 1: Basics
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 simplify-defun by creating the following
DEFUN form among others, silently submitting the created forms, and then
returning the new DEFUN form (as the value component of an ACL2::error-triple). The new function is named bar-simp because that is
what we specified with the :new-name argument above.
(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 BAR, but the
subterm (+ 1 1 (bar (+ -1 x))) of the body of bar has been replaced
by the simpler term (+ 2 (BAR-SIMP (+ -1 X))) in the body of
bar-simp, with the recursive call appropriately replaced.
Adding :verbose t shows simplified non-trivial :assumptions,
followed by the proposed simplified definition, and then prover output from
evaluating the generated ACL2::events.
To see the full expansion produced by the call of simplify-defun
above, we can use show-simplify-defun instead of simplify-defun, on
the same arguments (or, simply add keyword argument :show-only t to your
simplify-defun call). The result is as follows (elided somewhat).
(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
simplify-defun with :print nil. For example:
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 simplify-defun, :new-enable nil
and :thm-enable t, respectively.
Example Set 2: Assumptions
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 :assumptions argument, or indeed any
argument A of simplify-defun, simply replace A by (:eval
A). The simplify-defun call displayed just above is thus equivalent to
the following.
(simplify-defun foo :assumptions (:eval '((integerp x))))
Here is the result (either way). Notice that since we did not specify
:new-name, the generated function name is obtained by adding a suffix
"$1" to the given function symbol's name. In general, the least
natural number n will be used that results in a new function symbol when
adding the suffix "$n".
(DEFUN FOO$1 (X)
(DECLARE (XARGS :GUARD T
:VERIFY-GUARDS NIL))
X)
Notice that the body was simplified under the given assumption that x
is an integer; without any such assumption, simplification to x would not
have taken place.
The :hints argument allows you to supply ACL2::hints for the
key lemma that specifies preservation of the assumptions on recursive calls.
The following example illustrates how that works, based on this
definition.
(defun foo (x)
(declare (xargs :guard (true-listp x)))
(if (consp x)
(foo (cdr x))
x))
In this example we specify :assumptions :guard, which means that the
:assumptions value is taken to be the given function's guard.
(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 FOO-HYPS is defined above with the same formals as the given
function symbol, and with a body that represents the :assumptions
argument, which in this example specifies the guard of foo.
(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 (if (consp x) (foo$1 (cdr x)) x), we see
that x has been simplified to nil under the combination of the
top-level assumption of (true-listp x), from :assumptions :guard,
and the governing IF test of (not (consp x)).
Example Set 3: Simplifying the Guard and Measure
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 :guard and the :measure have been
simplified.
Notice that the body has not been simplified, even though ACL2 could easily
simplify (APPEND NIL (CDR X)) to (CDR X), because of the argument
:simplify-body nil. To simplify the body as well, we can omit
:simplify-body so that its value defaults to t, or we can specify
:simplify-body t explicitly.
Example Set 4: Guard and Measure Hints
Simplify-defun provides keywords :guard-hints and
:measure-hints for the guard verification and termination proofs of the
simplified function that is generated. To see how these work, we can add such
hints to the simplify-defun form displayed in the section just above.
Recall that the default hints generated for the guard and termination proofs
use the guard and termination theorems, respectively, for the function whose
definition is being simplified. Suppose now that we add our own hints, for
example rather nonsensical :guard-hints and :measure-hints as
follows.
(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 FOO$1
in place of those that are generated by default.
:GUARD-HINTS (("Goal" :USE CAR-CONS))
:HINTS (("Goal" :IN-THEORY (ENABLE NTH)))
Example Set 5: Controlling the Theory for Simplification
By default, simplification done on behalf of simplify-defun —
whether for the body, guard, or measure of a defun form — is
carried out in the current theory (see current-theory). However, the
:theory keyword allows control over that theory without changing the
current theory globally. Consider the following example.
(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 double and the definition of
natp were applied during the simplification, in spite of being globally
disabled, because of the specified :theory for simplification. Note
that this theory works its way into the generated :guard-hints for the
generated function.
For convenience, :enable and/or :disable keywords are available,
provided that they are not used when :theory is used. For example,
specifying :enable (double natp) instead of the :theory hint above
gives the following result. Notice that the body is further simplified
because the built-in rewrite rule car-cons is available this time,
because the theory is constructed by enabling double and natp,
rather than consisting of 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. By default, the value of this keyword is :auto,
meaning that the value of :verify-guards in the generated defun is
t if the input function symbol is guard-verified, and otherwise is
nil. If you supply :verify-guards nil explicitly in your
simplify-defun call, however, then nil will be used instead. For
example, that would change the defun for FOO$1 displayed just above
to include
:VERIFY-GUARDS NIL
instead of what it has currently, namely the following.
:VERIFY-GUARDS T
Example Set 6: Simplifying a Subterm
Examples above illustrate Boolean values for the :simplify-body
keyword (default t). However, :simplify-body can specify a pattern,
to indicate one or more specific subterms to be simplified. Consider the
following example.
(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 f, the first
subterm that matches the pattern — where @ is allowed to be
instantiated — is the subterm (if (foo x) (bar x) z). For that
match, the appropriate instantiation of @ is (bar x). Therefore,
the value of :simplify-body above instructs simplify-defun to
simplify not the entire body of f, but only the subterm (bar x).
That simplification is to be performed under the result of simplifying the
conjunction of the :assumptions (simply t in this case) with the
governors of the subterm, formed from the superior IF-tests. In this
case, (bar x) is governed by (foo x), so the subterm (bar x) is
simplified under the simplification of (foo x), i.e., under the
assumption of x (i.e., that x is non-nil). Under that
assumption, (bar x) simplifies to (cons x x), which explains how the
new body below is derived from the body of the input function symbol, f.
Notice that no other part of the body has changed.
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 (@) gets this special
treatment, that is, indicating a simplification site. We call such variables
``@-vars''. Variables whose name starts with the underscore
character (_), called ``_-vars'', also get special treatment: like
@-vars, they can be instantiated to match a subterm of the body, but unlike
@-vars, they do not indicate simplification sites. For the definitions of
foo, bar, and f as above, consider the following form.
(simplify-defun f
:simplify-body (if (foo a) @ z))
The specified pattern does not match the subterm (IF (FOO X) (CONS X X)
Z), because the variable A differs from the variable X. But we
can fix this by adding an underscore to the front of A, since the pattern
matches that subterm by instantiating _A to X.
(simplify-defun f
:simplify-body (if (foo _a) @ z))
For that matter, we can even replace Z in the pattern by any variable
whose name starts with an underscore, for example as follows.
(simplify-defun f
:simplify-body (if (foo _a) @ _b))
Both of the simplify-defun calls just above give rise to the same
definition of F$1 as before (i.e., as displayed above.).
On the other hand, the following call fails because the variable _a
would need to be instantiated both to X and to Z.
(simplify-defun f
:simplify-body (if (foo _a) @ _a))
The _-var, _ — that is the variable in the "ACL2" package
whose symbol-name, "_", consists of just a single underscore
character — gets special treatment. It is allowed to match different
subterms, so this succeeds:
(simplify-defun f
:simplify-body (if (foo _) @ _))
See simplify-defun (specifically, the section on the
:simplify-body argument) for a precise explanation of the sense in which
the variable _ gets special treatment by allowing matches to more than
one subterm.
We have seen that the language of patterns allows variables @ and
@XX to represent simplification sites, as well as variables _ and
_XX that also match arbitrary subterms; here XX denotes an arbitrary
non-empty suffix, and the symbol's package is arbitrary. But an additional
construct can be used to represent simplification sites: (:@ u), where
u is a term and the keyword :@ is used as a unary function symbol.
When a pattern is matched against a term, (:@ u) indicates not only that
u is to be matched, but also that we have a simplification site. Indeed,
@ is an abbreviation for (:@ _) and @XX is an abbreviation for
(:@ _@XX). The simplify-defun call immediately above could thus be
written equivalently as follows.
(simplify-defun f
:simplify-body (if (foo _) (:@ _) _))
Let's look at another example of the use of :@, starting with the
following (contrived) definition.
(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 nth above. Here's
a nice way to accomplish that.
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 @1 bound to the subterm (* 3 (+ 1 (+ 1 x))) and
the @-var @2 bound to the subterm (+ 1 (+ 1 y)), so that those two
subterms are simplified.
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, @ —
or equivalently, (:@ _) — to produce the same result, as follows.
See simplify-defun (specifically, the section on the
:simplify-body argument) for a precise explanation of the sense in which
the variables _ and @ get special treatment by allowing matches to
more than one subterm.
(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 v.
Notice that the binding of u is dropped, since u is now unusued.
Also notice that only the binding of v is simplified; the body of the
let* is left alone.
(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
(car (cons v y)) by v in the body. However, the new body is
simply:
X
To see why, consider how simplify-defun performs the simplification.
It actually simplifies (car (cons v y)) with respect to the bindings
above it; with that in mind, the result is obviously X. Since the term
(car u) does not appear in the result, the binding of v is
discarded, as is the binding of u as before. We are left simply with
X.
Example Set 7: Specifying an equivalence relation
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 fix-true-listp, but the
resulting call of member-equal is only Boolean-equivalent to the original
call, not equal to it (see member-fix-true-listp above). Thus, if we try
evaluating (simplify-defun foo) here, it will fail because no
simplification takes place. Instead, we can specify that the :equiv is
iff.
ACL2 !>(simplify-defun foo :equiv iff)
(DEFUN FOO$1 (E X)
(DECLARE (XARGS :GUARD T
:VERIFY-GUARDS NIL))
(MEMBER-EQUAL E X))
ACL2 !>
Example Set 8: Mutual-recursion
If (simplify-defun FN ...) is called where FN is defined using
mutual-recursion, then every function defined with FN will be
processed. Consider the following example.
(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 with
simplified bodies, as follows.
(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
:non-executable, :print, :verify-guards, and :show-only,
which we ignore in this example). Normally keyword arguments will be applied
to every function that is defined by the mutual-recursion. For example,
the simplify-defun call above is equivalent to (simplify-defun
foo :simplify-body t), which directs simplification of the body not only for
foo but also for foo-lst — that is, for every member of the
clique of functions introduced by the mutual-recursion. A special
construct, :map, allows different values of a keyword argument for
different members of that clique. For the given mutual-recursion above,
suppose that instead of the simplify-defun call above, we invoke:
(simplify-defun foo :simplify-body (:map (foo t) (foo-lst nil)))
Then, as specified, only the definition of foo is simplified in the
result.
(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))))))
