1#[allow(unused_imports)]
2use super::calc_macro::*;
3#[allow(unused_imports)]
4use super::multiset::Multiset;
5#[allow(unused_imports)]
6use super::pervasive::*;
7#[allow(unused_imports)]
8use super::prelude::*;
9#[allow(unused_imports)]
10use super::relations::*;
11#[allow(unused_imports)]
12use super::seq::*;
13#[allow(unused_imports)]
14use super::set::Set;
15
16verus! {
17
18broadcast use group_seq_axioms;
19
20impl<A> Seq<A> {
21 pub open spec fn map<B>(self, f: spec_fn(int, A) -> B) -> Seq<B> {
26 Seq::new(self.len(), |i: int| f(i, self[i]))
27 }
28
29 pub open spec fn map_values<B>(self, f: spec_fn(A) -> B) -> Seq<B> {
33 Seq::new(self.len(), |i: int| f(self[i]))
34 }
35
36 pub open spec fn flat_map<B>(self, f: spec_fn(A) -> Seq<B>) -> Seq<B> {
50 self.map_values(f).flatten()
51 }
52
53 pub open spec fn is_prefix_of(self, other: Self) -> bool {
65 self.len() <= other.len() && self =~= other.subrange(0, self.len() as int)
66 }
67
68 pub open spec fn is_suffix_of(self, other: Self) -> bool {
80 self.len() <= other.len() && self =~= other.subrange(
81 (other.len() - self.len()) as int,
82 other.len() as int,
83 )
84 }
85
86 pub closed spec fn sort_by(self, leq: spec_fn(A, A) -> bool) -> Seq<A>
94 recommends
95 total_ordering(leq),
96 decreases self.len(),
97 {
98 if self.len() <= 1 {
99 self
100 } else {
101 let split_index = self.len() / 2;
102 let left = self.subrange(0, split_index as int);
103 let right = self.subrange(split_index as int, self.len() as int);
104 let left_sorted = left.sort_by(leq);
105 let right_sorted = right.sort_by(leq);
106 merge_sorted_with(left_sorted, right_sorted, leq)
107 }
108 }
109
110 pub open spec fn all(self, pred: spec_fn(A) -> bool) -> bool {
121 forall|i: int| 0 <= i < self.len() ==> #[trigger] pred(self[i])
122 }
123
124 pub open spec fn any(self, pred: spec_fn(A) -> bool) -> bool {
135 exists|i: int| 0 <= i < self.len() && #[trigger] pred(self[i])
136 }
137
138 pub open spec fn exactly_one(self, pred: spec_fn(A) -> bool) -> bool {
148 self.filter(pred).len() == 1
149 }
150
151 pub proof fn lemma_sort_by_ensures(self, leq: spec_fn(A, A) -> bool)
152 requires
153 total_ordering(leq),
154 ensures
155 self.to_multiset() =~= self.sort_by(leq).to_multiset(),
156 sorted_by(self.sort_by(leq), leq),
157 forall|x: A| !self.contains(x) ==> !(#[trigger] self.sort_by(leq).contains(x)),
158 decreases self.len(),
159 {
160 if self.len() <= 1 {
161 } else {
162 let split_index = self.len() / 2;
163 let left = self.subrange(0, split_index as int);
164 let right = self.subrange(split_index as int, self.len() as int);
165 assert(self =~= left + right);
166 let left_sorted = left.sort_by(leq);
167 left.lemma_sort_by_ensures(leq);
168 let right_sorted = right.sort_by(leq);
169 right.lemma_sort_by_ensures(leq);
170 lemma_merge_sorted_with_ensures(left_sorted, right_sorted, leq);
171 lemma_multiset_commutative(left, right);
172 lemma_multiset_commutative(left_sorted, right_sorted);
173 assert forall|x: A| !self.contains(x) implies !(#[trigger] self.sort_by(leq).contains(
174 x,
175 )) by {
176 broadcast use group_to_multiset_ensures;
177
178 assert(!self.contains(x) ==> self.to_multiset().count(x) == 0);
179 }
180 }
181 }
182
183 #[verifier::opaque]
197 pub open spec fn filter(self, pred: spec_fn(A) -> bool) -> Self
198 decreases self.len(),
199 {
200 if self.len() == 0 {
201 self
202 } else {
203 let subseq = self.drop_last().filter(pred);
204 if pred(self.last()) {
205 subseq.push(self.last())
206 } else {
207 subseq
208 }
209 }
210 }
211
212 pub broadcast proof fn lemma_filter_len(self, pred: spec_fn(A) -> bool)
213 ensures
214 #[trigger] self.filter(pred).len() <= self.len(),
217 decreases self.len(),
218 {
219 reveal(Seq::filter);
220 let out = self.filter(pred);
221 if 0 < self.len() {
222 self.drop_last().lemma_filter_len(pred);
223 }
224 }
225
226 pub broadcast proof fn lemma_filter_pred(self, pred: spec_fn(A) -> bool, i: int)
227 requires
228 0 <= i < self.filter(pred).len(),
229 ensures
230 pred(#[trigger] self.filter(pred)[i]),
231 {
232 #[allow(deprecated)]
234 self.filter_lemma(pred);
235 }
236
237 pub broadcast proof fn lemma_filter_contains(self, pred: spec_fn(A) -> bool, i: int)
238 requires
239 0 <= i < self.len() && pred(self[i]),
240 ensures
241 #[trigger] self.filter(pred).contains(self[i]),
242 {
243 #[allow(deprecated)]
245 self.filter_lemma(pred);
246 }
247
248 #[deprecated = "Use `broadcast use group_filter_ensures` instead" ]
250 pub proof fn filter_lemma(self, pred: spec_fn(A) -> bool)
251 ensures
252 forall|i: int|
258 0 <= i < self.filter(pred).len() ==> pred(#[trigger] self.filter(pred)[i]),
259 forall|i: int|
261 0 <= i < self.len() && pred(self[i]) ==> #[trigger] self.filter(pred).contains(
262 self[i],
263 ),
264 #[trigger] self.filter(pred).len() <= self.len(),
266 decreases self.len(),
267 {
268 reveal(Seq::filter);
269 let out = self.filter(pred);
270 if 0 < self.len() {
271 self.drop_last().filter_lemma(pred);
272 assert forall|i: int| 0 <= i < out.len() implies pred(out[i]) by {
273 if i < out.len() - 1 {
274 assert(self.drop_last().filter(pred)[i] == out.drop_last()[i]); assert(pred(out[i])); }
277 }
278 assert forall|i: int|
279 0 <= i < self.len() && pred(self[i]) implies #[trigger] out.contains(self[i]) by {
280 if i == self.len() - 1 {
281 assert(self[i] == out[out.len() - 1]); } else {
283 let subseq = self.drop_last().filter(pred);
284 assert(subseq.contains(self.drop_last()[i])); let j = choose|j| 0 <= j < subseq.len() && subseq[j] == self[i];
286 assert(out[j] == self[i]); }
288 }
289 }
290 }
291
292 pub broadcast proof fn filter_distributes_over_add(a: Self, b: Self, pred: spec_fn(A) -> bool)
293 ensures
294 #[trigger] (a + b).filter(pred) == a.filter(pred) + b.filter(pred),
295 decreases b.len(),
296 {
297 reveal(Seq::filter);
298 if 0 < b.len() {
299 Self::drop_last_distributes_over_add(a, b);
300 Self::filter_distributes_over_add(a, b.drop_last(), pred);
301 if pred(b.last()) {
302 Self::push_distributes_over_add(
303 a.filter(pred),
304 b.drop_last().filter(pred),
305 b.last(),
306 );
307 }
308 } else {
309 Self::add_empty_right(a, b);
310 Self::add_empty_right(a.filter(pred), b.filter(pred));
311 }
312 }
313
314 pub broadcast proof fn add_empty_left(a: Self, b: Self)
315 requires
316 a.len() == 0,
317 ensures
318 #[trigger] (a + b) == b,
319 {
320 assert(a + b =~= b);
321 }
322
323 pub broadcast proof fn add_empty_right(a: Self, b: Self)
324 requires
325 b.len() == 0,
326 ensures
327 #[trigger] (a + b) == a,
328 {
329 assert(a + b =~= a);
330 }
331
332 pub broadcast proof fn push_distributes_over_add(a: Self, b: Self, elt: A)
333 ensures
334 #[trigger] (a + b).push(elt) == a + b.push(elt),
335 {
336 assert((a + b).push(elt) =~= a + b.push(elt));
337 }
338
339 pub open spec fn max_via(self, leq: spec_fn(A, A) -> bool) -> A
341 recommends
342 self.len() > 0,
343 decreases self.len(),
344 {
345 if self.len() > 1 {
346 if leq(self[0], self.subrange(1, self.len() as int).max_via(leq)) {
347 self.subrange(1, self.len() as int).max_via(leq)
348 } else {
349 self[0]
350 }
351 } else {
352 self[0]
353 }
354 }
355
356 pub open spec fn min_via(self, leq: spec_fn(A, A) -> bool) -> A
358 recommends
359 self.len() > 0,
360 decreases self.len(),
361 {
362 if self.len() > 1 {
363 let subseq = self.subrange(1, self.len() as int);
364 let elt = subseq.min_via(leq);
365 if leq(elt, self[0]) {
366 elt
367 } else {
368 self[0]
369 }
370 } else {
371 self[0]
372 }
373 }
374
375 pub open spec fn contains(self, needle: A) -> bool {
377 exists|i: int| 0 <= i < self.len() && self[i] == needle
378 }
379
380 pub open spec fn index_of(self, needle: A) -> int {
383 choose|i: int| 0 <= i < self.len() && self[i] == needle
384 }
385
386 pub closed spec fn index_of_first(self, needle: A) -> (result: Option<int>) {
389 if self.contains(needle) {
390 Some(self.first_index_helper(needle))
391 } else {
392 None
393 }
394 }
395
396 spec fn first_index_helper(self, needle: A) -> int
398 recommends
399 self.contains(needle),
400 decreases self.len(),
401 {
402 if self.len() <= 0 {
403 -1 } else if self[0] == needle {
406 0
407 } else {
408 1 + self.subrange(1, self.len() as int).first_index_helper(needle)
409 }
410 }
411
412 pub proof fn index_of_first_ensures(self, needle: A)
413 ensures
414 match self.index_of_first(needle) {
415 Some(index) => {
416 &&& self.contains(needle)
417 &&& 0 <= index < self.len()
418 &&& self[index] == needle
419 &&& forall|j: int| 0 <= j < index < self.len() ==> self[j] != needle
420 },
421 None => { !self.contains(needle) },
422 },
423 decreases self.len(),
424 {
425 if self.contains(needle) {
426 let index = self.index_of_first(needle).unwrap();
427 if self.len() <= 0 {
428 } else if self[0] == needle {
429 } else {
430 assert(Seq::empty().push(self.first()).add(self.drop_first()) =~= self);
431 self.drop_first().index_of_first_ensures(needle);
432 }
433 }
434 }
435
436 pub closed spec fn index_of_last(self, needle: A) -> Option<int> {
439 if self.contains(needle) {
440 Some(self.last_index_helper(needle))
441 } else {
442 None
443 }
444 }
445
446 spec fn last_index_helper(self, needle: A) -> int
448 recommends
449 self.contains(needle),
450 decreases self.len(),
451 {
452 if self.len() <= 0 {
453 -1 } else if self.last() == needle {
456 self.len() - 1
457 } else {
458 self.drop_last().last_index_helper(needle)
459 }
460 }
461
462 pub proof fn index_of_last_ensures(self, needle: A)
463 ensures
464 match self.index_of_last(needle) {
465 Some(index) => {
466 &&& self.contains(needle)
467 &&& 0 <= index < self.len()
468 &&& self[index] == needle
469 &&& forall|j: int| 0 <= index < j < self.len() ==> self[j] != needle
470 },
471 None => { !self.contains(needle) },
472 },
473 decreases self.len(),
474 {
475 if self.contains(needle) {
476 let index = self.index_of_last(needle).unwrap();
477 if self.len() <= 0 {
478 } else if self.last() == needle {
479 } else {
480 assert(self.drop_last().push(self.last()) =~= self);
481 self.drop_last().index_of_last_ensures(needle);
482 }
483 }
484 }
485
486 pub open spec fn drop_last(self) -> Seq<A>
491 recommends
492 self.len() >= 1,
493 {
494 self.subrange(0, self.len() as int - 1)
495 }
496
497 pub proof fn drop_last_distributes_over_add(a: Self, b: Self)
500 requires
501 0 < b.len(),
502 ensures
503 (a + b).drop_last() == a + b.drop_last(),
504 {
505 assert_seqs_equal!((a+b).drop_last(), a+b.drop_last());
506 }
507
508 pub open spec fn drop_first(self) -> Seq<A>
509 recommends
510 self.len() >= 1,
511 {
512 self.subrange(1, self.len() as int)
513 }
514
515 pub open spec fn no_duplicates(self) -> bool {
517 forall|i, j| (0 <= i < self.len() && 0 <= j < self.len() && i != j) ==> self[i] != self[j]
518 }
519
520 pub open spec fn disjoint(self, other: Self) -> bool {
522 forall|i: int, j: int| 0 <= i < self.len() && 0 <= j < other.len() ==> self[i] != other[j]
523 }
524
525 pub open spec fn to_set(self) -> Set<A> {
527 Set::new(|a: A| self.contains(a))
528 }
529
530 pub closed spec fn to_multiset(self) -> Multiset<A>
532 decreases self.len(),
533 {
534 if self.len() == 0 {
535 Multiset::<A>::empty()
536 } else {
537 Multiset::<A>::empty().insert(self.first()).add(self.drop_first().to_multiset())
538 }
539 }
540
541 pub broadcast proof fn to_multiset_ensures(self)
545 ensures
546 forall|a: A| #[trigger] (self.push(a).to_multiset()) =~= self.to_multiset().insert(a), forall|i: int|
548 0 <= i < self.len() ==> #[trigger] (self.remove(i).to_multiset())
549 =~= self.to_multiset().remove(self[i]), self.len() == #[trigger] self.to_multiset().len(), forall|a: A|
552 self.contains(a) <==> #[trigger] self.to_multiset().count(a)
553 > 0, {
555 broadcast use group_seq_properties;
556
557 }
558
559 pub open spec fn insert(self, i: int, a: A) -> Seq<A>
561 recommends
562 0 <= i <= self.len(),
563 {
564 self.subrange(0, i).push(a) + self.subrange(i, self.len() as int)
565 }
566
567 pub proof fn insert_ensures(self, pos: int, elt: A)
569 requires
570 0 <= pos <= self.len(),
571 ensures
572 self.insert(pos, elt).len() == self.len() + 1,
573 forall|i: int| 0 <= i < pos ==> #[trigger] self.insert(pos, elt)[i] == self[i],
574 forall|i: int| pos <= i < self.len() ==> self.insert(pos, elt)[i + 1] == self[i],
575 self.insert(pos, elt)[pos] == elt,
576 {
577 }
578
579 pub open spec fn remove(self, i: int) -> Seq<A>
581 recommends
582 0 <= i < self.len(),
583 {
584 self.subrange(0, i) + self.subrange(i + 1, self.len() as int)
585 }
586
587 pub proof fn remove_ensures(self, i: int)
589 requires
590 0 <= i < self.len(),
591 ensures
592 self.remove(i).len() == self.len() - 1,
593 forall|index: int| 0 <= index < i ==> #[trigger] self.remove(i)[index] == self[index],
594 forall|index: int|
595 i <= index < self.len() - 1 ==> #[trigger] self.remove(i)[index] == self[index + 1],
596 {
597 }
598
599 pub open spec fn remove_value(self, val: A) -> Seq<A> {
602 let index = self.index_of_first(val);
603 match index {
604 Some(i) => self.remove(i),
605 None => self,
606 }
607 }
608
609 pub open spec fn reverse(self) -> Seq<A>
611 decreases self.len(),
612 {
613 if self.len() == 0 {
614 Seq::empty()
615 } else {
616 Seq::new(self.len(), |i: int| self[self.len() - 1 - i])
617 }
618 }
619
620 pub open spec fn zip_with<B>(self, other: Seq<B>) -> Seq<(A, B)>
623 recommends
624 self.len() == other.len(),
625 decreases self.len(),
626 {
627 if self.len() != other.len() {
628 Seq::empty()
629 } else if self.len() == 0 {
630 Seq::empty()
631 } else {
632 Seq::new(self.len(), |i: int| (self[i], other[i]))
633 }
634 }
635
636 pub open spec fn fold_left<B>(self, b: B, f: spec_fn(B, A) -> B) -> (res: B)
643 decreases self.len(),
644 {
645 if self.len() == 0 {
646 b
647 } else {
648 f(self.drop_last().fold_left(b, f), self.last())
649 }
650 }
651
652 pub open spec fn fold_left_alt<B>(self, b: B, f: spec_fn(B, A) -> B) -> (res: B)
656 decreases self.len(),
657 {
658 if self.len() == 0 {
659 b
660 } else {
661 self.subrange(1, self.len() as int).fold_left_alt(f(b, self[0]), f)
662 }
663 }
664
665 pub broadcast proof fn lemma_fold_left_split<B>(self, b: B, f: spec_fn(B, A) -> B, k: int)
667 requires
668 0 <= k <= self.len(),
669 ensures
670 self.subrange(k, self.len() as int).fold_left(
671 (#[trigger] self.subrange(0, k).fold_left(b, f)),
672 f,
673 ) == self.fold_left(b, f),
674 decreases self.len(),
675 {
676 reveal_with_fuel(Seq::fold_left, 2);
677 if k == self.len() {
678 assert(self.subrange(0, self.len() as int) == self);
679 } else {
680 self.drop_last().lemma_fold_left_split(b, f, k);
681 assert_seqs_equal!(
682 self.drop_last().subrange(k, self.drop_last().len() as int) ==
683 self.subrange(k, self.len()-1)
684 );
685 assert_seqs_equal!(
686 self.drop_last().subrange(0, k) ==
687 self.subrange(0, k)
688 );
689 assert_seqs_equal!(
690 self.subrange(k, self.len() as int).drop_last() ==
691 self.subrange(k, self.len() - 1)
692 );
693 }
694 }
695
696 proof fn aux_lemma_fold_left_alt<B>(self, b: B, f: spec_fn(B, A) -> B, k: int)
698 requires
699 0 < k <= self.len(),
700 ensures
701 self.subrange(k, self.len() as int).fold_left_alt(
702 self.subrange(0, k).fold_left_alt(b, f),
703 f,
704 ) == self.fold_left_alt(b, f),
705 decreases k,
706 {
707 reveal_with_fuel(Seq::fold_left_alt, 2);
708 if k == 1 {
709 } else {
711 self.subrange(1, self.len() as int).aux_lemma_fold_left_alt(f(b, self[0]), f, k - 1);
712 assert_seqs_equal!(
713 self.subrange(1, self.len() as int)
714 .subrange(k - 1, self.subrange(1, self.len() as int).len() as int) ==
715 self.subrange(k, self.len() as int)
716 );
717 assert_seqs_equal!(
718 self.subrange(1, self.len() as int).subrange(0, k - 1) ==
719 self.subrange(1, k)
720 );
721 assert_seqs_equal!(
722 self.subrange(0, k).subrange(1, self.subrange(0, k).len() as int) ==
723 self.subrange(1, k)
724 );
725 }
726 }
727
728 pub proof fn lemma_fold_left_alt<B>(self, b: B, f: spec_fn(B, A) -> B)
730 ensures
731 self.fold_left(b, f) == self.fold_left_alt(b, f),
732 decreases self.len(),
733 {
734 reveal_with_fuel(Seq::fold_left, 2);
735 reveal_with_fuel(Seq::fold_left_alt, 2);
736 if self.len() <= 1 {
737 } else {
739 self.aux_lemma_fold_left_alt(b, f, self.len() - 1);
740 self.subrange(self.len() - 1, self.len() as int).lemma_fold_left_alt(
741 self.drop_last().fold_left_alt(b, f),
742 f,
743 );
744 self.subrange(0, self.len() - 1).lemma_fold_left_alt(b, f);
745 }
746 }
747
748 pub proof fn lemma_reverse_fold_left<B>(self, v: B, f: spec_fn(B, A) -> B)
751 ensures
752 self.reverse().fold_left(v, f) == self.fold_right(|a: A, b: B| f(b, a), v),
753 {
754 assert(self.reverse().reverse() =~= self);
755 let g = |a: A, b: B| f(b, a);
756 assert(f =~= |b: B, a: A| g(a, b));
757 self.reverse().lemma_reverse_fold_right(v, |a: A, b: B| f(b, a))
758 }
759
760 pub open spec fn fold_right<B>(self, f: spec_fn(A, B) -> B, b: B) -> (res: B)
767 decreases self.len(),
768 {
769 if self.len() == 0 {
770 b
771 } else {
772 self.drop_last().fold_right(f, f(self.last(), b))
773 }
774 }
775
776 pub open spec fn fold_right_alt<B>(self, f: spec_fn(A, B) -> B, b: B) -> (res: B)
780 decreases self.len(),
781 {
782 if self.len() == 0 {
783 b
784 } else {
785 f(self[0], self.subrange(1, self.len() as int).fold_right_alt(f, b))
786 }
787 }
788
789 pub broadcast proof fn lemma_fold_right_split<B>(self, f: spec_fn(A, B) -> B, b: B, k: int)
791 requires
792 0 <= k <= self.len(),
793 ensures
794 self.subrange(0, k).fold_right(
795 f,
796 (#[trigger] self.subrange(k, self.len() as int).fold_right(f, b)),
797 ) == self.fold_right(f, b),
798 decreases self.len(),
799 {
800 reveal_with_fuel(Seq::fold_right, 2);
801 if k == self.len() {
802 assert(self.subrange(0, k) == self);
803 } else if k == self.len() - 1 {
804 } else {
806 self.subrange(0, self.len() - 1).lemma_fold_right_split(f, f(self.last(), b), k);
807 assert_seqs_equal!(
808 self.subrange(0, self.len() - 1).subrange(0, k) ==
809 self.subrange(0, k)
810 );
811 assert_seqs_equal!(
812 self.subrange(0, self.len() - 1).subrange(k, self.subrange(0, self.len() - 1).len() as int) ==
813 self.subrange(k, self.len() - 1)
814 );
815 assert_seqs_equal!(
816 self.subrange(k, self.len() as int).drop_last() ==
817 self.subrange(k, self.len() - 1)
818 );
819 }
820 }
821
822 pub proof fn lemma_fold_right_commute_one<B>(self, a: A, f: spec_fn(A, B) -> B, v: B)
824 requires
825 commutative_foldr(f),
826 ensures
827 self.fold_right(f, f(a, v)) == f(a, self.fold_right(f, v)),
828 decreases self.len(),
829 {
830 if self.len() > 0 {
831 self.drop_last().lemma_fold_right_commute_one(a, f, f(self.last(), v));
832 }
833 }
834
835 pub proof fn lemma_fold_right_alt<B>(self, f: spec_fn(A, B) -> B, b: B)
837 ensures
838 self.fold_right(f, b) == self.fold_right_alt(f, b),
839 decreases self.len(),
840 {
841 reveal_with_fuel(Seq::fold_right, 2);
842 reveal_with_fuel(Seq::fold_right_alt, 2);
843 if self.len() <= 1 {
844 } else {
846 self.subrange(1, self.len() as int).lemma_fold_right_alt(f, b);
847 self.lemma_fold_right_split(f, b, 1);
848 }
849 }
850
851 pub proof fn lemma_reverse_fold_right<B>(self, v: B, f: spec_fn(A, B) -> B)
854 ensures
855 self.reverse().fold_right(f, v) == self.fold_left(v, |b: B, a: A| f(a, b)),
856 decreases self.len(),
857 {
858 let g = |b: B, a: A| f(a, b);
859 if self.len() > 0 {
860 let last = self.last();
861 let s0 = self.drop_last();
862 assert(self.reverse() =~= seq![last] + s0.reverse());
863 let res1 = self.reverse().fold_right(f, v);
864 let res2 = self.fold_left(v, g);
865 assert(res1 == self.reverse().fold_right_alt(f, v)) by {
866 self.reverse().lemma_fold_right_alt(f, v)
867 }
868 assert(res2 == g(s0.fold_left(v, g), last));
869 assert(self.reverse().first() == last);
870 assert(self.reverse().subrange(1, self.reverse().len() as int) =~= s0.reverse());
871 assert(res1 == f(last, s0.reverse().fold_right_alt(f, v)));
872 assert(res1 == f(last, s0.reverse().fold_right(f, v))) by {
873 s0.reverse().lemma_fold_right_alt(f, v)
874 }
875 assert(res2 == g(s0.fold_left(v, g), last));
876 s0.lemma_reverse_fold_right(v, f);
877 }
878 }
879
880 pub proof fn lemma_multiset_has_no_duplicates(self)
884 requires
885 self.no_duplicates(),
886 ensures
887 forall|x: A| self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1,
888 decreases self.len(),
889 {
890 broadcast use super::multiset::group_multiset_axioms;
891
892 if self.len() == 0 {
893 assert(forall|x: A|
894 self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1);
895 } else {
896 broadcast use group_seq_properties;
897
898 assert(self.drop_last().push(self.last()) =~= self);
899 self.drop_last().lemma_multiset_has_no_duplicates();
900 }
901 }
902
903 pub proof fn lemma_multiset_has_no_duplicates_conv(self)
906 requires
907 forall|x: A| self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1,
908 ensures
909 self.no_duplicates(),
910 {
911 broadcast use super::multiset::group_multiset_axioms;
912
913 assert forall|i, j| (0 <= i < self.len() && 0 <= j < self.len() && i != j) implies self[i]
914 != self[j] by {
915 let mut a = if (i < j) {
916 i
917 } else {
918 j
919 };
920 let mut b = if (i < j) {
921 j
922 } else {
923 i
924 };
925
926 if (self[a] == self[b]) {
927 let s0 = self.subrange(0, b);
928 let s1 = self.subrange(b, self.len() as int);
929 assert(self == s0 + s1);
930
931 broadcast use group_to_multiset_ensures;
932
933 lemma_multiset_commutative(s0, s1);
934 assert(self.to_multiset().count(self[a]) >= 2);
935 }
936 }
937 }
938
939 pub proof fn lemma_reverse_to_multiset(self)
941 ensures
942 self.reverse().to_multiset() =~= self.to_multiset(),
943 decreases self.len(),
944 {
945 broadcast use group_seq_properties;
946 broadcast use super::multiset::group_multiset_axioms;
947
948 if self.len() > 0 {
949 let s2 = self.drop_first();
950 let e = self.first();
951 assert(self =~= seq![e] + s2);
952 assert(self.to_multiset() =~= seq![e].to_multiset().add(s2.to_multiset())) by {
953 lemma_multiset_commutative(seq![e], s2)
954 }
955 assert(self.reverse() =~= s2.reverse().push(e));
956 assert(self.reverse().to_multiset() =~= s2.reverse().to_multiset().insert(e));
957 s2.lemma_reverse_to_multiset();
958 }
959 }
960
961 pub proof fn lemma_add_last_back(self)
965 requires
966 0 < self.len(),
967 ensures
968 #[trigger] self.drop_last().push(self.last()) =~= self,
969 {
970 }
971
972 pub proof fn lemma_indexing_implies_membership(self, f: spec_fn(A) -> bool)
977 requires
978 forall|i: int| 0 <= i < self.len() ==> #[trigger] f(#[trigger] self[i]),
979 ensures
980 forall|x: A| #[trigger] self.contains(x) ==> #[trigger] f(x),
981 {
982 assert(forall|i: int| 0 <= i < self.len() ==> #[trigger] self.contains(self[i]));
983 }
984
985 pub proof fn lemma_membership_implies_indexing(self, f: spec_fn(A) -> bool)
990 requires
991 forall|x: A| #[trigger] self.contains(x) ==> #[trigger] f(x),
992 ensures
993 forall|i: int| 0 <= i < self.len() ==> #[trigger] f(self[i]),
994 {
995 assert forall|i: int| 0 <= i < self.len() implies #[trigger] f(self[i]) by {
996 assert(self.contains(self[i]));
997 }
998 }
999
1000 pub proof fn lemma_split_at(self, pos: int)
1004 requires
1005 0 <= pos <= self.len(),
1006 ensures
1007 self.subrange(0, pos) + self.subrange(pos, self.len() as int) =~= self,
1008 {
1009 }
1010
1011 pub proof fn lemma_element_from_slice(self, new: Seq<A>, a: int, b: int, pos: int)
1013 requires
1014 0 <= a <= b <= self.len(),
1015 new == self.subrange(a, b),
1016 a <= pos < b,
1017 ensures
1018 pos - a < new.len(),
1019 new[pos - a] == self[pos],
1020 {
1021 }
1022
1023 pub proof fn lemma_slice_of_slice(self, s1: int, e1: int, s2: int, e2: int)
1026 requires
1027 0 <= s1 <= e1 <= self.len(),
1028 0 <= s2 <= e2 <= e1 - s1,
1029 ensures
1030 self.subrange(s1, e1).subrange(s2, e2) =~= self.subrange(s1 + s2, s1 + e2),
1031 {
1032 }
1033
1034 pub proof fn unique_seq_to_set(self)
1036 requires
1037 self.no_duplicates(),
1038 ensures
1039 self.len() == self.to_set().len(),
1040 decreases self.len(),
1041 {
1042 broadcast use super::set::group_set_axioms;
1043
1044 seq_to_set_equal_rec::<A>(self);
1045 if self.len() == 0 {
1046 } else {
1047 let rest = self.drop_last();
1048 rest.unique_seq_to_set();
1049 seq_to_set_equal_rec::<A>(rest);
1050 seq_to_set_rec_is_finite::<A>(rest);
1051 assert(!seq_to_set_rec(rest).contains(self.last()));
1052 assert(seq_to_set_rec(rest).insert(self.last()).len() == seq_to_set_rec(rest).len()
1053 + 1);
1054 }
1055 }
1056
1057 pub proof fn lemma_cardinality_of_set(self)
1060 ensures
1061 self.to_set().len() <= self.len(),
1062 decreases self.len(),
1063 {
1064 broadcast use {super::set::group_set_axioms, seq_to_set_is_finite};
1065 broadcast use group_seq_properties;
1066 broadcast use super::set_lib::group_set_properties;
1067
1068 if self.len() == 0 {
1069 } else {
1070 assert(self.drop_last().to_set().insert(self.last()) =~= self.to_set());
1071 self.drop_last().lemma_cardinality_of_set();
1072 }
1073 }
1074
1075 pub proof fn lemma_cardinality_of_empty_set_is_0(self)
1078 ensures
1079 self.to_set().len() == 0 <==> self.len() == 0,
1080 {
1081 broadcast use {super::set::group_set_axioms, seq_to_set_is_finite};
1082
1083 assert(self.len() == 0 ==> self.to_set().len() == 0) by { self.lemma_cardinality_of_set() }
1084 assert(!(self.len() == 0) ==> !(self.to_set().len() == 0)) by {
1085 if self.len() > 0 {
1086 assert(self.to_set().contains(self[0]));
1087 assert(self.to_set().remove(self[0]).len() <= self.to_set().len());
1088 }
1089 }
1090 }
1091
1092 pub proof fn lemma_no_dup_set_cardinality(self)
1095 requires
1096 self.to_set().len() == self.len(),
1097 ensures
1098 self.no_duplicates(),
1099 decreases self.len(),
1100 {
1101 broadcast use {super::set::group_set_axioms, seq_to_set_is_finite};
1102
1103 if self.len() == 0 {
1104 } else {
1105 assert(self =~= Seq::empty().push(self.first()).add(self.drop_first()));
1106 if self.drop_first().contains(self.first()) {
1107 assert(self.to_set() =~= self.drop_first().to_set());
1109 assert(self.to_set().len() <= self.drop_first().len()) by {
1110 self.drop_first().lemma_cardinality_of_set()
1111 }
1112 } else {
1113 assert(self.to_set().len() == 1 + self.drop_first().to_set().len()) by {
1114 assert(self.drop_first().to_set().insert(self.first()) =~= self.to_set());
1115 }
1116 self.drop_first().lemma_no_dup_set_cardinality();
1117 }
1118 }
1119 }
1120
1121 pub broadcast proof fn lemma_to_set_map_commutes<B>(self, f: spec_fn(A) -> B)
1124 ensures
1125 #[trigger] self.to_set().map(f) =~= self.map_values(f).to_set(),
1126 {
1127 broadcast use crate::vstd::group_vstd_default;
1128
1129 assert forall|elem: B|
1130 self.to_set().map(f).contains(elem) <==> self.map_values(f).to_set().contains(elem) by {
1131 if self.to_set().map(f).contains(elem) {
1132 let x = choose|x: A| self.to_set().contains(x) && f(x) == elem;
1133 let i = choose|i: int| 0 <= i < self.len() && self[i] == x;
1134 assert(self.map_values(f)[i] == elem);
1135 }
1136 if self.map_values(f).to_set().contains(elem) {
1137 let i = choose|i: int|
1138 0 <= i < self.map_values(f).len() && self.map_values(f)[i] == elem;
1139 let x = self[i];
1140 assert(self.to_set().contains(x));
1141 }
1142 };
1143 }
1144
1145 pub broadcast proof fn lemma_to_set_insert_commutes(sq: Seq<A>, elt: A)
1148 requires
1149 ensures
1150 #[trigger] (sq + seq![elt]).to_set() =~= sq.to_set().insert(elt),
1151 {
1152 broadcast use crate::vstd::group_vstd_default;
1153 broadcast use lemma_seq_concat_contains_all_elements;
1154 broadcast use lemma_seq_empty_contains_nothing;
1155 broadcast use lemma_seq_contains_after_push;
1156 broadcast use super::seq::group_seq_axioms;
1157 broadcast use super::set_lib::group_set_properties;
1158
1159 }
1160
1161 pub open spec fn update_subrange_with(self, off: int, vs: Self) -> Self
1165 recommends
1166 0 <= off,
1167 off + vs.len() <= self.len(),
1168 {
1169 Seq::new(
1170 self.len(),
1171 |i: int|
1172 if off <= i < off + vs.len() {
1173 vs[i - off]
1174 } else {
1175 self[i]
1176 },
1177 )
1178 }
1179
1180 pub broadcast proof fn lemma_seq_skip_skip(self, i: int)
1192 ensures
1193 0 <= i < self.len() ==> (self.skip(i)).skip(1) =~= #[trigger] self.skip(i + 1),
1194 {
1195 broadcast use group_seq_properties;
1196
1197 }
1198
1199 pub proof fn lemma_contains_to_index(self, elem: A) -> (idx: int)
1212 requires
1213 self.contains(elem),
1214 ensures
1215 0 <= idx < self.len() && self[idx] == elem,
1216 decreases self.len(),
1217 {
1218 broadcast use group_seq_properties;
1219
1220 if self[0] == elem {
1221 0
1222 } else {
1223 let i = self.skip(1).lemma_contains_to_index(elem);
1224 i + 1
1225 }
1226 }
1227
1228 pub proof fn lemma_all_from_head_tail(self, pred: spec_fn(A) -> bool)
1244 requires
1245 self.len() > 0,
1246 pred(self[0]) && self.skip(1).all(|x| pred(x)),
1247 ensures
1248 self.all(|x| pred(x)),
1249 {
1250 broadcast use group_seq_properties;
1251
1252 assert(seq![self[0]] + self.skip(1) == self);
1253 }
1254
1255 pub proof fn lemma_any_tail(self, pred: spec_fn(A) -> bool)
1271 requires
1272 self.any(|x| pred(x)),
1273 ensures
1274 !pred(self[0]) ==> self.skip(1).any(|x| pred(x)),
1275 {
1276 broadcast use group_seq_properties;
1277
1278 }
1279
1280 pub open spec fn remove_duplicates(self, seen: Seq<A>) -> Seq<A>
1298 decreases self.len(),
1299 {
1300 if self.len() == 0 {
1301 seen
1302 } else if seen.contains(self[0]) {
1303 self.skip(1).remove_duplicates(seen)
1304 } else {
1305 self.skip(1).remove_duplicates(seen + seq![self[0]])
1306 }
1307 }
1308
1309 pub broadcast proof fn lemma_remove_duplicates_properties(self, seen: Seq<A>)
1327 ensures
1328 forall|x|
1329 (self + seen).contains(x) <==> #[trigger] self.remove_duplicates(seen).contains(x),
1330 #[trigger] self.remove_duplicates(seen).len() <= self.len() + seen.len(),
1331 decreases self.len(),
1332 {
1333 broadcast use group_seq_properties;
1334
1335 if self.len() == 0 {
1336 } else if seen.contains(self[0]) {
1337 let rest = self.skip(1);
1338 rest.lemma_remove_duplicates_properties(seen);
1339 } else {
1340 let rest = self.skip(1);
1341 rest.lemma_remove_duplicates_properties(seen + seq![self[0]]);
1342 }
1343 }
1344
1345 pub proof fn lemma_remove_duplicates_append_index(self, i: int, seen: Seq<A>)
1361 requires
1362 0 <= i < self.len(),
1363 ensures
1364 self.remove_duplicates(seen) == self.skip(i).remove_duplicates(
1365 self.take(i).remove_duplicates(seen),
1366 ),
1367 decreases self.len(),
1368 {
1369 broadcast use {
1370 group_seq_properties,
1371 lemma_seq_skip_of_skip,
1372 Seq::lemma_remove_duplicates_properties,
1373 };
1374
1375 if i == 0 {
1376 } else if i == self.len() {
1377 assert(self.take(i) == self);
1378 } else {
1379 assert(self.skip(1).take(i - 1) == self.subrange(1, i));
1380 assert(self.take(i).skip(1) == self.subrange(1, i));
1381 assert(self.skip(1).take(i - 1) == self.take(i).skip(1));
1382 if seen.contains(self[0]) {
1383 self.skip(1).lemma_remove_duplicates_append_index(i - 1, seen);
1384 } else {
1385 self.skip(1).lemma_remove_duplicates_append_index(i - 1, seen + seq![self[0]]);
1386 }
1387 }
1388 }
1389
1390 proof fn lemma_skip1_concat(xs: Seq<A>, ys: Seq<A>)
1405 requires
1406 xs.len() > 0,
1407 ensures
1408 (xs + ys).skip(1) == xs.skip(1) + ys,
1409 {
1410 broadcast use group_seq_properties;
1411
1412 assert((xs + ys).skip(1) == xs.skip(1) + ys);
1413 }
1414
1415 pub proof fn lemma_remove_duplicates_append(self, x: A, seen: Seq<A>)
1431 ensures
1432 (self + seen).contains(x) ==> (self + seq![x]).remove_duplicates(seen)
1433 == self.remove_duplicates(seen),
1434 !(self + seen).contains(x) ==> (self + seq![x]).remove_duplicates(seen)
1435 == self.remove_duplicates(seen) + seq![x],
1436 decreases self.len(),
1437 {
1438 broadcast use group_seq_properties;
1439
1440 reveal_with_fuel(Seq::remove_duplicates, 2);
1441
1442 if self.len() != 0 {
1443 let head = self[0];
1444 let tail = self.skip(1);
1445
1446 let seen2 = if seen.contains(head) {
1447 seen
1448 } else {
1449 seen + seq![head]
1450 };
1451 tail.lemma_remove_duplicates_append(x, seen2);
1452 assert((self + seq![x]).skip(1) == tail + seq![x]) by {
1453 Seq::lemma_skip1_concat(self, seq![x]);
1454 };
1455 }
1456 }
1457
1458 pub proof fn lemma_all_neg_filter_empty(self, pred: spec_fn(A) -> bool)
1471 requires
1472 self.all(|x: A| !pred(x)),
1473 ensures
1474 self.filter(pred).len() == 0,
1475 decreases self.len(),
1476 {
1477 broadcast use group_seq_properties;
1478
1479 reveal(Seq::filter);
1480 if self.len() != 0 {
1481 let rest = self.drop_last();
1482 rest.lemma_all_neg_filter_empty(pred);
1483 rest.lemma_filter_len_push(pred, self.last());
1484 let neg_pred = |x| !pred(x);
1485 assert(neg_pred(self.last()));
1486 }
1487 }
1488
1489 pub open spec fn filter_map<B>(self, f: spec_fn(A) -> Option<B>) -> Seq<B>
1498 decreases self.len(),
1499 {
1500 if self.len() == 0 {
1504 Seq::empty()
1505 } else {
1506 let rest = self.drop_last();
1507 match f(self.last()) {
1508 Option::Some(s) => rest.filter_map(f) + seq![s],
1509 Option::None => rest.filter_map(f),
1510 }
1511 }
1512 }
1513
1514 pub broadcast proof fn lemma_filter_contains_rev(self, p: spec_fn(A) -> bool, elem: A)
1518 requires
1519 #[trigger] self.filter(p).contains(elem),
1520 ensures
1521 self.contains(elem),
1522 decreases self.len(),
1523 {
1524 broadcast use group_seq_properties;
1525
1526 reveal(Seq::filter);
1527 if self.len() == 0 {
1528 } else {
1529 let rest = self.drop_last();
1530 let last = self.last();
1531 if !p(last) || last != elem {
1532 rest.lemma_filter_contains_rev(p, elem);
1533 }
1534 }
1535 }
1536
1537 pub broadcast proof fn lemma_filter_map_contains<B>(self, f: spec_fn(A) -> Option<B>, elt: B)
1541 requires
1542 #[trigger] self.filter_map(f).contains(elt),
1543 ensures
1544 exists|t: A| #[trigger] self.contains(t) && f(t) == Some(elt),
1545 decreases self.len(),
1546 {
1547 broadcast use group_seq_properties;
1548
1549 if self.len() == 0 {
1550 } else {
1551 let last = self.last();
1552 let rest = self.drop_last();
1553 if f(last) == Some(elt) {
1554 assert(self.contains(last));
1555 } else {
1556 rest.lemma_filter_map_contains(f, elt);
1557 let t = choose|t: A| #[trigger] rest.contains(t) && f(t) == Some(elt);
1558 assert(self.contains(t));
1559 }
1560 }
1561 }
1562
1563 pub proof fn lemma_take_succ(xs: Seq<A>, k: int)
1572 requires
1573 0 <= k < xs.len(),
1574 ensures
1575 xs.take(k + 1) =~= xs.take(k) + seq![xs[k]],
1576 {
1577 broadcast use group_seq_properties;
1578
1579 }
1580
1581 pub proof fn lemma_filter_map_singleton<B>(a: A, f: spec_fn(A) -> Option<B>)
1585 ensures
1586 seq![a].filter_map(f) =~= match f(a) {
1587 Option::Some(b) => seq![b],
1588 Option::None => Seq::empty(),
1589 },
1590 {
1591 reveal_with_fuel(Seq::filter_map, 2);
1592 }
1593
1594 pub broadcast proof fn lemma_filter_map_take_succ<B>(self, f: spec_fn(A) -> Option<B>, i: int)
1606 requires
1607 0 <= i < self.len(),
1608 ensures
1609 #[trigger] self.take(i + 1).filter_map(f) =~= self.take(i).filter_map(f) + (match f(
1610 self[i],
1611 ) {
1612 Option::Some(s) => seq![s],
1613 Option::None => Seq::empty(),
1614 }),
1615 decreases self.len(),
1616 {
1617 broadcast use group_seq_properties;
1618
1619 if i != 0 {
1620 self.drop_last().lemma_filter_map_take_succ(f, i - 1);
1621 assert(self.take(i + 1).drop_last() == self.take(i));
1622 }
1623 }
1624
1625 pub open spec fn filter_alt(self, p: spec_fn(A) -> bool) -> Seq<A> {
1628 if self.len() == 0 {
1629 Seq::empty()
1630 } else {
1631 let rest = self.drop_first().filter(p);
1632 let first = self.first();
1633 if p(first) {
1634 seq![first] + rest
1635 } else {
1636 rest
1637 }
1638 }
1639 }
1640
1641 pub broadcast proof fn lemma_filter_prepend(self, x: A, p: spec_fn(A) -> bool)
1656 ensures
1657 #[trigger] (seq![x] + self).filter(p) == (if p(x) {
1658 seq![x]
1659 } else {
1660 Seq::empty()
1661 }) + self.filter(p),
1662 decreases self.len(),
1663 {
1664 broadcast use group_seq_properties;
1665
1666 reveal(Seq::filter);
1667 let lhs = (seq![x] + self).filter(p);
1668 let rhs = (if p(x) {
1669 seq![x]
1670 } else {
1671 Seq::empty()
1672 }) + self.filter(p);
1673
1674 if self.len() == 0 {
1675 assert(lhs =~= rhs);
1676 } else {
1677 let tail_seq = if p(self.last()) {
1678 seq![self.last()]
1679 } else {
1680 Seq::empty()
1681 };
1682
1683 assert(((seq![x] + self).drop_last()) =~= seq![x] + self.drop_last());
1684 let sub = (seq![x] + self.drop_last()).filter(p);
1685 assert(lhs =~= sub + tail_seq);
1686 assert(rhs =~= (if p(x) {
1687 seq![x]
1688 } else {
1689 Seq::empty()
1690 }) + self.drop_last().filter(p) + tail_seq);
1691 self.drop_last().lemma_filter_prepend(x, p);
1692 }
1693 }
1694
1695 pub proof fn lemma_filter_eq_filter_alt(self, p: spec_fn(A) -> bool)
1697 ensures
1698 self.filter(p) =~= self.filter_alt(p),
1699 decreases self.len(),
1700 {
1701 broadcast use group_seq_properties;
1702 broadcast use Seq::lemma_filter_prepend;
1703
1704 reveal(Seq::filter);
1705 if self.len() == 0 {
1706 } else {
1707 let first = self.first();
1708 let but_first = self.drop_first();
1709 assert(self =~= seq![first] + but_first);
1710 self.drop_first().lemma_filter_eq_filter_alt(p);
1711 }
1712 }
1713
1714 pub proof fn lemma_filter_monotone(self, ys: Seq<A>, p: spec_fn(A) -> bool)
1729 requires
1730 self.is_prefix_of(ys),
1731 ensures
1732 self.filter(p).is_prefix_of(ys.filter(p)),
1733 decreases self.len(),
1734 {
1735 broadcast use group_seq_properties;
1736
1737 self.lemma_filter_eq_filter_alt(p);
1738 ys.lemma_filter_eq_filter_alt(p);
1739 if self.len() == 0 {
1740 } else {
1741 self.drop_first().lemma_filter_monotone(ys.drop_first(), p);
1742 }
1743 }
1744
1745 pub proof fn lemma_filter_take_len(self, p: spec_fn(A) -> bool, i: int)
1760 requires
1761 0 <= i <= self.len(),
1762 ensures
1763 self.filter(p).len() >= self.take(i).filter(p).len(),
1764 decreases i,
1765 {
1766 broadcast use group_seq_properties;
1767 broadcast use Seq::lemma_filter_len_push;
1768 broadcast use Seq::lemma_filter_push;
1769
1770 self.take(i).lemma_filter_monotone(self, p);
1771 }
1772
1773 pub broadcast proof fn lemma_filter_len_push(self, p: spec_fn(A) -> bool, elem: A)
1785 ensures
1786 #[trigger] self.push(elem).filter(p).len() == self.filter(p).len() + (if p(elem) {
1787 1int
1788 } else {
1789 0int
1790 }),
1791 {
1792 broadcast use group_seq_properties;
1793 broadcast use Seq::lemma_filter_push;
1794
1795 }
1796
1797 pub broadcast proof fn lemma_index_contains(self, i: int)
1800 requires
1801 0 <= i < self.len(),
1802 ensures
1803 self.contains(#[trigger] self[i]),
1804 {
1805 }
1806
1807 pub broadcast proof fn lemma_take_succ_push(self, i: int)
1810 requires
1811 0 <= i < self.len(),
1812 ensures
1813 #[trigger] self.take(i + 1) =~= self.take(i).push(self[i]),
1814 {
1815 broadcast use group_seq_properties;
1816
1817 }
1818
1819 pub broadcast proof fn lemma_take_len(self)
1821 ensures
1822 #[trigger] self.take(self.len() as int) == self,
1823 {
1824 broadcast use group_seq_properties;
1825
1826 }
1827
1828 pub broadcast proof fn lemma_take_any_succ(self, p: spec_fn(A) -> bool, i: int)
1841 requires
1842 0 <= i < self.len(),
1843 ensures
1844 #[trigger] self.take(i + 1).any(p) <==> self.take(i).any(p) || p(self[i]),
1845 {
1846 broadcast use group_seq_properties;
1847
1848 self.lemma_take_succ_push(i);
1849 if self.take(i + 1).any(p) {
1850 let x = choose|x: A| self.take(i + 1).contains(x) && #[trigger] p(x);
1851 assert(self.take(i).contains(x) || x == self[i]);
1852 }
1853 if self.take(i).any(p) {
1854 let x = choose|x: A| self.take(i).contains(x) && #[trigger] p(x);
1855 assert(self.take(i + 1).contains(x));
1856 }
1857 if p(self[i]) {
1858 assert(self.take(i + 1).contains(self[i]));
1859 }
1860 }
1861
1862 pub proof fn lemma_no_duplicates_injective<B>(self, f: spec_fn(A) -> B)
1874 requires
1875 injective(f),
1876 ensures
1877 self.no_duplicates() <==> self.map_values(f).no_duplicates(),
1878 {
1879 broadcast use group_seq_properties;
1880 broadcast use super::set_lib::group_set_properties;
1881
1882 let mapped = self.map_values(f);
1883 assert(mapped.len() == self.len());
1884 if mapped.no_duplicates() {
1885 assert forall|i: int, j: int| 0 <= i < j < mapped.len() implies self[i] != self[j] by {
1886 assert(mapped[i] == f(self[i]));
1887 assert(mapped[j] == f(self[j]));
1888 }
1889 }
1890 }
1891
1892 pub broadcast proof fn lemma_push_map_commute<B>(self, f: spec_fn(A) -> B, x: A)
1904 ensures
1905 self.map_values(f).push(f(x)) =~= #[trigger] self.push(x).map_values(f),
1906 decreases self.len(),
1907 {
1908 broadcast use group_seq_properties;
1909
1910 }
1911
1912 pub broadcast proof fn lemma_push_to_set_commute(self, elem: A)
1923 ensures
1924 #[trigger] self.push(elem).to_set() =~= self.to_set().insert(elem),
1925 {
1926 broadcast use group_seq_properties;
1927 broadcast use super::set::group_set_axioms;
1928
1929 let lhs = self.push(elem).to_set();
1930 let rhs = self.to_set().insert(elem);
1931
1932 assert(lhs.subset_of(rhs));
1933 assert forall|x: A| rhs.contains(x) implies lhs.contains(x) by {
1934 lemma_seq_contains_after_push(self, elem, x);
1935 if x == elem {
1936 } else {
1937 lemma_seq_contains_after_push(self, elem, x);
1938 }
1939 }
1940 }
1941
1942 pub broadcast proof fn lemma_filter_push(self, elem: A, pred: spec_fn(A) -> bool)
1956 ensures
1957 #[trigger] self.push(elem).filter(pred) == if pred(elem) {
1958 self.filter(pred).push(elem)
1959 } else {
1960 self.filter(pred)
1961 },
1962 {
1963 broadcast use group_seq_properties;
1964
1965 reveal(Seq::filter);
1966 assert(self.push(elem).drop_last() =~= self);
1967 }
1968
1969 pub proof fn lemma_zip_with_contains_index<B>(self, b: Seq<B>, i: int)
1982 requires
1983 0 <= i < self.len(),
1984 self.len() == b.len(),
1985 ensures
1986 self.zip_with(b).contains((self[i], b[i])),
1987 {
1988 assert(self.zip_with(b)[i] == (self[i], b[i]));
1989 }
1990
1991 pub proof fn lemma_zip_with_uncurry_all<B>(self, b: Seq<B>, f: spec_fn(A, B) -> bool)
2008 requires
2009 self.len() == b.len(),
2010 ensures
2011 self.zip_with(b).all(|p: (A, B)| f(p.0, p.1)) <==> forall|i: int|
2012 0 <= i < self.len() ==> f(self[i], b[i]),
2013 {
2014 broadcast use group_seq_properties;
2015
2016 let zipped = self.zip_with(b);
2017 let f_uncurr = |p: (A, B)| f(p.0, p.1);
2018 let lhs = zipped.all(f_uncurr);
2019 let rhs = (forall|i: int| 0 <= i < self.len() ==> f(self[i], b[i]));
2020 if lhs {
2021 assert forall|i: int| 0 <= i < self.len() implies f(self[i], b[i]) by {
2022 self.lemma_zip_with_contains_index(b, i);
2023 assert(forall|j| 0 <= j < zipped.len() ==> f_uncurr(zipped[j]));
2024 }
2025 }
2026 }
2027
2028 pub proof fn lemma_flat_map_push<B>(self, f: spec_fn(A) -> Seq<B>, elem: A)
2042 ensures
2043 self.push(elem).flat_map(f) =~= self.flat_map(f) + f(elem),
2044 decreases self.len(),
2045 {
2046 broadcast use group_seq_properties;
2047 broadcast use Seq::lemma_flatten_push;
2048 broadcast use Seq::lemma_push_map_commute;
2049
2050 }
2051
2052 pub broadcast proof fn lemma_flat_map_take_append<B>(self, f: spec_fn(A) -> Seq<B>, i: int)
2067 requires
2068 0 <= i < self.len(),
2069 ensures
2070 #[trigger] self.take(i + 1).flat_map(f) =~= self.take(i).flat_map(f) + f(self[i]),
2071 decreases i,
2072 {
2073 broadcast use group_seq_properties;
2074
2075 self.lemma_take_succ_push(i);
2076 self.take(i).lemma_flat_map_push(f, self[i]);
2077 }
2078
2079 pub broadcast proof fn lemma_flat_map_singleton<B>(self, f: spec_fn(A) -> Seq<B>)
2082 requires
2083 #[trigger] self.len() == 1,
2084 ensures
2085 #[trigger] self.flat_map(f) == f(self[0]),
2086 {
2087 broadcast use Seq::lemma_flatten_singleton;
2088
2089 }
2090
2091 pub broadcast proof fn lemma_map_take_succ<B>(self, f: spec_fn(A) -> B, i: int)
2106 requires
2107 0 <= i < self.len(),
2108 ensures
2109 #[trigger] self.take(i + 1).map_values(f) =~= self.take(i).map_values(f).push(
2110 f(self[i]),
2111 ),
2112 {
2113 broadcast use group_seq_properties;
2114
2115 self.lemma_take_succ_push(i);
2116 }
2117
2118 pub broadcast proof fn lemma_prefix_index_eq(self, prefix: Seq<A>)
2131 requires
2132 #[trigger] prefix.is_prefix_of(self),
2133 ensures
2134 forall|i: int| 0 <= i < prefix.len() ==> prefix[i] == self[i],
2135 {
2136 }
2137
2138 pub broadcast proof fn lemma_prefix_concat(self, prefix1: Seq<A>, prefix2: Seq<A>)
2152 requires
2153 #[trigger] (prefix1 + prefix2).is_prefix_of(self),
2154 ensures
2155 prefix1.is_prefix_of(self),
2156 {
2157 broadcast use Seq::lemma_prefix_index_eq;
2158
2159 }
2160
2161 pub broadcast proof fn lemma_prefix_chain_contains(self, prefix1: Seq<A>, prefix2: Seq<A>, t: A)
2182 requires
2183 #[trigger] (prefix1 + seq![t]).is_prefix_of(self),
2184 #[trigger] prefix1.is_prefix_of(prefix2),
2185 prefix2.is_prefix_of(self),
2186 prefix1 != prefix2,
2187 !prefix1.contains(t),
2188 ensures
2189 prefix2.contains(t),
2190 {
2191 broadcast use Seq::lemma_prefix_concat;
2192 broadcast use Seq::lemma_prefix_index_eq;
2193
2194 assert(prefix2[prefix1.len() as int] == t);
2195 }
2196
2197 pub broadcast proof fn lemma_prefix_append_unique(self, prefix1: Seq<A>, prefix2: Seq<A>, t: A)
2201 requires
2202 #[trigger] (prefix1 + seq![t]).is_prefix_of(self),
2203 #[trigger] (prefix2 + seq![t]).is_prefix_of(self),
2204 !prefix1.contains(t),
2205 !prefix2.contains(t),
2206 ensures
2207 prefix1 == prefix2,
2208 {
2209 broadcast use Seq::lemma_prefix_concat;
2210 broadcast use Seq::lemma_prefix_index_eq;
2211 broadcast use Seq::lemma_prefix_chain_contains;
2212
2213 if prefix1 != prefix2 {
2214 assert(prefix1.is_prefix_of(prefix2) || prefix2.is_prefix_of(prefix1));
2215 }
2216 }
2217
2218 pub broadcast proof fn lemma_all_push(self, p: spec_fn(A) -> bool, elem: A)
2233 requires
2234 self.all(p),
2235 p(elem),
2236 ensures
2237 #[trigger] self.push(elem).all(p),
2238 {
2239 broadcast use group_seq_properties;
2240
2241 assert forall|x: A| self.push(elem).contains(x) implies p(x) by {
2242 lemma_seq_contains_after_push(self, elem, x);
2243 }
2244 }
2245
2246 pub proof fn lemma_concat_injective(self, s1: Seq<A>, s2: Seq<A>)
2249 ensures
2250 (self + s1 == self + s2) <==> (s1 == s2),
2251 {
2252 broadcast use group_seq_properties;
2253
2254 assert((self + s1).skip(self.len() as int) == s1);
2255 }
2256
2257 pub broadcast group group_seq_extra {
2258 Seq::<_>::lemma_seq_skip_skip,
2259 Seq::<_>::lemma_remove_duplicates_properties,
2260 Seq::<_>::lemma_filter_contains_rev,
2261 Seq::<_>::lemma_filter_map_take_succ,
2262 Seq::<_>::lemma_filter_prepend,
2263 Seq::<_>::lemma_filter_len_push,
2264 Seq::<_>::lemma_take_len,
2265 Seq::<_>::lemma_take_any_succ,
2266 Seq::<_>::lemma_push_map_commute,
2267 Seq::<_>::lemma_push_to_set_commute,
2268 Seq::<_>::lemma_filter_push,
2269 Seq::<_>::lemma_flat_map_take_append,
2270 Seq::<_>::lemma_flat_map_singleton,
2271 Seq::<_>::lemma_map_take_succ,
2272 Seq::<_>::lemma_prefix_index_eq,
2273 Seq::<_>::lemma_prefix_concat,
2274 Seq::<_>::lemma_prefix_chain_contains,
2275 Seq::<_>::lemma_prefix_append_unique,
2276 Seq::<_>::lemma_all_push,
2277 }
2278}
2279
2280pub proof fn lemma_filter_view_commute<S: View>(
2297 s: Seq<S>,
2298 p: spec_fn(S) -> bool,
2299 sp: spec_fn(S::V) -> bool,
2300)
2301 requires
2302 forall|s: S| p(s) <==> sp(s.view()),
2303 ensures
2304 s.filter(p).map_values(|x: S| x.view()) == s.map_values(|x: S| x.view()).filter(sp),
2305 decreases s.len(),
2306{
2307 broadcast use group_seq_properties;
2308 broadcast use Seq::lemma_push_map_commute;
2309 broadcast use Seq::lemma_filter_push;
2310
2311 reveal(Seq::filter);
2312 let view = |x: S| x.view();
2313 if s.len() > 0 {
2314 let rest = s.drop_last();
2315 let last = s.last();
2316 assert(s =~= rest.push(last));
2317 assert(s.map_values(view).last() == view(last));
2318 lemma_filter_view_commute(rest, p, sp);
2319 }
2320}
2321
2322pub proof fn lemma_exactly_one_view<S: View>(
2337 s: Seq<S>,
2338 p: spec_fn(S) -> bool,
2339 sp: spec_fn(S::V) -> bool,
2340)
2341 requires
2342 forall|s: S| p(s) <==> sp(s.view()),
2343 injective(|x: S| x.view()),
2344 ensures
2345 s.exactly_one(p) <==> s.map_values(|x: S| x.view()).exactly_one(sp),
2346{
2347 lemma_filter_view_commute(s, p, sp);
2348}
2349
2350impl<A, B> Seq<(A, B)> {
2351 pub closed spec fn unzip(self) -> (Seq<A>, Seq<B>) {
2353 (Seq::new(self.len(), |i: int| self[i].0), Seq::new(self.len(), |i: int| self[i].1))
2354 }
2355
2356 pub proof fn unzip_ensures(self)
2358 ensures
2359 self.unzip().0.len() == self.unzip().1.len(),
2360 self.unzip().0.len() == self.len(),
2361 self.unzip().1.len() == self.len(),
2362 forall|i: int|
2363 0 <= i < self.len() ==> (#[trigger] self.unzip().0[i], #[trigger] self.unzip().1[i])
2364 == self[i],
2365 decreases self.len(),
2366 {
2367 if self.len() > 0 {
2368 self.drop_last().unzip_ensures();
2369 }
2370 }
2371
2372 pub proof fn lemma_zip_of_unzip(self)
2375 ensures
2376 self.unzip().0.zip_with(self.unzip().1) =~= self,
2377 {
2378 }
2379}
2380
2381impl<A> Seq<Seq<A>> {
2382 pub open spec fn flatten(self) -> Seq<A>
2396 decreases self.len(),
2397 {
2398 if self.len() == 0 {
2399 Seq::empty()
2400 } else {
2401 self.first().add(self.drop_first().flatten())
2402 }
2403 }
2404
2405 pub open spec fn flatten_alt(self) -> Seq<A>
2410 decreases self.len(),
2411 {
2412 if self.len() == 0 {
2413 Seq::empty()
2414 } else {
2415 self.drop_last().flatten_alt().add(self.last())
2416 }
2417 }
2418
2419 pub proof fn lemma_flatten_one_element(self)
2422 ensures
2423 self.len() == 1 ==> self.flatten() == self.first(),
2424 {
2425 broadcast use Seq::add_empty_right;
2426
2427 if self.len() == 1 {
2428 assert(self.flatten() =~= self.first().add(self.drop_first().flatten()));
2429 }
2430 }
2431
2432 pub proof fn lemma_flatten_length_ge_single_element_length(self, i: int)
2435 requires
2436 0 <= i < self.len(),
2437 ensures
2438 self.flatten_alt().len() >= self[i].len(),
2439 decreases self.len(),
2440 {
2441 if self.len() == 1 {
2442 self.lemma_flatten_one_element();
2443 self.lemma_flatten_and_flatten_alt_are_equivalent();
2444 } else if i < self.len() - 1 {
2445 self.drop_last().lemma_flatten_length_ge_single_element_length(i);
2446 } else {
2447 assert(self.flatten_alt() == self.drop_last().flatten_alt().add(self.last()));
2448 }
2449 }
2450
2451 pub proof fn lemma_flatten_length_le_mul(self, j: int)
2455 requires
2456 forall|i: int| 0 <= i < self.len() ==> (#[trigger] self[i]).len() <= j,
2457 ensures
2458 self.flatten_alt().len() <= self.len() * j,
2459 decreases self.len(),
2460 {
2461 broadcast use group_seq_properties;
2462
2463 if self.len() == 0 {
2464 } else {
2465 self.drop_last().lemma_flatten_length_le_mul(j);
2466 assert((self.len() - 1) * j == (self.len() * j) - (1 * j)) by (nonlinear_arith); }
2468 }
2469
2470 pub proof fn lemma_flatten_and_flatten_alt_are_equivalent(self)
2473 ensures
2474 self.flatten() =~= self.flatten_alt(),
2475 decreases self.len(),
2476 {
2477 broadcast use {Seq::add_empty_right, Seq::push_distributes_over_add};
2478
2479 if self.len() != 0 {
2480 self.drop_last().lemma_flatten_and_flatten_alt_are_equivalent();
2481 seq![self.last()].lemma_flatten_one_element();
2485 assert(seq![self.last()].flatten() == self.last());
2486 lemma_flatten_concat(self.drop_last(), seq![self.last()]);
2487 assert((self.drop_last() + seq![self.last()]).flatten() == self.drop_last().flatten()
2488 + self.last());
2489 assert(self.drop_last() + seq![self.last()] =~= self);
2490 assert(self.flatten_alt() == self.drop_last().flatten_alt() + self.last());
2491 }
2492 }
2493
2494 pub broadcast proof fn lemma_flatten_push(self, elem: Seq<A>)
2497 ensures
2498 #[trigger] self.push(elem).flatten() =~= self.flatten() + elem,
2499 decreases self.len(),
2500 {
2501 broadcast use group_seq_properties;
2502
2503 assert(self.push(elem).last() == elem);
2504 assert(self.push(elem).drop_last() =~= self);
2505 calc! {
2506 (==)
2507 self.push(elem).flatten(); {
2508 self.push(elem).lemma_flatten_and_flatten_alt_are_equivalent();
2509 }
2510 self.push(elem).flatten_alt(); {}
2511 self.flatten_alt() + elem; {
2512 self.lemma_flatten_and_flatten_alt_are_equivalent();
2513 }
2514 self.flatten() + elem;
2515 }
2516 }
2517
2518 pub broadcast proof fn lemma_flatten_singleton(self)
2520 requires
2521 #[trigger] self.len() == 1,
2522 ensures
2523 #[trigger] self.flatten() == self[0],
2524 {
2525 assert(self.flatten() == self[0] + self.drop_first().flatten());
2526 assert(self.flatten() == self[0]);
2527 }
2528
2529 pub broadcast group group_seq_flatten {
2530 Seq::<_>::lemma_flatten_push,
2531 Seq::<_>::lemma_flatten_singleton,
2532 }
2533}
2534
2535impl Seq<int> {
2538 pub open spec fn max(self) -> int
2540 recommends
2541 0 < self.len(),
2542 decreases self.len(),
2543 {
2544 if self.len() == 1 {
2545 self[0]
2546 } else if self.len() == 0 {
2547 0
2548 } else {
2549 let later_max = self.drop_first().max();
2550 if self[0] >= later_max {
2551 self[0]
2552 } else {
2553 later_max
2554 }
2555 }
2556 }
2557
2558 pub proof fn max_ensures(self)
2560 ensures
2561 forall|x: int| self.contains(x) ==> x <= self.max(),
2562 forall|i: int| 0 <= i < self.len() ==> self[i] <= self.max(),
2563 self.len() == 0 || self.contains(self.max()),
2564 decreases self.len(),
2565 {
2566 if self.len() <= 1 {
2567 } else {
2568 let elt = self.drop_first().max();
2569 assert(self.drop_first().contains(elt)) by { self.drop_first().max_ensures() }
2570 assert forall|i: int| 0 <= i < self.len() implies self[i] <= self.max() by {
2571 assert(i == 0 || self[i] == self.drop_first()[i - 1]);
2572 assert(forall|j: int|
2573 0 <= j < self.drop_first().len() ==> self.drop_first()[j]
2574 <= self.drop_first().max()) by { self.drop_first().max_ensures() }
2575 }
2576 }
2577 }
2578
2579 pub open spec fn min(self) -> int
2581 recommends
2582 0 < self.len(),
2583 decreases self.len(),
2584 {
2585 if self.len() == 1 {
2586 self[0]
2587 } else if self.len() == 0 {
2588 0
2589 } else {
2590 let later_min = self.drop_first().min();
2591 if self[0] <= later_min {
2592 self[0]
2593 } else {
2594 later_min
2595 }
2596 }
2597 }
2598
2599 pub proof fn min_ensures(self)
2601 ensures
2602 forall|x: int| self.contains(x) ==> self.min() <= x,
2603 forall|i: int| 0 <= i < self.len() ==> self.min() <= self[i],
2604 self.len() == 0 || self.contains(self.min()),
2605 decreases self.len(),
2606 {
2607 if self.len() <= 1 {
2608 } else {
2609 let elt = self.drop_first().min();
2610 assert(self.subrange(1, self.len() as int).contains(elt)) by {
2611 self.drop_first().min_ensures()
2612 }
2613 assert forall|i: int| 0 <= i < self.len() implies self.min() <= self[i] by {
2614 assert(i == 0 || self[i] == self.drop_first()[i - 1]);
2615 assert(forall|j: int|
2616 0 <= j < self.drop_first().len() ==> self.drop_first().min()
2617 <= self.drop_first()[j]) by { self.drop_first().min_ensures() }
2618 }
2619 }
2620 }
2621
2622 pub closed spec fn sort(self) -> Self {
2623 self.sort_by(|x: int, y: int| x <= y)
2624 }
2625
2626 pub proof fn lemma_sort_ensures(self)
2627 ensures
2628 self.to_multiset() =~= self.sort().to_multiset(),
2629 sorted_by(self.sort(), |x: int, y: int| x <= y),
2630 {
2631 self.lemma_sort_by_ensures(|x: int, y: int| x <= y);
2632 }
2633
2634 pub proof fn lemma_subrange_max(self, from: int, to: int)
2637 requires
2638 0 <= from < to <= self.len(),
2639 ensures
2640 self.subrange(from, to).max() <= self.max(),
2641 {
2642 self.max_ensures();
2643 self.subrange(from, to).max_ensures();
2644 }
2645
2646 pub proof fn lemma_subrange_min(self, from: int, to: int)
2649 requires
2650 0 <= from < to <= self.len(),
2651 ensures
2652 self.subrange(from, to).min() >= self.min(),
2653 {
2654 self.min_ensures();
2655 self.subrange(from, to).min_ensures();
2656 }
2657}
2658
2659spec fn merge_sorted_with<A>(left: Seq<A>, right: Seq<A>, leq: spec_fn(A, A) -> bool) -> Seq<A>
2661 recommends
2662 sorted_by(left, leq),
2663 sorted_by(right, leq),
2664 total_ordering(leq),
2665 decreases left.len(), right.len(),
2666{
2667 if left.len() == 0 {
2668 right
2669 } else if right.len() == 0 {
2670 left
2671 } else if leq(left.first(), right.first()) {
2672 Seq::<A>::empty().push(left.first()) + merge_sorted_with(left.drop_first(), right, leq)
2673 } else {
2674 Seq::<A>::empty().push(right.first()) + merge_sorted_with(left, right.drop_first(), leq)
2675 }
2676}
2677
2678proof fn lemma_merge_sorted_with_ensures<A>(left: Seq<A>, right: Seq<A>, leq: spec_fn(A, A) -> bool)
2679 requires
2680 sorted_by(left, leq),
2681 sorted_by(right, leq),
2682 total_ordering(leq),
2683 ensures
2684 (left + right).to_multiset() =~= merge_sorted_with(left, right, leq).to_multiset(),
2685 sorted_by(merge_sorted_with(left, right, leq), leq),
2686 decreases left.len(), right.len(),
2687{
2688 broadcast use group_seq_properties;
2690
2691 if left.len() == 0 {
2692 assert(left + right =~= right);
2693 } else if right.len() == 0 {
2694 assert(left + right =~= left);
2695 } else if leq(left.first(), right.first()) {
2696 let result = Seq::<A>::empty().push(left.first()) + merge_sorted_with(
2697 left.drop_first(),
2698 right,
2699 leq,
2700 );
2701 lemma_merge_sorted_with_ensures(left.drop_first(), right, leq);
2702 let rest = merge_sorted_with(left.drop_first(), right, leq);
2703 assert(rest.len() == 0 || rest.first() == left.drop_first().first() || rest.first()
2704 == right.first()) by {
2705 if left.drop_first().len() == 0 {
2706 } else if leq(left.drop_first().first(), right.first()) {
2707 assert(rest =~= Seq::<A>::empty().push(left.drop_first().first())
2708 + merge_sorted_with(left.drop_first().drop_first(), right, leq));
2709 } else {
2710 assert(rest =~= Seq::<A>::empty().push(right.first()) + merge_sorted_with(
2711 left.drop_first(),
2712 right.drop_first(),
2713 leq,
2714 ));
2715 }
2716 }
2717 lemma_new_first_element_still_sorted_by(left.first(), rest, leq);
2718 assert((left.drop_first() + right) =~= (left + right).drop_first());
2719 } else {
2720 let result = Seq::<A>::empty().push(right.first()) + merge_sorted_with(
2721 left,
2722 right.drop_first(),
2723 leq,
2724 );
2725 lemma_merge_sorted_with_ensures(left, right.drop_first(), leq);
2726 let rest = merge_sorted_with(left, right.drop_first(), leq);
2727 assert(rest.len() == 0 || rest.first() == left.first() || rest.first()
2728 == right.drop_first().first()) by {
2729 assert(left.len() > 0);
2730 if right.drop_first().len() == 0 { } else if leq(left.first(), right.drop_first().first()) { assert(rest =~= Seq::<A>::empty().push(left.first()) + merge_sorted_with(
2733 left.drop_first(),
2734 right.drop_first(),
2735 leq,
2736 ));
2737 } else {
2738 assert(rest =~= Seq::<A>::empty().push(right.drop_first().first())
2739 + merge_sorted_with(left, right.drop_first().drop_first(), leq));
2740 }
2741 }
2742 lemma_new_first_element_still_sorted_by(
2743 right.first(),
2744 merge_sorted_with(left, right.drop_first(), leq),
2745 leq,
2746 );
2747 lemma_seq_union_to_multiset_commutative(left, right);
2748 assert((right.drop_first() + left) =~= (right + left).drop_first());
2749 lemma_seq_union_to_multiset_commutative(right.drop_first(), left);
2750 }
2751}
2752
2753pub proof fn lemma_max_of_concat(x: Seq<int>, y: Seq<int>)
2756 requires
2757 0 < x.len() && 0 < y.len(),
2758 ensures
2759 x.max() <= (x + y).max(),
2760 y.max() <= (x + y).max(),
2761 forall|elt: int| (x + y).contains(elt) ==> elt <= (x + y).max(),
2762 decreases x.len(),
2763{
2764 broadcast use group_seq_properties;
2765
2766 x.max_ensures();
2767 y.max_ensures();
2768 (x + y).max_ensures();
2769 assert(x.drop_first().len() == x.len() - 1);
2770 if x.len() == 1 {
2771 assert(y.max() <= (x + y).max()) by {
2772 assert((x + y).contains(y.max()));
2773 }
2774 } else {
2775 assert(x.max() <= (x + y).max()) by {
2776 assert(x.contains(x.max()));
2777 assert((x + y).contains(x.max()));
2778 }
2779 assert(x.drop_first() + y =~= (x + y).drop_first());
2780 lemma_max_of_concat(x.drop_first(), y);
2781 }
2782}
2783
2784pub proof fn lemma_min_of_concat(x: Seq<int>, y: Seq<int>)
2787 requires
2788 0 < x.len() && 0 < y.len(),
2789 ensures
2790 (x + y).min() <= x.min(),
2791 (x + y).min() <= y.min(),
2792 forall|elt: int| (x + y).contains(elt) ==> (x + y).min() <= elt,
2793 decreases x.len(),
2794{
2795 x.min_ensures();
2796 y.min_ensures();
2797 (x + y).min_ensures();
2798 broadcast use group_seq_properties;
2799
2800 if x.len() == 1 {
2801 assert((x + y).min() <= y.min()) by {
2802 assert((x + y).contains(y.min()));
2803 }
2804 } else {
2805 assert((x + y).min() <= x.min()) by {
2806 assert((x + y).contains(x.min()));
2807 }
2808 assert((x + y).min() <= y.min()) by {
2809 assert((x + y).contains(y.min()));
2810 }
2811 assert(x.drop_first() + y =~= (x + y).drop_first());
2812 lemma_max_of_concat(x.drop_first(), y)
2813 }
2814}
2815
2816pub broadcast proof fn to_multiset_build<A>(s: Seq<A>, a: A)
2820 ensures
2821 #![trigger s.push(a).to_multiset()]
2822 s.push(a).to_multiset() =~= s.to_multiset().insert(a),
2823 decreases s.len(),
2824{
2825 broadcast use super::multiset::group_multiset_axioms;
2826
2827 if s.len() == 0 {
2828 assert(s.to_multiset() =~= Multiset::<A>::empty());
2829 assert(s.push(a).drop_first() =~= Seq::<A>::empty());
2830 assert(s.push(a).to_multiset() =~= Multiset::<A>::empty().insert(a).add(
2831 Seq::<A>::empty().to_multiset(),
2832 ));
2833 } else {
2834 to_multiset_build(s.drop_first(), a);
2835 assert(s.drop_first().push(a).to_multiset() =~= s.drop_first().to_multiset().insert(a));
2836 assert(s.push(a).drop_first() =~= s.drop_first().push(a));
2837 }
2838}
2839
2840pub broadcast proof fn to_multiset_remove<A>(s: Seq<A>, i: int)
2841 requires
2842 0 <= i < s.len(),
2843 ensures
2844 #![trigger s.remove(i).to_multiset()]
2845 s.remove(i).to_multiset() == s.to_multiset().remove(s[i]),
2846{
2847 broadcast use super::multiset::group_multiset_axioms;
2848
2849 let s0 = s.subrange(0, i);
2850 let s1 = s.subrange(i, s.len() as int);
2851 let s2 = s.subrange(i + 1, s.len() as int);
2852 lemma_seq_union_to_multiset_commutative(s0, s2);
2853 lemma_seq_union_to_multiset_commutative(s0, s1);
2854 assert(s == s0 + s1);
2855 assert(s2 + s0 == (s1 + s0).drop_first());
2856 assert(s.remove(i).to_multiset() =~= s.to_multiset().remove(s[i]));
2857}
2858
2859pub broadcast proof fn to_multiset_insert<A>(s: Seq<A>, i: int, a: A)
2860 requires
2861 0 <= i <= s.len(),
2862 ensures
2863 #![trigger s.insert(i, a).to_multiset()]
2864 s.insert(i, a).to_multiset() == s.to_multiset().insert(a),
2865 decreases s.len(),
2866{
2867 broadcast use super::multiset::group_multiset_axioms;
2868
2869 let s0 = s.subrange(0, i);
2870 let s1 = s.subrange(i, s.len() as int);
2871
2872 assert(s =~= s0 + s1);
2873 assert(s.insert(i, a) =~= s0 + seq![a] + s1);
2874 assert(((s0 + seq![a]) + s1).to_multiset() =~= ((seq![a] + s0) + s1).to_multiset()) by {
2875 broadcast use lemma_multiset_commutative;
2876
2877 };
2878 assert((seq![a] + s0 + s1).drop_first() == s0 + s1);
2879 assert(s.insert(i, a).to_multiset() =~= s.to_multiset().insert(a));
2880}
2881
2882pub broadcast proof fn to_multiset_len<A>(s: Seq<A>)
2884 ensures
2885 s.len() == #[trigger] s.to_multiset().len(),
2886 decreases s.len(),
2887{
2888 broadcast use super::multiset::group_multiset_axioms;
2889
2890 if s.len() == 0 {
2891 assert(s.to_multiset() =~= Multiset::<A>::empty());
2892 assert(s.len() == 0);
2893 } else {
2894 to_multiset_len(s.drop_first());
2895 assert(s.len() == s.drop_first().len() + 1);
2896 assert(s.to_multiset().len() == s.drop_first().to_multiset().len() + 1);
2897 }
2898}
2899
2900pub broadcast proof fn to_multiset_contains<A>(s: Seq<A>, a: A)
2902 ensures
2903 #![trigger s.to_multiset().count(a)]
2904 s.contains(a) <==> s.to_multiset().count(a) > 0,
2905 decreases s.len(),
2906{
2907 broadcast use super::multiset::group_multiset_axioms;
2908
2909 if s.len() != 0 {
2910 if s.contains(a) {
2912 if s.first() == a {
2913 to_multiset_build(s, a);
2914 assert(s.to_multiset() =~= Multiset::<A>::empty().insert(s.first()).add(
2915 s.drop_first().to_multiset(),
2916 ));
2917 assert(Multiset::<A>::empty().insert(s.first()).contains(s.first()));
2918 } else {
2919 to_multiset_contains(s.drop_first(), a);
2920 assert(s.skip(1) =~= s.drop_first());
2921 lemma_seq_skip_contains(s, 1, a);
2922 assert(s.to_multiset().count(a) == s.drop_first().to_multiset().count(a));
2923 assert(s.contains(a) <==> s.to_multiset().count(a) > 0);
2924 }
2925 }
2926 if s.to_multiset().count(a) > 0 {
2929 to_multiset_contains(s.drop_first(), a);
2930 assert(s.contains(a) <==> s.to_multiset().count(a) > 0);
2931 } else {
2932 assert(s.contains(a) <==> s.to_multiset().count(a) > 0);
2933 }
2934 }
2935}
2936
2937pub broadcast proof fn to_multiset_update<A>(s: Seq<A>, i: int, a: A)
2938 requires
2939 0 <= i < s.len(),
2940 ensures
2941 #[trigger] s.update(i, a).to_multiset() == s.to_multiset().insert(a).remove(s[i]),
2942 decreases s.len(),
2943{
2944 broadcast use {
2945 super::seq_lib::lemma_seq_take_len,
2946 super::multiset::group_multiset_properties,
2947 super::multiset::group_multiset_axioms,
2948 to_multiset_insert,
2949 to_multiset_remove,
2950 to_multiset_contains,
2951 lemma_update_is_remove_insert,
2952 };
2953
2954 assert(s.update(i, a).to_multiset() =~= s.to_multiset().insert(a).remove(s[i]));
2955
2956}
2957
2958pub broadcast proof fn lemma_update_is_remove_insert<A>(s: Seq<A>, i: int, a: A)
2960 requires
2961 0 <= i < s.len(),
2962 ensures
2963 #[trigger] s.update(i, a) =~= s.remove(i).insert(i, a),
2964 decreases s.len(),
2965{
2966}
2967
2968pub proof fn lemma_append_last<A>(s1: Seq<A>, s2: Seq<A>)
2971 requires
2972 0 < s2.len(),
2973 ensures
2974 (s1 + s2).last() == s2.last(),
2975{
2976}
2977
2978pub proof fn lemma_concat_associative<A>(s1: Seq<A>, s2: Seq<A>, s3: Seq<A>)
2980 ensures
2981 s1.add(s2.add(s3)) =~= s1.add(s2).add(s3),
2982{
2983}
2984
2985spec fn seq_to_set_rec<A>(seq: Seq<A>) -> Set<A>
2987 decreases seq.len(),
2988{
2989 if seq.len() == 0 {
2990 Set::empty()
2991 } else {
2992 seq_to_set_rec(seq.drop_last()).insert(seq.last())
2993 }
2994}
2995
2996proof fn seq_to_set_rec_is_finite<A>(seq: Seq<A>)
2998 ensures
2999 seq_to_set_rec(seq).finite(),
3000 decreases seq.len(),
3001{
3002 broadcast use super::set::group_set_axioms;
3003
3004 if seq.len() > 0 {
3005 let sub_seq = seq.drop_last();
3006 assert(seq_to_set_rec(sub_seq).finite()) by {
3007 seq_to_set_rec_is_finite(sub_seq);
3008 }
3009 }
3010}
3011
3012proof fn seq_to_set_rec_contains<A>(seq: Seq<A>)
3014 ensures
3015 forall|a| #[trigger] seq.contains(a) <==> seq_to_set_rec(seq).contains(a),
3016 decreases seq.len(),
3017{
3018 broadcast use super::set::group_set_axioms;
3019
3020 if seq.len() > 0 {
3021 assert(forall|a| #[trigger]
3022 seq.drop_last().contains(a) <==> seq_to_set_rec(seq.drop_last()).contains(a)) by {
3023 seq_to_set_rec_contains(seq.drop_last());
3024 }
3025 assert(seq =~= seq.drop_last().push(seq.last()));
3026 assert forall|a| #[trigger] seq.contains(a) <==> seq_to_set_rec(seq).contains(a) by {
3027 if !seq.drop_last().contains(a) {
3028 if a == seq.last() {
3029 assert(seq.contains(a));
3030 assert(seq_to_set_rec(seq).contains(a));
3031 } else {
3032 assert(!seq_to_set_rec(seq).contains(a));
3033 }
3034 }
3035 }
3036 }
3037}
3038
3039proof fn seq_to_set_equal_rec<A>(seq: Seq<A>)
3041 ensures
3042 seq.to_set() == seq_to_set_rec(seq),
3043{
3044 broadcast use super::set::group_set_axioms;
3045
3046 assert(forall|n| #[trigger] seq.contains(n) <==> seq_to_set_rec(seq).contains(n)) by {
3047 seq_to_set_rec_contains(seq);
3048 }
3049 assert(forall|n| #[trigger] seq.contains(n) <==> seq.to_set().contains(n));
3050 assert(seq.to_set() =~= seq_to_set_rec(seq));
3051}
3052
3053pub broadcast proof fn seq_to_set_is_finite<A>(seq: Seq<A>)
3055 ensures
3056 #[trigger] seq.to_set().finite(),
3057{
3058 broadcast use super::set::group_set_axioms;
3059
3060 assert(seq.to_set().finite()) by {
3061 seq_to_set_equal_rec(seq);
3062 seq_to_set_rec_is_finite(seq);
3063 }
3064}
3065
3066pub proof fn seq_to_set_distributes_over_add<T>(s1: Seq<T>, s2: Seq<T>)
3067 ensures
3068 s1.to_set() + s2.to_set() =~= (s1 + s2).to_set(),
3069{
3070 broadcast use super::group_vstd_default;
3071 broadcast use super::set_lib::group_set_properties;
3072 broadcast use group_seq_properties;
3073
3074}
3075
3076pub proof fn lemma_no_dup_in_concat<A>(a: Seq<A>, b: Seq<A>)
3080 requires
3081 a.no_duplicates(),
3082 b.no_duplicates(),
3083 forall|i: int, j: int| 0 <= i < a.len() && 0 <= j < b.len() ==> a[i] != b[j],
3084 ensures
3085 #[trigger] (a + b).no_duplicates(),
3086{
3087}
3088
3089pub proof fn lemma_flatten_concat<A>(x: Seq<Seq<A>>, y: Seq<Seq<A>>)
3093 ensures
3094 (x + y).flatten() =~= x.flatten() + y.flatten(),
3095 decreases x.len(),
3096{
3097 if x.len() == 0 {
3098 assert(x + y =~= y);
3099 } else {
3100 assert((x + y).drop_first() =~= x.drop_first() + y);
3101 assert(x.first() + (x.drop_first() + y).flatten() =~= x.first() + x.drop_first().flatten()
3102 + y.flatten()) by {
3103 lemma_flatten_concat(x.drop_first(), y);
3104 }
3105 }
3106}
3107
3108pub proof fn lemma_flatten_alt_concat<A>(x: Seq<Seq<A>>, y: Seq<Seq<A>>)
3113 ensures
3114 (x + y).flatten_alt() =~= x.flatten_alt() + y.flatten_alt(),
3115 decreases y.len(),
3116{
3117 if y.len() == 0 {
3118 assert(x + y =~= x);
3119 } else {
3120 assert((x + y).drop_last() =~= x + y.drop_last());
3121 assert((x + y.drop_last()).flatten_alt() + y.last() =~= x.flatten_alt()
3122 + y.drop_last().flatten_alt() + y.last()) by {
3123 lemma_flatten_alt_concat(x, y.drop_last());
3124 }
3125 }
3126}
3127
3128pub broadcast proof fn lemma_seq_union_to_multiset_commutative<A>(a: Seq<A>, b: Seq<A>)
3131 ensures
3132 #[trigger] (a + b).to_multiset() =~= (b + a).to_multiset(),
3133{
3134 broadcast use super::multiset::group_multiset_axioms;
3135
3136 lemma_multiset_commutative(a, b);
3137 lemma_multiset_commutative(b, a);
3138}
3139
3140pub broadcast proof fn lemma_multiset_commutative<A>(a: Seq<A>, b: Seq<A>)
3143 ensures
3144 #[trigger] (a + b).to_multiset() =~= a.to_multiset().add(b.to_multiset()),
3145 decreases a.len(),
3146{
3147 broadcast use super::multiset::group_multiset_axioms;
3148
3149 if a.len() == 0 {
3150 assert(a + b =~= b);
3151 } else {
3152 lemma_multiset_commutative(a.drop_first(), b);
3153 assert(a.drop_first() + b =~= (a + b).drop_first());
3154 }
3155}
3156
3157pub proof fn lemma_sorted_unique<A>(x: Seq<A>, y: Seq<A>, leq: spec_fn(A, A) -> bool)
3159 requires
3160 sorted_by(x, leq),
3161 sorted_by(y, leq),
3162 total_ordering(leq),
3163 x.to_multiset() == y.to_multiset(),
3164 ensures
3165 x =~= y,
3166 decreases x.len(), y.len(),
3167{
3168 broadcast use super::multiset::group_multiset_axioms;
3169 broadcast use group_to_multiset_ensures;
3170
3171 if x.len() == 0 || y.len() == 0 {
3172 } else {
3173 assert(x.to_multiset().contains(x[0]));
3174 assert(x.to_multiset().contains(y[0]));
3175 let i = choose|i: int| #![trigger x.spec_index(i) ] 0 <= i < x.len() && x[i] == y[0];
3176 assert(leq(x[i], x[0]));
3177 assert(leq(x[0], x[i]));
3178 assert(x.drop_first().to_multiset() =~= x.to_multiset().remove(x[0]));
3179 assert(y.drop_first().to_multiset() =~= y.to_multiset().remove(y[0]));
3180 lemma_sorted_unique(x.drop_first(), y.drop_first(), leq);
3181 assert(x.drop_first() =~= y.drop_first());
3182 assert(x.first() == y.first());
3183 assert(x =~= Seq::<A>::empty().push(x.first()).add(x.drop_first()));
3184 assert(x =~= y);
3185 }
3186}
3187
3188pub broadcast proof fn lemma_seq_contains<A>(s: Seq<A>, x: A)
3190 ensures
3191 #[trigger] s.contains(x) <==> exists|i: int| 0 <= i < s.len() && #[trigger] s[i] == x,
3192{
3193}
3194
3195pub broadcast proof fn lemma_seq_empty_contains_nothing<A>(x: A)
3198 ensures
3199 !(#[trigger] Seq::<A>::empty().contains(x)),
3200{
3201}
3202
3203pub broadcast proof fn lemma_seq_empty_equality<A>(s: Seq<A>)
3207 ensures
3208 #[trigger] s.len() == 0 ==> s =~= Seq::<A>::empty(),
3209{
3210}
3211
3212pub broadcast proof fn lemma_seq_concat_contains_all_elements<A>(x: Seq<A>, y: Seq<A>, elt: A)
3216 ensures
3217 #[trigger] (x + y).contains(elt) <==> x.contains(elt) || y.contains(elt),
3218 decreases x.len(),
3219{
3220 if x.len() == 0 && y.len() > 0 {
3221 assert((x + y) =~= y);
3222 } else {
3223 assert forall|elt: A| #[trigger] x.contains(elt) implies #[trigger] (x + y).contains(
3224 elt,
3225 ) by {
3226 let index = choose|i: int| 0 <= i < x.len() && x[i] == elt;
3227 assert((x + y)[index] == elt);
3228 }
3229 assert forall|elt: A| #[trigger] y.contains(elt) implies #[trigger] (x + y).contains(
3230 elt,
3231 ) by {
3232 let index = choose|i: int| 0 <= i < y.len() && y[i] == elt;
3233 assert((x + y)[index + x.len()] == elt);
3234 }
3235 }
3236}
3237
3238pub broadcast proof fn lemma_seq_contains_after_push<A>(s: Seq<A>, v: A, x: A)
3241 ensures
3242 #[trigger] s.push(v).contains(x) <==> v == x || s.contains(x),
3243{
3244 assert forall|elt: A| #[trigger] s.contains(elt) implies #[trigger] s.push(v).contains(elt) by {
3245 let index = choose|i: int| 0 <= i < s.len() && s[i] == elt;
3246 assert(s.push(v)[index] == elt);
3247 }
3248 assert(s.push(v)[s.len() as int] == v);
3249}
3250
3251pub broadcast proof fn lemma_seq_subrange_elements<A>(s: Seq<A>, start: int, stop: int, x: A)
3255 requires
3256 0 <= start <= stop <= s.len(),
3257 ensures
3258 #[trigger] s.subrange(start, stop).contains(x) <==> (exists|i: int|
3259 0 <= start <= i < stop <= s.len() && #[trigger] s[i] == x),
3260{
3261 assert((exists|i: int| 0 <= start <= i < stop <= s.len() && s[i] == x) ==> s.subrange(
3262 start,
3263 stop,
3264 ).contains(x)) by {
3265 if exists|i: int| 0 <= start <= i < stop <= s.len() && s[i] == x {
3266 let index = choose|i: int| 0 <= start <= i < stop <= s.len() && s[i] == x;
3267 assert(s.subrange(start, stop)[index - start] == s[index]);
3268 }
3269 }
3270}
3271
3272pub open spec fn commutative_foldr<A, B>(f: spec_fn(A, B) -> B) -> bool {
3274 forall|x: A, y: A, v: B| #[trigger] f(x, f(y, v)) == f(y, f(x, v))
3275}
3276
3277pub open spec fn commutative_foldl<A, B>(f: spec_fn(B, A) -> B) -> bool {
3279 forall|x: A, y: A, v: B| #[trigger] f(f(v, x), y) == f(f(v, y), x)
3280}
3281
3282pub proof fn lemma_fold_right_permutation<A, B>(l1: Seq<A>, l2: Seq<A>, f: spec_fn(A, B) -> B, v: B)
3285 requires
3286 commutative_foldr(f),
3287 l1.to_multiset() == l2.to_multiset(),
3288 ensures
3289 l1.fold_right(f, v) == l2.fold_right(f, v),
3290 decreases l1.len(),
3291{
3292 broadcast use group_to_multiset_ensures;
3293
3294 if l1.len() > 0 {
3295 let a = l1.last();
3296 let i = l2.index_of(a);
3297 let l2r = l2.subrange(i + 1, l2.len() as int).fold_right(f, v);
3298
3299 assert(l1.to_multiset().count(a) > 0);
3300 l1.drop_last().lemma_fold_right_commute_one(a, f, v);
3301 l2.subrange(0, i).lemma_fold_right_commute_one(a, f, l2r);
3302
3303 l2.lemma_fold_right_split(f, v, i + 1);
3304 l2.remove(i).lemma_fold_right_split(f, v, i);
3305
3306 assert(l2.subrange(0, i + 1).drop_last() == l2.subrange(0, i));
3307 assert(l1.drop_last() == l1.remove(l1.len() - 1));
3308
3309 assert(l2.remove(i).subrange(0, i) == l2.subrange(0, i));
3310 assert(l2.remove(i).subrange(i, l2.remove(i).len() as int) == l2.subrange(
3311 i + 1,
3312 l2.len() as int,
3313 ));
3314
3315 lemma_fold_right_permutation(l1.drop_last(), l2.remove(i), f, v);
3316 } else {
3317 assert(l2.to_multiset().len() == 0);
3318 }
3319}
3320
3321pub proof fn lemma_fold_left_permutation<A, B>(l1: Seq<A>, l2: Seq<A>, f: spec_fn(B, A) -> B, v: B)
3324 requires
3325 commutative_foldl(f),
3326 l1.to_multiset() == l2.to_multiset(),
3327 ensures
3328 l1.fold_left(v, f) == l2.fold_left(v, f),
3329{
3330 let g = |a: A, b: B| f(b, a);
3331 assert(f =~= |b: B, a: A| g(a, b));
3332 assert(l1.fold_left(v, f) == l1.reverse().fold_right(g, v)) by {
3333 l1.lemma_reverse_fold_right(v, g)
3334 };
3335 assert(l2.fold_left(v, f) == l2.reverse().fold_right(g, v)) by {
3336 l2.lemma_reverse_fold_right(v, g)
3337 };
3338 assert(l1.reverse().to_multiset() =~= l2.reverse().to_multiset()) by {
3339 l1.lemma_reverse_to_multiset();
3340 l2.lemma_reverse_to_multiset();
3341 }
3342 assert(forall|x: A| #[trigger] l1.reverse().contains(x) ==> l1.contains(x));
3343 assert(forall|x: A| #[trigger] l2.reverse().contains(x) ==> l2.contains(x));
3344 lemma_fold_right_permutation(l1.reverse(), l2.reverse(), g, v);
3345}
3346
3347pub broadcast proof fn lemma_seq_take_len<A>(s: Seq<A>, n: int)
3353 ensures
3354 0 <= n <= s.len() ==> #[trigger] s.take(n).len() == n,
3355{
3356}
3357
3358pub broadcast proof fn lemma_seq_take_contains<A>(s: Seq<A>, n: int, x: A)
3362 requires
3363 0 <= n <= s.len(),
3364 ensures
3365 #[trigger] s.take(n).contains(x) <==> (exists|i: int|
3366 0 <= i < n <= s.len() && #[trigger] s[i] == x),
3367{
3368 assert((exists|i: int| 0 <= i < n <= s.len() && #[trigger] s[i] == x) ==> s.take(n).contains(x))
3369 by {
3370 if exists|i: int| 0 <= i < n <= s.len() && #[trigger] s[i] == x {
3371 let index = choose|i: int| 0 <= i < n <= s.len() && #[trigger] s[i] == x;
3372 assert(s.take(n)[index] == s[index]);
3373 }
3374 }
3375}
3376
3377pub broadcast proof fn lemma_seq_take_index<A>(s: Seq<A>, n: int, j: int)
3381 ensures
3382 0 <= j < n <= s.len() ==> #[trigger] s.take(n)[j] == s[j],
3383{
3384}
3385
3386pub proof fn subrange_of_matching_take<T>(a: Seq<T>, b: Seq<T>, s: int, e: int, l: int)
3387 requires
3388 a.take(l) == b.take(l),
3389 l <= a.len(),
3390 l <= b.len(),
3391 0 <= s <= e <= l,
3392 ensures
3393 a.subrange(s, e) == b.subrange(s, e),
3394{
3395 assert forall|i| 0 <= i < e - s implies a.subrange(s, e)[i] == b.subrange(s, e)[i] by {
3396 assert(a.subrange(s, e)[i] == a.take(l)[i + s]);
3397 }
3399 assert(a.subrange(s, e) == b.subrange(s, e));
3402}
3403
3404pub broadcast proof fn lemma_seq_skip_len<A>(s: Seq<A>, n: int)
3408 ensures
3409 0 <= n <= s.len() ==> #[trigger] s.skip(n).len() == s.len() - n,
3410{
3411}
3412
3413pub broadcast proof fn lemma_seq_skip_contains<A>(s: Seq<A>, n: int, x: A)
3417 requires
3418 0 <= n <= s.len(),
3419 ensures
3420 #[trigger] s.skip(n).contains(x) <==> (exists|i: int|
3421 0 <= n <= i < s.len() && #[trigger] s[i] == x),
3422{
3423 assert((exists|i: int| 0 <= n <= i < s.len() && #[trigger] s[i] == x) ==> s.skip(n).contains(x))
3424 by {
3425 let index = choose|i: int| 0 <= n <= i < s.len() && #[trigger] s[i] == x;
3426 lemma_seq_skip_index(s, n, index - n);
3427 }
3428}
3429
3430pub broadcast proof fn lemma_seq_skip_index<A>(s: Seq<A>, n: int, j: int)
3434 ensures
3435 0 <= n && 0 <= j < (s.len() - n) ==> #[trigger] s.skip(n)[j] == s[j + n],
3436{
3437}
3438
3439pub broadcast proof fn lemma_seq_skip_index2<A>(s: Seq<A>, n: int, k: int)
3444 ensures
3445 0 <= n <= k < s.len() ==> (#[trigger] s.skip(n))[k - n] == #[trigger] s[k],
3446{
3447}
3448
3449pub broadcast proof fn lemma_seq_append_take_skip<A>(a: Seq<A>, b: Seq<A>, n: int)
3454 ensures
3455 #![trigger (a + b).take(n)]
3456 #![trigger (a + b).skip(n)]
3457 n == a.len() ==> ((a + b).take(n) =~= a && (a + b).skip(n) =~= b),
3458{
3459}
3460
3461pub broadcast proof fn lemma_seq_take_update_commut1<A>(s: Seq<A>, i: int, v: A, n: int)
3468 ensures
3469 #![trigger s.update(i, v).take(n)]
3470 0 <= i < n <= s.len() ==> #[trigger] s.update(i, v).take(n) =~= s.take(n).update(i, v),
3471{
3472}
3473
3474pub broadcast proof fn lemma_seq_take_update_commut2<A>(s: Seq<A>, i: int, v: A, n: int)
3479 ensures
3480 0 <= n <= i < s.len() ==> #[trigger] s.update(i, v).take(n) =~= s.take(n),
3481{
3482}
3483
3484pub broadcast proof fn lemma_seq_skip_update_commut1<A>(s: Seq<A>, i: int, v: A, n: int)
3489 ensures
3490 0 <= n <= i < s.len() ==> #[trigger] s.update(i, v).skip(n) =~= s.skip(n).update(i - n, v),
3491{
3492}
3493
3494pub broadcast proof fn lemma_seq_skip_update_commut2<A>(s: Seq<A>, i: int, v: A, n: int)
3499 ensures
3500 0 <= i < n <= s.len() ==> #[trigger] s.update(i, v).skip(n) =~= s.skip(n),
3501{
3502}
3503
3504pub broadcast proof fn lemma_seq_skip_build_commut<A>(s: Seq<A>, v: A, n: int)
3508 ensures
3509 #![trigger s.push(v).skip(n)]
3510 0 <= n <= s.len() ==> s.push(v).skip(n) =~= s.skip(n).push(v),
3511{
3512}
3513
3514pub broadcast proof fn lemma_seq_skip_nothing<A>(s: Seq<A>, n: int)
3517 ensures
3518 n == 0 ==> #[trigger] s.skip(n) =~= s,
3519{
3520}
3521
3522pub broadcast proof fn lemma_seq_take_nothing<A>(s: Seq<A>, n: int)
3525 ensures
3526 n == 0 ==> #[trigger] s.take(n) =~= Seq::<A>::empty(),
3527{
3528}
3529
3530pub broadcast proof fn lemma_seq_skip_of_skip<A>(s: Seq<A>, m: int, n: int)
3535 ensures
3536 (0 <= m && 0 <= n && m + n <= s.len()) ==> #[trigger] s.skip(m).skip(n) =~= s.skip(m + n),
3537{
3538}
3539
3540#[deprecated = "Use `broadcast use group_seq_properties` instead"]
3542pub proof fn lemma_seq_properties<A>()
3543 ensures
3544 forall|s: Seq<A>, x: A|
3545 s.contains(x) <==> exists|i: int| 0 <= i < s.len() && #[trigger] s[i] == x, forall|x: A| !(#[trigger] Seq::<A>::empty().contains(x)), forall|s: Seq<A>| #[trigger] s.len() == 0 ==> s =~= Seq::<A>::empty(), forall|x: Seq<A>, y: Seq<A>, elt: A| #[trigger]
3549 (x + y).contains(elt) <==> x.contains(elt) || y.contains(elt), forall|s: Seq<A>, v: A, x: A| #[trigger] s.push(v).contains(x) <==> v == x || s.contains(x), forall|s: Seq<A>, start: int, stop: int, x: A|
3552 (0 <= start <= stop <= s.len() && #[trigger] s.subrange(start, stop).contains(x)) <==> (
3553 exists|i: int| 0 <= start <= i < stop <= s.len() && #[trigger] s[i] == x), forall|s: Seq<A>, n: int| 0 <= n <= s.len() ==> #[trigger] s.take(n).len() == n, forall|s: Seq<A>, n: int, x: A|
3556 (#[trigger] s.take(n).contains(x) && 0 <= n <= s.len()) <==> (exists|i: int|
3557 0 <= i < n <= s.len() && #[trigger] s[i] == x), forall|s: Seq<A>, n: int, j: int| 0 <= j < n <= s.len() ==> #[trigger] s.take(n)[j] == s[j], forall|s: Seq<A>, n: int| 0 <= n <= s.len() ==> #[trigger] s.skip(n).len() == s.len() - n, forall|s: Seq<A>, n: int, x: A|
3561 (#[trigger] s.skip(n).contains(x) && 0 <= n <= s.len()) <==> (exists|i: int|
3562 0 <= n <= i < s.len() && #[trigger] s[i] == x), forall|s: Seq<A>, n: int, j: int|
3564 0 <= n && 0 <= j < (s.len() - n) ==> #[trigger] s.skip(n)[j] == s[j + n], forall|a: Seq<A>, b: Seq<A>, n: int|
3566 #![trigger (a+b).take(n)]
3567 #![trigger (a+b).skip(n)]
3568 n == a.len() ==> ((a + b).take(n) =~= a && (a + b).skip(n) =~= b), forall|s: Seq<A>, i: int, v: A, n: int|
3570 0 <= i < n <= s.len() ==> #[trigger] s.update(i, v).take(n) == s.take(n).update(i, v), forall|s: Seq<A>, i: int, v: A, n: int|
3572 0 <= n <= i < s.len() ==> #[trigger] s.update(i, v).take(n) == s.take(n), forall|s: Seq<A>, i: int, v: A, n: int|
3574 0 <= n <= i < s.len() ==> #[trigger] s.update(i, v).skip(n) == s.skip(n).update(
3575 i - n,
3576 v,
3577 ), forall|s: Seq<A>, i: int, v: A, n: int|
3579 0 <= i < n <= s.len() ==> #[trigger] s.update(i, v).skip(n) == s.skip(n), forall|s: Seq<A>, v: A, n: int|
3581 0 <= n <= s.len() ==> #[trigger] s.push(v).skip(n) == s.skip(n).push(v), forall|s: Seq<A>, n: int| n == 0 ==> #[trigger] s.skip(n) == s, forall|s: Seq<A>, n: int| n == 0 ==> #[trigger] s.take(n) == Seq::<A>::empty(), forall|s: Seq<A>, m: int, n: int|
3585 (0 <= m && 0 <= n && m + n <= s.len()) ==> #[trigger] s.skip(m).skip(n) == s.skip(
3586 m + n,
3587 ), forall|s: Seq<A>, a: A| #[trigger] (s.push(a).to_multiset()) =~= s.to_multiset().insert(a), forall|s: Seq<A>| s.len() == #[trigger] s.to_multiset().len(), forall|s: Seq<A>, a: A|
3591 s.contains(a) <==> #[trigger] s.to_multiset().count(a)
3592 > 0, {
3594 broadcast use {group_seq_properties, lemma_seq_skip_of_skip};
3595
3596}
3597
3598#[doc(hidden)]
3599#[verifier::inline]
3600pub open spec fn check_argument_is_seq<A>(s: Seq<A>) -> Seq<A> {
3601 s
3602}
3603
3604#[macro_export]
3649macro_rules! assert_seqs_equal {
3650 [$($tail:tt)*] => {
3651 $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::seq_lib::assert_seqs_equal_internal!($($tail)*))
3652 };
3653}
3654
3655#[macro_export]
3656#[doc(hidden)]
3657macro_rules! assert_seqs_equal_internal {
3658 (::vstd::spec_eq($s1:expr, $s2:expr)) => {
3659 $crate::vstd::seq_lib::assert_seqs_equal_internal!($s1, $s2)
3660 };
3661 (::vstd::prelude::spec_eq($s1:expr, $s2:expr)) => {
3662 $crate::vstd::seq_lib::assert_seqs_equal_internal!($s1, $s2)
3663 };
3664 (::vstd::prelude::spec_eq($s1:expr, $s2:expr), $idx:ident => $bblock:block) => {
3665 $crate::vstd::seq_lib::assert_seqs_equal_internal!($s1, $s2, $idx => $bblock)
3666 };
3667 (crate::prelude::spec_eq($s1:expr, $s2:expr)) => {
3668 $crate::vstd::seq_lib::assert_seqs_equal_internal!($s1, $s2)
3669 };
3670 (crate::prelude::spec_eq($s1:expr, $s2:expr), $idx:ident => $bblock:block) => {
3671 $crate::vstd::seq_lib::assert_seqs_equal_internal!($s1, $s2, $idx => $bblock)
3672 };
3673 (crate::verus_builtin::spec_eq($s1:expr, $s2:expr)) => {
3674 $crate::vstd::seq_lib::assert_seqs_equal_internal!($s1, $s2)
3675 };
3676 (crate::verus_builtin::spec_eq($s1:expr, $s2:expr), $idx:ident => $bblock:block) => {
3677 $crate::vstd::seq_lib::assert_seqs_equal_internal!($s1, $s2, $idx => $bblock)
3678 };
3679 ($s1:expr, $s2:expr $(,)?) => {
3680 $crate::vstd::seq_lib::assert_seqs_equal_internal!($s1, $s2, idx => { })
3681 };
3682 ($s1:expr, $s2:expr, $idx:ident => $bblock:block) => {
3683 #[verifier::spec] let s1 = $crate::vstd::seq_lib::check_argument_is_seq($s1);
3684 #[verifier::spec] let s2 = $crate::vstd::seq_lib::check_argument_is_seq($s2);
3685 $crate::vstd::prelude::assert_by($crate::vstd::prelude::equal(s1, s2), {
3686 $crate::vstd::prelude::assert_(s1.len() == s2.len());
3687 $crate::vstd::prelude::assert_forall_by(|$idx : $crate::vstd::prelude::int| {
3688 $crate::vstd::prelude::requires($crate::vstd::prelude::verus_proof_expr!(0 <= $idx && $idx < s1.len()));
3689 $crate::vstd::prelude::ensures($crate::vstd::prelude::equal(s1.index($idx), s2.index($idx)));
3690 { $bblock }
3691 });
3692 $crate::vstd::prelude::assert_($crate::vstd::prelude::ext_equal(s1, s2));
3693 });
3694 }
3695}
3696
3697pub broadcast group group_filter_ensures {
3698 Seq::lemma_filter_len,
3699 Seq::lemma_filter_pred,
3700 Seq::lemma_filter_contains,
3701}
3702
3703pub broadcast group group_seq_lib_default {
3704 group_filter_ensures,
3705 Seq::add_empty_left,
3706 Seq::add_empty_right,
3707 Seq::push_distributes_over_add,
3708 Seq::filter_distributes_over_add,
3709 seq_to_set_is_finite,
3710 Seq::lemma_fold_right_split,
3711 Seq::lemma_fold_left_split,
3712}
3713
3714pub broadcast group group_to_multiset_ensures {
3715 to_multiset_build,
3716 to_multiset_remove,
3717 to_multiset_len,
3718 to_multiset_contains,
3719 to_multiset_insert,
3720 to_multiset_update,
3721}
3722
3723pub broadcast group group_seq_properties {
3725 lemma_seq_contains,
3726 lemma_seq_empty_contains_nothing,
3727 lemma_seq_empty_equality,
3728 lemma_seq_concat_contains_all_elements,
3729 lemma_seq_contains_after_push,
3730 lemma_seq_subrange_elements,
3731 lemma_seq_take_len,
3732 lemma_seq_take_contains,
3733 lemma_seq_take_index,
3734 lemma_seq_skip_len,
3735 lemma_seq_skip_contains,
3736 lemma_seq_skip_index,
3737 lemma_seq_skip_index2,
3738 lemma_seq_append_take_skip,
3739 lemma_seq_take_update_commut1,
3740 lemma_seq_take_update_commut2,
3741 lemma_seq_skip_update_commut1,
3742 lemma_seq_skip_update_commut2,
3743 lemma_seq_skip_build_commut,
3744 lemma_seq_skip_nothing,
3745 lemma_seq_take_nothing,
3746 group_to_multiset_ensures,
3750}
3751
3752#[doc(hidden)]
3753pub use assert_seqs_equal_internal;
3754pub use assert_seqs_equal;
3755
3756}