Details about equality-variants

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` 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

The actual definition of the macro

Consider the following definition from ACL2 source file

(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

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

Guard proof obligations generated by calls of

(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 `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 examplemember-equalor( member... :TEST 'equal) , in certain contexts:defmacro,defpkg,defconst, andvalue-tripleforms.

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, `mbe` call discussed above requires a
connection to be established between the

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

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.