Struct SetCopy item path

self.finite(),

is_fun_commutative(f),

Folds the set, applying f to perform the fold. The next element for the fold is chosen by the choose operator.

Given a set s = {x0, x1, x2, ..., xn}, applying this function s.fold(init, f) returns f(...f(f(init, x0), x1), ..., xn).

The “empty” set.

Usage Example:

let empty_set = Set::<A>::empty();

assert(empty_set.is_empty());
assert(empty_set.complement() =~= Set::<A>::full());
assert(Set::<A>::empty().finite());
assert(Set::<A>::empty().len() == 0);
assert(forall |x: A| !Set::<A>::empty().contains(x));

Axioms around the empty set are:

• axiom_set_empty_finite
  
• axiom_set_empty_len
  
• axiom_set_empty

Set whose membership is determined by the given boolean predicate.

Usage Examples:

let set_a = Set::new(|x : nat| x < 42);
let set_b = Set::<A>::new(|x| some_predicate(x));
assert(forall|x| some_predicate(x) <==> set_b.contains(x));

{ Set::empty().complement() }

The “full” set, i.e., set containing every element of type A.

Predicate indicating if the set contains the given element.

{ self.contains(a) }

Predicate indicating if the set contains the given element: supports self has a syntax.

{ forall |a: A| self.contains(a) ==> s2.contains(a) }

Returns true if the first argument is a subset of the second.

Returns a new set with the given element inserted. If that element is already in the set, then an identical set is returned.

Returns a new set with the given element removed. If that element is already absent from the set, then an identical set is returned.

Union of two sets.

{ self.union(s2) }

+ operator, synonymous with union

Intersection of two sets.

{ self.intersect(s2) }

* operator, synonymous with intersect

Set difference, i.e., the set of all elements in the first one but not in the second.

{ self.difference(s2) }

- operator, synonymous with difference

Set complement (within the space of all possible elements in A).

{ self.intersect(Self::new(f)) }

Set of all elements in the given set which satisfy the predicate f.

Returns true if the set is finite.

Cardinality of the set. (Only meaningful if a set is finite.)

{ choose |a: A| self.contains(a) }

Chooses an arbitrary element of the set.

This is often useful for proofs by induction.

(Note that, although the result is arbitrary, it is still a deterministic function like any other spec function.)

Creates a Map whose domain is the given set. The values of the map are given by f, a function of the keys.

{ forall |a: A| self.contains(a) ==> !s2.contains(a) }

Returns true if the sets are disjoint, i.e., if their interesection is the empty set.

{ self == Set::<A>::full() }

Is true if called by a “full” set, i.e., a set containing every element of type A.

{ self =~= Set::<A>::empty() }

Is true if called by an “empty” set, i.e., a set containing no elements and has length 0

{ Set::new(|a: B| exists |x: A| self.contains(x) && a == f(x)) }

Returns the set contains an element f(x) for every element x in self.

self.finite(),

{
    if self.len() == 0 {
        Seq::<A>::empty()
    } else {
        let x = self.choose();
        Seq::<A>::empty().push(x) + self.remove(x).to_seq()
    }
}

Converts a set into a sequence with an arbitrary ordering.

{ self.to_seq().sort_by(leq) }

Converts a set into a sequence sorted by the given ordering function leq

{
    &&& self.len() > 0
    &&& (forall |x: A, y: A| self.contains(x) && self.contains(y) ==> x == y)

}

A singleton set has at least one element and any two elements are equal.

total_ordering(r),

self.len() > 0,

self.finite(),

Any totally-ordered set contains a unique minimal (equivalently, least) element. Returns an arbitrary value if r is not a total ordering

self.finite(),

self.len() > 0,

total_ordering(r),

is_minimal(r, self.find_unique_minimal(r), self)
    && (forall |min: A| is_minimal(r, min, self) ==> self.find_unique_minimal(r) == min),

Proof of correctness and expected behavior for Set::find_unique_minimal.

total_ordering(r),

self.len() > 0,

Any totally-ordered set contains a unique maximal (equivalently, greatest) element. Returns an arbitrary value if r is not a total ordering

self.finite(),

self.len() > 0,

total_ordering(r),

is_maximal(r, self.find_unique_maximal(r), self)
    && (forall |max: A| is_maximal(r, max, self) ==> self.find_unique_maximal(r) == max),

Proof of correctness and expected behavior for Set::find_unique_maximal.

{
    if self.len() == 0 {
        Multiset::<A>::empty()
    } else {
        Multiset::<A>::empty()
            .insert(self.choose())
            .add(self.remove(self.choose()).to_multiset())
    }
}

Converts a set into a multiset where each element from the set has multiplicity 1 and any other element has multiplicity 0.

self.finite(),

self.len() == 0,

self == Set::<A>::empty(),

A finite set with length 0 is equivalent to the empty set.

self.is_singleton(),

self.len() == 1,

A singleton set has length 1.

s.finite(),

s.is_singleton() == (s.len() == 1),

A set has exactly one element, if and only if, it has at least one element and any two elements are equal.

self.finite(),

self.filter(f).finite(),

self.filter(f).len() <= self.len(),

The result of filtering a finite set is finite and has size less than or equal to the original set.

pre_ordering(r),

is_greatest(r, max, self) ==> is_maximal(r, max, self),

In a pre-ordered set, a greatest element is necessarily maximal.

pre_ordering(r),

is_least(r, min, self) ==> is_minimal(r, min, self),

In a pre-ordered set, a least element is necessarily minimal.

total_ordering(r),

is_greatest(r, max, self) <==> is_maximal(r, max, self),

In a totally-ordered set, an element is maximal if and only if it is a greatest element.

total_ordering(r),

is_least(r, min, self) <==> is_minimal(r, min, self),

In a totally-ordered set, an element is maximal if and only if it is a greatest element.

partial_ordering(r),

forall |min: A, min_prime: A| {
    is_least(r, min, self) && is_least(r, min_prime, self) ==> min == min_prime
},

In a partially-ordered set, there exists at most one least element.

partial_ordering(r),

forall |max: A, max_prime: A| {
    is_greatest(r, max, self) && is_greatest(r, max_prime, self) ==> max == max_prime
},

In a partially-ordered set, there exists at most one greatest element.

total_ordering(r),

forall |min: A, min_prime: A| {
    is_minimal(r, min, self) && is_minimal(r, min_prime, self) ==> min == min_prime
},

In a totally-ordered set, there exists at most one minimal element.

self.finite(),

total_ordering(r),

forall |max: A, max_prime: A| {
    is_maximal(r, max, self) && is_maximal(r, max_prime, self) ==> max == max_prime
},

In a totally-ordered set, there exists at most one maximal element.

self.contains(elt),

!s.contains(elt),

self.finite(),

#[trigger] self.difference(s.insert(elt)).len() < self.difference(s).len(),

Set difference with an additional element inserted decreases the size of the result. This can be useful for proving termination when traversing a set while tracking the elements that have already been handled.

self.subset_of(s2),

s2.finite(),

!self.contains(elt),

s2.contains(elt),

self.len() < s2.len(),

If there is an element not present in a subset, its length is stricly smaller.

#[trigger] self.insert(elt).map(f) =~= self.map(f).insert(f(elt)),

Inserting an element and mapping a function over a set commute

(self.union(t)).map(f) =~= self.map(f).union(t.map(f)),

map and union commute

{ forall |x: A| self.contains(x) ==> pred(x) }

Utility function for more concise universal quantification over sets

{ exists |x: A| self.contains(x) && pred(x) }

Utility function for more concise existential quantification over sets

#[trigger] self.any(p),

forall |x: A| #[trigger] p(x) ==> q(f(x)),

#[trigger] self.map(f).any(q),

any is preserved between predicates p and q if p implies q.

{
    self.map(|elem: A| match f(elem) {
            Option::Some(r) => {
                set! {
                    r
                }
            }
            Option::None => set! {},
        })
        .flatten()
}

Collecting all elements b where f returns Some(b)

#[trigger] s.insert(elem).filter_map(f)
    == (match f(elem) {
        Some(res) => s.filter_map(f).insert(res),
        None => s.filter_map(f),
    }),

Inserting commutes with filter_map

#[trigger] self.union(t).filter_map(f) == self.filter_map(f).union(t.filter_map(f)),

filter_map and union commute.

self.finite(),

self.map(f).finite(),

map preserves finiteness

self.finite(),

#[trigger] self.filter_map(f).finite(),

filter_map preserves finiteness.

self.finite(),

#[trigger] self.to_seq().to_set() =~= self,

Conversion to a sequence and back to a set is the identity function.

Returns the argument unchanged.

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.