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    /// The "full" set, i.e., set containing every element of type `A`.
138    /// Note that if `A` is infinite, then this produces None.
139    #[rustc_diagnostic_item = "verus::vstd::set::Set::full"]
140    pub open spec fn full() -> Option<Set<A>> {
141        Set::new(|a: A| true)
142    }
143
144    /// Predicate indicating if the set contains the given element.
145    #[rustc_diagnostic_item = "verus::vstd::set::Set::contains"]
146    #[verifier::inline]
147    pub open spec fn contains(self, a: A) -> bool {
148        self.to_iset().contains(a)
149    }
150
151    /// Predicate indicating if the set contains the given element: supports `self has a` syntax.
152    #[verifier::inline]
153    pub open spec fn spec_has(self, a: A) -> bool {
154        self.contains(a)
155    }
156
157    /// Returns `true` if the first argument is a subset of the second.
158    #[rustc_diagnostic_item = "verus::vstd::set::Set::subset_of"]
159    pub open spec fn subset_of(self, s2: Set<A>) -> bool {
160        forall|a: A| self.contains(a) ==> s2.contains(a)
161    }
162
163    #[verifier::inline]
164    pub open spec fn spec_le(self, s2: Set<A>) -> bool {
165        self.subset_of(s2)
166    }
167
168    /// Returns a new set with the given element inserted.
169    /// If that element is already in the set, then an identical set is returned.
170    #[rustc_diagnostic_item = "verus::vstd::set::Set::insert"]
171    pub closed spec fn insert(self, a: A) -> Set<A> {
172        Self::make_set(self.to_iset().insert(a))
173    }
174
175    /// Returns a new set with the given element removed.
176    /// If that element is already absent from the set, then an identical set is returned.
177    #[rustc_diagnostic_item = "verus::vstd::set::Set::remove"]
178    pub closed spec fn remove(self, a: A) -> Set<A> {
179        Self::make_set(self.to_iset().remove(a))
180    }
181
182    /// Union of two sets.
183    pub closed spec fn union(self, s2: Set<A>) -> Set<A> {
184        Self::make_set(self.to_iset().union(s2.to_iset()))
185    }
186
187    /// `+` operator, synonymous with `union`
188    #[verifier::inline]
189    pub open spec fn spec_add(self, s2: Set<A>) -> Set<A> {
190        self.union(s2)
191    }
192
193    /// Intersection of two sets.
194    pub closed spec fn intersect(self, s2: Set<A>) -> Set<A> {
195        Self::make_set(self.to_iset().intersect(s2.to_iset()))
196    }
197
198    /// `*` operator, synonymous with `intersect`
199    #[verifier::inline]
200    pub open spec fn spec_mul(self, s2: Set<A>) -> Set<A> {
201        self.intersect(s2)
202    }
203
204    /// Set difference, i.e., the set of all elements in the first one but not in the second.
205    pub closed spec fn difference(self, s2: Set<A>) -> Set<A> {
206        Self::make_set(self.to_iset().difference(s2.to_iset()))
207    }
208
209    /// `-` operator, synonymous with `difference`
210    #[verifier::inline]
211    pub open spec fn spec_sub(self, s2: Set<A>) -> Set<A> {
212        self.difference(s2)
213    }
214
215    /// Set complement (within the space of all possible elements in `A`).
216    /// Returns None if this would be an infinite set.
217    pub open spec fn complement(self) -> Option<Set<A>> {
218        Set::new(|a| !self.contains(a))
219    }
220
221    /// Set of all elements in the given set which satisfy the predicate `f`.
222    pub closed spec fn filter(self, f: spec_fn(A) -> bool) -> Set<A> {
223        Self::make_set(self.to_iset().filter(f))
224    }
225
226    /// Returns `true` if the set is finite.
227    #[deprecated(note = "Every Set is always finite, so this is always true.")]
228    pub open spec fn finite(self) -> bool {
229        true
230    }
231
232    /// Returns `true` if this set is congruent to (contains the same elements as)
233    /// a given ISet.
234    pub open spec fn congruent(self, s2: ISet<A>) -> bool {
235        forall|a: A| #![all_triggers] self.contains(a) <==> s2.contains(a)
236    }
237
238    /// Cardinality of the set.
239    pub closed spec fn len(self) -> nat {
240        self.to_iset().len()
241    }
242
243    /// Chooses an arbitrary element of the set.
244    ///
245    /// This is often useful for proofs by induction.
246    ///
247    /// (Note that, although the result is arbitrary, it is still a _deterministic_ function
248    /// like any other `spec` function.)
249    pub open spec fn choose(self) -> A {
250        choose|a: A| self.contains(a)
251    }
252
253    /// Returns `true` if the sets are disjoint, i.e., if their interesection is
254    /// the empty set.
255    pub open spec fn disjoint(self, s2: Self) -> bool {
256        forall|a: A| self.contains(a) ==> !s2.contains(a)
257    }
258}
259
260/// Sets `s1` and `s2` are considered equal if and only if they contain all of the same elements.
261/// This has to be an axiom because `Set` is `external_body`.
262pub broadcast proof fn axiom_set_ext_equal<A>(s1: Set<A>, s2: Set<A>)
263    ensures
264        #[trigger] (s1 =~= s2) <==> (forall|a: A| s1.contains(a) == s2.contains(a)),
265{
266    admit();
267}
268
269/// Sets `s1` and `s2` are considered equal if and only if they contain all of the same elements.
270/// This has to be an axiom because `Set` is `external_body`.
271pub broadcast proof fn axiom_set_ext_equal_deep<A>(s1: Set<A>, s2: Set<A>)
272    ensures
273        #[trigger] (s1 =~~= s2) <==> s1 =~= s2,
274{
275    admit();
276}
277
278broadcast use super::iset::group_iset_lemmas;
279
280pub mod fold {
281    use super::*;
282
283    impl<A> Set<A> {
284        /// Folds the set, applying `f` to perform the fold. The next element for the fold is chosen by
285        /// the choose operator.
286        ///
287        /// Given a set `s = {x0, x1, x2, ..., xn}`, applying this function `s.fold(init, f)`
288        /// returns `f(...f(f(init, x0), x1), ..., xn)`.
289        #[verifier::inline]
290        pub open spec fn fold<B>(self, z: B, f: spec_fn(B, A) -> B) -> B
291            recommends
292                super::super::iset::fold::is_fun_commutative(f),
293        {
294            self.to_iset().fold(z, f)
295        }
296    }
297
298}
299
300/// The empty set contains no elements
301pub broadcast proof fn lemma_set_empty<A>(a: A)
302    ensures
303        !(#[trigger] Set::empty().contains(a)),
304{
305    broadcast use Set::axiom_make_set;
306
307}
308
309/// If `Set::<A>::new(f)` produces `Some(s)`, then `s` contains `a`
310/// if and only if `f(a)` is true.
311pub broadcast proof fn lemma_set_new<A>(f: spec_fn(A) -> bool, a: A)
312    requires
313        Set::<A>::new(f) is Some,
314    ensures
315        #[trigger] Set::<A>::new(f).unwrap().contains(a) == f(a),
316{
317    broadcast use Set::axiom_make_set;
318
319}
320
321/// If `ISet::<A>::new(f)` is finite, then `Set::<A>::new(f)`
322/// produces `Some(s)`. Useful for triggering the `lemma_set_new`
323/// to show that `s` contains `a` if and only if `f(a)` is true.
324pub broadcast proof fn lemma_set_new_some<A>(f: spec_fn(A) -> bool)
325    requires
326        ISet::<A>::new(f).finite(),
327    ensures
328        #[trigger] Set::<A>::new(f) is Some,
329{
330    broadcast use Set::axiom_make_set;
331
332}
333
334/// If an iset `s` is finite, then `Set::new_from_iset(s)` has the same
335/// contents as `s`.
336pub broadcast proof fn lemma_set_new_from_iset<A>(s: ISet<A>)
337    requires
338        s.finite(),
339    ensures
340        #![trigger Set::<A>::new_from_iset(s)]
341        Set::<A>::new_from_iset(s) is Some,
342        Set::<A>::new_from_iset(s).unwrap().to_iset() == s,
343{
344    broadcast use Set::axiom_make_set;
345
346    assert(ISet::new(|a: A| s.contains(a)) =~= s);
347}
348
349/// The result of inserting element `a` into set `s` must contains `a`.
350pub broadcast proof fn lemma_set_insert_same<A>(s: Set<A>, a: A)
351    ensures
352        #[trigger] s.insert(a).contains(a),
353{
354    broadcast use Set::axiom_make_set;
355    broadcast use Set::axiom_is_finite;
356
357}
358
359/// If `a1` does not equal `a2`, then the result of inserting element `a2` into set `s`
360/// must contain `a1` if and only if the set contained `a1` before the insertion of `a2`.
361pub broadcast proof fn lemma_set_insert_different<A>(s: Set<A>, a1: A, a2: A)
362    requires
363        a1 != a2,
364    ensures
365        #[trigger] s.insert(a2).contains(a1) == s.contains(a1),
366{
367    broadcast use Set::axiom_make_set;
368    broadcast use Set::axiom_is_finite;
369
370}
371
372/// The result of removing element `a` from set `s` must not contain `a`.
373pub broadcast proof fn lemma_set_remove_same<A>(s: Set<A>, a: A)
374    ensures
375        !(#[trigger] s.remove(a).contains(a)),
376{
377    broadcast use Set::axiom_make_set;
378    broadcast use Set::axiom_is_finite;
379
380}
381
382/// Removing an element `a` from a set `s` and then inserting `a` back into the set`
383/// is equivalent to the original set `s`.
384pub broadcast proof fn lemma_set_remove_insert<A>(s: Set<A>, a: A)
385    requires
386        s.contains(a),
387    ensures
388        (#[trigger] s.remove(a)).insert(a) == s,
389{
390    assert forall|aa| #![all_triggers] s.remove(a).insert(a).contains(aa) implies s.contains(
391        aa,
392    ) by {
393        if a == aa {
394        } else {
395            lemma_set_remove_different(s, aa, a);
396            lemma_set_insert_different(s.remove(a), aa, a);
397        }
398    };
399    assert forall|aa| #![all_triggers] s.contains(aa) implies s.remove(a).insert(a).contains(
400        aa,
401    ) by {
402        if a == aa {
403            lemma_set_insert_same(s.remove(a), a);
404        } else {
405            lemma_set_remove_different(s, aa, a);
406            lemma_set_insert_different(s.remove(a), aa, a);
407        }
408    };
409    axiom_set_ext_equal(s.remove(a).insert(a), s);
410}
411
412/// If `a1` does not equal `a2`, then the result of removing element `a2` from set `s`
413/// must contain `a1` if and only if the set contained `a1` before the removal of `a2`.
414pub broadcast proof fn lemma_set_remove_different<A>(s: Set<A>, a1: A, a2: A)
415    requires
416        a1 != a2,
417    ensures
418        #[trigger] s.remove(a2).contains(a1) == s.contains(a1),
419{
420    broadcast use axiom_set_ext_equal;
421    broadcast use Set::axiom_make_set;
422    broadcast use Set::axiom_is_finite;
423
424}
425
426/// The union of sets `s1` and `s2` contains element `a` if and only if
427/// `s1` contains `a` and/or `s2` contains `a`.
428pub broadcast proof fn lemma_set_union<A>(s1: Set<A>, s2: Set<A>, a: A)
429    ensures
430        #[trigger] s1.union(s2).contains(a) == (s1.contains(a) || s2.contains(a)),
431{
432    broadcast use axiom_set_ext_equal;
433    broadcast use Set::axiom_make_set;
434    broadcast use Set::axiom_is_finite;
435
436}
437
438/// The intersection of sets `s1` and `s2` contains element `a` if and only if
439/// both `s1` and `s2` contain `a`.
440pub broadcast proof fn lemma_set_intersect<A>(s1: Set<A>, s2: Set<A>, a: A)
441    ensures
442        #[trigger] s1.intersect(s2).contains(a) == (s1.contains(a) && s2.contains(a)),
443{
444    broadcast use axiom_set_ext_equal;
445    broadcast use Set::axiom_make_set;
446    broadcast use Set::axiom_is_finite;
447
448}
449
450/// The set difference between `s1` and `s2` contains element `a` if and only if
451/// `s1` contains `a` and `s2` does not contain `a`.
452pub broadcast proof fn lemma_set_difference<A>(s1: Set<A>, s2: Set<A>, a: A)
453    ensures
454        #[trigger] s1.difference(s2).contains(a) == (s1.contains(a) && !s2.contains(a)),
455{
456    broadcast use Set::axiom_make_set;
457    broadcast use Set::axiom_is_finite;
458
459}
460
461/// The complement of set `s` contains element `a` if and only if `s` does not contain `a`.
462pub broadcast proof fn lemma_set_complement<A>(s: Set<A>, a: A)
463    requires
464        ISet::new(|a| !s.contains(a)).finite(),
465    ensures
466        #[trigger] s.complement().unwrap().contains(a) == !s.contains(a),
467{
468    broadcast use Set::axiom_make_set;
469
470}
471
472/// The filter of set `s` using function `f` contains element `a` if and only if `s` contains `a`
473/// and `f(a)` is true.
474pub broadcast proof fn lemma_set_filter<A>(s: Set<A>, f: spec_fn(A) -> bool, a: A)
475    ensures
476        #[trigger] s.filter(f).contains(a) == (s.contains(a) && f(a)),
477{
478    broadcast use Set::axiom_make_set;
479    broadcast use Set::axiom_is_finite;
480
481}
482
483// Lemmas about len
484// The following, with lemma_set_ext_equal, are enough to build libraries about len.
485/// The empty set has length 0.
486pub broadcast proof fn lemma_set_empty_len<A>()
487    ensures
488        #[trigger] Set::<A>::empty().len() == 0,
489{
490    broadcast use Set::axiom_make_set;
491
492}
493
494/// The result of inserting an element `a` into a finite set `s` has length
495/// `s.len() + 1` if `a` is not already in `s` and length `s.len()` otherwise.
496pub broadcast proof fn lemma_set_insert_len<A>(s: Set<A>, a: A)
497    ensures
498        #[trigger] s.insert(a).len() == s.len() + (if s.contains(a) {
499            0int
500        } else {
501            1
502        }),
503{
504    broadcast use Set::axiom_make_set;
505    broadcast use Set::axiom_is_finite;
506
507}
508
509/// The result of removing an element `a` from a finite set `s` has length
510/// `s.len() - 1` if `a` is in `s` and length `s.len()` otherwise.
511pub broadcast proof fn lemma_set_remove_len<A>(s: Set<A>, a: A)
512    ensures
513        s.len() == #[trigger] s.remove(a).len() + (if s.contains(a) {
514            1int
515        } else {
516            0
517        }),
518{
519    broadcast use Set::axiom_make_set;
520    broadcast use Set::axiom_is_finite;
521
522}
523
524/// If a finite set `s` contains any element, it has length greater than 0.
525pub broadcast proof fn lemma_set_contains_len<A>(s: Set<A>, a: A)
526    requires
527        #[trigger] s.contains(a),
528    ensures
529        #[trigger] s.len() != 0,
530{
531    broadcast use Set::axiom_make_set;
532    broadcast use Set::axiom_is_finite;
533
534}
535
536/// A finite set `s` contains the element `s.choose()` if it has length greater than 0.
537pub broadcast proof fn lemma_set_choose_len<A>(s: Set<A>)
538    requires
539        #[trigger] s.len() != 0,
540    ensures
541        #[trigger] s.contains(s.choose()),
542{
543    assert(s.to_iset().contains(s.to_iset().choose()));
544}
545
546/// Converting a `Set` to an `ISet` produces a finite result.
547pub broadcast proof fn lemma_to_iset_finite<A>(s: Set<A>)
548    ensures
549        #[trigger] s.to_iset().finite(),
550{
551    broadcast use Set::axiom_make_set;
552    broadcast use Set::axiom_is_finite;
553
554}
555
556/// Converting a `Set` to an `ISet` produces a result with the same
557/// length.
558pub broadcast proof fn lemma_to_iset_len<A>(s: Set<A>)
559    ensures
560        #[trigger] s.to_iset().len() == s.len(),
561{
562    broadcast use Set::axiom_make_set;
563    broadcast use Set::axiom_is_finite;
564
565}
566
567pub broadcast group group_set_lemmas {
568    axiom_set_ext_equal,
569    axiom_set_ext_equal_deep,
570    lemma_set_empty,
571    lemma_set_new,
572    lemma_set_new_from_iset,
573    lemma_set_new_some,
574    lemma_set_insert_same,
575    lemma_set_insert_different,
576    lemma_set_remove_same,
577    lemma_set_remove_insert,
578    lemma_set_remove_different,
579    lemma_set_union,
580    lemma_set_intersect,
581    lemma_set_difference,
582    lemma_set_complement,
583    lemma_set_filter,
584    lemma_set_empty_len,
585    lemma_set_insert_len,
586    lemma_set_remove_len,
587    lemma_set_contains_len,
588    lemma_set_choose_len,
589    lemma_set_new,
590    lemma_to_iset_finite,
591    lemma_to_iset_len,
592}
593
594// Macros
595#[doc(hidden)]
596#[macro_export]
597macro_rules! set_internal {
598    [$($elem:expr),* $(,)?] => {
599        $crate::vstd::set::Set::empty()
600            $(.insert($elem))*
601    };
602}
603
604#[macro_export]
605macro_rules! set {
606    [$($tail:tt)*] => {
607        $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::set::set_internal!($($tail)*))
608    };
609}
610
611pub use set_internal;
612pub use set;
613
614} // verus!
vstd/set.rs

vstd/
set.rs
