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-setassocdelete-associntersection$; (see Note below)intersectpmemberno-duplicatespposition-acpositionput-assocrassocremove-duplicatesremove1removeset-difference$; (see Note below)subsetpunion$; (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.
