vstd/
set.rs

1#[allow(unused_imports)]
2use super::iset::*;
3#[allow(unused_imports)]
4use super::map::*;
5#[allow(unused_imports)]
6use super::pervasive::*;
7#[allow(unused_imports)]
8use super::prelude::*;
9
10verus! {
11
12/// `Set<A>` is a finite set type for specifications.
13///
14/// An object `set: Set<A>` is a subset of the set of all values `a: A`.
15/// Equivalently, it can be thought of as a boolean predicate on `A`.
16///
17/// Sets can be constructed in a few different ways:
18///  * [`Set::empty`] gives an empty set
19///  * [`Set::new`] constructs a set from a boolean predicate
20///  * The [`set!`] macro, to construct small sets of a fixed size
21///  * By manipulating an existing sequence with [`Set::union`], [`Set::intersect`],
22///    [`Set::difference`], [`Set::complement`], [`Set::filter`], [`Set::insert`],
23///    or [`Set::remove`].
24///
25/// To prove that two sequences are equal, it is usually easiest to use the extensionality
26/// operator `=~=`.
27///
28/// `Set` only holds finite sets, so it can be used in recursive types.
29/// For instance, a type `T` can contain a `Set<T>`.
30#[verifier::ext_equal]
31#[verifier::external_body]
32#[verifier::accept_recursive_types(A)]
33#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::set::Set")]
34pub struct Set<A> {
35    // To prevent Verus's internal checks from rejecting recursive types,
36    // we use an artificial definition of `Set` that hides its inclusion
37    // of a function from `A` to `bool`.
38    //
39    // To make sure that proofs in this file don't take advantage of
40    // this artificial structure (e.g., to prove that any two `Set`s are
41    // equal), we mark this definition as `external_body`.
42    //
43    // For future work, we may figure out how to have `Set` use a
44    // `Seq`-like representation that is inherently finite, to eliminate
45    // the need for this. We haven't done this yet, though, because it would
46    // introduce the problem of multiple representations of equivalent
47    // sets, which creates a different problem with extensional equality.
48    dummy: core::marker::PhantomData<A>,
49}
50
51impl<A> Set<A> {
52    /// Generates an `ISet` with the same elements
53    pub uninterp spec fn to_iset(self) -> ISet<A>;
54
55    /// Generates a `Set` from the given `ISet`, governed by
56    /// `axiom_make_set`. Thanks to the axiom `axiom_make_set`, this
57    /// function is known to produce a `Set` with the same elements as
58    /// the given `ISet`, provided that `ISet` is finite. If the given
59    /// `ISet` is infinite, it produces an arbitrary finite set.
60    uninterp spec fn make_set(s: ISet<A>) -> Set<A>;
61
62    /// This axiom says that `make_set` produces a `Set` with the same
63    /// elements as the given `ISet`, provided that `ISet` is finite.
64    /// (If the given `ISet` is infinite, `make_set` produces an
65    /// arbitrary finite set.)
66    broadcast axiom fn axiom_make_set(s: ISet<A>)
67        requires
68            s.finite(),
69        ensures
70            #![trigger Self::make_set(s).to_iset()]
71            Self::make_set(s).to_iset() == s,
72    ;
73
74    /// This axiom says that the set represented by a `Set` is always
75    /// finite.
76    broadcast axiom fn axiom_is_finite(self)
77        ensures
78            #![trigger self.to_iset().finite()]
79            self.to_iset().finite(),
80    ;
81
82    /// The "empty" set.
83    ///
84    /// Usage Example: <br>
85    /// ```rust
86    /// let empty_set = Set::<A>::empty();
87    ///
88    /// assert(empty_set.is_empty());
89    /// assert(empty_set.complement() =~= Set::<A>::full());
90    /// assert(Set::<A>::empty().finite());
91    /// assert(Set::<A>::empty().len() == 0);
92    /// assert(forall |x: A| !Set::<A>::empty().contains(x));
93    /// ```
94    /// Axioms around the empty set are: <br>
95    /// * [`lemma_set_empty_len`] <br>
96    /// * [`lemma_set_empty`]
97    #[rustc_diagnostic_item = "verus::vstd::set::Set::empty"]
98    pub closed spec fn empty() -> Set<A> {
99        Self::make_set(ISet::<A>::empty())
100    }
101
102    /// Set whose membership is determined by the given `ISet`,
103    /// but only if that `ISet` is finite.
104    ///
105    /// Usage Examples:
106    /// ```rust
107    /// let iset_a = ISet::new(|x : nat| x < 42);
108    /// let option_set_b = Set::<A>::new(iset_a);
109    /// assert(iset_a.finite() ==>
110    ///        option_set_b matches Some(s) &&
111    ///        forall|x| x < 42 <==> s.contains(x));
112    /// ```
113    pub closed spec fn new_from_iset(s: ISet<A>) -> Option<Set<A>> {
114        if s.finite() {
115            Some(Self::make_set(s))
116        } else {
117            None
118        }
119    }
120
121    /// Set whose membership is determined by the given boolean predicate,
122    /// but only if the predicate produces a finite set. (If it produces an
123    /// infinite set, the result of this function is None.)
124    ///
125    /// Usage Examples:
126    /// ```rust
127    /// let option_set_a = Set::new(|x : nat| x < 42);
128    /// let option_set_b = Set::<A>::new(|x| some_predicate(x));
129    /// assert(ISet::new(|x| some_predicate(x)).finite()) ==>
130    ///        option_set_b matches Some(s) &&
131    ///        forall|x| some_predicate(x) <==> s.contains(x));
132    /// ```
133    pub closed spec fn new(f: spec_fn(A) -> bool) -> Option<Set<A>> {
134        Self::new_from_iset(ISet::new(f))
135    }
136
137    /// Set whose membership is determined by the given boolean predicate,
138    /// assuming the predicate produces a finite set.
139    ///
140    /// Usage Examples:
141    /// ```rust
142    /// let set_a = Set::new_assuming_finite(|x : nat| x < 42);
143    /// let set_b = Set::<A>::new_assuming_finite(|x| some_predicate(x));
144    /// assert(forall|x| some_predicate(x) <==> set_b.contains(x));
145    /// ```
146    #[deprecated(note = "Set::new_assuming_finite is helpful for incremental porting of existing code to the new version of Verus supporting finite sets. But it's dangerous since it assumes the given function describes a finite set.")]
147    pub closed spec fn new_assuming_finite(f: spec_fn(A) -> bool) -> Set<A> {
148        Self::make_set(ISet::new(f))
149    }
150
151    /// The "full" set, i.e., set containing every element of type `A`.
152    /// Note that if `A` is infinite, then this produces None.
153    #[rustc_diagnostic_item = "verus::vstd::set::Set::full"]
154    pub open spec fn full() -> Option<Set<A>> {
155        Set::new(|a: A| true)
156    }
157
158    /// Predicate indicating if the set contains the given element.
159    #[rustc_diagnostic_item = "verus::vstd::set::Set::contains"]
160    #[verifier::inline]
161    pub open spec fn contains(self, a: A) -> bool {
162        self.to_iset().contains(a)
163    }
164
165    /// Predicate indicating if the set contains the given element: supports `self has a` syntax.
166    #[verifier::inline]
167    pub open spec fn spec_has(self, a: A) -> bool {
168        self.contains(a)
169    }
170
171    /// Returns `true` if the first argument is a subset of the second.
172    #[rustc_diagnostic_item = "verus::vstd::set::Set::subset_of"]
173    pub open spec fn subset_of(self, s2: Set<A>) -> bool {
174        forall|a: A| self.contains(a) ==> s2.contains(a)
175    }
176
177    #[verifier::inline]
178    pub open spec fn spec_le(self, s2: Set<A>) -> bool {
179        self.subset_of(s2)
180    }
181
182    /// Returns a new set with the given element inserted.
183    /// If that element is already in the set, then an identical set is returned.
184    #[rustc_diagnostic_item = "verus::vstd::set::Set::insert"]
185    pub closed spec fn insert(self, a: A) -> Set<A> {
186        Self::make_set(self.to_iset().insert(a))
187    }
188
189    /// Returns a new set with the given element removed.
190    /// If that element is already absent from the set, then an identical set is returned.
191    #[rustc_diagnostic_item = "verus::vstd::set::Set::remove"]
192    pub closed spec fn remove(self, a: A) -> Set<A> {
193        Self::make_set(self.to_iset().remove(a))
194    }
195
196    /// Union of two sets.
197    pub closed spec fn union(self, s2: Set<A>) -> Set<A> {
198        Self::make_set(self.to_iset().union(s2.to_iset()))
199    }
200
201    /// `+` operator, synonymous with `union`
202    #[verifier::inline]
203    pub open spec fn spec_add(self, s2: Set<A>) -> Set<A> {
204        self.union(s2)
205    }
206
207    /// Intersection of two sets.
208    pub closed spec fn intersect(self, s2: Set<A>) -> Set<A> {
209        Self::make_set(self.to_iset().intersect(s2.to_iset()))
210    }
211
212    /// `*` operator, synonymous with `intersect`
213    #[verifier::inline]
214    pub open spec fn spec_mul(self, s2: Set<A>) -> Set<A> {
215        self.intersect(s2)
216    }
217
218    /// Set difference, i.e., the set of all elements in the first one but not in the second.
219    pub closed spec fn difference(self, s2: Set<A>) -> Set<A> {
220        Self::make_set(self.to_iset().difference(s2.to_iset()))
221    }
222
223    /// `-` operator, synonymous with `difference`
224    #[verifier::inline]
225    pub open spec fn spec_sub(self, s2: Set<A>) -> Set<A> {
226        self.difference(s2)
227    }
228
229    /// Set complement (within the space of all possible elements in `A`).
230    /// Returns None if this would be an infinite set.
231    pub open spec fn complement(self) -> Option<Set<A>> {
232        Set::new(|a| !self.contains(a))
233    }
234
235    /// Set of all elements in the given set which satisfy the predicate `f`.
236    pub closed spec fn filter(self, f: spec_fn(A) -> bool) -> Set<A> {
237        Self::make_set(self.to_iset().filter(f))
238    }
239
240    /// Returns `true` if the set is finite.
241    #[deprecated(note = "Every Set is always finite, so this is always true.")]
242    pub open spec fn finite(self) -> bool {
243        true
244    }
245
246    /// Returns `true` if this set is congruent to (contains the same elements as)
247    /// a given ISet.
248    pub open spec fn congruent(self, s2: ISet<A>) -> bool {
249        forall|a: A| #![all_triggers] self.contains(a) <==> s2.contains(a)
250    }
251
252    /// Cardinality of the set.
253    pub closed spec fn len(self) -> nat {
254        self.to_iset().len()
255    }
256
257    /// Chooses an arbitrary element of the set.
258    ///
259    /// This is often useful for proofs by induction.
260    ///
261    /// (Note that, although the result is arbitrary, it is still a _deterministic_ function
262    /// like any other `spec` function.)
263    pub open spec fn choose(self) -> A {
264        choose|a: A| self.contains(a)
265    }
266
267    /// Returns `true` if the sets are disjoint, i.e., if their interesection is
268    /// the empty set.
269    pub open spec fn disjoint(self, s2: Self) -> bool {
270        forall|a: A| self.contains(a) ==> !s2.contains(a)
271    }
272}
273
274/// Sets `s1` and `s2` are considered equal if and only if they contain all of the same elements.
275/// This has to be an axiom because `Set` is `external_body`.
276pub broadcast proof fn axiom_set_ext_equal<A>(s1: Set<A>, s2: Set<A>)
277    ensures
278        #[trigger] (s1 =~= s2) <==> (forall|a: A| s1.contains(a) == s2.contains(a)),
279{
280    admit();
281}
282
283/// Sets `s1` and `s2` are considered equal if and only if they contain all of the same elements.
284/// This has to be an axiom because `Set` is `external_body`.
285pub broadcast proof fn axiom_set_ext_equal_deep<A>(s1: Set<A>, s2: Set<A>)
286    ensures
287        #[trigger] (s1 =~~= s2) <==> s1 =~= s2,
288{
289    admit();
290}
291
292broadcast use super::iset::group_iset_lemmas;
293
294pub mod fold {
295    use super::*;
296
297    impl<A> Set<A> {
298        /// Folds the set, applying `f` to perform the fold. The next element for the fold is chosen by
299        /// the choose operator.
300        ///
301        /// Given a set `s = {x0, x1, x2, ..., xn}`, applying this function `s.fold(init, f)`
302        /// returns `f(...f(f(init, x0), x1), ..., xn)`.
303        #[verifier::inline]
304        pub open spec fn fold<B>(self, z: B, f: spec_fn(B, A) -> B) -> B
305            recommends
306                super::super::iset::fold::is_fun_commutative(f),
307        {
308            self.to_iset().fold(z, f)
309        }
310    }
311
312}
313
314/// The empty set contains no elements
315pub broadcast proof fn lemma_set_empty<A>(a: A)
316    ensures
317        !(#[trigger] Set::empty().contains(a)),
318{
319    broadcast use Set::axiom_make_set;
320
321}
322
323/// If `Set::<A>::new(f)` produces `Some(s)`, then `s` contains `a`
324/// if and only if `f(a)` is true.
325pub broadcast proof fn lemma_set_new<A>(f: spec_fn(A) -> bool, a: A)
326    requires
327        Set::<A>::new(f) is Some,
328    ensures
329        #[trigger] Set::<A>::new(f).unwrap().contains(a) == f(a),
330{
331    broadcast use Set::axiom_make_set;
332
333}
334
335/// If `ISet::<A>::new(f)` is finite, then `Set::<A>::new(f)`
336/// produces `Some(s)`. Useful for triggering the `lemma_set_new`
337/// to show that `s` contains `a` if and only if `f(a)` is true.
338pub broadcast proof fn lemma_set_new_some<A>(f: spec_fn(A) -> bool)
339    requires
340        ISet::<A>::new(f).finite(),
341    ensures
342        #[trigger] Set::<A>::new(f) is Some,
343{
344    broadcast use Set::axiom_make_set;
345
346}
347
348/// Shows that `Set::<A>::new_assuming_finite(f)` contains `a`
349/// if and only if `f(a)` is true.
350#[allow(deprecated)]
351pub broadcast proof fn lemma_set_new_assuming_finite<A>(f: spec_fn(A) -> bool, a: A)
352    ensures
353        #[trigger] Set::<A>::new_assuming_finite(f).contains(a) == f(a),
354{
355    broadcast use Set::axiom_make_set;
356
357    assume(ISet::new(f).finite());  // This is the assumption
358}
359
360/// If an iset `s` is finite, then `Set::new_from_iset(s)` has the same
361/// contents as `s`.
362pub broadcast proof fn lemma_set_new_from_iset<A>(s: ISet<A>)
363    requires
364        s.finite(),
365    ensures
366        #![trigger Set::<A>::new_from_iset(s)]
367        Set::<A>::new_from_iset(s) is Some,
368        Set::<A>::new_from_iset(s).unwrap().to_iset() == s,
369{
370    broadcast use Set::axiom_make_set;
371
372    assert(ISet::new(|a: A| s.contains(a)) =~= s);
373}
374
375/// The result of inserting element `a` into set `s` must contains `a`.
376pub broadcast proof fn lemma_set_insert_same<A>(s: Set<A>, a: A)
377    ensures
378        #[trigger] s.insert(a).contains(a),
379{
380    broadcast use Set::axiom_make_set;
381    broadcast use Set::axiom_is_finite;
382
383}
384
385/// If `a1` does not equal `a2`, then the result of inserting element `a2` into set `s`
386/// must contain `a1` if and only if the set contained `a1` before the insertion of `a2`.
387pub broadcast proof fn lemma_set_insert_different<A>(s: Set<A>, a1: A, a2: A)
388    requires
389        a1 != a2,
390    ensures
391        #[trigger] s.insert(a2).contains(a1) == s.contains(a1),
392{
393    broadcast use Set::axiom_make_set;
394    broadcast use Set::axiom_is_finite;
395
396}
397
398/// The result of removing element `a` from set `s` must not contain `a`.
399pub broadcast proof fn lemma_set_remove_same<A>(s: Set<A>, a: A)
400    ensures
401        !(#[trigger] s.remove(a).contains(a)),
402{
403    broadcast use Set::axiom_make_set;
404    broadcast use Set::axiom_is_finite;
405
406}
407
408/// Removing an element `a` from a set `s` and then inserting `a` back into the set`
409/// is equivalent to the original set `s`.
410pub broadcast proof fn lemma_set_remove_insert<A>(s: Set<A>, a: A)
411    requires
412        s.contains(a),
413    ensures
414        (#[trigger] s.remove(a)).insert(a) == s,
415{
416    assert forall|aa| #![all_triggers] s.remove(a).insert(a).contains(aa) implies s.contains(
417        aa,
418    ) by {
419        if a == aa {
420        } else {
421            lemma_set_remove_different(s, aa, a);
422            lemma_set_insert_different(s.remove(a), aa, a);
423        }
424    };
425    assert forall|aa| #![all_triggers] s.contains(aa) implies s.remove(a).insert(a).contains(
426        aa,
427    ) by {
428        if a == aa {
429            lemma_set_insert_same(s.remove(a), a);
430        } else {
431            lemma_set_remove_different(s, aa, a);
432            lemma_set_insert_different(s.remove(a), aa, a);
433        }
434    };
435    axiom_set_ext_equal(s.remove(a).insert(a), s);
436}
437
438/// If `a1` does not equal `a2`, then the result of removing element `a2` from set `s`
439/// must contain `a1` if and only if the set contained `a1` before the removal of `a2`.
440pub broadcast proof fn lemma_set_remove_different<A>(s: Set<A>, a1: A, a2: A)
441    requires
442        a1 != a2,
443    ensures
444        #[trigger] s.remove(a2).contains(a1) == s.contains(a1),
445{
446    broadcast use axiom_set_ext_equal;
447    broadcast use Set::axiom_make_set;
448    broadcast use Set::axiom_is_finite;
449
450}
451
452/// The union of sets `s1` and `s2` contains element `a` if and only if
453/// `s1` contains `a` and/or `s2` contains `a`.
454pub broadcast proof fn lemma_set_union<A>(s1: Set<A>, s2: Set<A>, a: A)
455    ensures
456        #[trigger] s1.union(s2).contains(a) == (s1.contains(a) || s2.contains(a)),
457{
458    broadcast use axiom_set_ext_equal;
459    broadcast use Set::axiom_make_set;
460    broadcast use Set::axiom_is_finite;
461
462}
463
464/// The intersection of sets `s1` and `s2` contains element `a` if and only if
465/// both `s1` and `s2` contain `a`.
466pub broadcast proof fn lemma_set_intersect<A>(s1: Set<A>, s2: Set<A>, a: A)
467    ensures
468        #[trigger] s1.intersect(s2).contains(a) == (s1.contains(a) && s2.contains(a)),
469{
470    broadcast use axiom_set_ext_equal;
471    broadcast use Set::axiom_make_set;
472    broadcast use Set::axiom_is_finite;
473
474}
475
476/// The set difference between `s1` and `s2` contains element `a` if and only if
477/// `s1` contains `a` and `s2` does not contain `a`.
478pub broadcast proof fn lemma_set_difference<A>(s1: Set<A>, s2: Set<A>, a: A)
479    ensures
480        #[trigger] s1.difference(s2).contains(a) == (s1.contains(a) && !s2.contains(a)),
481{
482    broadcast use Set::axiom_make_set;
483    broadcast use Set::axiom_is_finite;
484
485}
486
487/// The complement of set `s` contains element `a` if and only if `s` does not contain `a`.
488pub broadcast proof fn lemma_set_complement<A>(s: Set<A>, a: A)
489    requires
490        ISet::new(|a| !s.contains(a)).finite(),
491    ensures
492        #[trigger] s.complement().unwrap().contains(a) == !s.contains(a),
493{
494    broadcast use Set::axiom_make_set;
495
496}
497
498/// The filter of set `s` using function `f` contains element `a` if and only if `s` contains `a`
499/// and `f(a)` is true.
500pub broadcast proof fn lemma_set_filter<A>(s: Set<A>, f: spec_fn(A) -> bool, a: A)
501    ensures
502        #[trigger] s.filter(f).contains(a) == (s.contains(a) && f(a)),
503{
504    broadcast use Set::axiom_make_set;
505    broadcast use Set::axiom_is_finite;
506
507}
508
509// Lemmas about len
510// The following, with lemma_set_ext_equal, are enough to build libraries about len.
511/// The empty set has length 0.
512pub broadcast proof fn lemma_set_empty_len<A>()
513    ensures
514        #[trigger] Set::<A>::empty().len() == 0,
515{
516    broadcast use Set::axiom_make_set;
517
518}
519
520/// The result of inserting an element `a` into a finite set `s` has length
521/// `s.len() + 1` if `a` is not already in `s` and length `s.len()` otherwise.
522pub broadcast proof fn lemma_set_insert_len<A>(s: Set<A>, a: A)
523    ensures
524        #[trigger] s.insert(a).len() == s.len() + (if s.contains(a) {
525            0int
526        } else {
527            1
528        }),
529{
530    broadcast use Set::axiom_make_set;
531    broadcast use Set::axiom_is_finite;
532
533}
534
535/// The result of removing an element `a` from a finite set `s` has length
536/// `s.len() - 1` if `a` is in `s` and length `s.len()` otherwise.
537pub broadcast proof fn lemma_set_remove_len<A>(s: Set<A>, a: A)
538    ensures
539        s.len() == #[trigger] s.remove(a).len() + (if s.contains(a) {
540            1int
541        } else {
542            0
543        }),
544{
545    broadcast use Set::axiom_make_set;
546    broadcast use Set::axiom_is_finite;
547
548}
549
550/// If a finite set `s` contains any element, it has length greater than 0.
551pub broadcast proof fn lemma_set_contains_len<A>(s: Set<A>, a: A)
552    requires
553        #[trigger] s.contains(a),
554    ensures
555        #[trigger] s.len() != 0,
556{
557    broadcast use Set::axiom_make_set;
558    broadcast use Set::axiom_is_finite;
559
560}
561
562/// A finite set `s` contains the element `s.choose()` if it has length greater than 0.
563pub broadcast proof fn lemma_set_choose_len<A>(s: Set<A>)
564    requires
565        #[trigger] s.len() != 0,
566    ensures
567        #[trigger] s.contains(s.choose()),
568{
569    assert(s.to_iset().contains(s.to_iset().choose()));
570}
571
572/// Converting a `Set` to an `ISet` produces a finite result.
573pub broadcast proof fn lemma_to_iset_finite<A>(s: Set<A>)
574    ensures
575        #[trigger] s.to_iset().finite(),
576{
577    broadcast use Set::axiom_make_set;
578    broadcast use Set::axiom_is_finite;
579
580}
581
582/// Converting a `Set` to an `ISet` produces a result with the same
583/// length.
584pub broadcast proof fn lemma_to_iset_len<A>(s: Set<A>)
585    ensures
586        #[trigger] s.to_iset().len() == s.len(),
587{
588    broadcast use Set::axiom_make_set;
589    broadcast use Set::axiom_is_finite;
590
591}
592
593pub broadcast group group_set_lemmas {
594    axiom_set_ext_equal,
595    axiom_set_ext_equal_deep,
596    lemma_set_empty,
597    lemma_set_new,
598    lemma_set_new_assuming_finite,
599    lemma_set_new_from_iset,
600    lemma_set_new_some,
601    lemma_set_insert_same,
602    lemma_set_insert_different,
603    lemma_set_remove_same,
604    lemma_set_remove_insert,
605    lemma_set_remove_different,
606    lemma_set_union,
607    lemma_set_intersect,
608    lemma_set_difference,
609    lemma_set_complement,
610    lemma_set_filter,
611    lemma_set_empty_len,
612    lemma_set_insert_len,
613    lemma_set_remove_len,
614    lemma_set_contains_len,
615    lemma_set_choose_len,
616    lemma_set_new,
617    lemma_to_iset_finite,
618    lemma_to_iset_len,
619}
620
621// Macros
622#[doc(hidden)]
623#[macro_export]
624macro_rules! set_internal {
625    [$($elem:expr),* $(,)?] => {
626        $crate::vstd::set::Set::empty()
627            $(.insert($elem))*
628    };
629}
630
631#[macro_export]
632macro_rules! set {
633    [$($tail:tt)*] => {
634        $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::set::set_internal!($($tail)*))
635    };
636}
637
638pub use set_internal;
639pub use set;
640
641} // verus!
vstd/set.rs

vstd/
set.rs
