vstd/
set.rs

1#[allow(unused_imports)]
2use super::map::*;
3#[allow(unused_imports)]
4use super::pervasive::*;
5#[allow(unused_imports)]
6use super::prelude::*;
7
8verus! {
9
10/// `Set<A>` is a set type for specifications.
11///
12/// An object `set: Set<A>` is a subset of the set of all values `a: A`.
13/// Equivalently, it can be thought of as a boolean predicate on `A`.
14///
15/// In general, a set might be infinite.
16/// To work specifically with finite sets, see the [`self.finite()`](Set::finite) predicate.
17///
18/// Sets can be constructed in a few different ways:
19///  * [`Set::empty`] gives an empty set
20///  * [`Set::full`] gives the set of all elements in `A`
21///  * [`Set::new`] constructs a set from a boolean predicate
22///  * The [`set!`] macro, to construct small sets of a fixed size
23///  * By manipulating an existing sequence with [`Set::union`], [`Set::intersect`],
24///    [`Set::difference`], [`Set::complement`], [`Set::filter`], [`Set::insert`],
25///    or [`Set::remove`].
26///
27/// To prove that two sequences are equal, it is usually easiest to use the extensionality
28/// operator `=~=`.
29#[verifier::ext_equal]
30#[verifier::reject_recursive_types(A)]
31pub struct Set<A> {
32    set: spec_fn(A) -> bool,
33}
34
35impl<A> Set<A> {
36    /// The "empty" set.
37    ///
38    /// Usage Example: <br>
39    /// ```rust
40    /// let empty_set = Set::<A>::empty();
41    ///
42    /// assert(empty_set.is_empty());
43    /// assert(empty_set.complement() =~= Set::<A>::full());
44    /// assert(Set::<A>::empty().finite());
45    /// assert(Set::<A>::empty().len() == 0);
46    /// assert(forall |x: A| !Set::<A>::empty().contains(x));
47    /// ```
48    /// Axioms around the empty set are: <br>
49    /// * [`axiom_set_empty_finite`](crate::set::axiom_set_empty_finite) <br>
50    /// * [`axiom_set_empty_len`](crate::set::axiom_set_empty_len) <br>
51    /// * [`axiom_set_empty`](crate::set::axiom_set_empty)
52    #[rustc_diagnostic_item = "verus::vstd::set::Set::empty"]
53    pub closed spec fn empty() -> Set<A> {
54        Set { set: |a| false }
55    }
56
57    /// Set whose membership is determined by the given boolean predicate.
58    ///
59    /// Usage Examples:
60    /// ```rust
61    /// let set_a = Set::new(|x : nat| x < 42);
62    /// let set_b = Set::<A>::new(|x| some_predicate(x));
63    /// assert(forall|x| some_predicate(x) <==> set_b.contains(x));
64    /// ```
65    pub closed spec fn new(f: spec_fn(A) -> bool) -> Set<A> {
66        Set {
67            set: |a|
68                if f(a) {
69                    true
70                } else {
71                    false
72                },
73        }
74    }
75
76    /// The "full" set, i.e., set containing every element of type `A`.
77    #[rustc_diagnostic_item = "verus::vstd::set::Set::full"]
78    pub open spec fn full() -> Set<A> {
79        Set::empty().complement()
80    }
81
82    /// Predicate indicating if the set contains the given element.
83    #[rustc_diagnostic_item = "verus::vstd::set::Set::contains"]
84    pub closed spec fn contains(self, a: A) -> bool {
85        (self.set)(a)
86    }
87
88    /// Predicate indicating if the set contains the given element: supports `self has a` syntax.
89    #[verifier::inline]
90    pub open spec fn spec_has(self, a: A) -> bool {
91        self.contains(a)
92    }
93
94    /// Returns `true` if the first argument is a subset of the second.
95    #[rustc_diagnostic_item = "verus::vstd::set::Set::subset_of"]
96    pub open spec fn subset_of(self, s2: Set<A>) -> bool {
97        forall|a: A| self.contains(a) ==> s2.contains(a)
98    }
99
100    #[verifier::inline]
101    pub open spec fn spec_le(self, s2: Set<A>) -> bool {
102        self.subset_of(s2)
103    }
104
105    /// Returns a new set with the given element inserted.
106    /// If that element is already in the set, then an identical set is returned.
107    #[rustc_diagnostic_item = "verus::vstd::set::Set::insert"]
108    pub closed spec fn insert(self, a: A) -> Set<A> {
109        Set {
110            set: |a2|
111                if a2 == a {
112                    true
113                } else {
114                    (self.set)(a2)
115                },
116        }
117    }
118
119    /// Returns a new set with the given element removed.
120    /// If that element is already absent from the set, then an identical set is returned.
121    #[rustc_diagnostic_item = "verus::vstd::set::Set::remove"]
122    pub closed spec fn remove(self, a: A) -> Set<A> {
123        Set {
124            set: |a2|
125                if a2 == a {
126                    false
127                } else {
128                    (self.set)(a2)
129                },
130        }
131    }
132
133    /// Union of two sets.
134    pub closed spec fn union(self, s2: Set<A>) -> Set<A> {
135        Set { set: |a| (self.set)(a) || (s2.set)(a) }
136    }
137
138    /// `+` operator, synonymous with `union`
139    #[verifier::inline]
140    pub open spec fn spec_add(self, s2: Set<A>) -> Set<A> {
141        self.union(s2)
142    }
143
144    /// Intersection of two sets.
145    pub closed spec fn intersect(self, s2: Set<A>) -> Set<A> {
146        Set { set: |a| (self.set)(a) && (s2.set)(a) }
147    }
148
149    /// `*` operator, synonymous with `intersect`
150    #[verifier::inline]
151    pub open spec fn spec_mul(self, s2: Set<A>) -> Set<A> {
152        self.intersect(s2)
153    }
154
155    /// Set difference, i.e., the set of all elements in the first one but not in the second.
156    pub closed spec fn difference(self, s2: Set<A>) -> Set<A> {
157        Set { set: |a| (self.set)(a) && !(s2.set)(a) }
158    }
159
160    /// `-` operator, synonymous with `difference`
161    #[verifier::inline]
162    pub open spec fn spec_sub(self, s2: Set<A>) -> Set<A> {
163        self.difference(s2)
164    }
165
166    /// Set complement (within the space of all possible elements in `A`).
167    pub closed spec fn complement(self) -> Set<A> {
168        Set { set: |a| !(self.set)(a) }
169    }
170
171    /// Set of all elements in the given set which satisfy the predicate `f`.
172    pub open spec fn filter(self, f: spec_fn(A) -> bool) -> Set<A> {
173        self.intersect(Self::new(f))
174    }
175
176    /// Returns `true` if the set is finite.
177    pub closed spec fn finite(self) -> bool {
178        exists|f: spec_fn(A) -> nat, ub: nat|
179            {
180                &&& #[trigger] trigger_finite(f, ub)
181                &&& surj_on(f, self)
182                &&& forall|a| self.contains(a) ==> f(a) < ub
183            }
184    }
185
186    /// Cardinality of the set. (Only meaningful if a set is finite.)
187    pub closed spec fn len(self) -> nat {
188        self.fold(0, |acc: nat, a| acc + 1)
189    }
190
191    /// Chooses an arbitrary element of the set.
192    ///
193    /// This is often useful for proofs by induction.
194    ///
195    /// (Note that, although the result is arbitrary, it is still a _deterministic_ function
196    /// like any other `spec` function.)
197    pub open spec fn choose(self) -> A {
198        choose|a: A| self.contains(a)
199    }
200
201    /// Creates a [`Map`] whose domain is the given set.
202    /// The values of the map are given by `f`, a function of the keys.
203    pub uninterp spec fn mk_map<V>(self, f: spec_fn(A) -> V) -> Map<A, V>;
204
205    /// Returns `true` if the sets are disjoint, i.e., if their interesection is
206    /// the empty set.
207    pub open spec fn disjoint(self, s2: Self) -> bool {
208        forall|a: A| self.contains(a) ==> !s2.contains(a)
209    }
210}
211
212// Closures make triggering finicky but using this to trigger explicitly works well.
213spec fn trigger_finite<A>(f: spec_fn(A) -> nat, ub: nat) -> bool {
214    true
215}
216
217spec fn surj_on<A, B>(f: spec_fn(A) -> B, s: Set<A>) -> bool {
218    forall|a1, a2| #![all_triggers] s.contains(a1) && s.contains(a2) && a1 != a2 ==> f(a1) != f(a2)
219}
220
221pub mod fold {
222    //! This module defines a fold function for finite sets and proves a number of associated
223    //! lemmas.
224    //!
225    //! The module was ported (with some modifications) from Isabelle/HOL's finite set theory in:
226    //! `HOL/Finite_Set.thy`
227    //! That file contains the following author list:
228    //!
229    //!
230    //! (*  Title:      HOL/Finite_Set.thy
231    //!     Author:     Tobias Nipkow
232    //!     Author:     Lawrence C Paulson
233    //!     Author:     Markus Wenzel
234    //!     Author:     Jeremy Avigad
235    //!     Author:     Andrei Popescu
236    //! *)
237    //!
238    //!
239    //! The file is distributed under a 3-clause BSD license as indicated in the file `COPYRIGHT`
240    //! in Isabelle's root directory, which also carries the following copyright notice:
241    //!
242    //! Copyright (c) 1986-2024,
243    //! University of Cambridge,
244    //! Technische Universitaet Muenchen,
245    //! and contributors.
246    use super::*;
247
248    broadcast group group_set_axioms_early {
249        axiom_set_empty,
250        axiom_set_new,
251        axiom_set_insert_same,
252        axiom_set_insert_different,
253        axiom_set_remove_same,
254        axiom_set_remove_insert,
255        axiom_set_remove_different,
256        axiom_set_union,
257        axiom_set_intersect,
258        axiom_set_difference,
259        axiom_set_complement,
260        axiom_set_ext_equal,
261        axiom_set_ext_equal_deep,
262        axiom_set_empty_finite,
263        axiom_set_insert_finite,
264        axiom_set_remove_finite,
265    }
266
267    pub open spec fn is_fun_commutative<A, B>(f: spec_fn(B, A) -> B) -> bool {
268        forall|a1, a2, b| #[trigger] f(f(b, a2), a1) == f(f(b, a1), a2)
269    }
270
271    // This predicate is intended to be used like an inductive predicate, with the corresponding
272    // introduction, elimination and induction rules proved below.
273    #[verifier(opaque)]
274    spec fn fold_graph<A, B>(z: B, f: spec_fn(B, A) -> B, s: Set<A>, y: B, d: nat) -> bool
275        decreases d,
276    {
277        if s === Set::empty() {
278            &&& z == y
279            &&& d == 0
280        } else {
281            exists|yr, a|
282                {
283                    &&& #[trigger] trigger_fold_graph(yr, a)
284                    &&& d > 0
285                    &&& s.remove(a).finite()
286                    &&& s.contains(a)
287                    &&& fold_graph(z, f, s.remove(a), yr, sub(d, 1))
288                    &&& y == f(yr, a)
289                }
290        }
291    }
292
293    spec fn trigger_fold_graph<A, B>(yr: B, a: A) -> bool {
294        true
295    }
296
297    // Introduction rules
298    proof fn lemma_fold_graph_empty_intro<A, B>(z: B, f: spec_fn(B, A) -> B)
299        ensures
300            fold_graph(z, f, Set::empty(), z, 0),
301    {
302        reveal(fold_graph);
303    }
304
305    proof fn lemma_fold_graph_insert_intro<A, B>(
306        z: B,
307        f: spec_fn(B, A) -> B,
308        s: Set<A>,
309        y: B,
310        d: nat,
311        a: A,
312    )
313        requires
314            fold_graph(z, f, s, y, d),
315            !s.contains(a),
316        ensures
317            fold_graph(z, f, s.insert(a), f(y, a), d + 1),
318    {
319        broadcast use group_set_axioms_early;
320
321        reveal(fold_graph);
322        let _ = trigger_fold_graph(y, a);
323        assert(s == s.insert(a).remove(a));
324    }
325
326    // Elimination rules
327    proof fn lemma_fold_graph_empty_elim<A, B>(z: B, f: spec_fn(B, A) -> B, y: B, d: nat)
328        requires
329            fold_graph(z, f, Set::empty(), y, d),
330        ensures
331            z == y,
332            d == 0,
333    {
334        reveal(fold_graph);
335    }
336
337    proof fn lemma_fold_graph_insert_elim<A, B>(
338        z: B,
339        f: spec_fn(B, A) -> B,
340        s: Set<A>,
341        y: B,
342        d: nat,
343        a: A,
344    )
345        requires
346            is_fun_commutative(f),
347            fold_graph(z, f, s.insert(a), y, d),
348            !s.contains(a),
349        ensures
350            d > 0,
351            exists|yp| y == f(yp, a) && #[trigger] fold_graph(z, f, s, yp, sub(d, 1)),
352    {
353        reveal(fold_graph);
354        lemma_fold_graph_insert_elim_aux(z, f, s.insert(a), y, d, a);
355        assert(s.insert(a).remove(a) =~= s);
356        let yp = choose|yp| y == f(yp, a) && #[trigger] fold_graph(z, f, s, yp, sub(d, 1));
357    }
358
359    proof fn lemma_fold_graph_insert_elim_aux<A, B>(
360        z: B,
361        f: spec_fn(B, A) -> B,
362        s: Set<A>,
363        y: B,
364        d: nat,
365        a: A,
366    )
367        requires
368            is_fun_commutative(f),
369            fold_graph(z, f, s, y, d),
370            s.contains(a),
371        ensures
372            exists|yp| y == f(yp, a) && #[trigger] fold_graph(z, f, s.remove(a), yp, sub(d, 1)),
373        decreases d,
374    {
375        broadcast use group_set_axioms_early;
376
377        reveal(fold_graph);
378        let (yr, aa): (B, A) = choose|yr, aa|
379            #![all_triggers]
380            {
381                &&& trigger_fold_graph(yr, a)
382                &&& d > 0
383                &&& s.remove(aa).finite()
384                &&& s.contains(aa)
385                &&& fold_graph(z, f, s.remove(aa), yr, sub(d, 1))
386                &&& y == f(yr, aa)
387            };
388        assert(trigger_fold_graph(yr, a));
389        if s.remove(aa) === Set::empty() {
390        } else {
391            if a == aa {
392            } else {
393                lemma_fold_graph_insert_elim_aux(z, f, s.remove(aa), yr, sub(d, 1), a);
394                let yrp = choose|yrp|
395                    yr == f(yrp, a) && #[trigger] fold_graph(
396                        z,
397                        f,
398                        s.remove(aa).remove(a),
399                        yrp,
400                        sub(d, 2),
401                    );
402                assert(fold_graph(z, f, s.remove(aa).insert(aa).remove(a), f(yrp, aa), sub(d, 1)))
403                    by {
404                    assert(s.remove(aa).remove(a) == s.remove(aa).insert(aa).remove(a).remove(aa));
405                    assert(trigger_fold_graph(yrp, aa));
406                };
407            }
408        }
409    }
410
411    // Induction rule
412    proof fn lemma_fold_graph_induct<A, B>(
413        z: B,
414        f: spec_fn(B, A) -> B,
415        s: Set<A>,
416        y: B,
417        d: nat,
418        pred: spec_fn(Set<A>, B, nat) -> bool,
419    )
420        requires
421            is_fun_commutative(f),
422            fold_graph(z, f, s, y, d),
423            pred(Set::empty(), z, 0),
424            forall|a, s, y, d|
425                pred(s, y, d) && !s.contains(a) && #[trigger] fold_graph(z, f, s, y, d) ==> pred(
426                    #[trigger] s.insert(a),
427                    f(y, a),
428                    d + 1,
429                ),
430        ensures
431            pred(s, y, d),
432        decreases d,
433    {
434        broadcast use group_set_axioms_early;
435
436        reveal(fold_graph);
437        if s === Set::empty() {
438            lemma_fold_graph_empty_elim(z, f, y, d);
439        } else {
440            let a = s.choose();
441            lemma_fold_graph_insert_elim(z, f, s.remove(a), y, d, a);
442            let yp = choose|yp|
443                y == f(yp, a) && #[trigger] fold_graph(z, f, s.remove(a), yp, sub(d, 1));
444            lemma_fold_graph_induct(z, f, s.remove(a), yp, sub(d, 1), pred);
445        }
446    }
447
448    impl<A> Set<A> {
449        /// Folds the set, applying `f` to perform the fold. The next element for the fold is chosen by
450        /// the choose operator.
451        ///
452        /// Given a set `s = {x0, x1, x2, ..., xn}`, applying this function `s.fold(init, f)`
453        /// returns `f(...f(f(init, x0), x1), ..., xn)`.
454        pub closed spec fn fold<B>(self, z: B, f: spec_fn(B, A) -> B) -> B
455            recommends
456                self.finite(),
457                is_fun_commutative(f),
458        {
459            let (y, d): (B, nat) = choose|y, d| fold_graph(z, f, self, y, d);
460            y
461        }
462    }
463
464    proof fn lemma_fold_graph_finite<A, B>(z: B, f: spec_fn(B, A) -> B, s: Set<A>, y: B, d: nat)
465        requires
466            is_fun_commutative(f),
467            fold_graph(z, f, s, y, d),
468        ensures
469            s.finite(),
470    {
471        broadcast use group_set_axioms_early;
472
473        let pred = |s: Set<A>, y, d| s.finite();
474        lemma_fold_graph_induct(z, f, s, y, d, pred);
475    }
476
477    proof fn lemma_fold_graph_deterministic<A, B>(
478        z: B,
479        f: spec_fn(B, A) -> B,
480        s: Set<A>,
481        y1: B,
482        y2: B,
483        d1: nat,
484        d2: nat,
485    )
486        requires
487            is_fun_commutative(f),
488            fold_graph(z, f, s, y1, d1),
489            fold_graph(z, f, s, y2, d2),
490        ensures
491            y1 == y2,
492            d1 == d2,
493    {
494        let pred = |s: Set<A>, y1: B, d1: nat|
495            forall|y2, d2| fold_graph(z, f, s, y2, d2) ==> y1 == y2 && d2 == d1;
496        // Base case
497        assert(pred(Set::empty(), z, 0)) by {
498            assert forall|y2, d2| fold_graph(z, f, Set::empty(), y2, d2) implies z == y2 && d2
499                == 0 by {
500                lemma_fold_graph_empty_elim(z, f, y2, d2);
501            };
502        };
503        // Step case
504        assert forall|a, s, y1, d1|
505            pred(s, y1, d1) && !s.contains(a) && #[trigger] fold_graph(
506                z,
507                f,
508                s,
509                y1,
510                d1,
511            ) implies pred(#[trigger] s.insert(a), f(y1, a), d1 + 1) by {
512            assert forall|y2, d2| fold_graph(z, f, s.insert(a), y2, d2) implies f(y1, a) == y2 && d2
513                == d1 + 1 by {
514                lemma_fold_graph_insert_elim(z, f, s, y2, d2, a);
515            };
516        };
517        lemma_fold_graph_induct(z, f, s, y2, d2, pred);
518    }
519
520    proof fn lemma_fold_is_fold_graph<A, B>(z: B, f: spec_fn(B, A) -> B, s: Set<A>, y: B, d: nat)
521        requires
522            is_fun_commutative(f),
523            fold_graph(z, f, s, y, d),
524        ensures
525            s.fold(z, f) == y,
526    {
527        lemma_fold_graph_finite(z, f, s, y, d);
528        if s.fold(z, f) != y {
529            let (y2, d2) = choose|y2, d2| fold_graph(z, f, s, y2, d2) && y2 != y;
530            lemma_fold_graph_deterministic(z, f, s, y2, y, d2, d);
531            assert(false);
532        }
533    }
534
535    // At this point set cardinality is not yet defined, so we can't easily give a decreasing
536    // measure to prove the subsequent lemma `lemma_fold_graph_exists`. Instead, we first prove
537    // this lemma, for which we use the upper bound of a finiteness witness as the decreasing
538    // measure.
539    pub proof fn lemma_finite_set_induct<A>(s: Set<A>, pred: spec_fn(Set<A>) -> bool)
540        requires
541            s.finite(),
542            pred(Set::empty()),
543            forall|s, a| pred(s) && s.finite() && !s.contains(a) ==> #[trigger] pred(s.insert(a)),
544        ensures
545            pred(s),
546    {
547        let (f, ub) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger]
548            trigger_finite(f, ub) && surj_on(f, s) && (forall|a| s.contains(a) ==> f(a) < ub);
549        lemma_finite_set_induct_aux(s, f, ub, pred);
550    }
551
552    proof fn lemma_finite_set_induct_aux<A>(
553        s: Set<A>,
554        f: spec_fn(A) -> nat,
555        ub: nat,
556        pred: spec_fn(Set<A>) -> bool,
557    )
558        requires
559            surj_on(f, s),
560            s.finite(),
561            forall|a| s.contains(a) ==> f(a) < ub,
562            pred(Set::empty()),
563            forall|s, a| pred(s) && s.finite() && !s.contains(a) ==> #[trigger] pred(s.insert(a)),
564        ensures
565            pred(s),
566        decreases ub,
567    {
568        broadcast use group_set_axioms_early;
569
570        if s =~= Set::empty() {
571        } else {
572            let a = s.choose();
573            // If `f` maps something to `ub - 1`, remap it to `f(a)` so we can decrease ub
574            let fp = |aa|
575                if f(aa) == ub - 1 {
576                    f(a)
577                } else {
578                    f(aa)
579                };
580            lemma_finite_set_induct_aux(s.remove(a), fp, sub(ub, 1), pred);
581        }
582    }
583
584    proof fn lemma_fold_graph_exists<A, B>(z: B, f: spec_fn(B, A) -> B, s: Set<A>)
585        requires
586            s.finite(),
587            is_fun_commutative(f),
588        ensures
589            exists|y, d| fold_graph(z, f, s, y, d),
590    {
591        let pred = |s| exists|y, d| fold_graph(z, f, s, y, d);
592        // Base case
593        assert(fold_graph(z, f, Set::empty(), z, 0)) by {
594            lemma_fold_graph_empty_intro(z, f);
595        };
596        // Step case
597        assert forall|s, a| pred(s) && s.finite() && !s.contains(a) implies #[trigger] pred(
598            s.insert(a),
599        ) by {
600            let (y, d): (B, nat) = choose|y, d| fold_graph(z, f, s, y, d);
601            lemma_fold_graph_insert_intro(z, f, s, y, d, a);
602        };
603        lemma_finite_set_induct(s, pred);
604    }
605
606    pub broadcast proof fn lemma_fold_insert<A, B>(s: Set<A>, z: B, f: spec_fn(B, A) -> B, a: A)
607        requires
608            s.finite(),
609            !s.contains(a),
610            is_fun_commutative(f),
611        ensures
612            #[trigger] s.insert(a).fold(z, f) == f(s.fold(z, f), a),
613    {
614        lemma_fold_graph_exists(z, f, s);
615        let (y, d): (B, nat) = choose|y, d| fold_graph(z, f, s, y, d);
616        lemma_fold_graph_insert_intro(z, f, s, s.fold(z, f), d, a);
617        lemma_fold_is_fold_graph(z, f, s.insert(a), f(s.fold(z, f), a), d + 1);
618    }
619
620    pub broadcast proof fn lemma_fold_empty<A, B>(z: B, f: spec_fn(B, A) -> B)
621        ensures
622            #[trigger] Set::empty().fold(z, f) == z,
623    {
624        let (y, d): (B, nat) = choose|y, d| fold_graph(z, f, Set::empty(), y, d);
625        lemma_fold_graph_empty_intro(z, f);
626        lemma_fold_graph_empty_elim(z, f, y, d);
627    }
628
629}
630
631// Axioms
632/// The empty set contains no elements
633pub broadcast proof fn axiom_set_empty<A>(a: A)
634    ensures
635        !(#[trigger] Set::empty().contains(a)),
636{
637}
638
639/// A call to `Set::new` with the predicate `f` contains `a` if and only if `f(a)` is true.
640pub broadcast proof fn axiom_set_new<A>(f: spec_fn(A) -> bool, a: A)
641    ensures
642        #[trigger] Set::new(f).contains(a) == f(a),
643{
644}
645
646/// The result of inserting element `a` into set `s` must contains `a`.
647pub broadcast proof fn axiom_set_insert_same<A>(s: Set<A>, a: A)
648    ensures
649        #[trigger] s.insert(a).contains(a),
650{
651}
652
653/// If `a1` does not equal `a2`, then the result of inserting element `a2` into set `s`
654/// must contain `a1` if and only if the set contained `a1` before the insertion of `a2`.
655pub broadcast proof fn axiom_set_insert_different<A>(s: Set<A>, a1: A, a2: A)
656    requires
657        a1 != a2,
658    ensures
659        #[trigger] s.insert(a2).contains(a1) == s.contains(a1),
660{
661}
662
663/// The result of removing element `a` from set `s` must not contain `a`.
664pub broadcast proof fn axiom_set_remove_same<A>(s: Set<A>, a: A)
665    ensures
666        !(#[trigger] s.remove(a).contains(a)),
667{
668}
669
670/// Removing an element `a` from a set `s` and then inserting `a` back into the set`
671/// is equivalent to the original set `s`.
672pub broadcast proof fn axiom_set_remove_insert<A>(s: Set<A>, a: A)
673    requires
674        s.contains(a),
675    ensures
676        (#[trigger] s.remove(a)).insert(a) == s,
677{
678    assert forall|aa| #![all_triggers] s.remove(a).insert(a).contains(aa) implies s.contains(
679        aa,
680    ) by {
681        if a == aa {
682        } else {
683            axiom_set_remove_different(s, aa, a);
684            axiom_set_insert_different(s.remove(a), aa, a);
685        }
686    };
687    assert forall|aa| #![all_triggers] s.contains(aa) implies s.remove(a).insert(a).contains(
688        aa,
689    ) by {
690        if a == aa {
691            axiom_set_insert_same(s.remove(a), a);
692        } else {
693            axiom_set_remove_different(s, aa, a);
694            axiom_set_insert_different(s.remove(a), aa, a);
695        }
696    };
697    axiom_set_ext_equal(s.remove(a).insert(a), s);
698}
699
700/// If `a1` does not equal `a2`, then the result of removing element `a2` from set `s`
701/// must contain `a1` if and only if the set contained `a1` before the removal of `a2`.
702pub broadcast proof fn axiom_set_remove_different<A>(s: Set<A>, a1: A, a2: A)
703    requires
704        a1 != a2,
705    ensures
706        #[trigger] s.remove(a2).contains(a1) == s.contains(a1),
707{
708}
709
710/// The union of sets `s1` and `s2` contains element `a` if and only if
711/// `s1` contains `a` and/or `s2` contains `a`.
712pub broadcast proof fn axiom_set_union<A>(s1: Set<A>, s2: Set<A>, a: A)
713    ensures
714        #[trigger] s1.union(s2).contains(a) == (s1.contains(a) || s2.contains(a)),
715{
716}
717
718/// The intersection of sets `s1` and `s2` contains element `a` if and only if
719/// both `s1` and `s2` contain `a`.
720pub broadcast proof fn axiom_set_intersect<A>(s1: Set<A>, s2: Set<A>, a: A)
721    ensures
722        #[trigger] s1.intersect(s2).contains(a) == (s1.contains(a) && s2.contains(a)),
723{
724}
725
726/// The set difference between `s1` and `s2` contains element `a` if and only if
727/// `s1` contains `a` and `s2` does not contain `a`.
728pub broadcast proof fn axiom_set_difference<A>(s1: Set<A>, s2: Set<A>, a: A)
729    ensures
730        #[trigger] s1.difference(s2).contains(a) == (s1.contains(a) && !s2.contains(a)),
731{
732}
733
734/// The complement of set `s` contains element `a` if and only if `s` does not contain `a`.
735pub broadcast proof fn axiom_set_complement<A>(s: Set<A>, a: A)
736    ensures
737        #[trigger] s.complement().contains(a) == !s.contains(a),
738{
739}
740
741/// Sets `s1` and `s2` are equal if and only if they contain all of the same elements.
742pub broadcast proof fn axiom_set_ext_equal<A>(s1: Set<A>, s2: Set<A>)
743    ensures
744        #[trigger] (s1 =~= s2) <==> (forall|a: A| s1.contains(a) == s2.contains(a)),
745{
746    if s1 =~= s2 {
747        assert(forall|a: A| s1.contains(a) == s2.contains(a));
748    }
749    if forall|a: A| s1.contains(a) == s2.contains(a) {
750        if !(forall|a: A| #[trigger] (s1.set)(a) <==> (s2.set)(a)) {
751            assert(exists|a: A| #[trigger] (s1.set)(a) != (s2.set)(a));
752            let a = choose|a: A| #[trigger] (s1.set)(a) != (s2.set)(a);
753            assert(s1.contains(a));
754            assert(false);
755        }
756        assert(s1 =~= s2);
757    }
758}
759
760pub broadcast proof fn axiom_set_ext_equal_deep<A>(s1: Set<A>, s2: Set<A>)
761    ensures
762        #[trigger] (s1 =~~= s2) <==> s1 =~= s2,
763{
764}
765
766pub broadcast axiom fn axiom_mk_map_domain<K, V>(s: Set<K>, f: spec_fn(K) -> V)
767    ensures
768        #[trigger] s.mk_map(f).dom() == s,
769;
770
771pub broadcast axiom fn axiom_mk_map_index<K, V>(s: Set<K>, f: spec_fn(K) -> V, key: K)
772    requires
773        s.contains(key),
774    ensures
775        #[trigger] s.mk_map(f)[key] == f(key),
776;
777
778// Trusted axioms about finite
779/// The empty set is finite.
780pub broadcast proof fn axiom_set_empty_finite<A>()
781    ensures
782        #[trigger] Set::<A>::empty().finite(),
783{
784    let f = |a: A| 0;
785    let ub = 0;
786    let _ = trigger_finite(f, ub);
787}
788
789/// The result of inserting an element `a` into a finite set `s` is also finite.
790pub broadcast proof fn axiom_set_insert_finite<A>(s: Set<A>, a: A)
791    requires
792        s.finite(),
793    ensures
794        #[trigger] s.insert(a).finite(),
795{
796    let (f, ub) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger]
797        trigger_finite(f, ub) && surj_on(f, s) && (forall|a| s.contains(a) ==> f(a) < ub);
798    let f2 = |a2: A|
799        if a2 == a {
800            ub
801        } else {
802            f(a2)
803        };
804    let ub2 = ub + 1;
805    let _ = trigger_finite(f2, ub2);
806    assert forall|a1, a2|
807        #![all_triggers]
808        s.insert(a).contains(a1) && s.insert(a).contains(a2) && a1 != a2 implies f2(a1) != f2(
809        a2,
810    ) by {
811        if a != a1 {
812            assert(s.contains(a1));
813        }
814        if a != a2 {
815            assert(s.contains(a2));
816        }
817    };
818    assert forall|a2| s.insert(a).contains(a2) implies #[trigger] f2(a2) < ub2 by {
819        if a == a2 {
820        } else {
821            assert(s.contains(a2));
822        }
823    };
824}
825
826/// The result of removing an element `a` from a finite set `s` is also finite.
827pub broadcast proof fn axiom_set_remove_finite<A>(s: Set<A>, a: A)
828    requires
829        s.finite(),
830    ensures
831        #[trigger] s.remove(a).finite(),
832{
833    let (f, ub) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger]
834        trigger_finite(f, ub) && surj_on(f, s) && (forall|a| s.contains(a) ==> f(a) < ub);
835    assert forall|a1, a2|
836        #![all_triggers]
837        s.remove(a).contains(a1) && s.remove(a).contains(a2) && a1 != a2 implies f(a1) != f(a2) by {
838        if a != a1 {
839            assert(s.contains(a1));
840        }
841        if a != a2 {
842            assert(s.contains(a2));
843        }
844    };
845    assert(surj_on(f, s.remove(a)));
846    assert forall|a2| s.remove(a).contains(a2) implies #[trigger] f(a2) < ub by {
847        if a == a2 {
848        } else {
849            assert(s.contains(a2));
850        }
851    };
852}
853
854/// The union of two finite sets is finite.
855pub broadcast proof fn axiom_set_union_finite<A>(s1: Set<A>, s2: Set<A>)
856    requires
857        s1.finite(),
858        s2.finite(),
859    ensures
860        #[trigger] s1.union(s2).finite(),
861{
862    let (f1, ub1) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger]
863        trigger_finite(f, ub) && surj_on(f, s1) && (forall|a| s1.contains(a) ==> f(a) < ub);
864    let (f2, ub2) = choose|f: spec_fn(A) -> nat, ub: nat| #[trigger]
865        trigger_finite(f, ub) && surj_on(f, s2) && (forall|a| s2.contains(a) ==> f(a) < ub);
866    let f3 = |a|
867        if s1.contains(a) {
868            f1(a)
869        } else {
870            ub1 + f2(a)
871        };
872    let ub3 = ub1 + ub2;
873    assert(trigger_finite(f3, ub3));
874    assert(forall|a|
875        #![all_triggers]
876        s1.union(s2).contains(a) ==> s1.contains(a) || s2.contains(a));
877}
878
879/// The intersection of two finite sets is finite.
880pub broadcast proof fn axiom_set_intersect_finite<A>(s1: Set<A>, s2: Set<A>)
881    requires
882        s1.finite() || s2.finite(),
883    ensures
884        #[trigger] s1.intersect(s2).finite(),
885{
886    assert(forall|a|
887        #![all_triggers]
888        s1.intersect(s2).contains(a) ==> s1.contains(a) && s2.contains(a));
889}
890
891/// The set difference between two finite sets is finite.
892pub broadcast proof fn axiom_set_difference_finite<A>(s1: Set<A>, s2: Set<A>)
893    requires
894        s1.finite(),
895    ensures
896        #[trigger] s1.difference(s2).finite(),
897{
898    assert(forall|a|
899        #![all_triggers]
900        s1.difference(s2).contains(a) ==> s1.contains(a) && !s2.contains(a));
901}
902
903/// An infinite set `s` contains the element `s.choose()`.
904pub broadcast proof fn axiom_set_choose_finite<A>(s: Set<A>)
905    requires
906        !s.finite(),
907    ensures
908        #[trigger] s.contains(s.choose()),
909{
910    let f = |a: A| 0;
911    let ub = 0;
912    let _ = trigger_finite(f, ub);
913}
914
915// Trusted axioms about len
916// Note: we could add more axioms about len, but they would be incomplete.
917// The following, with axiom_set_ext_equal, are enough to build libraries about len.
918/// The empty set has length 0.
919pub broadcast proof fn axiom_set_empty_len<A>()
920    ensures
921        #[trigger] Set::<A>::empty().len() == 0,
922{
923    fold::lemma_fold_empty(0, |b: nat, a: A| b + 1);
924}
925
926/// The result of inserting an element `a` into a finite set `s` has length
927/// `s.len() + 1` if `a` is not already in `s` and length `s.len()` otherwise.
928pub broadcast proof fn axiom_set_insert_len<A>(s: Set<A>, a: A)
929    requires
930        s.finite(),
931    ensures
932        #[trigger] s.insert(a).len() == s.len() + (if s.contains(a) {
933            0int
934        } else {
935            1
936        }),
937{
938    if s.contains(a) {
939        assert(s =~= s.insert(a));
940    } else {
941        fold::lemma_fold_insert(s, 0, |b: nat, a: A| b + 1, a);
942    }
943}
944
945/// The result of removing an element `a` from a finite set `s` has length
946/// `s.len() - 1` if `a` is in `s` and length `s.len()` otherwise.
947pub broadcast proof fn axiom_set_remove_len<A>(s: Set<A>, a: A)
948    requires
949        s.finite(),
950    ensures
951        s.len() == #[trigger] s.remove(a).len() + (if s.contains(a) {
952            1int
953        } else {
954            0
955        }),
956{
957    axiom_set_remove_finite(s, a);
958    axiom_set_insert_len(s.remove(a), a);
959    if s.contains(a) {
960        assert(s =~= s.remove(a).insert(a));
961    } else {
962        assert(s =~= s.remove(a));
963    }
964}
965
966/// If a finite set `s` contains any element, it has length greater than 0.
967pub broadcast proof fn axiom_set_contains_len<A>(s: Set<A>, a: A)
968    requires
969        s.finite(),
970        #[trigger] s.contains(a),
971    ensures
972        #[trigger] s.len() != 0,
973{
974    let a = s.choose();
975    assert(s.remove(a).insert(a) =~= s);
976    axiom_set_remove_finite(s, a);
977    axiom_set_insert_finite(s.remove(a), a);
978    axiom_set_insert_len(s.remove(a), a);
979}
980
981/// A finite set `s` contains the element `s.choose()` if it has length greater than 0.
982pub broadcast proof fn axiom_set_choose_len<A>(s: Set<A>)
983    requires
984        s.finite(),
985        #[trigger] s.len() != 0,
986    ensures
987        #[trigger] s.contains(s.choose()),
988{
989    // Separate statements to work around https://github.com/verus-lang/verusfmt/issues/86
990    broadcast use axiom_set_contains_len;
991    broadcast use axiom_set_empty_len;
992    broadcast use axiom_set_ext_equal;
993    broadcast use axiom_set_insert_finite;
994
995    let pred = |s: Set<A>| s.finite() ==> s.len() == 0 <==> s =~= Set::empty();
996    fold::lemma_finite_set_induct(s, pred);
997}
998
999pub broadcast group group_set_axioms {
1000    axiom_set_empty,
1001    axiom_set_new,
1002    axiom_set_insert_same,
1003    axiom_set_insert_different,
1004    axiom_set_remove_same,
1005    axiom_set_remove_insert,
1006    axiom_set_remove_different,
1007    axiom_set_union,
1008    axiom_set_intersect,
1009    axiom_set_difference,
1010    axiom_set_complement,
1011    axiom_set_ext_equal,
1012    axiom_set_ext_equal_deep,
1013    axiom_mk_map_domain,
1014    axiom_mk_map_index,
1015    axiom_set_empty_finite,
1016    axiom_set_insert_finite,
1017    axiom_set_remove_finite,
1018    axiom_set_union_finite,
1019    axiom_set_intersect_finite,
1020    axiom_set_difference_finite,
1021    axiom_set_choose_finite,
1022    axiom_set_empty_len,
1023    axiom_set_insert_len,
1024    axiom_set_remove_len,
1025    axiom_set_contains_len,
1026    axiom_set_choose_len,
1027}
1028
1029// Macros
1030#[doc(hidden)]
1031#[macro_export]
1032macro_rules! set_internal {
1033    [$($elem:expr),* $(,)?] => {
1034        $crate::vstd::set::Set::empty()
1035            $(.insert($elem))*
1036    };
1037}
1038
1039#[macro_export]
1040macro_rules! set {
1041    [$($tail:tt)*] => {
1042        ::builtin_macros::verus_proof_macro_exprs!($crate::vstd::set::set_internal!($($tail)*))
1043    };
1044}
1045
1046pub use set_internal;
1047pub use set;
1048
1049} // verus!