vstd/
multiset_lib.rs

1#[allow(unused_imports)]
2use super::multiset::Multiset;
3#[allow(unused_imports)]
4use super::prelude::*;
5
6verus! {
7
8broadcast use super::multiset::group_multiset_axioms;
9
10impl<A> Multiset<A> {
11    /// Is `true` if called by an "empty" multiset, i.e., a set containing no elements and has length 0
12    pub open spec fn is_empty(self) -> (b: bool) {
13        self.len() == 0
14    }
15
16    /// A singleton multiset has at least one element with multiplicity 1 and any two elements are equal.
17    pub open spec fn is_singleton(self) -> bool {
18        &&& self.len() > 0
19        &&& (forall|x: A| self.contains(x) ==> self.count(x) == 1)
20        &&& (forall|x: A, y: A| self.contains(x) && self.contains(y) ==> x == y)
21    }
22
23    /// A singleton multiset that contains an alement is equivalent to the singleton multiset with that element.
24    pub proof fn lemma_is_singleton_contains_elem_equal_singleton(self, x: A)
25        requires
26            self.is_singleton(),
27            self.contains(x),
28        ensures
29            self =~= Multiset::singleton(x),
30    {
31        assert forall|y: A| #[trigger] Multiset::singleton(x).count(y) == self.count(y) by {
32            if self.contains(y) {
33            } else {
34            }
35        };
36    }
37
38    /// A singleton multiset has length 1.
39    pub proof fn lemma_singleton_size(self)
40        requires
41            self.is_singleton(),
42        ensures
43            self.len() == 1,
44    {
45        self.lemma_is_singleton_contains_elem_equal_singleton(self.choose());
46    }
47
48    /// A multiset has exactly one element, if and only if, it has at least one element with multiplicity 1 and any two elements are equal.
49    pub proof fn lemma_is_singleton(s: Multiset<A>)
50        ensures
51            s.is_singleton() <==> (s.len() == 1),
52    {
53        if s.is_singleton() {
54            s.lemma_singleton_size();
55        }
56        if s.len() == 1 {
57            assert forall|x: A, y: A| s.contains(x) && s.contains(y) implies x == y by {
58                assert(s.remove(x).len() == 0);
59                if x != y {
60                    assert(s.remove(x).count(y) == 0);
61                    assert(s.remove(x).insert(x) =~= s);
62                }
63            }
64        }
65    }
66}
67
68} // verus!
vstd/multiset_lib.rs

vstd/
multiset_lib.rs
