vstd/
set_lib.rs

1#[allow(unused_imports)]
2use super::multiset::Multiset;
3#[allow(unused_imports)]
4use super::pervasive::*;
5use super::prelude::Seq;
6#[allow(unused_imports)]
7use super::prelude::*;
8#[allow(unused_imports)]
9use super::relations::*;
10#[allow(unused_imports)]
11use super::set::*;
12
13verus! {
14
15broadcast use super::set::group_set_axioms;
16
17impl<A> Set<A> {
18    /// Is `true` if called by a "full" set, i.e., a set containing every element of type `A`.
19    pub open spec fn is_full(self) -> bool {
20        self == Set::<A>::full()
21    }
22
23    /// Is `true` if called by an "empty" set, i.e., a set containing no elements and has length 0
24    pub open spec fn is_empty(self) -> (b: bool) {
25        self =~= Set::<A>::empty()
26    }
27
28    /// Returns the set contains an element `f(x)` for every element `x` in `self`.
29    pub open spec fn map<B>(self, f: spec_fn(A) -> B) -> Set<B> {
30        Set::new(|a: B| exists|x: A| self.contains(x) && a == f(x))
31    }
32
33    /// Converts a set into a sequence with an arbitrary ordering.
34    pub open spec fn to_seq(self) -> Seq<A>
35        recommends
36            self.finite(),
37        decreases self.len(),
38        when self.finite()
39    {
40        if self.len() == 0 {
41            Seq::<A>::empty()
42        } else {
43            let x = self.choose();
44            Seq::<A>::empty().push(x) + self.remove(x).to_seq()
45        }
46    }
47
48    /// Converts a set into a sequence sorted by the given ordering function `leq`
49    pub open spec fn to_sorted_seq(self, leq: spec_fn(A, A) -> bool) -> Seq<A> {
50        self.to_seq().sort_by(leq)
51    }
52
53    /// A singleton set has at least one element and any two elements are equal.
54    pub open spec fn is_singleton(self) -> bool {
55        &&& self.len() > 0
56        &&& (forall|x: A, y: A| self.contains(x) && self.contains(y) ==> x == y)
57    }
58
59    /// Any totally-ordered set contains a unique minimal (equivalently, least) element.
60    /// Returns an arbitrary value if r is not a total ordering
61    pub closed spec fn find_unique_minimal(self, r: spec_fn(A, A) -> bool) -> A
62        recommends
63            total_ordering(r),
64            self.len() > 0,
65            self.finite(),
66        decreases self.len(),
67        when self.finite()
68    {
69        proof {
70            broadcast use group_set_properties;
71
72        }
73        if self.len() <= 1 {
74            self.choose()
75        } else {
76            let x = choose|x: A| self.contains(x);
77            let min = self.remove(x).find_unique_minimal(r);
78            if r(min, x) {
79                min
80            } else {
81                x
82            }
83        }
84    }
85
86    /// Proof of correctness and expected behavior for `Set::find_unique_minimal`.
87    pub proof fn find_unique_minimal_ensures(self, r: spec_fn(A, A) -> bool)
88        requires
89            self.finite(),
90            self.len() > 0,
91            total_ordering(r),
92        ensures
93            is_minimal(r, self.find_unique_minimal(r), self) && (forall|min: A|
94                is_minimal(r, min, self) ==> self.find_unique_minimal(r) == min),
95        decreases self.len(),
96    {
97        broadcast use group_set_properties;
98
99        if self.len() == 1 {
100            let x = choose|x: A| self.contains(x);
101            assert(self.remove(x).insert(x) =~= self);
102            assert(is_minimal(r, self.find_unique_minimal(r), self));
103        } else {
104            let x = choose|x: A| self.contains(x);
105            self.remove(x).find_unique_minimal_ensures(r);
106            assert(is_minimal(r, self.remove(x).find_unique_minimal(r), self.remove(x)));
107            let y = self.remove(x).find_unique_minimal(r);
108            let min_updated = self.find_unique_minimal(r);
109            assert(!r(y, x) ==> min_updated == x);
110            assert(forall|elt: A|
111                self.remove(x).contains(elt) && #[trigger] r(elt, y) ==> #[trigger] r(y, elt));
112            assert forall|elt: A|
113                self.contains(elt) && #[trigger] r(elt, min_updated) implies #[trigger] r(
114                min_updated,
115                elt,
116            ) by {
117                assert(r(min_updated, x) || r(min_updated, y));
118                if min_updated == y {  // Case where the new min is the old min
119                    assert(is_minimal(r, self.find_unique_minimal(r), self));
120                } else {  //Case where the new min is the newest element
121                    assert(self.remove(x).contains(elt) || elt == x);
122                    assert(min_updated == x);
123                    assert(r(x, y) || r(y, x));
124                    assert(!r(x, y) || !r(y, x));
125                    assert(!(min_updated == y) ==> !r(y, x));
126                    assert(r(x, y));
127                    if (self.remove(x).contains(elt)) {
128                        assert(r(elt, y) && r(y, elt) ==> elt == y);
129                    } else {
130                    }
131                }
132            }
133            assert forall|min_poss: A|
134                is_minimal(r, min_poss, self) implies self.find_unique_minimal(r) == min_poss by {
135                assert(is_minimal(r, min_poss, self.remove(x)) || x == min_poss);
136                assert(r(min_poss, self.find_unique_minimal(r)));
137            }
138        }
139    }
140
141    /// Any totally-ordered set contains a unique maximal (equivalently, greatest) element.
142    /// Returns an arbitrary value if r is not a total ordering
143    pub closed spec fn find_unique_maximal(self, r: spec_fn(A, A) -> bool) -> A
144        recommends
145            total_ordering(r),
146            self.len() > 0,
147        decreases self.len(),
148        when self.finite()
149    {
150        proof {
151            broadcast use group_set_properties;
152
153        }
154        if self.len() <= 1 {
155            self.choose()
156        } else {
157            let x = choose|x: A| self.contains(x);
158            let max = self.remove(x).find_unique_maximal(r);
159            if r(x, max) {
160                max
161            } else {
162                x
163            }
164        }
165    }
166
167    /// Proof of correctness and expected behavior for `Set::find_unique_maximal`.
168    pub proof fn find_unique_maximal_ensures(self, r: spec_fn(A, A) -> bool)
169        requires
170            self.finite(),
171            self.len() > 0,
172            total_ordering(r),
173        ensures
174            is_maximal(r, self.find_unique_maximal(r), self) && (forall|max: A|
175                is_maximal(r, max, self) ==> self.find_unique_maximal(r) == max),
176        decreases self.len(),
177    {
178        broadcast use group_set_properties;
179
180        if self.len() == 1 {
181            let x = choose|x: A| self.contains(x);
182            assert(self.remove(x) =~= Set::<A>::empty());
183            assert(self.contains(self.find_unique_maximal(r)));
184        } else {
185            let x = choose|x: A| self.contains(x);
186            self.remove(x).find_unique_maximal_ensures(r);
187            assert(is_maximal(r, self.remove(x).find_unique_maximal(r), self.remove(x)));
188            assert(self.remove(x).insert(x) =~= self);
189            let y = self.remove(x).find_unique_maximal(r);
190            let max_updated = self.find_unique_maximal(r);
191            assert(max_updated == x || max_updated == y);
192            assert(!r(x, y) ==> max_updated == x);
193            assert forall|elt: A|
194                self.contains(elt) && #[trigger] r(max_updated, elt) implies #[trigger] r(
195                elt,
196                max_updated,
197            ) by {
198                assert(r(x, max_updated) || r(y, max_updated));
199                if max_updated == y {  // Case where the new max is the old max
200                    assert(r(elt, max_updated));
201                    assert(r(x, max_updated));
202                    assert(is_maximal(r, self.find_unique_maximal(r), self));
203                } else {  //Case where the new max is the newest element
204                    assert(self.remove(x).contains(elt) || elt == x);
205                    assert(max_updated == x);
206                    assert(r(x, y) || r(y, x));
207                    assert(!r(x, y) || !r(y, x));
208                    assert(!(max_updated == y) ==> !r(x, y));
209                    assert(r(y, x));
210                    if (self.remove(x).contains(elt)) {
211                        assert(r(y, elt) ==> r(elt, y));
212                        assert(r(y, elt) && r(elt, y) ==> elt == y);
213                        assert(r(elt, x));
214                        assert(r(elt, max_updated))
215                    } else {
216                    }
217                }
218            }
219            assert forall|max_poss: A|
220                is_maximal(r, max_poss, self) implies self.find_unique_maximal(r) == max_poss by {
221                assert(is_maximal(r, max_poss, self.remove(x)) || x == max_poss);
222                assert(r(max_poss, self.find_unique_maximal(r)));
223                assert(r(self.find_unique_maximal(r), max_poss));
224            }
225        }
226    }
227
228    /// Converts a set into a multiset where each element from the set has
229    /// multiplicity 1 and any other element has multiplicity 0.
230    pub open spec fn to_multiset(self) -> Multiset<A>
231        decreases self.len(),
232        when self.finite()
233    {
234        if self.len() == 0 {
235            Multiset::<A>::empty()
236        } else {
237            Multiset::<A>::empty().insert(self.choose()).add(
238                self.remove(self.choose()).to_multiset(),
239            )
240        }
241    }
242
243    /// A finite set with length 0 is equivalent to the empty set.
244    pub proof fn lemma_len0_is_empty(self)
245        requires
246            self.finite(),
247            self.len() == 0,
248        ensures
249            self == Set::<A>::empty(),
250    {
251        if exists|a: A| self.contains(a) {
252            // derive contradiction:
253            assert(self.remove(self.choose()).len() + 1 == 0);
254        }
255        assert(self =~= Set::empty());
256    }
257
258    /// A singleton set has length 1.
259    pub proof fn lemma_singleton_size(self)
260        requires
261            self.is_singleton(),
262        ensures
263            self.len() == 1,
264    {
265        broadcast use group_set_properties;
266
267        assert(self.remove(self.choose()) =~= Set::empty());
268    }
269
270    /// A set has exactly one element, if and only if, it has at least one element and any two elements are equal.
271    pub proof fn lemma_is_singleton(s: Set<A>)
272        requires
273            s.finite(),
274        ensures
275            s.is_singleton() == (s.len() == 1),
276    {
277        if s.is_singleton() {
278            s.lemma_singleton_size();
279        }
280        if s.len() == 1 {
281            assert forall|x: A, y: A| s.contains(x) && s.contains(y) implies x == y by {
282                let x = choose|x: A| s.contains(x);
283                broadcast use group_set_properties;
284
285                assert(s.remove(x).len() == 0);
286                assert(s.insert(x) =~= s);
287            }
288        }
289    }
290
291    /// The result of filtering a finite set is finite and has size less than or equal to the original set.
292    pub proof fn lemma_len_filter(self, f: spec_fn(A) -> bool)
293        requires
294            self.finite(),
295        ensures
296            self.filter(f).finite(),
297            self.filter(f).len() <= self.len(),
298        decreases self.len(),
299    {
300        lemma_len_intersect::<A>(self, Set::new(f));
301    }
302
303    /// In a pre-ordered set, a greatest element is necessarily maximal.
304    pub proof fn lemma_greatest_implies_maximal(self, r: spec_fn(A, A) -> bool, max: A)
305        requires
306            pre_ordering(r),
307        ensures
308            is_greatest(r, max, self) ==> is_maximal(r, max, self),
309    {
310    }
311
312    /// In a pre-ordered set, a least element is necessarily minimal.
313    pub proof fn lemma_least_implies_minimal(self, r: spec_fn(A, A) -> bool, min: A)
314        requires
315            pre_ordering(r),
316        ensures
317            is_least(r, min, self) ==> is_minimal(r, min, self),
318    {
319    }
320
321    /// In a totally-ordered set, an element is maximal if and only if it is a greatest element.
322    pub proof fn lemma_maximal_equivalent_greatest(self, r: spec_fn(A, A) -> bool, max: A)
323        requires
324            total_ordering(r),
325        ensures
326            is_greatest(r, max, self) <==> is_maximal(r, max, self),
327    {
328        assert(is_maximal(r, max, self) ==> forall|x: A|
329            !self.contains(x) || !r(max, x) || r(x, max));
330    }
331
332    /// In a totally-ordered set, an element is maximal if and only if it is a greatest element.
333    pub proof fn lemma_minimal_equivalent_least(self, r: spec_fn(A, A) -> bool, min: A)
334        requires
335            total_ordering(r),
336        ensures
337            is_least(r, min, self) <==> is_minimal(r, min, self),
338    {
339        assert(is_minimal(r, min, self) ==> forall|x: A|
340            !self.contains(x) || !r(x, min) || r(min, x));
341    }
342
343    /// In a partially-ordered set, there exists at most one least element.
344    pub proof fn lemma_least_is_unique(self, r: spec_fn(A, A) -> bool)
345        requires
346            partial_ordering(r),
347        ensures
348            forall|min: A, min_prime: A|
349                is_least(r, min, self) && is_least(r, min_prime, self) ==> min == min_prime,
350    {
351        assert forall|min: A, min_prime: A|
352            is_least(r, min, self) && is_least(r, min_prime, self) implies min == min_prime by {
353            assert(r(min, min_prime));
354            assert(r(min_prime, min));
355        }
356    }
357
358    /// In a partially-ordered set, there exists at most one greatest element.
359    pub proof fn lemma_greatest_is_unique(self, r: spec_fn(A, A) -> bool)
360        requires
361            partial_ordering(r),
362        ensures
363            forall|max: A, max_prime: A|
364                is_greatest(r, max, self) && is_greatest(r, max_prime, self) ==> max == max_prime,
365    {
366        assert forall|max: A, max_prime: A|
367            is_greatest(r, max, self) && is_greatest(r, max_prime, self) implies max
368            == max_prime by {
369            assert(r(max_prime, max));
370            assert(r(max, max_prime));
371        }
372    }
373
374    /// In a totally-ordered set, there exists at most one minimal element.
375    pub proof fn lemma_minimal_is_unique(self, r: spec_fn(A, A) -> bool)
376        requires
377            total_ordering(r),
378        ensures
379            forall|min: A, min_prime: A|
380                is_minimal(r, min, self) && is_minimal(r, min_prime, self) ==> min == min_prime,
381    {
382        assert forall|min: A, min_prime: A|
383            is_minimal(r, min, self) && is_minimal(r, min_prime, self) implies min == min_prime by {
384            self.lemma_minimal_equivalent_least(r, min);
385            self.lemma_minimal_equivalent_least(r, min_prime);
386            self.lemma_least_is_unique(r);
387        }
388    }
389
390    /// In a totally-ordered set, there exists at most one maximal element.
391    pub proof fn lemma_maximal_is_unique(self, r: spec_fn(A, A) -> bool)
392        requires
393            self.finite(),
394            total_ordering(r),
395        ensures
396            forall|max: A, max_prime: A|
397                is_maximal(r, max, self) && is_maximal(r, max_prime, self) ==> max == max_prime,
398    {
399        assert forall|max: A, max_prime: A|
400            is_maximal(r, max, self) && is_maximal(r, max_prime, self) implies max == max_prime by {
401            self.lemma_maximal_equivalent_greatest(r, max);
402            self.lemma_maximal_equivalent_greatest(r, max_prime);
403            self.lemma_greatest_is_unique(r);
404        }
405    }
406
407    /// Set difference with an additional element inserted decreases the size of
408    /// the result. This can be useful for proving termination when traversing
409    /// a set while tracking the elements that have already been handled.
410    pub broadcast proof fn lemma_set_insert_diff_decreases(self, s: Set<A>, elt: A)
411        requires
412            self.contains(elt),
413            !s.contains(elt),
414            self.finite(),
415        ensures
416            #[trigger] self.difference(s.insert(elt)).len() < self.difference(s).len(),
417    {
418        self.difference(s.insert(elt)).lemma_subset_not_in_lt(self.difference(s), elt);
419    }
420
421    /// If there is an element not present in a subset, its length is stricly smaller.
422    pub proof fn lemma_subset_not_in_lt(self: Set<A>, s2: Set<A>, elt: A)
423        requires
424            self.subset_of(s2),
425            s2.finite(),
426            !self.contains(elt),
427            s2.contains(elt),
428        ensures
429            self.len() < s2.len(),
430    {
431        let s2_no_elt = s2.remove(elt);
432        assert(self.len() <= s2_no_elt.len()) by {
433            lemma_len_subset(self, s2_no_elt);
434        }
435    }
436
437    /// Inserting an element and mapping a function over a set commute
438    pub broadcast proof fn lemma_set_map_insert_commute<B>(self, elt: A, f: spec_fn(A) -> B)
439        ensures
440            #[trigger] self.insert(elt).map(f) =~= self.map(f).insert(f(elt)),
441    {
442        assert forall|x: B| self.map(f).insert(f(elt)).contains(x) implies self.insert(elt).map(
443            f,
444        ).contains(x) by {
445            if x == f(elt) {
446                assert(self.insert(elt).contains(elt));
447            } else {
448                let y = choose|y: A| self.contains(y) && f(y) == x;
449                assert(self.insert(elt).contains(y));
450            }
451        }
452    }
453
454    /// `map` and `union` commute
455    pub proof fn lemma_map_union_commute<B>(self, t: Set<A>, f: spec_fn(A) -> B)
456        ensures
457            (self.union(t)).map(f) =~= self.map(f).union(t.map(f)),
458    {
459        broadcast use group_set_axioms;
460
461        let lhs = self.union(t).map(f);
462        let rhs = self.map(f).union(t.map(f));
463
464        assert forall|elem: B| rhs.contains(elem) implies lhs.contains(elem) by {
465            if self.map(f).contains(elem) {
466                let preimage = choose|preimage: A| self.contains(preimage) && f(preimage) == elem;
467                assert(self.union(t).contains(preimage));
468            } else {
469                assert(t.map(f).contains(elem));
470                let preimage = choose|preimage: A| t.contains(preimage) && f(preimage) == elem;
471                assert(self.union(t).contains(preimage));
472            }
473        }
474    }
475
476    /// Utility function for more concise universal quantification over sets
477    pub open spec fn all(&self, pred: spec_fn(A) -> bool) -> bool {
478        forall|x: A| self.contains(x) ==> pred(x)
479    }
480
481    /// Utility function for more concise existential quantification over sets
482    pub open spec fn any(&self, pred: spec_fn(A) -> bool) -> bool {
483        exists|x: A| self.contains(x) && pred(x)
484    }
485
486    /// `any` is preserved between predicates `p` and `q` if `p` implies `q`.
487    pub broadcast proof fn lemma_any_map_preserved_pred<B>(
488        self,
489        p: spec_fn(A) -> bool,
490        q: spec_fn(B) -> bool,
491        f: spec_fn(A) -> B,
492    )
493        requires
494            #[trigger] self.any(p),
495            forall|x: A| #[trigger] p(x) ==> q(f(x)),
496        ensures
497            #[trigger] self.map(f).any(q),
498    {
499        let x = choose|x: A| self.contains(x) && p(x);
500        assert(self.map(f).contains(f(x)));
501    }
502
503    /// Collecting all elements `b` where `f` returns `Some(b)`
504    pub open spec fn filter_map<B>(self, f: spec_fn(A) -> Option<B>) -> Set<B> {
505        self.map(
506            |elem: A|
507                match f(elem) {
508                    Option::Some(r) => set!{r},
509                    Option::None => set!{},
510                },
511        ).flatten()
512    }
513
514    /// Inserting commutes with `filter_map`
515    pub broadcast proof fn lemma_filter_map_insert<B>(
516        s: Set<A>,
517        f: spec_fn(A) -> Option<B>,
518        elem: A,
519    )
520        ensures
521            #[trigger] s.insert(elem).filter_map(f) == (match f(elem) {
522                Some(res) => s.filter_map(f).insert(res),
523                None => s.filter_map(f),
524            }),
525    {
526        broadcast use group_set_axioms;
527        broadcast use Set::lemma_set_map_insert_commute;
528
529        let lhs = s.insert(elem).filter_map(f);
530        let rhs = match f(elem) {
531            Some(res) => s.filter_map(f).insert(res),
532            None => s.filter_map(f),
533        };
534        let to_set = |elem: A|
535            match f(elem) {
536                Option::Some(r) => set!{r},
537                Option::None => set!{},
538            };
539        assert forall|r: B| #[trigger] lhs.contains(r) implies rhs.contains(r) by {
540            if f(elem) != Some(r) {
541                let orig = choose|orig: A| #[trigger]
542                    s.contains(orig) && f(orig) == Option::Some(r);
543                assert(to_set(orig) == set!{r});
544                assert(s.map(to_set).contains(to_set(orig)));
545            }
546        }
547        assert forall|r: B| #[trigger] rhs.contains(r) implies lhs.contains(r) by {
548            if Some(r) == f(elem) {
549                assert(s.insert(elem).map(to_set).contains(to_set(elem)));
550            } else {
551                let orig = choose|orig: A| #[trigger]
552                    s.contains(orig) && f(orig) == Option::Some(r);
553                assert(s.insert(elem).map(to_set).contains(to_set(orig)));
554            }
555        }
556        assert(lhs =~= rhs);
557    }
558
559    /// `filter_map` and `union` commute.
560    pub broadcast proof fn lemma_filter_map_union<B>(self, f: spec_fn(A) -> Option<B>, t: Set<A>)
561        ensures
562            #[trigger] self.union(t).filter_map(f) == self.filter_map(f).union(t.filter_map(f)),
563    {
564        broadcast use group_set_axioms;
565
566        let lhs = self.union(t).filter_map(f);
567        let rhs = self.filter_map(f).union(t.filter_map(f));
568        let to_set = |elem: A|
569            match f(elem) {
570                Option::Some(r) => set!{r},
571                Option::None => set!{},
572            };
573
574        assert forall|elem: B| rhs.contains(elem) implies lhs.contains(elem) by {
575            if self.filter_map(f).contains(elem) {
576                let x = choose|x: A| self.contains(x) && f(x) == Option::Some(elem);
577                assert(self.union(t).contains(x));
578                assert(self.union(t).map(to_set).contains(to_set(x)));
579            }
580            if t.filter_map(f).contains(elem) {
581                let x = choose|x: A| t.contains(x) && f(x) == Option::Some(elem);
582                assert(self.union(t).contains(x));
583                assert(self.union(t).map(to_set).contains(to_set(x)));
584            }
585        }
586        assert forall|elem: B| lhs.contains(elem) implies rhs.contains(elem) by {
587            let x = choose|x: A| self.union(t).contains(x) && f(x) == Option::Some(elem);
588            if self.contains(x) {
589                assert(self.map(to_set).contains(to_set(x)));
590                assert(self.filter_map(f).contains(elem));
591            } else {
592                assert(t.contains(x));
593                assert(t.map(to_set).contains(to_set(x)));
594                assert(t.filter_map(f).contains(elem));
595            }
596        }
597        assert(lhs =~= rhs);
598    }
599
600    /// `map` preserves finiteness
601    pub proof fn lemma_map_finite<B>(self, f: spec_fn(A) -> B)
602        requires
603            self.finite(),
604        ensures
605            self.map(f).finite(),
606        decreases self.len(),
607    {
608        broadcast use group_set_axioms;
609        broadcast use lemma_set_empty_equivalency_len;
610
611        if self.len() == 0 {
612            assert(forall|elem: A| !(#[trigger] self.contains(elem)));
613            assert forall|res: B| #[trigger] self.map(f).contains(res) implies false by {
614                let x = choose|x: A| self.contains(x) && f(x) == res;
615            }
616            assert(self.map(f) =~= Set::<B>::empty());
617        } else {
618            let x = choose|x: A| self.contains(x);
619            assert(self.map(f).contains(f(x)));
620            self.remove(x).lemma_map_finite(f);
621            assert(self.remove(x).insert(x) == self);
622            assert(self.map(f) == self.remove(x).map(f).insert(f(x)));
623        }
624    }
625
626    pub broadcast proof fn lemma_set_all_subset(self, s2: Set<A>, p: spec_fn(A) -> bool)
627        requires
628            #[trigger] self.subset_of(s2),
629            s2.all(p),
630        ensures
631            #[trigger] self.all(p),
632    {
633        broadcast use group_set_axioms;
634
635    }
636
637    /// `filter_map` preserves finiteness.
638    pub broadcast proof fn lemma_filter_map_finite<B>(self, f: spec_fn(A) -> Option<B>)
639        requires
640            self.finite(),
641        ensures
642            #[trigger] self.filter_map(f).finite(),
643        decreases self.len(),
644    {
645        broadcast use group_set_axioms;
646        broadcast use Set::lemma_filter_map_insert;
647
648        let mapped = self.filter_map(f);
649        if self.len() == 0 {
650            assert(self.filter_map(f) =~= Set::<B>::empty());
651        } else {
652            let elem = self.choose();
653            self.remove(elem).lemma_filter_map_finite(f);
654            assert(self =~= self.remove(elem).insert(elem));
655        }
656    }
657
658    /// Conversion to a sequence and back to a set is the identity function.
659    pub broadcast proof fn lemma_to_seq_to_set_id(self)
660        requires
661            self.finite(),
662        ensures
663            #[trigger] self.to_seq().to_set() =~= self,
664        decreases self.len(),
665    {
666        broadcast use group_set_axioms;
667        broadcast use lemma_set_empty_equivalency_len;
668        broadcast use super::seq_lib::group_seq_properties;
669
670        if self.len() == 0 {
671            assert(self.to_seq().to_set() =~= Set::<A>::empty());
672        } else {
673            let elem = self.choose();
674            self.remove(elem).lemma_to_seq_to_set_id();
675            assert(self =~= self.remove(elem).insert(elem));
676            assert(self.to_seq().to_set() =~= self.remove(elem).to_seq().to_set().insert(elem));
677        }
678    }
679}
680
681impl<A> Set<Set<A>> {
682    pub open spec fn flatten(self) -> Set<A> {
683        Set::new(
684            |elem| exists|elem_s: Set<A>| #[trigger] self.contains(elem_s) && elem_s.contains(elem),
685        )
686    }
687
688    pub broadcast proof fn flatten_insert_union_commute(self, other: Set<A>)
689        ensures
690            self.flatten().union(other) =~= #[trigger] self.insert(other).flatten(),
691    {
692        broadcast use group_set_axioms;
693
694        let lhs = self.flatten().union(other);
695        let rhs = self.insert(other).flatten();
696
697        assert forall|elem: A| lhs.contains(elem) implies rhs.contains(elem) by {
698            if exists|s: Set<A>| self.contains(s) && s.contains(elem) {
699                let s = choose|s: Set<A>| self.contains(s) && s.contains(elem);
700                assert(self.insert(other).contains(s));
701                assert(s.contains(elem));
702            } else {
703                assert(self.insert(other).contains(other));
704            }
705        }
706    }
707}
708
709/// Two sets are equal iff mapping `f` results in equal sets, if `f` is injective.
710pub proof fn lemma_sets_eq_iff_injective_map_eq<T, S>(s1: Set<T>, s2: Set<T>, f: spec_fn(T) -> S)
711    requires
712        super::relations::injective(f),
713    ensures
714        (s1 == s2) <==> (s1.map(f) == s2.map(f)),
715{
716    broadcast use group_set_axioms;
717
718    if (s1.map(f) == s2.map(f)) {
719        assert(s1.map(f).len() == s2.map(f).len());
720        if !s1.subset_of(s2) {
721            let x = choose|x: T| s1.contains(x) && !s2.contains(x);
722            assert(s1.map(f).contains(f(x)));
723        } else if !s2.subset_of(s1) {
724            let x = choose|x: T| s2.contains(x) && !s1.contains(x);
725            assert(s2.map(f).contains(f(x)));
726        }
727        assert(s1 =~= s2);
728    }
729}
730
731/// The result of inserting an element `a` into a set `s` is finite iff `s` is finite.
732pub broadcast proof fn lemma_set_insert_finite_iff<A>(s: Set<A>, a: A)
733    ensures
734        #[trigger] s.insert(a).finite() <==> s.finite(),
735{
736    if s.insert(a).finite() {
737        if s.contains(a) {
738            assert(s == s.insert(a));
739        } else {
740            assert(s == s.insert(a).remove(a));
741        }
742    }
743    assert(s.insert(a).finite() ==> s.finite());
744}
745
746/// The result of removing an element `a` into a set `s` is finite iff `s` is finite.
747pub broadcast proof fn lemma_set_remove_finite_iff<A>(s: Set<A>, a: A)
748    ensures
749        #[trigger] s.remove(a).finite() <==> s.finite(),
750{
751    if s.remove(a).finite() {
752        if s.contains(a) {
753            assert(s == s.remove(a).insert(a));
754        } else {
755            assert(s == s.remove(a));
756        }
757    }
758}
759
760/// The union of two sets is finite iff both sets are finite.
761pub broadcast proof fn lemma_set_union_finite_iff<A>(s1: Set<A>, s2: Set<A>)
762    ensures
763        #[trigger] s1.union(s2).finite() <==> s1.finite() && s2.finite(),
764{
765    if s1.union(s2).finite() {
766        lemma_set_union_finite_implies_sets_finite(s1, s2);
767    }
768}
769
770pub proof fn lemma_set_union_finite_implies_sets_finite<A>(s1: Set<A>, s2: Set<A>)
771    requires
772        s1.union(s2).finite(),
773    ensures
774        s1.finite(),
775        s2.finite(),
776    decreases s1.union(s2).len(),
777{
778    if s1.union(s2) =~= set![] {
779        assert(s1 =~= set![]);
780        assert(s2 =~= set![]);
781    } else {
782        let a = s1.union(s2).choose();
783        assert(s1.remove(a).union(s2.remove(a)) == s1.union(s2).remove(a));
784        axiom_set_remove_len(s1.union(s2), a);
785        lemma_set_union_finite_implies_sets_finite(s1.remove(a), s2.remove(a));
786        assert(forall|s: Set<A>|
787            #![auto]
788            s.remove(a).insert(a) == if s.contains(a) {
789                s
790            } else {
791                s.insert(a)
792            });
793        lemma_set_insert_finite_iff(s1, a);
794        lemma_set_insert_finite_iff(s2, a);
795    }
796}
797
798/// The size of a union of two sets is less than or equal to the size of
799/// both individual sets combined.
800pub proof fn lemma_len_union<A>(s1: Set<A>, s2: Set<A>)
801    requires
802        s1.finite(),
803        s2.finite(),
804    ensures
805        s1.union(s2).len() <= s1.len() + s2.len(),
806    decreases s1.len(),
807{
808    if s1.is_empty() {
809        assert(s1.union(s2) =~= s2);
810    } else {
811        let a = s1.choose();
812        if s2.contains(a) {
813            assert(s1.union(s2) =~= s1.remove(a).union(s2));
814        } else {
815            assert(s1.union(s2).remove(a) =~= s1.remove(a).union(s2));
816        }
817        lemma_len_union::<A>(s1.remove(a), s2);
818    }
819}
820
821/// The size of a union of two sets is greater than or equal to the size of
822/// both individual sets.
823pub proof fn lemma_len_union_ind<A>(s1: Set<A>, s2: Set<A>)
824    requires
825        s1.finite(),
826        s2.finite(),
827    ensures
828        s1.union(s2).len() >= s1.len(),
829        s1.union(s2).len() >= s2.len(),
830    decreases s2.len(),
831{
832    broadcast use group_set_properties;
833
834    if s2.len() == 0 {
835    } else {
836        let y = choose|y: A| s2.contains(y);
837        if s1.contains(y) {
838            assert(s1.remove(y).union(s2.remove(y)) =~= s1.union(s2).remove(y));
839            lemma_len_union_ind(s1.remove(y), s2.remove(y))
840        } else {
841            assert(s1.union(s2.remove(y)) =~= s1.union(s2).remove(y));
842            lemma_len_union_ind(s1, s2.remove(y))
843        }
844    }
845}
846
847/// The size of the intersection of finite set `s1` and set `s2` is less than or equal to the size of `s1`.
848pub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>)
849    requires
850        s1.finite(),
851    ensures
852        s1.intersect(s2).len() <= s1.len(),
853    decreases s1.len(),
854{
855    if s1.is_empty() {
856        assert(s1.intersect(s2) =~= s1);
857    } else {
858        let a = s1.choose();
859        assert(s1.intersect(s2).remove(a) =~= s1.remove(a).intersect(s2));
860        lemma_len_intersect::<A>(s1.remove(a), s2);
861    }
862}
863
864/// If `s1` is a subset of finite set `s2`, then the size of `s1` is less than or equal to
865/// the size of `s2` and `s1` must be finite.
866pub proof fn lemma_len_subset<A>(s1: Set<A>, s2: Set<A>)
867    requires
868        s2.finite(),
869        s1.subset_of(s2),
870    ensures
871        s1.len() <= s2.len(),
872        s1.finite(),
873{
874    lemma_len_intersect::<A>(s2, s1);
875    assert(s2.intersect(s1) =~= s1);
876}
877
878/// A subset of a finite set `s` is finite.
879pub broadcast proof fn lemma_set_subset_finite<A>(s: Set<A>, sub: Set<A>)
880    requires
881        s.finite(),
882        sub.subset_of(s),
883    ensures
884        #![trigger sub.subset_of(s)]
885        sub.finite(),
886{
887    let complement = s.difference(sub);
888    assert(sub =~= s.difference(complement));
889}
890
891/// The size of the difference of finite set `s1` and set `s2` is less than or equal to the size of `s1`.
892pub proof fn lemma_len_difference<A>(s1: Set<A>, s2: Set<A>)
893    requires
894        s1.finite(),
895    ensures
896        s1.difference(s2).len() <= s1.len(),
897    decreases s1.len(),
898{
899    if s1.is_empty() {
900        assert(s1.difference(s2) =~= s1);
901    } else {
902        let a = s1.choose();
903        assert(s1.difference(s2).remove(a) =~= s1.remove(a).difference(s2));
904        lemma_len_difference::<A>(s1.remove(a), s2);
905    }
906}
907
908/// Creates a finite set of integers in the range [lo, hi).
909pub open spec fn set_int_range(lo: int, hi: int) -> Set<int> {
910    Set::new(|i: int| lo <= i && i < hi)
911}
912
913/// If a set solely contains integers in the range [a, b), then its size is
914/// bounded by b - a.
915pub proof fn lemma_int_range(lo: int, hi: int)
916    requires
917        lo <= hi,
918    ensures
919        set_int_range(lo, hi).finite(),
920        set_int_range(lo, hi).len() == hi - lo,
921    decreases hi - lo,
922{
923    if lo == hi {
924        assert(set_int_range(lo, hi) =~= Set::empty());
925    } else {
926        lemma_int_range(lo, hi - 1);
927        assert(set_int_range(lo, hi - 1).insert(hi - 1) =~= set_int_range(lo, hi));
928    }
929}
930
931/// If x is a subset of y and the size of x is equal to the size of y, x is equal to y.
932pub proof fn lemma_subset_equality<A>(x: Set<A>, y: Set<A>)
933    requires
934        x.subset_of(y),
935        x.finite(),
936        y.finite(),
937        x.len() == y.len(),
938    ensures
939        x =~= y,
940    decreases x.len(),
941{
942    broadcast use group_set_properties;
943
944    if x =~= Set::<A>::empty() {
945    } else {
946        let e = x.choose();
947        lemma_subset_equality(x.remove(e), y.remove(e));
948    }
949}
950
951/// If an injective function is applied to each element of a set to construct
952/// another set, the two sets have the same size.
953// the dafny original lemma reasons with partial function f
954pub proof fn lemma_map_size<A, B>(x: Set<A>, y: Set<B>, f: spec_fn(A) -> B)
955    requires
956        injective(f),
957        forall|a: A| x.contains(a) ==> y.contains(#[trigger] f(a)),
958        forall|b: B| (#[trigger] y.contains(b)) ==> exists|a: A| x.contains(a) && f(a) == b,
959        x.finite(),
960    ensures
961        y.finite(),
962        x.len() == y.len(),
963    decreases x.len(),
964{
965    broadcast use group_set_properties;
966
967    if x.len() == 0 {
968        if !y.is_empty() {
969            let e = y.choose();
970        }
971    } else {
972        let a = x.choose();
973        lemma_map_size(x.remove(a), y.remove(f(a)), f);
974        assert(y == y.remove(f(a)).insert(f(a)));
975    }
976}
977
978// This verified lemma used to be an axiom in the Dafny prelude
979/// Taking the union of sets `a` and `b` and then taking the union of the result with `b`
980/// is the same as taking the union of `a` and `b` once.
981pub broadcast proof fn lemma_set_union_again1<A>(a: Set<A>, b: Set<A>)
982    ensures
983        #[trigger] a.union(b).union(b) =~= a.union(b),
984{
985}
986
987// This verified lemma used to be an axiom in the Dafny prelude
988/// Taking the union of sets `a` and `b` and then taking the union of the result with `a`
989/// is the same as taking the union of `a` and `b` once.
990pub broadcast proof fn lemma_set_union_again2<A>(a: Set<A>, b: Set<A>)
991    ensures
992        #[trigger] a.union(b).union(a) =~= a.union(b),
993{
994}
995
996// This verified lemma used to be an axiom in the Dafny prelude
997/// Taking the intersection of sets `a` and `b` and then taking the intersection of the result with `b`
998/// is the same as taking the intersection of `a` and `b` once.
999pub broadcast proof fn lemma_set_intersect_again1<A>(a: Set<A>, b: Set<A>)
1000    ensures
1001        #![trigger (a.intersect(b)).intersect(b)]
1002        (a.intersect(b)).intersect(b) =~= a.intersect(b),
1003{
1004}
1005
1006// This verified lemma used to be an axiom in the Dafny prelude
1007/// Taking the intersection of sets `a` and `b` and then taking the intersection of the result with `a`
1008/// is the same as taking the intersection of `a` and `b` once.
1009pub broadcast proof fn lemma_set_intersect_again2<A>(a: Set<A>, b: Set<A>)
1010    ensures
1011        #![trigger (a.intersect(b)).intersect(a)]
1012        (a.intersect(b)).intersect(a) =~= a.intersect(b),
1013{
1014}
1015
1016// This verified lemma used to be an axiom in the Dafny prelude
1017/// If set `s2` contains element `a`, then the set difference of `s1` and `s2` does not contain `a`.
1018pub broadcast proof fn lemma_set_difference2<A>(s1: Set<A>, s2: Set<A>, a: A)
1019    ensures
1020        #![trigger s1.difference(s2).contains(a)]
1021        s2.contains(a) ==> !s1.difference(s2).contains(a),
1022{
1023}
1024
1025// This verified lemma used to be an axiom in the Dafny prelude
1026/// If sets `a` and `b` are disjoint, meaning they have no elements in common, then the set difference
1027/// of `a + b` and `b` is equal to `a` and the set difference of `a + b` and `a` is equal to `b`.
1028pub broadcast proof fn lemma_set_disjoint<A>(a: Set<A>, b: Set<A>)
1029    ensures
1030        #![trigger (a + b).difference(a)]  //TODO: this might be too free
1031        a.disjoint(b) ==> ((a + b).difference(a) =~= b && (a + b).difference(b) =~= a),
1032{
1033}
1034
1035// This verified lemma used to be an axiom in the Dafny prelude
1036// Dafny encodes the second clause with a single directional, although
1037// it should be fine with both directions?
1038// REVIEW: excluded from broadcast group if trigger is too free
1039//         also not that some proofs in seq_lib requires this lemma
1040/// Set `s` has length 0 if and only if it is equal to the empty set. If `s` has length greater than 0,
1041/// Then there must exist an element `x` such that `s` contains `x`.
1042pub broadcast proof fn lemma_set_empty_equivalency_len<A>(s: Set<A>)
1043    requires
1044        s.finite(),
1045    ensures
1046        #![trigger s.len()]
1047        (s.len() == 0 <==> s == Set::<A>::empty()) && (s.len() != 0 ==> exists|x: A| s.contains(x)),
1048{
1049    assert(s.len() == 0 ==> s =~= Set::empty()) by {
1050        if s.len() == 0 {
1051            assert(forall|a: A| !(Set::empty().contains(a)));
1052            assert(Set::<A>::empty().len() == 0);
1053            assert(Set::<A>::empty().len() == s.len());
1054            assert((exists|a: A| s.contains(a)) || (forall|a: A| !s.contains(a)));
1055            if exists|a: A| s.contains(a) {
1056                let a = s.choose();
1057                assert(s.remove(a).len() == s.len() - 1) by {
1058                    axiom_set_remove_len(s, a);
1059                }
1060            }
1061        }
1062    }
1063    assert(s.len() == 0 <== s =~= Set::empty());
1064}
1065
1066// This verified lemma used to be an axiom in the Dafny prelude
1067/// If sets `a` and `b` are disjoint, meaning they share no elements in common, then the length
1068/// of the union `a + b` is equal to the sum of the lengths of `a` and `b`.
1069pub broadcast proof fn lemma_set_disjoint_lens<A>(a: Set<A>, b: Set<A>)
1070    requires
1071        a.finite(),
1072        b.finite(),
1073    ensures
1074        a.disjoint(b) ==> #[trigger] (a + b).len() == a.len() + b.len(),
1075    decreases a.len(),
1076{
1077    if a.len() == 0 {
1078        lemma_set_empty_equivalency_len(a);
1079        assert(a + b =~= b);
1080    } else {
1081        if a.disjoint(b) {
1082            let x = a.choose();
1083            assert(a.remove(x) + b =~= (a + b).remove(x));
1084            lemma_set_disjoint_lens(a.remove(x), b);
1085        }
1086    }
1087}
1088
1089// This verified lemma used to be an axiom in the Dafny prelude
1090/// The length of the union between two sets added to the length of the intersection between the
1091/// two sets is equal to the sum of the lengths of the two sets.
1092pub broadcast proof fn lemma_set_intersect_union_lens<A>(a: Set<A>, b: Set<A>)
1093    requires
1094        a.finite(),
1095        b.finite(),
1096    ensures
1097        #[trigger] (a + b).len() + #[trigger] a.intersect(b).len() == a.len() + b.len(),
1098    decreases a.len(),
1099{
1100    if a.len() == 0 {
1101        lemma_set_empty_equivalency_len(a);
1102        assert(a + b =~= b);
1103        assert(a.intersect(b) =~= Set::empty());
1104        assert(a.intersect(b).len() == 0);
1105    } else {
1106        let x = a.choose();
1107        lemma_set_intersect_union_lens(a.remove(x), b);
1108        if (b.contains(x)) {
1109            assert(a.remove(x) + b =~= (a + b));
1110            assert(a.intersect(b).remove(x) =~= a.remove(x).intersect(b));
1111        } else {
1112            assert(a.remove(x) + b =~= (a + b).remove(x));
1113            assert(a.remove(x).intersect(b) =~= a.intersect(b));
1114        }
1115    }
1116}
1117
1118// This verified lemma used to be an axiom in the Dafny prelude
1119/// The length of the set difference `A \ B` added to the length of the set difference `B \ A` added to
1120/// the length of the intersection `A ∩ B` is equal to the length of the union `A + B`.
1121///
1122/// The length of the set difference `A \ B` is equal to the length of `A` minus the length of the
1123/// intersection `A ∩ B`.
1124pub broadcast proof fn lemma_set_difference_len<A>(a: Set<A>, b: Set<A>)
1125    requires
1126        a.finite(),
1127        b.finite(),
1128    ensures
1129        (#[trigger] a.difference(b).len() + b.difference(a).len() + a.intersect(b).len() == (a
1130            + b).len()) && (a.difference(b).len() == a.len() - a.intersect(b).len()),
1131    decreases a.len(),
1132{
1133    if a.len() == 0 {
1134        lemma_set_empty_equivalency_len(a);
1135        assert(a.difference(b) =~= Set::empty());
1136        assert(b.difference(a) =~= b);
1137        assert(a.intersect(b) =~= Set::empty());
1138        assert(a + b =~= b);
1139    } else {
1140        let x = a.choose();
1141        lemma_set_difference_len(a.remove(x), b);
1142        if b.contains(x) {
1143            assert(a.intersect(b).remove(x) =~= a.remove(x).intersect(b));
1144            assert(a.remove(x).difference(b) =~= a.difference(b));
1145            assert(b.difference(a.remove(x)).remove(x) =~= b.difference(a));
1146            assert(a.remove(x) + b =~= a + b);
1147        } else {
1148            assert(a.remove(x) + b =~= (a + b).remove(x));
1149            assert(a.remove(x).difference(b) =~= a.difference(b).remove(x));
1150            assert(b.difference(a.remove(x)) =~= b.difference(a));
1151            assert(a.remove(x).intersect(b) =~= a.intersect(b));
1152        }
1153    }
1154}
1155
1156/// Properties of sets from the Dafny prelude (which were axioms in Dafny, but proven here in Verus)
1157#[deprecated = "Use `broadcast use group_set_properties` instead"]
1158pub proof fn lemma_set_properties<A>()
1159    ensures
1160        forall|a: Set<A>, b: Set<A>| #[trigger] a.union(b).union(b) == a.union(b),  //from lemma_set_union_again1
1161        forall|a: Set<A>, b: Set<A>| #[trigger] a.union(b).union(a) == a.union(b),  //from lemma_set_union_again2
1162        forall|a: Set<A>, b: Set<A>| #[trigger] (a.intersect(b)).intersect(b) == a.intersect(b),  //from lemma_set_intersect_again1
1163        forall|a: Set<A>, b: Set<A>| #[trigger] (a.intersect(b)).intersect(a) == a.intersect(b),  //from lemma_set_intersect_again2
1164        forall|s1: Set<A>, s2: Set<A>, a: A| s2.contains(a) ==> !s1.difference(s2).contains(a),  //from lemma_set_difference2
1165        forall|a: Set<A>, b: Set<A>|
1166            #![trigger (a + b).difference(a)]
1167            a.disjoint(b) ==> ((a + b).difference(a) =~= b && (a + b).difference(b) =~= a),  //from lemma_set_disjoint
1168        forall|s: Set<A>| #[trigger] s.len() != 0 && s.finite() ==> exists|a: A| s.contains(a),  // half of lemma_set_empty_equivalency_len
1169        forall|a: Set<A>, b: Set<A>|
1170            (a.finite() && b.finite() && a.disjoint(b)) ==> #[trigger] (a + b).len() == a.len()
1171                + b.len(),  //from lemma_set_disjoint_lens
1172        forall|a: Set<A>, b: Set<A>|
1173            (a.finite() && b.finite()) ==> #[trigger] (a + b).len() + #[trigger] a.intersect(
1174                b,
1175            ).len() == a.len() + b.len(),  //from lemma_set_intersect_union_lens
1176        forall|a: Set<A>, b: Set<A>|
1177            (a.finite() && b.finite()) ==> ((#[trigger] a.difference(b).len() + b.difference(
1178                a,
1179            ).len() + a.intersect(b).len() == (a + b).len()) && (a.difference(b).len() == a.len()
1180                - a.intersect(b).len())),  //from lemma_set_difference_len
1181{
1182    broadcast use group_set_properties;
1183
1184    assert forall|s: Set<A>| #[trigger] s.len() != 0 && s.finite() implies exists|a: A|
1185        s.contains(a) by {
1186        assert(s.contains(s.choose()));
1187    }
1188}
1189
1190pub broadcast group group_set_properties {
1191    lemma_set_union_again1,
1192    lemma_set_union_again2,
1193    lemma_set_intersect_again1,
1194    lemma_set_intersect_again2,
1195    lemma_set_difference2,
1196    lemma_set_disjoint,
1197    lemma_set_disjoint_lens,
1198    lemma_set_intersect_union_lens,
1199    lemma_set_difference_len,
1200    // REVIEW: exclude from broadcast group if trigger is too free
1201    //         also note that some proofs in seq_lib requires this lemma
1202    lemma_set_empty_equivalency_len,
1203}
1204
1205pub broadcast proof fn axiom_is_empty<A>(s: Set<A>)
1206    requires
1207        !(#[trigger] s.is_empty()),
1208    ensures
1209        exists|a: A| s.contains(a),
1210{
1211    admit();  // REVIEW, should this be in `set`, or have a proof?
1212}
1213
1214pub broadcast proof fn axiom_is_empty_len0<A>(s: Set<A>)
1215    ensures
1216        #[trigger] s.is_empty() <==> (s.finite() && s.len() == 0),
1217{
1218}
1219
1220#[doc(hidden)]
1221#[verifier::inline]
1222pub open spec fn check_argument_is_set<A>(s: Set<A>) -> Set<A> {
1223    s
1224}
1225
1226/// Prove two sets equal by extensionality. Usage is:
1227///
1228/// ```rust
1229/// assert_sets_equal!(set1 == set2);
1230/// ```
1231///
1232/// or,
1233///
1234/// ```rust
1235/// assert_sets_equal!(set1 == set2, elem => {
1236///     // prove that set1.contains(elem) iff set2.contains(elem)
1237/// });
1238/// ```
1239#[macro_export]
1240macro_rules! assert_sets_equal {
1241    [$($tail:tt)*] => {
1242        $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::set_lib::assert_sets_equal_internal!($($tail)*))
1243    };
1244}
1245
1246#[macro_export]
1247#[doc(hidden)]
1248macro_rules! assert_sets_equal_internal {
1249    (::vstd::prelude::spec_eq($s1:expr, $s2:expr)) => {
1250        $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2)
1251    };
1252    (::vstd::prelude::spec_eq($s1:expr, $s2:expr), $elem:ident $( : $t:ty )? => $bblock:block) => {
1253        $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2, $elem $( : $t )? => $bblock)
1254    };
1255    (crate::prelude::spec_eq($s1:expr, $s2:expr)) => {
1256        $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2)
1257    };
1258    (crate::prelude::spec_eq($s1:expr, $s2:expr), $elem:ident $( : $t:ty )? => $bblock:block) => {
1259        $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2, $elem $( : $t )? => $bblock)
1260    };
1261    (crate::verus_builtin::spec_eq($s1:expr, $s2:expr)) => {
1262        $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2)
1263    };
1264    (crate::verus_builtin::spec_eq($s1:expr, $s2:expr), $elem:ident $( : $t:ty )? => $bblock:block) => {
1265        $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2, $elem $( : $t )? => $bblock)
1266    };
1267    ($s1:expr, $s2:expr $(,)?) => {
1268        $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2, elem => { })
1269    };
1270    ($s1:expr, $s2:expr, $elem:ident $( : $t:ty )? => $bblock:block) => {
1271        #[verifier::spec] let s1 = $crate::vstd::set_lib::check_argument_is_set($s1);
1272        #[verifier::spec] let s2 = $crate::vstd::set_lib::check_argument_is_set($s2);
1273        $crate::vstd::prelude::assert_by($crate::vstd::prelude::equal(s1, s2), {
1274            $crate::vstd::prelude::assert_forall_by(|$elem $( : $t )?| {
1275                $crate::vstd::prelude::ensures(
1276                    $crate::vstd::prelude::imply(s1.contains($elem), s2.contains($elem))
1277                    &&
1278                    $crate::vstd::prelude::imply(s2.contains($elem), s1.contains($elem))
1279                );
1280                { $bblock }
1281            });
1282            $crate::vstd::prelude::assert_($crate::vstd::prelude::ext_equal(s1, s2));
1283        });
1284    }
1285}
1286
1287pub broadcast group group_set_lib_default {
1288    axiom_is_empty,
1289    axiom_is_empty_len0,
1290    lemma_set_subset_finite,
1291}
1292
1293pub use assert_sets_equal_internal;
1294pub use assert_sets_equal;
1295
1296} // verus!