Struct vstd::set::SetCopy item path

The “empty” set.

Set whose membership is determined by the given boolean predicate.

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

{ self =~= s2 }

DEPRECATED: use =~= or =~~= instead. Returns true if for every value a: A, it is either in both input sets or neither. This is equivalent to the sets being actually equal by axiom_set_ext_equal.

To prove that two sets are equal via extensionality, it may be easier to use the general-purpose =~= or =~~= or to use the assert_sets_equal! macro, rather than using .ext_equal directly.

{ 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) }

Set complement (within the space of all possible elements in A). - operator, synonymous with difference

{ 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.len() == 0 }

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.

{
    if self.finite() {
        if self.len() == 0 {
            init
        } else {
            let a = self.choose();
            self.remove(a).fold(f(init, a), f)
        }
    } else {
        arbitrary()
    }
}

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

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.

Returns the argument unchanged.

Calls U::from(self).

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