		Search-engine friendly clone of the ACL2 documentation.

Std/osets

Primitives

Replacements for car, cdr, etc., that respect the non-set convention.

Since the osets library uses ordered lists as the underlying representation of sets, at some point we have to use list primitives (car, cdr, endp, cons) to operate on sets. A problem with using these functions directly is that they do not follow the non-set convention.

The non-set convention is: set operations should treat improper sets (i.e., non-nil atoms and lists that have duplicated or mis-ordered elements) as the empty set. We adopt this convention throughout the library. It allows most of our rewrite rules to have no setp hypotheses.

The primitive list functions do follow the non-set convention. For instance:

(car '(1 1 1)) = 1, but (car nil) = nil
(cdr '(1 1 1)) = (1 1), but (cdr nil) = nil
(cons 1 '(1 1 1)) = (1 1 1 1), but (cons 1 nil) = (1)
(endp '(1 1 1)) = nil, but (endp nil) = t

These behaviors make it harder to reason about set operations that are written directly in terms of the list primitives. When we try to do so, we usually have to do lots of work to consider all the cases about whether the inputs are ordered, etc.

To solve lots of these problems, we introduce new set primitives that are mostly like the list primitives, except that they follow the non-set convention. These primitives are:

(head X) - the first element of a set, nil for non/empty sets
(tail X) - all rest of the set, nil for non/empty sets
(insert a X) - ordered insert of a into X
(empty X) - recognizer for non/empty sets.

The general idea is that set operations should be written in terms of these set primitives instead of the list primitives, and the definitions of the set primitives should be kept disabled to avoid having to reason about the low level structure of sets.

Subtopics

Setp: (setp x) recognizes well-formed ordered sets.
Insert: (insert a x) adds the element a to the set X.
Head: (head x) returns the smallest element in a set.
Tail: (tail x) returns the remainder of a set after removing its head.
Sfix: (sfix x) is a fixing function for sets.
Empty: (empty x) recognizes empty sets.