Equality-variants
Versions of a function using different equality tests
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 involve a notion of ``macro alias'' and 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 (member ... :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
intersection$ ; (see Note below)
intersectp
member
no-duplicatesp
position-ac
position
put-assoc
rassoc
remove
remove-assoc
remove-duplicates
remove1
remove1-assoc
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.
We conclude with a brief discussion of guards. The expansion of any
of the above macros depends on the keyword argument, which generates a
function call with a guard suitable for the equality test being used.
Consider for example the call (member x lst :test 'eq), or equivalently,
(member-eq x lst). Expanding these macros leads to a call of mbe; you can see how that goes by using :trans1. Ultimately,
the guard being checked is that of the function member-eq-exec, which is
as follows.
(if (symbolp x)
(true-listp lst)
(symbol-listp lst))
Care has been taken to ensure that this guard is checked during evaluation
and also that it generates suitable proof obligations for guard verification
(see verify-guards). A guard violation might look something like
this:
ACL2 !>(member-eq 3 '(4 5))
ACL2 Error in TOP-LEVEL: The guard for the function call
(MEMBER-EQ-EXEC$GUARD-CHECK X LST), which is
(IF (SYMBOLP X) (TRUE-LISTP LST) (SYMBOL-LISTP LST)), is violated by
the arguments in the call (MEMBER-EQ-EXEC$GUARD-CHECK 3 '(4 5)).
See :DOC set-guard-checking for information about suppressing this
check with (set-guard-checking :none), as recommended for new users.
To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.
ACL2 !>
Above, member-eq-exec$guard-check is a function generated as part of
ACL2's expansion of member with :test 'eq, and this function symbol
can be quite reasonably ignored. The important thing is that it refers to the
guard for member-eq-exec, which as the name may suggest is intended to
guard the execution of a call of member-eq, or a call of member with :test 'eq. The important part of the message above is the
guard actually being violated: (IF (SYMBOLP X) (TRUE-LISTP
LST) (SYMBOL-LISTP LST)).
Subtopics
- Eql
- Test equality (of two numbers, symbols, or characters)
- Equality-variants-details
- Details about equality-variants
- Eq
- Equality of symbols
- =
- Test equality of two numbers
