vstd_extra/
set_extra.rs

1//! Extra properties of [`vstd::set::Set`](https://verus-lang.github.io/verus/verusdoc/vstd/set/struct.Set.html).
2use vstd::{iset::fold::*, prelude::*, set::fold::*, set_lib::*};
3
4verus! {
5
6/// A finite `Set<int>` cannot contain every integer: there always exists
7/// an `int` outside the set. Used to prove the freshness axioms.
8pub proof fn lemma_finite_int_set_has_unused(s: Set<int>)
9    ensures
10        exists|id: int| !s.contains(id),
11{
12    let n = s.len() as int;
13    vstd::set_lib::lemma_int_range(0, n + 1);
14    if forall|i: int| 0 <= i < n + 1 ==> s.contains(i) {
15        assert(Set::range(0, n + 1).subset_of(s)) by {
16            assert forall|i: int| Set::<int>::range(0, n + 1).contains(i) implies s.contains(
17                i,
18            ) by {}
19        }
20        vstd::set_lib::lemma_len_subset(Set::range(0, n + 1), s);
21        assert(false);
22    }
23}
24
25/// If all elements in set `s` does not satisfy the predicate `f`, then the filtered set
26/// is empty.
27pub proof fn lemma_filter_all_false<T>(s: Set<T>, f: spec_fn(T) -> bool)
28    requires
29        s.all(|x: T| !f(x)),
30    ensures
31        s.filter(f).is_empty(),
32{
33}
34
35/// If `x` satisfies the predicate `f` and set `s` does not contain `x`, then first inserting `x` into
36/// the set `s` and then applying the filter is equivalent to applying the filter first and then
37/// inserting `x` into the result.
38pub proof fn lemma_insert_filter_true<T>(s: Set<T>, f: spec_fn(T) -> bool, x: T)
39    requires
40        !s.contains(x),
41        f(x),
42    ensures
43        s.insert(x).filter(f) == s.filter(f).insert(x),
44{
45}
46
47/// If `x` does not satisfy the predicate `f` and set `s` does not contain `x`, then first inserting `x` into
48/// the set `s` and then applying the filter is equivalent to directly applying the filter to the original set `s`.
49pub proof fn lemma_insert_filter_false<T>(s: Set<T>, f: spec_fn(T) -> bool, x: T)
50    requires
51        !s.contains(x),
52        !f(x),
53    ensures
54        s.insert(x).filter(f) == s.filter(f),
55{
56}
57
58/// If `x` satisfies the predicate `f` and set `s` contains `x`, then first removing `x` from
59/// the set `s` and then applying the filter is equivalent to applying the filter first and then
60/// removing `x` from the result.
61pub proof fn lemma_remove_filter_true<T>(s: Set<T>, f: spec_fn(T) -> bool, x: T)
62    requires
63        s.contains(x),
64        f(x),
65    ensures
66        s.remove(x).filter(f) == s.filter(f).remove(x),
67{
68}
69
70/// The length of a set of natural numbers between `l` and `r` equals `r - l`.
71pub proof fn lemma_nat_range_finite(l: nat, r: nat)
72    requires
73        l <= r,
74    ensures
75        Set::<nat>::range(l, r).len() == (r - l) as nat,
76{
77    broadcast use vstd::set_lib::range_set_properties;
78
79}
80
81/// A finite set can be separated by a predicate into two disjoint sets.
82pub proof fn lemma_set_separation<T>(s: Set<T>, f: spec_fn(T) -> bool)
83    ensures
84        #![trigger s.filter(f)]
85        s.filter(f).disjoint(s.filter(|x| !f(x))),
86        s == s.filter(f) + s.filter(|x| !f(x)),
87        s.filter(f).len() + s.filter(|x| !f(x)).len() == s.len(),
88    decreases s.len(),
89{
90    if s.is_empty() {
91        assert(s.filter(f) == Set::<T>::empty());
92        assert(s.filter(|x| !f(x)) == Set::<T>::empty());
93    } else {
94        let x = s.choose();
95        lemma_set_separation(s.remove(x), f);
96        if f(x) {
97            assert(s.filter(f) == s.remove(x).filter(f).insert(x));
98            assert(s.filter(|x| !f(x)) == s.remove(x).filter(|x| !f(x)));
99        } else {
100            assert(s.filter(f) == s.remove(x).filter(f));
101            assert(s.filter(|x| !f(x)) == s.remove(x).filter(|x| !f(x)).insert(x));
102        }
103    }
104}
105
106/// If the length of the filtered set is equal to the length of the original set,
107/// then the filtered set is equal to the original set.
108pub proof fn lemma_filter_len_unchanged_implies_equal<T>(s: Set<T>, f: spec_fn(T) -> bool)
109    requires
110        s.filter(f).len() == s.len(),
111    ensures
112        s.filter(f) == s,
113{
114    lemma_set_separation(s, f)
115}
116
117/// If no element in set `s` fails the predicate `q`, then all elements in `s` satisfy `q`.
118pub proof fn lemma_empty_bad_set_implies_forall<T>(s: Set<T>, q: spec_fn(T) -> bool)
119    requires
120        s.filter(|x| !q(x)).is_empty(),
121    ensures
122        forall|x: T| #[trigger] s.contains(x) ==> q(x),
123{
124    assert forall|x: T| #[trigger] s.contains(x) implies q(x) by {
125        if !q(x) {
126            assert(s.filter(|x| !q(x)).contains(x));
127        };
128    }
129}
130
131/// If all elements in the set `s` satisfy predicate `q` (i.e., the filtered set has the same length),
132/// then every element of `s` satisfies `q`.
133pub proof fn lemma_full_good_set_implies_forall<T>(s: Set<T>, q: spec_fn(T) -> bool)
134    requires
135        s.len() == s.filter(q).len(),
136    ensures
137        forall|x: T| #[trigger] s.contains(x) ==> q(x),
138{
139    lemma_set_separation(s, q);
140    assert forall|x: T| #[trigger] s.contains(x) implies q(x) by {
141        if !q(x) {
142            assert(s.filter(|x| !q(x)).contains(x));
143        };
144    }
145}
146
147/// A set of sets is pairwise disjoint if all distinct sets are disjoint.
148pub open spec fn pairwise_disjoint<A>(sets: Set<Set<A>>) -> bool {
149    forall|s1: Set<A>, s2: Set<A>|
150        #![trigger sets.contains(s1), sets.contains(s2)]
151        sets.contains(s1) && sets.contains(s2) && s1 != s2 ==> s1.disjoint(s2)
152}
153
154pub open spec fn is_partition<A>(s: Set<A>, parts: Set<Set<A>>) -> bool {
155    // Each part is non-empty and subset of s
156    forall|part: Set<A>| #[trigger]
157        parts.contains(part) ==> !part.is_empty() && part <= s
158            &&
159        // Parts are pairwise disjoint
160        pairwise_disjoint(parts) &&
161        // Union of parts is s
162        s == parts.flatten()
163}
164
165/// If `parts` is a finite set of finite, pairwise-disjoint sets,
166/// then the cardinality of the union is the sum of cardinalities.
167pub proof fn lemma_flatten_cardinality_under_disjointness<A>(parts: Set<Set<A>>)
168    requires
169        pairwise_disjoint(parts),
170    ensures
171        parts.flatten().len() == parts.fold(0nat, |acc: nat, p: Set<A>| acc + p.len()),
172    decreases parts.len(),
173{
174    if parts.is_empty() {
175        assert(parts.flatten() == Set::<A>::empty());
176        assert(parts.to_iset() == ISet::empty());
177        lemma_fold_empty(0nat, |acc: nat, p: Set<A>| acc + p.len());
178    } else {
179        let p = parts.choose();
180        let rest = parts.remove(p);
181        assert(parts == rest.insert(p));
182        lemma_flatten_cardinality_under_disjointness(rest);
183        assert(rest.flatten().len() == rest.fold(0nat, |acc: nat, p: Set<A>| acc + p.len()));
184        assert(parts.flatten() == rest.flatten().union(p));
185        assert(parts.flatten().len() == rest.flatten().len() + p.len()) by {
186            lemma_set_disjoint_lens(rest.flatten(), p);
187        }
188        assert(parts.to_iset() == rest.to_iset().insert(p));
189        lemma_fold_insert(rest.to_iset(), 0nat, |acc: nat, p: Set<A>| acc + p.len(), p);
190    }
191}
192
193/// If `parts` is a finite set of finite, pairwise-disjoint sets, and each set has the same length `c`,
194/// then the cardinality of the union is the product of the number of sets and `c`.
195pub proof fn lemma_flatten_cardinality_under_disjointness_same_length<A>(parts: Set<Set<A>>, c: nat)
196    requires
197        pairwise_disjoint(parts),
198        parts.all(|p: Set<A>| p.len() == c),
199    ensures
200        parts.flatten().len() == parts.len() * c,
201    decreases parts.len(),
202{
203    if parts.is_empty() {
204        assert(parts.flatten() == Set::<A>::empty());
205    } else {
206        let p = parts.choose();
207        let rest = parts.remove(p);
208        assert(parts == rest.insert(p));
209        lemma_flatten_cardinality_under_disjointness_same_length(rest, c);
210        assert(parts.flatten() == rest.flatten().union(p));
211        assert(parts.flatten().len() == rest.flatten().len() + p.len()) by {
212            lemma_set_disjoint_lens(rest.flatten(), p);
213        }
214        assert(parts.flatten().len() == (rest.len() + 1) * c) by (nonlinear_arith)
215            requires
216                parts.flatten().len() == rest.len() * c + c,
217        ;
218    }
219}
220
221pub open spec fn set_prop_mutual_exclusion<A>(s: Set<A>, f: spec_fn(A) -> bool) -> bool {
222    forall|x: A, y: A| #[trigger]
223        s.contains(x) && #[trigger] s.contains(y) && x != y ==> !(f(x) && f(y))
224}
225
226proof fn lemma_set_prop_mutual_exclusion_internal<A>(s: Set<A>, f: spec_fn(A) -> bool)
227    requires
228        set_prop_mutual_exclusion(s, f),
229    ensures
230        s.filter(f).len() <= 1,
231    decreases s.len(),
232{
233    if s.len() == 0 {
234        assert(s.filter(f).is_empty());
235    } else {
236        let x = s.choose();
237        lemma_set_prop_mutual_exclusion_internal(s.remove(x), f);
238        if s.remove(x).filter(f).len() == 0 {
239            if f(x) {
240                assert(s.filter(f) == s.remove(x).filter(f).insert(x));
241            } else {
242                assert(s.filter(f) == s.remove(x).filter(f));
243            }
244        } else {
245            let a = s.remove(x).filter(f).choose();
246            assert(s.remove(x).filter(f).contains(a));
247            assert(s.filter(f) == s.remove(x).filter(f));
248        }
249    }
250}
251
252pub proof fn lemma_set_prop_mutual_exclusion<A>(s: Set<A>, f: spec_fn(A) -> bool)
253    ensures
254        set_prop_mutual_exclusion(s, f) <==> s.filter(f).len() <= 1,
255{
256    if set_prop_mutual_exclusion(s, f) {
257        lemma_set_prop_mutual_exclusion_internal(s, f);
258    }
259    if s.filter(f).len() <= 1 {
260        assert forall|x: A, y: A| #[trigger]
261            s.contains(x) && #[trigger] s.contains(y) && x != y implies !(f(x) && f(y)) by {
262            if f(x) && f(y) {
263                assert(s.filter(f).contains(x));
264                assert(s.filter(f).contains(y));
265                if s.filter(f).len() == 1 {
266                    Set::lemma_is_singleton(s.filter(f));
267                }
268            }
269        };
270    }
271}
272
273} // verus!
vstd_extra/set_extra.rs

vstd_extra/
set_extra.rs
