A library for reasoning about association list (alist) operations
like alist-keys, alist-vals, hons-get, etc.
An association list is a fundamental data structure that
associates ("binds") some keys to values. In other programming
languages, alists may go by names like dictionaries, maps,
hashes, associative arrays, and the like.
The std/alists library provides functions and lemmas about:
In the "traditional" view, an alist is something recognized by alistp—a true-listp of conses. This alistp recognizer
serves as a guard for functions like assoc, rassoc, strip-cars, and so forth.
In contrast, in the "modern" view, the final-cdr of an alist is not
expected to be nil; instead it may be any atom. (This can be used, e.g.,
to name fast-alists and to govern the sizes of their initial hash
tables; see hons-acons for details.) Any traditional alistp is
still perfectly valid under this modern view, but these new kinds of alists,
with their weird final cdrs, are incompatible with traditional alist functions
The Non-Alist Convention
Going further, in the modern view, we do not even expect that the elements
of an alist must necessarily be conses. Instead, a modern alist function
simply skips past any atoms in its input. We call this the non-alist
Following the non-alist convention means that functions like alist-keys and hons-assoc-equal avoid needing any guard, which is
occasionally convenient. More importantly, it means that when reasoning about
modern alist functions, we typically do not need any alistp style
hypotheses. For instance, here is a typical, beautiful, hypothesis-free
theorem about hons-assoc-equal:
(equal (hons-assoc-equal key (append x y))
(or (hons-assoc-equal key x)
(hons-assoc-equal key y)))
By comparison, the analogous theorem for the traditional assoc
function requires a hypothesis like (alistp a) or (not (equal key
nil)). Without such a hypothesis, we run into "degenerate" cases due to
taking the cars of arbitrary atoms. For instance,
let key = nil
let x = (nil 1 2)
let y = (a b c)
then (assoc key x) --> nil
(assoc key y) --> a
(assoc nil (append x y)) --> nil }
(or (assoc key x) --> (or nil a) --> a }
(assoc key y))
This weird behavior for (assoc nil x) leads to complications for many
theorems about traditional alist operations. Following the non-alist
convention allows modern alist operations to avoid this problem.
Loading the Library
The recommended way to load the library, especially for beginning to
intermediate ACL2 users, is to simply include the top book, e.g.,
(include-book "std/alists/top" :dir :system)
This book loads quickly (typically in under a second), gives you everything
we have to offer, and sets up a "recommended" theory.
Note: Loading the std/alists/top book will also result in loading
the std/lists library. See the documentation for std/lists for
important notes about its equivalence relations, the functions it will
Things to Note
When you include the top book, several basic, built-in ACL2 alist
functions like alistp, strip-cars, assoc, and so forth
will be disabled. As a result, ACL2 will sometimes not automatically
try to induct as it did before. You may find that you need to give explicit
:induct hints, or explicitly re-enable these basic functions
during certain theorems. (On the flip side, you may also find that you are
spending less time trying to prove theorems using incorrect induction
A very useful equivalence relation when working with association
lists is alist-equiv, which says whether alists agree on the
value of every key. Many alist operations respect this equivalence relation.
It is generally a good idea to define appropriate alist-equiv congruence rules for new alist-processing functions.
- (alist-keys x) collects all keys bound in an alist.
- Remove all pairs with given keys from an alist.
- (alist-vals x) collects all values bound in an alist.
- Values of the map represented by an alist.
- Keys of the map represented by an alist.
- Lemmas about strip-cdrs available in the std/alists
- (hons-rassoc-equal val alist) returns the first pair found in the alist
alist whose value is val, if one exists, or nil otherwise.
- Lemmas about hons-assoc-equal available in the std/alists library.
- Lemmas about strip-cars available in the std/alists
- Find the first of many keys bound in a fast alist.
- (fal-extract keys al) extracts a "subset" of the alist al by
binding every key in keys to its value in al, skipping any unbound
- Abstract theories for alist predicates
- (fal-extract keys al) extracts the values associated with the given
keys in the alist al. For unbound keys, we arbitrarily assign the
- (fal-all-boundp keys alist) determines if every key in keys is bound
in the alist alist.
- Lemmas about alistp available in the std/alists
- (append-alist-vals x) appends all of the values from the alist
x into a single list.
- (append-alist-keys x) appends all of the values from the alist
x into a single list.
- (alist-equiv a b) determines whether the alists a and b
are equivalent up to hons-assoc-equal, i.e., whether they bind the same
value to every key.
- Remove a particular key from a "modern" alist.
- Lemmas about pairlis$ available in the std/alists
- Heuristic for deciding when to use fast-alists.
- (alists-agree keys al1 al2) determines if the alists al1 and al2
agree on the value of every key in keys.
- (sub-alistp a b) determines whether every key bound in the
alist a is also bound to the same value in the alist b.
- Basic fixing function for "modern" alists that respects the
behavior of hons-assoc-equal.
- Theorems about remove-assoc-equal
in the std/alists library.
- Theorems about assoc-equal
in the std/alists library.