Struct ISet 

pub struct ISet<A> { /* private fields */ }

ISet<A> is a set type for specifications.

An object set: ISet<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.

ISets can be constructed in a few different ways:

• ISet::empty gives an empty set
• ISet::full gives the set of all elements in A
• ISet::new constructs a set from a boolean predicate
• The iset! macro, to construct small sets of a fixed size
• By manipulating an existing sequence with ISet::union, ISet::intersect, ISet::difference, ISet::complement, ISet::filter, ISet::insert, or ISet::remove.

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

Implementations

impl<A> ISet<A>

pub fn empty() -> ISet<A>

The “empty” set.

Usage Example:

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

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

Axioms around the empty set are:

• [lemma_iset_empty_finite]
• [lemma_iset_empty_len]
  
• [lemma_iset_empty]

pub fn new(f: FnSpec<(A,), bool>) -> ISet<A>

ISet whose membership is determined by the given boolean predicate.

Usage Examples:

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

pub fn full() -> ISet<A>

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

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

Predicate indicating if the set contains the given element.

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

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

pub fn subset_of(self, s2: ISet<A>) -> bool

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

pub fn spec_le(self, s2: ISet<A>) -> bool

pub fn insert(self, a: A) -> ISet<A>

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

pub fn remove(self, a: A) -> ISet<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.

pub fn union(self, s2: ISet<A>) -> ISet<A>

Union of two sets.

pub fn spec_add(self, s2: ISet<A>) -> ISet<A>

+ operator, synonymous with union

pub fn intersect(self, s2: ISet<A>) -> ISet<A>

Intersection of two sets.

pub fn spec_mul(self, s2: ISet<A>) -> ISet<A>

* operator, synonymous with intersect

pub fn difference(self, s2: ISet<A>) -> ISet<A>

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

pub fn spec_sub(self, s2: ISet<A>) -> ISet<A>

- operator, synonymous with difference

pub fn complement(self) -> ISet<A>

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

pub fn filter(self, f: FnSpec<(A,), bool>) -> ISet<A>

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

pub fn finite(self) -> bool

Returns true if the set is finite.

pub fn to_set(self) -> Option<Set<A>>

pub fn len(self) -> nat

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

pub fn choose(self) -> 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.)

pub fn mk_map<V>(self, f: FnSpec<(A,), V>) -> IMap<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.

pub fn disjoint(self, s2: ISet<A>) -> bool

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

pub fn congruent(self, s2: Set<A>) -> bool

Returns true if this set is congruent to (contains the same elements as) a given finite Set.

impl<A> ISet<A>

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

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

impl<A> ISet<A>

pub fn is_full(self) -> bool

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

pub fn is_empty(self) -> bool

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

pub fn map<B>(self, f: FnSpec<(A,), B>) -> ISet<B>

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

pub fn map_by<B>(self, fwd: FnSpec<(A,), B>, rev: FnSpec<(B,), A>) -> ISet<B>

ISet::map_by is like ISet::map, but map only takes a forward function fwd: spec_fn(A) -> B, while map_by also takes a reverse function rev: spec_fn(B) -> A such that rev(fwd(a)) == a. When fwd has such a reverse function, ISet::map_by can make proofs easier by avoiding the “exists” that appears in lemmas about ISet::map. Example: for a set s: ISet<int>, to map each i in s to (i, 10 * i), we can write either s.map(|i: int| (i, 10 * i)) or s.map_by(|i: int| (i, 10 * i), |p: (int, int)| p.0); the version with map_by is usually easier to use in proofs. If the recommendation forall|a: A| self.contains(a) ==> rev(fwd(a)) == a is satisfied, it is trivially guaranteed that self.map_by(fwd, rev) == self.map(fwd). Also see the set_build! macro for a convenient interface to map_by.

pub fn map_flatten_by<B>( self, fwd: FnSpec<(A,), ISet<B>>, rev: FnSpec<(B,), A>, ) -> ISet<B>

Similar to ISet::map_by, but the forward function returns ISet<B> rather than B, and map_flatten_by flattens the final result from ISet<ISet<B>> to just ISet<B>. This can be easier to work with in proofs than calling map and flatten separately, since map and flatten introduce “exists”, while map_flatten_by does not. Also see the set_build! macro for a convenient interface to map_flatten_by.

pub fn map_flatten_by_is_map_flatten<B>( self, fwd: FnSpec<(A,), ISet<B>>, rev: FnSpec<(B,), A>, )

This proof demonstrates that calling map_flatten_by is equivalent to first calling map, then calling flatten.

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

Converts a set into a sequence with an arbitrary ordering.

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

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

pub fn is_singleton(self) -> bool

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

pub fn injective_on<B>(self, r: FnSpec<(A,), B>) -> bool

Indicates if the function given by r is injective on this set, i.e., whether each element of this set is mapped to a different value by r.

pub fn has_least(self, leq: FnSpec<(A, A), bool>, min: A) -> bool

An element in an ordered set is called a least element (or a minimum), if it is less than every other element of the set.

pub fn has_minimum(self, leq: FnSpec<(A, A), bool>, min: A) -> bool

An element in an ordered set is called a minimal element, if no other element is less than it.

pub fn has_greatest(self, leq: FnSpec<(A, A), bool>, max: A) -> bool

An element in an ordered set is called a greatest element (or a maximum), if it is greater than every other element of the set.

pub fn has_maximum(self, leq: FnSpec<(A, A), bool>, max: A) -> bool

An element in an ordered set is called a maximal element, if no other element is greater than it.

pub fn lemma_injective_on_subset<B>(self, r: FnSpec<(A,), B>, other: ISet<A>)

If a function is injective on the set self, then it is also injective on any subset other of self.

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

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

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

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

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

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

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

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

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

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

pub fn lemma_len0_is_empty(self)

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

pub fn lemma_singleton_size(self)

A singleton set has length 1.

pub fn lemma_is_singleton(s: ISet<A>)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

pub fn lemma_iset_insert_diff_decreases(self, s: ISet<A>, elt: A)

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

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

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

pub fn lemma_iset_map_insert_commute<B>(self, elt: A, f: FnSpec<(A,), B>)

Inserting an element and mapping a function over a set commute

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

map and union commute

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

Utility function for more concise universal quantification over sets

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

Utility function for more concise existential quantification over sets

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

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

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

Collecting all elements b where f returns Some(b)

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

Inserting commutes with filter_map

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

filter_map and union commute.

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

map preserves finiteness

pub fn lemma_map_by_finite<B>(self, fwd: FnSpec<(A,), B>, rev: FnSpec<(B,), A>)

map_by preserves finiteness.

pub fn lemma_map_flatten_by_finite<B>( self, fwd: FnSpec<(A,), ISet<B>>, rev: FnSpec<(B,), A>, )

map_flatten_by preserves finiteness.

pub fn lemma_iset_all_subset(self, s2: ISet<A>, p: FnSpec<(A,), bool>)

If self is a subset of s2, and all elements of s2 satisfy predicate p, then all elements of self satisfy predicate p.

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

filter_map preserves finiteness.

pub fn lemma_to_seq_to_set_id(self)

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

pub fn lemma_to_seq_no_duplicates(self)

Any sequence converted from finite iset has no duplicates

pub fn lemma_to_seq_len(self)

Conversion from finite iset to seq preserves the length

impl<A> ISet<ISet<A>>

pub fn flatten(self) -> ISet<A>

This function creates a set from all the elements of all the elements of self.

pub fn flatten_insert_union_commute(self, other: ISet<A>)

Flattening then unioning with another set is equivalent to inserting that other set and then flattening.

pub fn lemma_flatten_finite(self)

If self is finite and all its elements are finite, then self.flatten() is also finite.