vstd::set

Struct Set

Source
pub struct Set<A> { /* private fields */ }
Expand description

Set<A> is a set type for specifications.

An object set: Set<A> is a subset of the set of all values a: A. Equivalently, it can be thought of as a boolean predicate on A.

In general, a set might be infinite. To work specifically with finite sets, see the self.finite() predicate.

Sets can be constructed in a few different ways:

To prove that two sequences are equal, it is usually easiest to use the extensionality operator =~=.

Implementations§

Source§

impl<A> Set<A>

Source

pub closed spec fn fold<B>(self, z: B, f: FnSpec<(B, A), B>) -> B

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

Source§

impl<A> Set<A>

Source

pub closed spec fn empty() -> Set<A>

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:

Source

pub closed spec fn new(f: FnSpec<(A,), bool>) -> Set<A>

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));
Source

pub open spec fn full() -> Set<A>

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

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

Source

pub closed spec fn contains(self, a: A) -> bool

Predicate indicating if the set contains the given element.

Source

pub open spec fn spec_has(self, a: A) -> bool

{ self.contains(a) }

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

Source

pub open spec fn subset_of(self, s2: Set<A>) -> bool

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

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

Source

pub open spec fn spec_le(self, s2: Set<A>) -> bool

{ self.subset_of(s2) }
Source

pub closed spec fn insert(self, a: A) -> Set<A>

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

Source

pub closed spec fn remove(self, a: A) -> Set<A>

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

Source

pub closed spec fn union(self, s2: Set<A>) -> Set<A>

Union of two sets.

Source

pub open spec fn spec_add(self, s2: Set<A>) -> Set<A>

{ self.union(s2) }

+ operator, synonymous with union

Source

pub closed spec fn intersect(self, s2: Set<A>) -> Set<A>

Intersection of two sets.

Source

pub open spec fn spec_mul(self, s2: Set<A>) -> Set<A>

{ self.intersect(s2) }

* operator, synonymous with intersect

Source

pub closed spec fn difference(self, s2: Set<A>) -> Set<A>

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

Source

pub open spec fn spec_sub(self, s2: Set<A>) -> Set<A>

{ self.difference(s2) }

- operator, synonymous with difference

Source

pub closed spec fn complement(self) -> Set<A>

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

Source

pub open spec fn filter(self, f: FnSpec<(A,), bool>) -> Set<A>

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

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

Source

pub closed spec fn finite(self) -> bool

Returns true if the set is finite.

Source

pub closed spec fn len(self) -> nat

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

Source

pub open spec fn choose(self) -> A

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

Source

pub uninterp fn mk_map<V>(self, f: FnSpec<(A,), V>) -> Map<A, V>

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

Source

pub open spec fn disjoint(self, s2: Self) -> bool

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

Source§

impl<A> Set<A>

Source

pub open spec fn is_full(self) -> bool

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

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

Source

pub open spec fn is_empty(self) -> b : bool

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

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

Source

pub open spec fn map<B>(self, f: FnSpec<(A,), B>) -> Set<B>

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

Source

pub open spec fn to_seq(self) -> Seq<A>

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

Source

pub open spec fn to_sorted_seq(self, leq: FnSpec<(A, A), bool>) -> Seq<A>

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

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

Source

pub open spec fn is_singleton(self) -> bool

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

Source

pub closed spec fn find_unique_minimal(self, r: FnSpec<(A, A), bool>) -> A

recommends
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

Source

pub proof fn find_unique_minimal_ensures(self, r: FnSpec<(A, A), bool>)

requires
self.finite(),
self.len() > 0,
total_ordering(r),
ensures
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.

Source

pub closed spec fn find_unique_maximal(self, r: FnSpec<(A, A), bool>) -> A

recommends
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

Source

pub proof fn find_unique_maximal_ensures(self, r: FnSpec<(A, A), bool>)

requires
self.finite(),
self.len() > 0,
total_ordering(r),
ensures
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.

Source

pub open spec fn to_multiset(self) -> Multiset<A>

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

Source

pub proof fn lemma_len0_is_empty(self)

requires
self.finite(),
self.len() == 0,
ensures
self == Set::<A>::empty(),

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

Source

pub proof fn lemma_singleton_size(self)

requires
self.is_singleton(),
ensures
self.len() == 1,

A singleton set has length 1.

Source

pub proof fn lemma_is_singleton(s: Set<A>)

requires
s.finite(),
ensures
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.

Source

pub proof fn lemma_len_filter(self, f: FnSpec<(A,), bool>)

requires
self.finite(),
ensures
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.

Source

pub proof fn lemma_greatest_implies_maximal(self, r: FnSpec<(A, A), bool>, max: A)

requires
pre_ordering(r),
ensures
is_greatest(r, max, self) ==> is_maximal(r, max, self),

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

Source

pub proof fn lemma_least_implies_minimal(self, r: FnSpec<(A, A), bool>, min: A)

requires
pre_ordering(r),
ensures
is_least(r, min, self) ==> is_minimal(r, min, self),

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

Source

pub proof fn lemma_maximal_equivalent_greatest(self, r: FnSpec<(A, A), bool>, max: A)

requires
total_ordering(r),
ensures
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.

Source

pub proof fn lemma_minimal_equivalent_least(self, r: FnSpec<(A, A), bool>, min: A)

requires
total_ordering(r),
ensures
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.

Source

pub proof fn lemma_least_is_unique(self, r: FnSpec<(A, A), bool>)

requires
partial_ordering(r),
ensures
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.

Source

pub proof fn lemma_greatest_is_unique(self, r: FnSpec<(A, A), bool>)

requires
partial_ordering(r),
ensures
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.

Source

pub proof fn lemma_minimal_is_unique(self, r: FnSpec<(A, A), bool>)

requires
total_ordering(r),
ensures
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.

Source

pub proof fn lemma_maximal_is_unique(self, r: FnSpec<(A, A), bool>)

requires
self.finite(),
total_ordering(r),
ensures
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.

Source

pub broadcast proof fn lemma_set_insert_diff_decreases(self, s: Set<A>, elt: A)

requires
self.contains(elt),
!s.contains(elt),
self.finite(),
ensures
#[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.

Source

pub proof fn lemma_subset_not_in_lt(self: Set<A>, s2: Set<A>, elt: A)

requires
self.subset_of(s2),
s2.finite(),
!self.contains(elt),
s2.contains(elt),
ensures
self.len() < s2.len(),

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

Source

pub broadcast proof fn lemma_set_map_insert_commute<B>(self, elt: A, f: FnSpec<(A,), B>)

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

Inserting an element and mapping a function over a set commute

Source

pub proof fn lemma_map_union_commute<B>(self, t: Set<A>, f: FnSpec<(A,), B>)

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

map and union commute

Source

pub open spec fn all(&self, pred: FnSpec<(A,), bool>) -> bool

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

Utility function for more concise universal quantification over sets

Source

pub open spec fn any(&self, pred: FnSpec<(A,), bool>) -> bool

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

Utility function for more concise existential quantification over sets

Source

pub broadcast proof fn lemma_any_map_preserved_pred<B>( self, p: FnSpec<(A,), bool>, q: FnSpec<(B,), bool>, f: FnSpec<(A,), B>, )

requires
#[trigger] self.any(p),
forall |x: A| #[trigger] p(x) ==> q(f(x)),
ensures
#[trigger] self.map(f).any(q),

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

Source

pub open spec fn filter_map<B>(self, f: FnSpec<(A,), Option<B>>) -> Set<B>

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

Source

pub broadcast proof fn lemma_filter_map_insert<B>( s: Set<A>, f: FnSpec<(A,), Option<B>>, elem: A, )

ensures
#[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

Source

pub broadcast proof fn lemma_filter_map_union<B>(self, f: FnSpec<(A,), Option<B>>, t: Set<A>)

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

filter_map and union commute.

Source

pub proof fn lemma_map_finite<B>(self, f: FnSpec<(A,), B>)

requires
self.finite(),
ensures
self.map(f).finite(),

map preserves finiteness

Source

pub broadcast proof fn lemma_set_all_subset(self, s2: Set<A>, p: FnSpec<(A,), bool>)

requires
#[trigger] self.subset_of(s2),
s2.all(p),
ensures
#[trigger] self.all(p),
Source

pub broadcast proof fn lemma_filter_map_finite<B>(self, f: FnSpec<(A,), Option<B>>)

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

filter_map preserves finiteness.

Source

pub broadcast proof fn lemma_to_seq_to_set_id(self)

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

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

Source§

impl<A> Set<Set<A>>

Source

pub open spec fn flatten(self) -> Set<A>

{
    Set::new(|elem| {
        exists |elem_s: Set<A>| #[trigger] self.contains(elem_s) && elem_s.contains(elem)
    })
}
Source

pub broadcast proof fn flatten_insert_union_commute(self, other: Set<A>)

ensures
self.flatten().union(other) =~= #[trigger] self.insert(other).flatten(),

Auto Trait Implementations§

§

impl<A> Freeze for Set<A>

§

impl<A> RefUnwindSafe for Set<A>
where A: RefUnwindSafe,

§

impl<A> Send for Set<A>
where A: Send,

§

impl<A> Sync for Set<A>
where A: Sync,

§

impl<A> Unpin for Set<A>
where A: Unpin,

§

impl<A> UnwindSafe for Set<A>
where A: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

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

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.