A library for reasoning about basic list operations like append, len, member, take, etc.

The

The

The recommended way to load the library, especially for beginning to
intermediate ACL2 users, is to simply include the

(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

(include-book "std/lists/list-defuns" :dir :system)

which adds the new

(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

When you include the

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 ofset-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.

- Std/lists/abstract
- Abstract theories for listp, projection, and mapappend functions
- Defsort
- Define a sorting function for a given comparator.
- Rev
- Logically simple alternative to reverse for lists.
- List-fix
`(list-fix x)`convertsx into a true-listp by, if necessary, changing its final-cdr tonil .- 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 whetherx andy have the same members, in the sense of member.- Duplicity
`(duplicity a x)`counts how many times the elementa occurs within the listx .- Prefixp
`(prefixp x y)`determines if the listx occurs at the front of the listy .- 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 ofx es with lengthn ; it is a simpler alternative to make-list.- Index-of
`(index-of k x)`returns the index of the first occurrence of elementk in listx if it exists,NIL otherwise.- All-equalp
`(all-equalp a x)`determines if every member ofx is equal toa .- Sublistp
`(sublistp x y)`checks whether the listx ever occurs within the listy .- 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 sublistx within the listy , orNIL if there is no such occurrence.- List-equiv
`(list-equiv x y)`is an equivalence relation that determines whetherx andy are identical except perhaps in their final-cdrs.- Final-cdr
`(final-cdr x)`returns the atom in the "cdr-most branch" ofx .- 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 ofx .- Suffixp
`(suffixp x y)`determines if the listx occurs at the end of the listy .- 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 bothx andy , if one exists.- Subsetp-witness
`(subsetp-witness x y)`finds an element ofx that is not a member ofy , 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.