Std/lists
A library for reasoning about basic list operations like append, len, member, take, etc.
Introduction
The std/lists library provides lemmas that are useful when reasoning
about the basic list functions that are built into ACL2, and also defines some
additional functions like list-fix, rev, set-equiv, and so
on.
The std/lists library is based largely on books that were previously
part of the unicode library, but also incorporates ideas from earlier
books such as data-structures/list-defthms and
data-structures/number-list-defthms and also from coi/lists.
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/lists/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. See below for some
general comments about this theory.
For advanced users, we recommend using the top book if possible.
However, in case you find this book to be too heavy or too incompatible with
your existing developments, the library is mostly arranged in a "buffet"
style that is meant to allow you to load as little or as much as you like. A
particularly useful book is
(include-book "std/lists/list-defuns" :dir :system)
which adds the new std/lists functions like list-fix, but
has (almost) no theorems. Typically, you would then want to (perhaps locally)
include individual books for the particular list functions you are dealing
with. The books have sensible names, e.g., you might write:
(include-book "std/lists/list-defuns" :dir :system)
(local (include-book "std/lists/append" :dir :system))
(local (include-book "std/lists/rev" :dir :system))
(local (include-book "std/lists/repeat" :dir :system))
The best way to see what books are available is to just run ls in the
std/lists directory. Unlike the top book, most individual books are meant
to be reasonably unobtrusive, e.g., loading the append book will not
disable append.
Things to Note
When you include the top book, note that many basic, built-in ACL2 list
functions like append and len 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.)
The library introduces a couple of useful equivalence relations,
namely:
- list-equiv
- Equivalences of lists based on list-fix.
- Respected in some way by most list-processing functions.
- set-equiv
- Equivalence of lists up to membership, but ignoring order and duplicity.
- list-equiv is a refinement of set-equiv.
- Respected in a strong way by most "lists as sets" functions, e.g., subsetp, union$, etc.
- Preserved by many other ordinary list functions like append, rev, etc.
These rules allow for some very powerful equivalence-based reasoning. When
introducing new list-processing functions, it is generally a good idea to
define the appropriate congruence rules for these relations.
Subtopics
- Std/lists/abstract
- Abstract theories for listp, projection, and mapappend functions
- Rev
- Logically simple alternative to reverse for lists.
- Defsort
- Define a sorting function for a given comparator.
- List-fix
- (list-fix x) converts x into a true-listp by, if
necessary, changing its final-cdr to nil.
- Std/lists/nth
- Lemmas about nth available in the std/lists library.
- Hons-remove-duplicates
- (hons-remove-duplicates l) removes duplicate elements from a
list, and is implemented using fast-alists.
- Std/lists/update-nth
- Lemmas about update-nth available in the std/lists
library.
- Set-equiv
- (set-equiv x y) is an equivalence relation that determines
whether x and y have the same members, in the sense of member.
- Duplicity
- (duplicity a x) counts how many times the element a occurs
within the list x.
- Prefixp
- (prefixp x y) determines if the list x occurs at the front of
the list y.
- Std/lists/take
- Lemmas about take available in the std/lists library.
- Std/lists/intersection$
- Lemmas about intersection$ available in the std/lists
library.
- Nats-equiv
- Recognizer for lists that are the same length and that are pairwise
equivalent up to nfix.
- Repeat
- (repeat n x) creates a list of xes with length n; it
is a simpler alternative to make-list.
- Index-of
- (index-of k x) returns the index of the first occurrence of element
k in list x if it exists, NIL otherwise.
- All-equalp
- (all-equalp a x) determines if every member of x is equal to
a.
- Sublistp
- (sublistp x y) checks whether the list x ever occurs within
the list y.
- Std/lists/nthcdr
- Lemmas about nthcdr available in the std/lists
library.
- Std/lists/append
- Lemmas about append available in the std/lists
library.
- Listpos
- (listpos x y) returns the starting position of the first occurrence
of the sublist x within the list y, or NIL if there is no such
occurrence.
- List-equiv
- (list-equiv x y) is an equivalence relation that determines
whether x and y are identical except perhaps in their final-cdrs.
- Final-cdr
- (final-cdr x) returns the atom in the "cdr-most branch" of
x.
- Std/lists/remove
- Lemmas about remove available in the std/lists
library.
- Subseq-list
- Lemmas about subseq-list available in the std/lists
library.
- Rcons
- Cons onto the back of a list.
- Std/lists/revappend
- Lemmas about revappend available in the std/lists
library.
- Std/lists/remove-duplicates-equal
- Lemmas about remove-duplicates-equal available in the std/lists library.
- Std/lists/last
- Lemmas about last available in the std/lists library.
- Std/lists/reverse
- Lemmas about reverse available in the std/lists
library.
- Std/lists/resize-list
- Lemmas about resize-list available in the std/lists
library.
- Flatten
- (flatten x) appends together the elements of x.
- Suffixp
- (suffixp x y) determines if the list x occurs at the end of
the list y.
- Std/lists/set-difference
- Lemmas about set-difference$ available in the std/lists
library.
- Std/lists/butlast
- Lemmas about butlast available in the std/lists
library.
- Std/lists/len
- Lemmas about len available in the std/lists library.
- Std/lists/intersectp
- Lemmas about intersectp available in the std/lists
library.
- Std/lists/true-listp
- Lemmas about true-listp available in the std/lists
library.
- Intersectp-witness
- (intersectp-witness x y) finds a some element that is a member
of both x and y, if one exists.
- Subsetp-witness
- (subsetp-witness x y) finds an element of x that is not a
member of y, if one exists.
- Std/lists/remove1-equal
- Lemmas about remove1 available in the std/lists
library.
- Rest-n
- rest-n is identical to nthcdr, but its guard does not
require (true-listp x).
- First-n
- (first-n n x) is logically identical to (take n x), but its
guard does not require (true-listp x).
- Std/lists/union
- Theorems about union$ in the std/lists library.
- Append-without-guard
- Version of append that has a guard of t
- Std/lists/subsetp
- Lemmas about subsetp available in the std/lists
library.
- Std/lists/member
- Lemmas about member available in the std/lists
library.
