		Search-engine friendly clone of the ACL2 documentation.

Equality-variants

Equality-variants-details

Here we present details about equality variants, none of which is likely to be important to the majority of ACL2 users. Please see equality-variants for relevant background.

We begin by presenting events that implement the equality variants for member, as these illustrate the events introduced for all macros having equality variants. The definition of member, just below, calls the macro let-mbe, which in turn is just an abbreviation for a combination of let and mbe. Here is a simplified version of the definition of this macro. For relevant background, see mbe.

(defmacro let-mbe (bindings &key logic exec)
  `(let ,bindings
     (mbe :logic ,logic
          :exec ,exec)))

This use of let arranges that each argument of a call of member is evaluated only once.

The actual definition of the macro let-mbe is a bit more complex, in order to guarantee that guards are appropriately checked. For purposes of this discussion we ignore this simplification. (You can find the definition of let-mbe in ACL2 source file axioms.lisp.)

Consider the following definition from ACL2 source file axioms.lisp. Notice that it invokes the macro let-mbe, discussed above.

(defmacro member (x l &key (test ''eql))
  (declare (xargs :guard (or (equal test ''eq)
                             (equal test ''eql)
                             (equal test ''equal))))
  (cond
   ((equal test ''eq)
    `(let-mbe ((x ,x) (l ,l))
              :logic (member-equal x l)
              :exec  (member-eq-exec x l)))
   ((equal test ''eql)
    `(let-mbe ((x ,x) (l ,l))
              :logic (member-equal x l)
              :exec  (member-eql-exec x l)))
   (t ; (equal test 'equal)
    `(member-equal ,x ,l))))

Inspection of the definition above shows that every call of member expands to one that is logically equivalent to the corresponding call of member-equal, which is defined as follows.

(defun member-equal (x lst)
  (declare (xargs :guard (true-listp lst)))
  (cond ((endp lst) nil)
        ((equal x (car lst)) lst)
        (t (member-equal x (cdr lst)))))

The following two definitions model equality variants of member for tests eq and eql, respectively.

(defun member-eq-exec (x lst)
  (declare (xargs :guard (if (symbolp x)
                             (true-listp lst)
                           (symbol-listp lst))))
  (cond ((endp lst) nil)
        ((eq x (car lst)) lst)
        (t (member-eq-exec x (cdr lst)))))

(defun member-eql-exec (x lst)
  (declare (xargs :guard (if (eqlablep x)
                             (true-listp lst)
                           (eqlable-listp lst))))
  (cond ((endp lst) nil)
        ((eql x (car lst)) lst)
        (t (member-eql-exec x (cdr lst)))))

At this point the user can write (member x y) or (member-equal x y) to call equality variants of member with test eql or equal, respectively. We thus provide the following macro for the eq variant.

(defmacro member-eq (x lst)
  `(member ,x ,lst :test 'eq))

Guard proof obligations generated by calls of member will include those based on its use of mbe, and are supported by the following two lemmas.

(defthm member-eq-exec-is-member-equal
  (equal (member-eq-exec x l)
         (member-equal x l)))

(defthm member-eql-exec-is-member-equal
  (equal (member-eql-exec x l)
         (member-equal x l)))

Finally, the following two events arrange that in certain contexts such as theories (including the use of in-theory in events and hints), member-eq and member are treated as references to member-equal.

(add-macro-alias member-eq member-equal)
(add-macro-alias member member-equal)

Note however that these events do not affect printing of calls during proofs: calls of member and member-eq will be macroexpanded away, leaving you with calls of member-equal that are displayed in proof output. For a way to change this behavior, see add-macro-fn.

We conclude this topic by exploring the following recommendation made in the documentation for equality-variants.

For efficiency we recommend using the -equal equality variant, for example member-equal or (member ... :TEST 'equal), in certain contexts: defmacro, defpkg, defconst, and value-triple forms.

ACL2 relies on the underlying Common Lisp for evaluation. It also processes events in the ACL2 logic. In order to guarantee consistency of its logical and Common Lisp evaluations, ACL2 uses a ``safe mode'' to avoid ill-guarded calls. In particular, consider the use of mbe in execution of a call of an equality variant of a primitive, F, other than its F-equal variant. The mbe call discussed above requires a connection to be established between the :logic and :exec forms. For example, if F is called with :TEST 'eql (either explicitly or as the default), then ACL2 will call both F-eql-exec and F-equal, and check that the two results are equal.

The following partial log illustrates the point above. We define a macro that calls member, and when a call of this macro is expanded during processing of a subsequent definition, we see that two membership functions are called on the same arguments.

ACL2 !>(defmacro mac (lst)
         (list 'quote (and (true-listp lst)
                           (member 'c lst :test 'eq))))

Summary
Form:  ( DEFMACRO MAC ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 MAC
ACL2 !>(trace$ member-equal member-eq-exec)
 ((MEMBER-EQUAL) (MEMBER-EQ-EXEC))
ACL2 !>(defun f () (mac (a b c d)))
1> (ACL2_*1*_ACL2::MEMBER-EQ-EXEC C (A B C D))
  2> (MEMBER-EQ-EXEC C (A B C D))
  <2 (MEMBER-EQ-EXEC (C D))
<1 (ACL2_*1*_ACL2::MEMBER-EQ-EXEC (C D))
1> (ACL2_*1*_ACL2::MEMBER-EQUAL C (A B C D))
  2> (MEMBER-EQUAL C (A B C D))
  <2 (MEMBER-EQUAL (C D))
<1 (ACL2_*1*_ACL2::MEMBER-EQUAL (C D))

Since F is non-recursive, its admission is trivial.

If performance is an issue then we can avoid such a problem, for example as follows. In a fresh session, let us define a suitable wrapper for calling member with :TEST 'eq. This time, the trace in our partial log shows that we have avoided calling two membership functions.

ACL2 !>(defun mem-eq (x lst)
         (declare (xargs :guard (if (symbolp x)
                                    (true-listp lst)
                                  (symbol-listp lst))))
         (member x lst :test 'eq))
[[ ... output omitted here ... ]]
 MEM-EQ
ACL2 !>(defmacro mac (lst)
         (list 'quote (and (true-listp lst)
                           (mem-eq 'c lst))))

Summary
Form:  ( DEFMACRO MAC ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 MAC
ACL2 !>(trace$ member-equal member-eq-exec mem-eq)
 ((MEMBER-EQUAL)
  (MEMBER-EQ-EXEC)
  (MEM-EQ))
ACL2 !>(defun f () (mac (a b c d)))
1> (ACL2_*1*_ACL2::MEM-EQ C (A B C D))
  2> (MEM-EQ C (A B C D))
  <2 (MEM-EQ (C D))
<1 (ACL2_*1*_ACL2::MEM-EQ (C D))

Since F is non-recursive, its admission is trivial.