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

vstd/
set.rs
