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#[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 #[rustc_diagnostic_item = "verus::vstd::set::Set::empty"]
53 pub closed spec fn empty() -> Set<A> {
54 Set { set: |a| false }
55 }
56
57 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 #[rustc_diagnostic_item = "verus::vstd::set::Set::full"]
78 pub open spec fn full() -> Set<A> {
79 Set::empty().complement()
80 }
81
82 #[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 #[verifier::inline]
90 pub open spec fn spec_has(self, a: A) -> bool {
91 self.contains(a)
92 }
93
94 #[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 #[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 #[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 pub closed spec fn union(self, s2: Set<A>) -> Set<A> {
135 Set { set: |a| (self.set)(a) || (s2.set)(a) }
136 }
137
138 #[verifier::inline]
140 pub open spec fn spec_add(self, s2: Set<A>) -> Set<A> {
141 self.union(s2)
142 }
143
144 pub closed spec fn intersect(self, s2: Set<A>) -> Set<A> {
146 Set { set: |a| (self.set)(a) && (s2.set)(a) }
147 }
148
149 #[verifier::inline]
151 pub open spec fn spec_mul(self, s2: Set<A>) -> Set<A> {
152 self.intersect(s2)
153 }
154
155 pub closed spec fn difference(self, s2: Set<A>) -> Set<A> {
157 Set { set: |a| (self.set)(a) && !(s2.set)(a) }
158 }
159
160 #[verifier::inline]
162 pub open spec fn spec_sub(self, s2: Set<A>) -> Set<A> {
163 self.difference(s2)
164 }
165
166 pub closed spec fn complement(self) -> Set<A> {
168 Set { set: |a| !(self.set)(a) }
169 }
170
171 pub open spec fn filter(self, f: spec_fn(A) -> bool) -> Set<A> {
173 self.intersect(Self::new(f))
174 }
175
176 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 pub closed spec fn len(self) -> nat {
188 self.fold(0, |acc: nat, a| acc + 1)
189 }
190
191 pub open spec fn choose(self) -> A {
198 choose|a: A| self.contains(a)
199 }
200
201 pub uninterp spec fn mk_map<V>(self, f: spec_fn(A) -> V) -> Map<A, V>;
204
205 pub open spec fn disjoint(self, s2: Self) -> bool {
208 forall|a: A| self.contains(a) ==> !s2.contains(a)
209 }
210}
211
212spec 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 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 #[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 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 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 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 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 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 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 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 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 assert(fold_graph(z, f, Set::empty(), z, 0)) by {
594 lemma_fold_graph_empty_intro(z, f);
595 };
596 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
631pub broadcast proof fn axiom_set_empty<A>(a: A)
634 ensures
635 !(#[trigger] Set::empty().contains(a)),
636{
637}
638
639pub 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
646pub 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
653pub 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
663pub 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
670pub 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
700pub 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
710pub 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
718pub 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
726pub 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
734pub 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
741pub 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
778pub 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
789pub 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
826pub 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
854pub 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
879pub 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
891pub 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
903pub 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
915pub 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
926pub 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
945pub 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
966pub 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
981pub 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 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#[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}