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:
Set::empty
gives an empty setSet::full
gives the set of all elements inA
Set::new
constructs a set from a boolean predicate- The
set!
macro, to construct small sets of a fixed size - By manipulating an existing sequence with
Set::union
,Set::intersect
,Set::difference
,Set::complement
,Set::filter
,Set::insert
, orSet::remove
.
To prove that two sequences are equal, it is usually easiest to use the extensionality
operator =~=
.
Implementations§
Source§impl<A> Set<A>
impl<A> Set<A>
Sourcepub closed spec fn fold<B>(self, z: B, f: FnSpec<(B, A), B>) -> B
pub closed spec fn fold<B>(self, z: B, f: FnSpec<(B, A), B>) -> B
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>
impl<A> Set<A>
Sourcepub closed spec fn empty() -> Set<A>
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:
Sourcepub closed spec fn new(f: FnSpec<(A,), bool>) -> Set<A>
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));
Sourcepub open spec fn full() -> Set<A>
pub open spec fn full() -> Set<A>
{ Set::empty().complement() }
The “full” set, i.e., set containing every element of type A
.
Sourcepub closed spec fn contains(self, a: A) -> bool
pub closed spec fn contains(self, a: A) -> bool
Predicate indicating if the set contains the given element.
Sourcepub open spec fn spec_has(self, a: A) -> bool
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.
Sourcepub open spec fn subset_of(self, s2: Set<A>) -> bool
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.
Sourcepub closed spec fn insert(self, a: A) -> Set<A>
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.
Sourcepub closed spec fn remove(self, a: A) -> Set<A>
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.
Sourcepub open spec fn spec_add(self, s2: Set<A>) -> Set<A>
pub open spec fn spec_add(self, s2: Set<A>) -> Set<A>
{ self.union(s2) }
+
operator, synonymous with union
Sourcepub open spec fn spec_mul(self, s2: Set<A>) -> Set<A>
pub open spec fn spec_mul(self, s2: Set<A>) -> Set<A>
{ self.intersect(s2) }
*
operator, synonymous with intersect
Sourcepub closed spec fn difference(self, s2: Set<A>) -> Set<A>
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.
Sourcepub open spec fn spec_sub(self, s2: Set<A>) -> Set<A>
pub open spec fn spec_sub(self, s2: Set<A>) -> Set<A>
{ self.difference(s2) }
-
operator, synonymous with difference
Sourcepub closed spec fn complement(self) -> Set<A>
pub closed spec fn complement(self) -> Set<A>
Set complement (within the space of all possible elements in A
).
Sourcepub open spec fn filter(self, f: FnSpec<(A,), bool>) -> Set<A>
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
.
Sourcepub closed spec fn len(self) -> nat
pub closed spec fn len(self) -> nat
Cardinality of the set. (Only meaningful if a set is finite.)
Sourcepub open spec fn choose(self) -> A
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§impl<A> Set<A>
impl<A> Set<A>
Sourcepub open spec fn is_full(self) -> bool
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
.
Sourcepub open spec fn is_empty(self) -> b : bool
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
Sourcepub open spec fn map<B>(self, f: FnSpec<(A,), B>) -> Set<B>
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
.
Sourcepub open spec fn to_seq(self) -> Seq<A>
pub open spec fn to_seq(self) -> Seq<A>
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.
Sourcepub open spec fn to_sorted_seq(self, leq: FnSpec<(A, A), bool>) -> Seq<A>
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
Sourcepub open spec fn is_singleton(self) -> bool
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.
Sourcepub closed spec fn find_unique_minimal(self, r: FnSpec<(A, A), bool>) -> A
pub closed spec fn find_unique_minimal(self, r: FnSpec<(A, A), bool>) -> A
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
Sourcepub proof fn find_unique_minimal_ensures(self, r: FnSpec<(A, A), bool>)
pub proof fn find_unique_minimal_ensures(self, r: FnSpec<(A, A), bool>)
self.finite(),
self.len() > 0,
total_ordering(r),
ensuresis_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
.
Sourcepub closed spec fn find_unique_maximal(self, r: FnSpec<(A, A), bool>) -> A
pub closed spec fn find_unique_maximal(self, r: FnSpec<(A, A), bool>) -> A
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
Sourcepub proof fn find_unique_maximal_ensures(self, r: FnSpec<(A, A), bool>)
pub proof fn find_unique_maximal_ensures(self, r: FnSpec<(A, A), bool>)
self.finite(),
self.len() > 0,
total_ordering(r),
ensuresis_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
.
Sourcepub open spec fn to_multiset(self) -> Multiset<A>
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.
Sourcepub proof fn lemma_len0_is_empty(self)
pub proof fn lemma_len0_is_empty(self)
self.finite(),
self.len() == 0,
ensuresself == Set::<A>::empty(),
A finite set with length 0 is equivalent to the empty set.
Sourcepub proof fn lemma_singleton_size(self)
pub proof fn lemma_singleton_size(self)
self.is_singleton(),
ensuresself.len() == 1,
A singleton set has length 1.
Sourcepub proof fn lemma_is_singleton(s: Set<A>)
pub proof fn lemma_is_singleton(s: Set<A>)
s.finite(),
ensuress.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.
Sourcepub proof fn lemma_len_filter(self, f: FnSpec<(A,), bool>)
pub proof fn lemma_len_filter(self, f: FnSpec<(A,), bool>)
self.finite(),
ensuresself.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.
Sourcepub proof fn lemma_greatest_implies_maximal(self, r: FnSpec<(A, A), bool>, max: A)
pub proof fn lemma_greatest_implies_maximal(self, r: FnSpec<(A, A), bool>, max: A)
pre_ordering(r),
ensuresis_greatest(r, max, self) ==> is_maximal(r, max, self),
In a pre-ordered set, a greatest element is necessarily maximal.
Sourcepub proof fn lemma_least_implies_minimal(self, r: FnSpec<(A, A), bool>, min: A)
pub proof fn lemma_least_implies_minimal(self, r: FnSpec<(A, A), bool>, min: A)
pre_ordering(r),
ensuresis_least(r, min, self) ==> is_minimal(r, min, self),
In a pre-ordered set, a least element is necessarily minimal.
Sourcepub proof fn lemma_maximal_equivalent_greatest(self, r: FnSpec<(A, A), bool>, max: A)
pub proof fn lemma_maximal_equivalent_greatest(self, r: FnSpec<(A, A), bool>, max: A)
total_ordering(r),
ensuresis_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.
Sourcepub proof fn lemma_minimal_equivalent_least(self, r: FnSpec<(A, A), bool>, min: A)
pub proof fn lemma_minimal_equivalent_least(self, r: FnSpec<(A, A), bool>, min: A)
total_ordering(r),
ensuresis_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.
Sourcepub proof fn lemma_least_is_unique(self, r: FnSpec<(A, A), bool>)
pub proof fn lemma_least_is_unique(self, r: FnSpec<(A, A), bool>)
partial_ordering(r),
ensuresforall |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.
Sourcepub proof fn lemma_greatest_is_unique(self, r: FnSpec<(A, A), bool>)
pub proof fn lemma_greatest_is_unique(self, r: FnSpec<(A, A), bool>)
partial_ordering(r),
ensuresforall |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.
Sourcepub proof fn lemma_minimal_is_unique(self, r: FnSpec<(A, A), bool>)
pub proof fn lemma_minimal_is_unique(self, r: FnSpec<(A, A), bool>)
total_ordering(r),
ensuresforall |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.
Sourcepub proof fn lemma_maximal_is_unique(self, r: FnSpec<(A, A), bool>)
pub proof fn lemma_maximal_is_unique(self, r: FnSpec<(A, A), bool>)
self.finite(),
total_ordering(r),
ensuresforall |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.
Sourcepub broadcast proof fn lemma_set_insert_diff_decreases(self, s: Set<A>, elt: A)
pub broadcast proof fn lemma_set_insert_diff_decreases(self, s: Set<A>, elt: A)
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.
Sourcepub proof fn lemma_subset_not_in_lt(self: Set<A>, s2: Set<A>, elt: A)
pub proof fn lemma_subset_not_in_lt(self: Set<A>, s2: Set<A>, elt: A)
self.subset_of(s2),
s2.finite(),
!self.contains(elt),
s2.contains(elt),
ensuresself.len() < s2.len(),
If there is an element not present in a subset, its length is stricly smaller.
Sourcepub broadcast proof fn lemma_set_map_insert_commute<B>(self, elt: A, f: FnSpec<(A,), B>)
pub broadcast proof fn lemma_set_map_insert_commute<B>(self, elt: A, f: FnSpec<(A,), B>)
#[trigger] self.insert(elt).map(f) =~= self.map(f).insert(f(elt)),
Inserting an element and mapping a function over a set commute
Sourcepub proof fn lemma_map_union_commute<B>(self, t: Set<A>, f: FnSpec<(A,), B>)
pub proof fn lemma_map_union_commute<B>(self, t: Set<A>, f: FnSpec<(A,), B>)
(self.union(t)).map(f) =~= self.map(f).union(t.map(f)),
map
and union
commute
Sourcepub open spec fn all(&self, pred: FnSpec<(A,), bool>) -> bool
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
Sourcepub open spec fn any(&self, pred: FnSpec<(A,), bool>) -> bool
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
Sourcepub broadcast proof fn lemma_any_map_preserved_pred<B>(
self,
p: FnSpec<(A,), bool>,
q: FnSpec<(B,), bool>,
f: FnSpec<(A,), B>,
)
pub broadcast proof fn lemma_any_map_preserved_pred<B>( self, p: FnSpec<(A,), bool>, q: FnSpec<(B,), bool>, f: FnSpec<(A,), B>, )
#[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
.
Sourcepub open spec fn filter_map<B>(self, f: FnSpec<(A,), Option<B>>) -> Set<B>
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)
Sourcepub broadcast proof fn lemma_filter_map_insert<B>(
s: Set<A>,
f: FnSpec<(A,), Option<B>>,
elem: A,
)
pub broadcast proof fn lemma_filter_map_insert<B>( s: Set<A>, f: FnSpec<(A,), Option<B>>, elem: A, )
#[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
Sourcepub broadcast proof fn lemma_filter_map_union<B>(self, f: FnSpec<(A,), Option<B>>, t: Set<A>)
pub broadcast proof fn lemma_filter_map_union<B>(self, f: FnSpec<(A,), Option<B>>, t: Set<A>)
#[trigger] self.union(t).filter_map(f) == self.filter_map(f).union(t.filter_map(f)),
filter_map
and union
commute.
Sourcepub proof fn lemma_map_finite<B>(self, f: FnSpec<(A,), B>)
pub proof fn lemma_map_finite<B>(self, f: FnSpec<(A,), B>)
self.finite(),
ensuresself.map(f).finite(),
map
preserves finiteness
Sourcepub broadcast proof fn lemma_set_all_subset(self, s2: Set<A>, p: FnSpec<(A,), bool>)
pub broadcast proof fn lemma_set_all_subset(self, s2: Set<A>, p: FnSpec<(A,), bool>)
#[trigger] self.subset_of(s2),
s2.all(p),
ensures#[trigger] self.all(p),
Sourcepub broadcast proof fn lemma_filter_map_finite<B>(self, f: FnSpec<(A,), Option<B>>)
pub broadcast proof fn lemma_filter_map_finite<B>(self, f: FnSpec<(A,), Option<B>>)
self.finite(),
ensures#[trigger] self.filter_map(f).finite(),
filter_map
preserves finiteness.
Sourcepub broadcast proof fn lemma_to_seq_to_set_id(self)
pub broadcast proof fn lemma_to_seq_to_set_id(self)
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>>
impl<A> Set<Set<A>>
Sourcepub open spec fn flatten(self) -> Set<A>
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)
})
}
Sourcepub broadcast proof fn flatten_insert_union_commute(self, other: Set<A>)
pub broadcast proof fn flatten_insert_union_commute(self, other: Set<A>)
self.flatten().union(other) =~= #[trigger] self.insert(other).flatten(),