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 *dictionaries*, *maps*,
*hashes*, *associative arrays*, and the like.

The

**"traditional" alist operations**like alistp, assoc, and strip-cars, which have long been built into ACL2.**"modern" alist operations**like hons-assoc-equal, alist-keys, make-fal, etc., which have better compatibility with fast-alists.

In the "traditional" view, an alist is something recognized by alistp—a true-listp of conses. This

In contrast, in the "modern" view, the final-cdr of an alist is not
expected to be

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
convention**.

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

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 } } different! (or (assoc key x) --> (or nil a) --> a } (assoc key y))

This weird behavior for

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

When you include the

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-keys
`(alist-keys x)`collects all keys bound in an alist.- Remove-assocs
- Remove all pairs with given keys from an alist.
- Alist-vals
`(alist-vals x)`collects all values bound in an alist.- Alist-map-vals
- Values of the map represented by an alist.
- Std/alists/strip-cdrs
- Lemmas about strip-cdrs available in the std/alists library.
- Hons-rassoc-equal
`(hons-rassoc-equal val alist)`returns the first pair found in the alistalist whose value isval , if one exists, ornil otherwise.- Alist-map-keys
- Keys of the map represented by an alist.
- Std/alists/hons-assoc-equal
- Lemmas about hons-assoc-equal available in the std/alists library.
- Fal-extract
`(fal-extract keys al)`extracts a "subset" of the alistal by binding every key inkeys to its value inal , skipping any unbound keys.- Std/alists/strip-cars
- Lemmas about strip-cars available in the std/alists library.
- Fal-find-any
- Find the first of many keys bound in a fast alist.
- Fal-extract-vals
`(fal-extract keys al)`extracts the values associated with the givenkeys in the alistal . For unbound keys, we arbitrarily assign the valuenil .- Std/alists/abstract
- Abstract theories for alist predicates
- Fal-all-boundp
`(fal-all-boundp keys alist)`determines if every key inkeys is bound in the alistalist .- Std/alists/alistp
- Lemmas about alistp available in the std/alists library.
- Append-alist-vals
`(append-alist-vals x)`appends all of the values from the alistx into a single list.- Append-alist-keys
`(append-alist-keys x)`appends all of the values from the alistx into a single list.- Alist-equiv
`(alist-equiv a b)`determines whether the alistsa andb are equivalent up to hons-assoc-equal, i.e., whether they bind the same value to every key.- Hons-remove-assoc
- Remove a particular key from a "modern" alist.
- Std/alists/pairlis$
- Lemmas about pairlis$ available in the std/alists library.
- Alists-agree
`(alists-agree keys al1 al2)`determines if the alistsal1 andal2 agree on the value of every key inkeys .- Worth-hashing
- Heuristic for deciding when to use fast-alists.
- Sub-alistp
`(sub-alistp a b)`determines whether everykey bound in the alista is also bound to the same value in the alistb .- Alist-fix
- Basic fixing function for "modern" alists that respects the behavior of hons-assoc-equal.
- Std/alists/remove-assoc-equal
- Theorems about
`remove-assoc-equal`in the std/alists library. - Std/alists/assoc-equal
- Theorems about
`assoc-equal`in the std/alists library.