## EQUALITY-VARIANTS

versions of a function using different equality tests
```Major Section:  PROGRAMMING
```

The ACL2 environment includes not only a logic but also a programming language, which is based on Common Lisp. Execution efficiency may be increased by using fast equality tests: `eq` for symbols and `eql` for numbers, symbols, and characters (see eqlablep). Several list-processing functions built into ACL2 thus have three variants, depending on whether the equality function used is `eq`, `eql`, or `equal`; a list is provided below. ACL2 has taken measures to ensure that one can reason about a single logical function even when one uses these different variants.

Consider for example the case of list membership. Common Lisp provides a utility for this purposes, `member`, which can take a `:TEST` keyword argument, default `eql`. So for example, one might write

```(member a x :TEST 'eq)
```
if either `a` is a symbol or `x` is a list of symbols, so that the fastest equality test (`eq`) may be used when comparing `a` to successive elements of the list, `x`. One might elsewhere write `(member b (foo y))`, which is equivalent to `(member b (foo y) :TEST 'eql)`, for example if `b` is a number. If one wants to reason about both `(member a x :TEST 'eq)` and `(member b y)`, it might be helpful for both calls of `member` to be the same logically, even though Common Lisp will execute them differently (using `eq` or `eql`, respectively). ACL2 arranges that in fact, both references to `member` generate calls of `member-equal` in the theorem prover.

In fact, since `member` can take the optional `:TEST` keyword argument, then in ACl2 it must be defined as a macro, not a function (see defun). ACL2 arranges that a call of `member` generates a corresponding call of the function `member-equal`, regardless of the value of `TEST`, in a manner that produces `member-equal` in prover output. More generally, you can expect ACL2 to treat your use of `member` as though you had written `member-equal`, for example in the way it stores `rewrite` rules and other kinds of rules as well (see rule-classes). We say little here about how this is all arranged by ACL2, other than to mention that `mbe` is utilized (so, you might see mention in proof logs) of the function `return-last` that implements `mbe`. Such details, which probably can be ignored by most users, may be found elsewhere; see equality-variants-details.

As a convenience to the user, the macro `member-eq` is provided that expands to a corresponding call of `member` with `:TEST 'eq`, as follows.

```ACL2 !>:trans1 (member-eq (foo x) (bar y))
(MEMBER (FOO X) (BAR Y) :TEST 'EQ)
ACL2 !>
```

For efficiency we recommend using the `-equal` equality variant, for example `member-equal` or `... :TEST 'equal`, in certain contexts: `defmacro`, `defpkg`, `defconst`, and `value-triple` forms. However, the implementation of equality variants has been designed so that when defining a function, one may choose freely in a definition an equality variant of primitive `F`, to get efficient execution but where subsequent reasoning is about `F-equal`. For details about the above recommendation and for a discussion of the implementation, see equality-variants-details.

The following alphabetical list includes all primitives that have equality variants. Each macro `F` listed below takes an optional `:TEST` keyword argument of `'eq`, `'eql`, or `'equal`, where `'eql` is the default. For each such `F`, a function `F-equal` is defined such that for logical purposes (in particular theorem proving), each call of `F` expands to a corresponding call of `F-equal`. For convenience, a macro `F-eq` is also defined, so that a call of `F-eq` expands to a corresponding call of `F` with `:TEST 'eq`.

````add-to-set`
`assoc`
`delete-assoc`
`intersection\$` ; (see Note below)
`intersectp`
`member`
`no-duplicatesp`
`position-ac`
`position`
`put-assoc`
`rassoc`
`remove-duplicates`
`remove1`
`remove`
`set-difference\$` ; (see Note below)
`subsetp`
`union\$` ; (see Note below)
```

Note: Three of the macros above have names ending with the character, ``\$`': `intersection\$`, `set-difference\$`, and `union\$`. In each case there is a corresponding Common Lisp primitive without the trailing ``\$`': `intersection`, `set-difference`, and `union`. However, Common Lisp does not specify the order of elements in the list returned by those primitives, so ACL2 has its own. Nevertheless, the only use of the trailing ``\$`' is to distinguish the primitives; associated functions and macros, for example `union-eq` and `intersection-equal`, do not include the ``\$`' character in their names.