		Search-engine friendly clone of the ACL2 documentation.

Simplify-defun-sk

Simplify-defun-sk-examples

Examples illustrating simplify-defun-sk.

The examples below are deliberately quite trivial, in order to make clear how simplify-defun-sk behaves with various keyword arguments. For all those examples, we assume that the following event has already been evaluated.

(defthm member-equal-fix-true-list
  (iff (member-equal a (fix-true-list lst))
       (member-equal a lst)))

Example Set 1: Basics

We start with the following basic example. The keywords can all be omitted with minimal change to the outcome, but we include them as a way to introduce some of the simplest keywords.

(defun-sk foo (lst)
  (exists x (member-equal x (fix-true-list lst))))
; redundant (see above)
(defthm member-equal-fix-true-list
  (iff (member-equal a (fix-true-list lst))
       (member-equal a lst)))
(simplify-defun-sk foo
                   :new-name foo-simp
                   :thm-name foo-simplified
                   :function-disabled nil
                   :thm-enable t
                   :skolem-name foo-simp-sk)

ACL2 responds to the call above of simplify-defun-sk by creating the following DEFUN-SK form among others, silently submitting the created forms, and then returning the new DEFUN-SK form (as the value component of an ACL2::error-triple). The new function is named foo-simp because that is what we specified with the :new-name argument above. Similarly, the :skolem-name below comes directly from the keyword above and otherwise would be omitted below. Notice that the rewrite rule member-fix-true-listp, displayed above, was applied to create the new definition.

(DEFUN-SK FOO-SIMP (LST)
          (EXISTS (X) (MEMBER-EQUAL X LST))
          :QUANT-OK T
          :SKOLEM-NAME FOO-SIMP-SK)

You can add :verbose t, to get output from the prover when evaluating the ACL2::events generated by the simplify-defun-sk call.

To see the full expansion produced by the call of simplify-defun-sk above, we can use show-simplify-defun-sk instead of simplify-defun-sk, on the same arguments (or, simply add keyword argument :show-only t to your simplify-defun-sk call). The result is as follows (elided somewhat).

(ENCAPSULATE
     NIL
     ... ; helpful stuff local to the encapsulate
     (DEFUN-SK FOO-SIMP ...)  ; as shown above
     ... ; local helper events, not shown here
     (DEFTHM FOO-SIMPLIFIED ; the value of keyword argument :thm-name
             (IFF (FOO LST) (FOO-SIMP LST))
             :HINTS ...)
     (IN-THEORY (DISABLE FOO-SIMP)))

Notice that new function symbol FOO-SIMP and new theorem FOO-SIMPLIFIED are disabled and enabled, respectively, because of keyword arguments supplied :function-disabled t and :thm-enable t, respectively.

On the other hand, if you want less output, not more, use simplify-defun-sk with :print nil. For example:

ACL2 !>(simplify-defun-sk foo
                          :new-name foo-simp
                          :thm-name foo-simplified
                          :function-disabled t
                          :thm-enable t
                          :skolem-name foo-simp-sk
                          :print nil)
 T
ACL2 !>:pe foo-simp
   d       4:x(SIMPLIFY-DEFUN-SK FOO
                                 :NEW-NAME ...)
              
>L d           (DEFUN FOO-SIMP (LST)
                      (DECLARE (XARGS :NON-EXECUTABLE T :MODE :LOGIC))
                      (PROG2$ (THROW-NONEXEC-ERROR 'FOO-SIMP
                                                   (LIST LST))
                              (LET ((X (FOO-SIMP-SK LST)))
                                   (MEMBER-EQUAL X LST))))
ACL2 !>

Example Set 2: Assumptions

The following trivial example illustrates the use of assumptions.

(defthm fix-true-list-is-identity
  (implies (true-listp x)
           (equal (fix-true-list x)
                  x)))
(defun-sk foo (lst1 lst2)
  (forall x (equal (member-equal x (fix-true-list lst1))
                   (member-equal x (fix-true-list lst2)))))
(simplify-defun-sk foo :assumptions ((and (true-listp lst1)
                                          (true-listp lst2))))

Here is the result. 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-SK FOO$1 (LST1 LST2)
          (FORALL (X)
                  (EQUAL (MEMBER-EQUAL X LST1)
                         (MEMBER-EQUAL X LST2)))
          :QUANT-OK T)

Notice that the body was simplified under the given assumption that lst1 and lst2 satisfy true-listp; without any such assumption, no simplification would have taken place.

The following example has a non-trivial guard, and illustrates that the value of keyword :assumptions can be :guard, which means that the :assumptions value is taken to be the given function's guard.

(defun-sk foo (lst1 lst2)
 (declare (xargs :guard (and (true-listp lst1)
                             (true-listp lst2))
                 :verify-guards nil))
  (forall x (equal (member-equal x (fix-true-list lst1))
                   (member-equal x (fix-true-list lst2)))))
(simplify-defun-sk foo :assumptions :guard)

Here is the result. Notice that the simplified body is the same as before.

(DEFUN-SK FOO$1 (LST1 LST2)
          (DECLARE (XARGS :NON-EXECUTABLE NIL))
                         (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LST1)
                                                     (TRUE-LISTP LST2))
                                         :VERIFY-GUARDS NIL))
          (FORALL (X)
                  (EQUAL (MEMBER-EQUAL X LST1)
                         (MEMBER-EQUAL X LST2)))
          :QUANT-OK T)

Unlike simplify-defun, simplify-defun-sk does not support keywords :assumption-disable, :assumption-enable, and :assumption-theory, and :hyp-fn, since there is no need, as defun-sk does not support recursion.

Example Set 3: Guard Verification

Consider the preceding example, but where we verify guards before attempting simplification, as follows.

(verify-guards foo)
(simplify-defun-sk foo :assumptions :guard)

The new defun-sk form is the same as before. However, this time the new function symbol is guard-verified. If we use show-simplify-defun-sk in place of simplify-defun-sk just above, we can see that the following verify-guards event is generated for the new function symbol.

(VERIFY-GUARDS FOO$1
               :HINTS (("Goal" :USE (:GUARD-THEOREM FOO))))

This illustrates that by default, guard verification will be attempted for the new function symbol exactly when the original function symbol is guard-verified. However, that default behavior can be overridden by using the :verify-guards keyword. For example, suppose that the preceding call of simplify-defun-sk displayed above is replaced by the following.

(simplify-defun-sk foo
                   :assumptions :guard
                   :verify-guards nil)

In this case, guard verification will not be attempted for the new function symbol.

Simplify-defun-sk provides the keyword :guard-hints for the simplified function's guard verification proofs. For example, suppose that instead of the simplify-defun-sk forms above we evaluate this (rather silly) form.

(simplify-defun-sk foo
                   :assumptions :guard
                   :guard-hints (("Goal" :in-theory (enable append))))

Then in place of the default :hints supplied to the call of verify-guards, as displayed above, the guard hints supplied in our simplify-defun-sk are used.

(VERIFY-GUARDS FOO$1
               :HINTS (("Goal" :IN-THEORY (ENABLE APPEND))))

Example Set 4: Defun-sk specific: defun-sk2 and :rewrite

Next, we discuss two features of simplify-defun-sk that do not correspond to features of simplify-defun.

The macro defun-sk2 is part of the SOFT tool suite (see soft::soft). It is a wrapper for defun-sk. When simplify-defun-sk is called on a function that was introduced with defun-sk2, the new function is also introduced with defun-sk2. Here is an example.

(include-book "simplify-defun-sk")
(include-book "kestrel/soft/top" :dir :system)
(defunvar ?foo (*) => *)
(defun-sk2 spec[?foo] (?foo) ()
  (forall (x) (equal (?foo x) (* x 2))))
(simplify-defun-sk spec[?foo])

The resulting definition benefits from simplification of (* x 2) to (* 2 x). More interesting: it too is a call of defun-sk2.

(DEFUN-SK2 SPEC[?FOO]$1 (?FOO)
           NIL
           (FORALL (X) (EQUAL (?FOO X) (* 2 X)))
           :QUANT-OK T)

A second capability offered by simplify-defun-sk is the :rewrite keyword. By default, the :rewrite field of the generated defun-sk form (or defun-sk2 form) corresponds to that of the corresponding form for the input function symbol. (Exception: currently, custom :rewrite fields are dropped. A comment about a proposed simplify-defthm in source file simplify-defun-sk.lisp discusses this issue.) Here is an example showing a new :rewrite field, based closedly on the first example in this topic.

; Start a fresh ACL2 session.
(include-book "simplify-defun-sk")
(defthm member-equal-fix-true-list
  (iff (member-equal a (fix-true-list lst))
       (member-equal a lst)))
(defun-sk foo (lst)
  (forall x (not (member-equal x (fix-true-list lst)))))
(simplify-defun-sk foo :rewrite :direct)

As a result of the :rewrite argument above, the resulting defun-sk form includes :rewrite :direct.

(DEFUN-SK FOO$1 (LST)
          (FORALL (X) (NOT (MEMBER-EQUAL X LST)))
          :QUANT-OK T
          :REWRITE :DIRECT)

As for defun-sk, the value of the :rewrite option of simplify-defun-sk can ony be :direct if the quantifier is forall.

Example Set 5: Controlling the Theory for Simplification

By default, simplification done on behalf of simplify-defun-sk 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. Let us return to our original example, without extra keywords this time; but this time, let's introduce the key lemma with defthmd (not because it helps our proofs to disable it, but because that will help us to illustrate the :theory keyword).

; Start a fresh ACL2 session.
(include-book "simplify-defun-sk")
(defthmd member-equal-fix-true-list
  (iff (member-equal a (fix-true-list lst))
       (member-equal a lst)))
(defun-sk foo (lst)
  (exists x (member-equal x (fix-true-list lst))))
(simplify-defun-sk foo :theory (enable member-equal-fix-true-list))

If we omit the :theory value above, the call of simplify-defun-sk fails because member-equal-fix-true-list is disabled. The :theory keyword value causes simplification (and some subsequent reasoning) to be done in the indicated theory.

For convenience, :enable and/or :disable keywords are available, provided that they are not used when :theory is used. For example, the following form is treated equivaletly to the simplify-defun-sk call displayed just above.

(simplify-defun-sk foo :enable (member-equal-fix-true-list))

Example Set 6: Simplifying Subterms

Like simplify-defun, value of the :simplify-body keyword of simplify-defun-sk can be t, nil, or a pattern. It may be surprising that nil is allowed, since (unlike simplify-defun) the body is the only piece of the definition that is simplified (not the guard or measure). However, it is anticipated that sometimes simplify-defun-sk may be called without knowing if simplification will succeed, but nevertheless wanting a new function symbol to be defined. (If that same functionality is desired for simplify-defun then it could be changed as well.)

The handling of patterns is the same as for simplify-defun; see simplify-defun for further discussion of ``Simplifying a Subterm''. Here we present a simple example with a single subterm simplified, but as with simplify-defun, it is legal to specify more than one such subterm.

; Start a fresh ACL2 session.
(include-book "simplify-defun-sk")
; Books included above define set-equiv as an equivalence relation,
; and provide some nice congruence rules.
(defthm set-equiv-fix-true-list
  (set-equiv (fix-true-list lst)
             lst))
(defun-sk foo (lst1 lst2)
  (exists x (iff (and (member-equal x (fix-true-list lst1))
                      (member-equal x (fix-true-list lst2)))
                 t)))
(simplify-defun-sk foo
                   :simplify-body
                   (and (member-equal x @)
                        (member-equal x (fix-true-list lst2))))

The result is below. Notice that simplification has taken place at the subterm labeled with @, and nowhere else.

(DEFUN-SK FOO$1 (LST1 LST2)
          (EXISTS (X)
                  (IFF (AND (MEMBER-EQUAL X LST1)
                            (MEMBER-EQUAL X (FIX-TRUE-LIST LST2)))
                       T))
          :QUANT-OK T)

It is interesting to note that our original lemma, member-equal-fix-true-list, is not sufficient for the simplification. That is because it is a rule to rewrite calls of member-equal, but the subterm in question has no such calls.

; Start a fresh ACL2 session.
(include-book "simplify-defun-sk")
(defthm member-equal-fix-true-list
  (iff (member-equal a (fix-true-list lst))
       (member-equal a lst)))
(defun-sk foo (lst1 lst2)
  (exists x (and (member-equal x (fix-true-list lst1))
                 (member-equal x (fix-true-list lst2)))))
(simplify-defun-sk foo
                   :simplify-body
                   (and (member-equal x @)
                        (member-equal x (fix-true-list lst2))))