		Search-engine friendly clone of the ACL2 documentation.

Std/alists

A library for reasoning about association list (alist) operations like alist-keys, alist-vals, hons-get, etc.

Introduction

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:

"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 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 like assoc.

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 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 (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   }
                                                } different!
(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 disable, etc.

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 schemes.)

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.

Subtopics

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.
Alist-map-keys: Keys 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 alist alist whose value is val, if one exists, or nil otherwise.
Std/alists/hons-assoc-equal: Lemmas about hons-assoc-equal available in the std/alists library.
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: (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 keys.
Std/alists/abstract: Abstract theories for alist predicates
Fal-extract-vals: (fal-extract keys al) extracts the values associated with the given keys in the alist al. For unbound keys, we arbitrarily assign the value nil.
Fal-all-boundp: (fal-all-boundp keys alist) determines if every key in keys is bound in the alist alist.
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 alist x into a single list.
Append-alist-keys: (append-alist-keys x) appends all of the values from the alist x into a single list.
Alist-equiv: (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.
Hons-remove-assoc: Remove a particular key from a "modern" alist.
Std/alists/pairlis$: Lemmas about pairlis$ available in the std/alists library.
Worth-hashing: Heuristic for deciding when to use fast-alists.
Alists-agree: (alists-agree keys al1 al2) determines if the alists al1 and al2 agree on the value of every key in keys.
Sub-alistp: (sub-alistp a b) determines whether every key bound in the alist a is also bound to the same value in the alist b.
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.