vstd/
seq_lib.rs

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    /// Applies the function `f` to each element of the sequence, and returns
22    /// the resulting sequence.
23    /// The `int` parameter of `f` is the index of the element being mapped.
24    // TODO(verus): rename to map_entries, for consistency with Map::map
25    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    /// Applies the function `f` to each element of the sequence, and returns
30    /// the resulting sequence.
31    // TODO(verus): rename to map, because this is what everybody wants.
32    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    /// Applies the function `f` to each element of the sequence,
37    /// producing a sequence of sequences, and then concatenates (flattens)
38    /// those into a single flat sequence of `B`.
39    ///
40    /// ## Example
41    ///
42    /// ```rust
43    /// fn example() {
44    ///     let s = seq![1, 2, 3];
45    ///     let result = s.flat_map(|x| seq![x, x]);
46    ///     assert_eq!(result, seq![1, 1, 2, 2, 3, 3]);
47    /// }
48    /// ``
49    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    /// Is true if the calling sequence is a prefix of the given sequence 'other'.
54    ///
55    /// ## Example
56    ///
57    /// ```rust
58    /// proof fn prefix_test() {
59    ///     let pre: Seq<int> = seq![1, 2, 3];
60    ///     let whole: Seq<int> = seq![1, 2, 3, 4, 5];
61    ///     assert(pre.is_prefix_of(whole));
62    /// }
63    /// ```
64    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    /// Is true if the calling sequence is a suffix of the given sequence 'other'.
69    ///
70    /// ## Example
71    ///
72    /// ```rust
73    /// proof fn suffix_test() {
74    ///     let end: Seq<int> = seq![3, 4, 5];
75    ///     let whole: Seq<int> = seq![1, 2, 3, 4, 5];
76    ///     assert(end.is_suffix_of(whole));
77    /// }
78    /// ```
79    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    /// Sorts the sequence according to the given leq function
87    ///
88    /// ## Example
89    ///
90    /// ```rust
91    /// {{#include ../../../../examples/multiset.rs:sorted_by_leq}}
92    /// ```
93    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    /// Tests if all elements in the sequence satisfy the predicate.
111    ///
112    /// ## Example
113    ///
114    /// ```rust
115    /// fn example() {
116    ///     let s = seq![2, 4, 6, 8];
117    ///     assert!(s.all(|x| x % 2 == 0));
118    /// }
119    /// ```
120    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    /// Tests if any element in the sequence satisfies the predicate.
125    ///
126    /// ## Example
127    ///
128    /// ```rust
129    /// fn example() {
130    ///     let s = seq![1, 2, 3, 4];
131    ///     assert!(s.any(|x| x > 3));
132    /// }
133    /// ```
134    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    /// Checks that exactly one element in the sequence satisfies the given predicate.
139    /// ## Example
140    ///
141    /// ```rust
142    /// fn example() {
143    ///     let s = seq![1, 2, 3];
144    ///     assert!(s.exactly_one(|x| x == 2));
145    /// }
146    /// ```
147    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    /// Returns the sequence containing only the elements of the original sequence
184    /// such that pred(element) is true.
185    ///
186    /// ## Example
187    ///
188    /// ```rust
189    /// proof fn filter_test() {
190    ///    let seq: Seq<int> = seq![1, 2, 3, 4, 5];
191    ///    let even: Seq<int> = seq.filter(|x| x % 2 == 0);
192    ///    reveal_with_fuel(Seq::<int>::filter, 6); //Needed for Verus to unfold the recursive definition of filter
193    ///    assert(even =~= seq![2, 4]);
194    /// }
195    /// ```
196    #[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    // the filtered list can't grow
215
216            #[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        // TODO: remove this after proved filter_lemma is proved
233        #[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        // TODO: remove this after proved filter_lemma is proved
244        #[allow(deprecated)]
245        self.filter_lemma(pred);
246    }
247
248    // deprecated since the triggers inside of 2 of the conjuncts are blocked
249    #[deprecated = "Use `broadcast use group_filter_ensures` instead" ]
250    pub proof fn filter_lemma(self, pred: spec_fn(A) -> bool)
251        ensures
252    // we don't keep anything bad
253    // TODO(andrea): recommends didn't catch this error, where i isn't known to be in
254    // self.filter(pred).len()
255    //forall |i: int| 0 <= i < self.len() ==> pred(#[trigger] self.filter(pred)[i]),
256
257            forall|i: int|
258                0 <= i < self.filter(pred).len() ==> pred(#[trigger] self.filter(pred)[i]),
259            // we keep everything we should
260            forall|i: int|
261                0 <= i < self.len() && pred(self[i]) ==> #[trigger] self.filter(pred).contains(
262                    self[i],
263                ),
264            // the filtered list can't grow
265            #[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]);  // trigger drop_last
275                    assert(pred(out[i]));  // TODO(andrea): why is this line required? It's the conclusion of the assert-forall.
276                }
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]);  // witness to contains
282                } else {
283                    let subseq = self.drop_last().filter(pred);
284                    assert(subseq.contains(self.drop_last()[i]));  // trigger recursive invocation
285                    let j = choose|j| 0 <= j < subseq.len() && subseq[j] == self[i];
286                    assert(out[j] == self[i]);  // TODO(andrea): same, seems needless
287                }
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    /// Returns the maximum value in a non-empty sequence, given sorting function leq
340    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    /// Returns the minimum value in a non-empty sequence, given sorting function leq
357    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    // TODO is_sorted -- extract from summer_school e22
376    pub open spec fn contains(self, needle: A) -> bool {
377        exists|i: int| 0 <= i < self.len() && self[i] == needle
378    }
379
380    /// Returns an index where `needle` appears in the sequence.
381    /// Returns an arbitrary value if the sequence does not contain the `needle`.
382    pub open spec fn index_of(self, needle: A) -> int {
383        choose|i: int| 0 <= i < self.len() && self[i] == needle
384    }
385
386    /// For an element that occurs at least once in a sequence, if its first occurence
387    /// is at index i, Some(i) is returned. Otherwise, None is returned
388    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    // Recursive helper function for index_of_first
397    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  //arbitrary, will never get to this case
404
405        } 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    /// For an element that occurs at least once in a sequence, if its last occurence
437    /// is at index i, Some(i) is returned. Otherwise, None is returned
438    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    // Recursive helper function for last_index_of
447    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  //arbitrary, will never get to this case
454
455        } 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    /// Drops the last element of a sequence and returns a sequence whose length is
487    /// thereby 1 smaller.
488    ///
489    /// If the input sequence is empty, the result is meaningless and arbitrary.
490    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    /// Dropping the last element of a concatenation of `a` and `b` is equivalent
498    /// to skipping the last element of `b` and then concatenating `a` and `b`
499    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    /// returns `true` if the sequence has no duplicate elements
516    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    /// Returns `true` if two sequences are disjoint
521    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    /// Converts a sequence into a set
526    pub open spec fn to_set(self) -> Set<A> {
527        Set::new(|a: A| self.contains(a))
528    }
529
530    /// Converts a sequence into a multiset
531    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    // Parts of verified lemma used to be an axiom in the Dafny prelude
542    // Note: the inner triggers in this lemma are blocked by `to_multiset_len`
543    /// Proof of function to_multiset() correctness
544    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),  // to_multiset_build
547            forall|i: int|
548                0 <= i < self.len() ==> #[trigger] (self.remove(i).to_multiset())
549                    =~= self.to_multiset().remove(self[i]),  // to_multiset_remove
550            self.len() == #[trigger] self.to_multiset().len(),  // to_multiset_len
551            forall|a: A|
552                self.contains(a) <==> #[trigger] self.to_multiset().count(a)
553                    > 0,  // to_multiset_contains
554    {
555        broadcast use group_seq_properties;
556
557    }
558
559    /// Insert item a at index i, shifting remaining elements (if any) to the right
560    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    /// Proof of correctness and expected properties of insert function
568    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    /// Remove item at index i, shifting remaining elements to the left
580    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    /// Proof of function remove() correctness
588    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    /// If a given element occurs at least once in a sequence, the sequence without
600    /// its first occurrence is returned. Otherwise the same sequence is returned.
601    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    /// Returns the sequence that is in reverse order to a given sequence.
610    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    /// Zips two sequences of equal length into one sequence that consists of pairs.
621    /// If the two sequences are different lengths, returns an empty sequence
622    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    /// Folds the sequence to the left, applying `f` to perform the fold.
637    ///
638    /// Equivalent to `Iterator::fold` in Rust.
639    ///
640    /// Given a sequence `s = [x0, x1, x2, ..., xn]`, applying this function `s.fold_left(b, f)`
641    /// returns `f(...f(f(b, x0), x1), ..., xn)`.
642    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    /// Equivalent to [`Self::fold_left`] but defined by breaking off the leftmost element when
653    /// recursing, rather than the rightmost. See [`Self::lemma_fold_left_alt`] that proves
654    /// equivalence.
655    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    /// A lemma that proves how [`Self::fold_left`] distributes over splitting a sequence.
666    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    /// An auxiliary lemma for proving [`Self::lemma_fold_left_alt`].
697    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            // trivial base case
710        } 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    /// [`Self::fold_left`] and [`Self::fold_left_alt`] are equivalent.
729    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            // trivial base cases
738        } 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    /// [`Self::fold_left`] on the reversed sequence is equivalent to
749    /// [`Self::fold_right`] on the original sequence with corresponding folding operator
750    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    /// Folds the sequence to the right, applying `f` to perform the fold.
761    ///
762    /// Equivalent to `DoubleEndedIterator::rfold` in Rust.
763    ///
764    /// Given a sequence `s = [x0, x1, x2, ..., xn]`, applying this function `s.fold_right(b, f)`
765    /// returns `f(x0, f(x1, f(x2, ..., f(xn, b)...)))`.
766    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    /// Equivalent to [`Self::fold_right`] but defined by breaking off the leftmost element when
777    /// recursing, rather than the rightmost. See [`Self::lemma_fold_right_alt`] that proves
778    /// equivalence.
779    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    /// A lemma that proves how [`Self::fold_right`] distributes over splitting a sequence.
790    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            // trivial base case
805        } 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    // Lemma that proves it's possible to commute a commutative operator across fold_right.
823    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    /// [`Self::fold_right`] and [`Self::fold_right_alt`] are equivalent.
836    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            // trivial base cases
845        } 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    /// [`Self::fold_right`] on the reversed sequence is equivalent to
852    /// [`Self::fold_left`] on the original sequence with corresponding folding operator
853    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    // Proven lemmas
881    /// Given a sequence with no duplicates, each element occurs only
882    /// once in its conversion to a multiset
883    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    /// If, in a sequence's conversion to a multiset, each element occurs only once,
904    /// the sequence has no duplicates.
905    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    /// Conversion of a sequence to multiset is equivalent to conversion of its reversion to multiset
940    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    /// The concatenation of two subsequences derived from a non-empty sequence,
962    /// the first obtained from skipping the last element, the second consisting only
963    /// of the last element, is the original sequence.
964    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    /// If a predicate is true at every index of a sequence,
973    /// it is true for every member of the sequence as a collection.
974    /// Useful for converting quantifiers between the two forms
975    /// to satisfy a precondition in the latter form.
976    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    /// If a predicate is true for every member of a sequence as a collection,
986    /// it is true at every index of the sequence.
987    /// Useful for converting quantifiers between the two forms
988    /// to satisfy a precondition in the latter form.
989    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    /// A sequence that is sliced at the pos-th element, concatenated
1001    /// with that same sequence sliced from the pos-th element, is equal to the
1002    /// original unsliced sequence.
1003    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    /// Any element in a slice is included in the original sequence.
1012    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    /// A slice (from s2..e2) of a slice (from s1..e1) of a sequence is equal to just a
1024    /// slice (s1+s2..s1+e2) of the original sequence.
1025    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    /// A sequence of unique items, when converted to a set, produces a set with matching length
1035    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    /// The cardinality of a set of elements is always less than or
1058    /// equal to that of the full sequence of elements.
1059    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    /// A sequence is of length 0 if and only if its conversion to
1076    /// a set results in the empty set.
1077    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    /// A sequence with cardinality equal to its set has no duplicates.
1093    /// Inverse property of that shown in lemma unique_seq_to_set
1094    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                // If there is a duplicate, then we show that |s.to_set()| == |s| cannot hold.
1108                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    /// Mapping a function over a sequence and converting to a set is the same
1122    /// as mapping it over the sequence converted to a set.
1123    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    /// Appending an element to a sequence and converting to set, is equal
1146    /// to converting to set and inserting it.
1147    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    /// Update a subrange of a sequence starting at `off` to values `vs`.
1162    /// Expects that the updated subrange `off` up to `off+vs.len()` fits
1163    /// in the existing sequence.
1164    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    /// Skipping `i` elements and then 1 more is equivalent to skipping `i + 1` elements.
1181    ///
1182    /// ## Example
1183    ///
1184    /// ```rust
1185    /// proof fn example() {
1186    ///     let s = seq![1, 2, 3, 4];
1187    ///     s.lemma_seq_skip_skip(2);
1188    ///     assert(s.skip(2).skip(1) =~= s.skip(3));
1189    /// }
1190    /// ```
1191    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    /// If an element is contained in a sequence, then there exists an index where that element appears.
1200    ///
1201    /// ## Example
1202    ///
1203    /// ```rust
1204    /// proof fn example() {
1205    ///     let s = seq![10, 20, 30];
1206    ///     assert(s.contains(20));
1207    ///     let idx = s.lemma_contains_to_index(20);
1208    ///     assert(s[idx] == 20);
1209    /// }
1210    /// ```
1211    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    /// If a predicate holds for the first element and for all elements in the tail,
1229    /// then it holds for the entire sequence.
1230    ///
1231    /// ## Example
1232    ///
1233    /// ```rust
1234    /// proof fn example() {
1235    ///     let s = seq![2, 4, 6, 8];
1236    ///     let is_even = |x| x % 2 == 0;
1237    ///     assert(is_even(s[0]));
1238    ///     assert(s.skip(1).all(is_even));
1239    ///     s.lemma_all_from_head_tail(is_even);
1240    ///     assert(s.all(is_even));
1241    /// }
1242    /// ```
1243    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    /// If a predicate holds for any element in the sequence and does not hold for the first element,
1256    /// then the predicate must hold for some element in the tail.
1257    ///
1258    /// ## Example
1259    ///
1260    /// ```rust
1261    /// proof fn example() {
1262    ///     let s = seq![1, 4, 6, 8];
1263    ///     let is_even = |x| x % 2 == 0;
1264    ///     assert(s.any(is_even));
1265    ///     assert(!is_even(s[0]));
1266    ///     s.lemma_any_tail(is_even);
1267    ///     assert(s.skip(1).any(is_even));
1268    /// }
1269    /// ```
1270    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    /// Removes duplicate elements from a sequence, maintaining the order of first appearance.
1281    /// Takes a `seen` sequence parameter to track previously encountered elements.
1282    ///
1283    /// ## Example
1284    ///
1285    /// ```rust
1286    /// fn example() {
1287    ///     let s = seq![1, 2, 1, 3, 2, 4];
1288    ///     let seen = seq![];
1289    ///     let result = s.remove_duplicates(seen);
1290    ///     assert_eq!(result, seq![1, 2, 3, 4]);
1291    ///
1292    ///     let seen2 = seq![2, 3];
1293    ///     let result2 = s.remove_duplicates(seen2);
1294    ///     assert_eq!(result2, seq![1, 4]);
1295    /// }
1296    /// ```
1297    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    /// Properties of remove_duplicates:
1310    /// - The output contains x if and only if x was in the input sequence or seen set
1311    /// - The output length is at most the sum of input and seen lengths
1312    ///
1313    /// ## Example
1314    ///
1315    /// ```rust
1316    /// proof fn example() {
1317    ///     let s = seq![1, 2, 1, 3];
1318    ///     let seen = seq![2];
1319    ///     s.lemma_remove_duplicates_properties(seen);
1320    ///     assert(s.remove_duplicates(seen).contains(1));
1321    ///     assert(s.remove_duplicates(seen).contains(3));
1322    ///     assert(!s.remove_duplicates(seen).contains(2));
1323    ///     assert(s.remove_duplicates(seen).len() <= s.len() + seen.len());
1324    /// }
1325    /// ```
1326    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    /// Shows that removing duplicates from a sequence is equivalent to:
1346    /// 1. First removing duplicates from the prefix up to index i (with the given seen set)
1347    /// 2. Using that result as the new seen set for removing duplicates from the suffix after i
1348    ///
1349    /// ## Example
1350    ///
1351    /// ```rust
1352    /// proof fn example() {
1353    ///     let s = seq![1, 2, 1, 3, 2, 4];
1354    ///     let seen = seq![];
1355    ///     s.lemma_remove_duplicates_append_index(seen, 2);
1356    ///     assert(s.remove_duplicates(seen)
1357    ///         =~= seq![1, 3, 2, 4].remove_duplicates(seq![1, 2].remove_duplicates(seen)));
1358    /// }
1359    /// ```
1360    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    /// For two sequences, skipping one element after concatenation equals concatenating
1391    /// the result of skipping one element of the first sequence (which must be non-empty)
1392    /// with the second sequence.
1393    ///
1394    /// ## Example
1395    /// ```rust
1396    /// proof fn example() {
1397    ///     let s1 = seq![1, 2];
1398    ///     let s2 = seq![3, 4, 5];
1399    ///
1400    ///     lemma_skip1_concat(s1, s2);
1401    ///     assert((s1 + s2).skip(1) =~= seq![2, 3, 4, 5]);
1402    /// }
1403    /// ```
1404    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    /// When appending an element `x` to a sequence:
1416    /// - If `x` is in `self + seen`, removing duplicates equals removing duplicates from self
1417    /// - If x is not in (self + seen), removing duplicates equals removing duplicates from self,
1418    ///   concatenated with [x]
1419    ///
1420    /// ## Example
1421    /// ```rust
1422    /// proof fn example() {
1423    ///     let s1 = seq![1, 2];
1424    ///     let seen = seq![];
1425    ///     assert!(!s1.contains(3));
1426    ///     lemma_remove_duplicates_append(s1, 3, seen);
1427    ///     assert((s1 + seq![3]).remove_duplicates(seen) =~= s1.remove_duplicates(seen) + seq![3]);
1428    /// }
1429    /// ```
1430    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    /// If all elements in a sequence fail the predicate,
1459    /// filtering by that predicate yields an empty sequence
1460    ///
1461    /// ## Example
1462    /// ```rust
1463    /// proof fn example() {
1464    ///     let s = seq![1, 2, 3];
1465    ///     let pred = |x| x > 5;
1466    ///     lemma_all_neg_filter_empty(s, pred);
1467    ///     assert(s.filter(pred).len() == 0);
1468    /// }
1469    /// ```
1470    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    /// Applies an Option-returning function to each element, keeping only successful (Some) results
1490    ///
1491    /// ## Example
1492    /// ```rust
1493    /// let s = seq![1, 2, 3];
1494    /// let f = |x| if x % 2 == 0 { Some(x * 2) } else { None };
1495    /// assert(s.filter_map(f) =~= seq![4]);
1496    /// ```
1497    pub open spec fn filter_map<B>(self, f: spec_fn(A) -> Option<B>) -> Seq<B>
1498        decreases self.len(),
1499    {
1500        // We're defining this by starting at the end of the list since it makes it
1501        // easier to reason about in the common case of looping over a vector in the
1502        // implementation.
1503        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    /// If an element exists in the filtered sequence,
1515    /// it must exist in the original sequence
1516    /// ```
1517    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    /// If an element exists in filter_map's output,
1538    /// there must be an input element that mapped to it
1539    /// ```
1540    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    /// Taking k+1 elements is the same as taking k elements plus the kth element
1564    ///
1565    /// ## Example
1566    /// ```rust
1567    /// let s = seq![1, 2, 3];
1568    /// lemma_take_plus_one(s, 1);
1569    /// seq![1, 2] == seq![1] + seq![2]
1570    /// ```
1571    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    /// filter_map on a single element sequence
1582    /// either produces a new single element sequence (if f returns Some)
1583    /// or an empty sequence (if f returns None)
1584    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    /// filter_map of take(i+1) equals
1595    /// filter_map of take(i) plus maybe the mapped i'th element
1596    ///
1597    /// ## Example
1598    /// ```rust
1599    /// let s = seq![1, 2, 3];
1600    /// let f = |x| if x % 2 == 0 { Some(x * 2) } else { None };
1601    /// s.lemma_filter_map_take_succ(s, f, 1);
1602    /// assert(s.take(2).filter_map(f) == s.take(1).filter_map(f) + seq![f(s[1]).unwrap()]);
1603    /// assert(s.take(2).filter_map(f) == seq![] + seq![4]);
1604    /// ```
1605    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    /// An alternative implementation of filter that processes the sequence recursively from
1626    /// left to right, in contrast to the standard filter which processes from right to left.
1627    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    /// When filtering (x + sequence), if x satisfies the predicate, x is prepended to
1642    /// the filtered sequence. Otherwise, only the filtered sequence remains.
1643    ///
1644    /// ## Example
1645    /// ```rust
1646    /// proof fn filter_prepend_test() {
1647    ///     let s = seq![2, 3, 4];
1648    ///     let is_even = |x: int| x % 2 == 0;
1649    ///     let with_five = seq![5] + s;
1650    ///     assert(with_five.filter(is_even) =~= seq![2, 4]); // 5 filtered out
1651    ///     let with_six = seq![6] + s;
1652    ///     assert(with_six.filter(is_even) =~= seq![6, 2, 4]); // 6 included
1653    /// }
1654    /// ```
1655    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    /// The filter() and filter_alt() methods produce equivalent results for any sequence
1696    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    /// Filtering preserves the prefix relationship between sequences.
1715    ///
1716    /// ## Example
1717    /// ```rust
1718    /// proof fn filter_monotone_test() {
1719    ///     let s = seq![1, 2, 3];
1720    ///     let ys = seq![1, 2, 3, 4, 5];
1721    ///     let is_even = |x: int| x % 2 == 0;
1722    ///     assert(s.is_prefix_of(ys));
1723    ///     assert(s.filter(is_even).is_prefix_of(ys.filter(is_even)));
1724    ///     assert(s.filter(is_even) =~= seq![2]);
1725    ///     assert(ys.filter(is_even) =~= seq![2, 4]);
1726    /// }
1727    /// ```
1728    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    /// The length of filter(take(i)) is never greater than the length of filter(entire_sequence).
1746    ///
1747    /// ## Example
1748    /// ```rust
1749    /// proof fn filter_take_len_test() {
1750    ///     let s = seq![1, 2, 3, 4, 5];
1751    ///     let is_even = |x: int| x % 2 == 0;
1752    ///     let i = 3;
1753    ///     assert(s.take(i) =~= seq![1, 2, 3]);
1754    ///     assert(s.take(i).filter(is_even) =~= seq![2]);
1755    ///     assert(s.filter(is_even) =~= seq![2, 4]);
1756    ///     assert(s.filter(is_even).len() >= s.take(i).filter(is_even).len());
1757    /// }
1758    /// ```
1759    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    /// Filtering a prefix of a sequence produces the same number or fewer elements
1774    /// as filtering the entire sequence.
1775    ///
1776    /// ## Example
1777    /// ```rust
1778    /// proof fn filter_take_len_test() {
1779    ///     let s = seq![1, 2, 3, 4, 5];
1780    ///     let is_even = |x: int| x % 2 == 0;
1781    ///     assert(s.filter(is_even).len() >= s.take(3).filter(is_even).len());
1782    /// }
1783    /// ```
1784    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    /// If an index i is valid for a sequence (0 ≤ i < len), then the element at that index
1798    /// is contained in the sequence.
1799    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    /// Taking i+1 elements from a sequence is equivalent to taking i elements
1808    /// and then pushing the element at index i.
1809    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    /// Taking the full length of a sequence returns the sequence itself.
1820    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    /// Taking i+1 elements and checking if any element satisfies predicate p is equivalent to:
1829    /// either taking i elements and checking if any satisfies p, OR checking if the i-th element satisfies p.
1830    ///
1831    /// ## Example
1832    /// ```rust
1833    /// proof fn take_any_succ_test() {
1834    ///     let s = seq![1, 2, 3];
1835    ///     let is_even = |x| x % 2 == 0;
1836    ///     let i = 1;
1837    ///     assert(s.take(i + 1).any(is_even) == (s.take(i).any(is_even) || is_even(s[i])));
1838    /// }
1839    /// ```
1840    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    /// A sequence has no duplicates iff mapping an injective function over it
1863    /// produces a sequence with no duplicates.
1864    ///
1865    /// ## Example
1866    /// ```rust
1867    /// proof fn no_duplicates_injective_test() {
1868    ///     let s = seq![1, 2];
1869    ///     let f = |x| x + 1;  // injective function
1870    ///     assert(s.no_duplicates() == s.map_values(f).no_duplicates());
1871    /// }
1872    /// ```
1873    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    /// Pushing an element and then mapping a function over a sequence is equivalent to
1893    /// mapping the function over the sequence and then pushing the function applied to that element.
1894    ///
1895    /// ## Example
1896    /// ```rust
1897    /// proof fn push_map_test() {
1898    ///     let s = seq![1, 2];
1899    ///     let f = |x| x + 1;
1900    ///     assert(s.push(3).map_values(f) =~= s.map_values(f).push(f(3)));
1901    /// }
1902    /// ```
1903    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    /// Converting a sequence to a set after pushing an element is equivalent to
1913    /// converting to a set first and then inserting that element.
1914    ///
1915    /// ## Example
1916    /// ```rust
1917    /// proof fn push_to_set_test() {
1918    ///     let s = seq![1, 2];
1919    ///     assert(s.push(3).to_set() =~= s.to_set().insert(3));
1920    /// }
1921    /// ```
1922    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    /// Filtering a sequence after pushing an element is equivalent to:
1943    /// if the element satisfies the predicate, filter the sequence and push the element
1944    /// otherwise, just filter the sequence without the element.
1945    ///
1946    /// ## Example
1947    /// ```rust
1948    /// proof fn filter_push_test() {
1949    ///     let s = seq![1, 2];
1950    ///     let is_even = |x| x % 2 == 0;
1951    ///     assert(s.push(4).filter(is_even) == s.filter(is_even).push(4));
1952    ///     assert(s.push(3).filter(is_even) == s.filter(is_even));
1953    /// }
1954    /// ```
1955    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    /// If two sequences have the same length and `i` is a valid index,
1970    /// then the pair (a[i], b[i]) is contained in their zip.
1971    ///
1972    /// ## Example
1973    /// ```rust
1974    /// proof fn zip_contains_test() {
1975    ///     let a = seq![1, 2];
1976    ///     let b = seq!["a", "b"];
1977    ///     assert(a.zip_with(b).contains((a[0], b[0])));
1978    ///     assert(a.zip_with(b).contains((a[1], b[1])));
1979    /// }
1980    /// ```
1981    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    /// Proves equivalence between checking a predicate over zipped sequences and checking
1992    /// corresponding elements by index. Requires sequences of equal length.
1993    ///
1994    /// # Example
1995    /// ```rust
1996    /// proof fn example() {
1997    ///     let xs = seq![1, 2];
1998    ///     let ys = seq![2, 3];
1999    ///     let f = |x, y| x < y;
2000    ///     assert(xs.zip_with(ys).all(|(x, y)| f(x, y)) <==>
2001    ///            forall|i| 0 <= i < xs.len() ==> f(xs[i], ys[i]));
2002    ///     // We can now prove specific index relationships
2003    ///     assert(xs[0] < ys[0]); // 1 < 2
2004    ///     assert(xs[1] < ys[1]); // 2 < 3
2005    /// }
2006    /// ```
2007    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    /// flat_mapping after pushing an element is the same as
2029    /// flat_mapping first and then appending f of that element.
2030    ///
2031    /// # Example
2032    /// ```rust
2033    /// proof fn example() {
2034    ///     let xs = seq![1, 2];
2035    ///     let f = |x| seq![x, x + 1];
2036    ///     assert(xs.push(3).flat_map(f) =~= xs.flat_map(f) + f(3));
2037    ///     // xs.push(3).flat_map(f)    = [1,2,2,3,3,4]
2038    ///     // xs.flat_map(f) + f(3)     = [1,2,2,3] + [3,4]
2039    /// }
2040    /// ```
2041    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    /// flat_mapping a sequence up to index i+1 is equivalent to
2053    /// flat_mapping up to index i and appending f of the element at index i.
2054    ///
2055    /// # Example
2056    /// ```rust
2057    /// proof fn example() {
2058    ///     let xs = seq![1, 2, 3];
2059    ///     let f = |x| seq![x, x + 1];
2060    ///
2061    ///     assert(xs.take(2).flat_map(f) =~= xs.take(1).flat_map(f) + f(xs[1]));
2062    ///     // xs.take(2).flat_map(f)        = [1,2,2,3]
2063    ///     // xs.take(1).flat_map(f) + f(2) = [1,2] + [2,3]
2064    /// }
2065    /// ```
2066    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    /// flat_mapping a sequence with a single element
2080    /// is equivalent to applying the function f to that element.
2081    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    /// Mapping a sequence's first i+1 elements equals
2092    /// mapping its first i elements plus f of the i-th element.
2093    ///
2094    /// # Example
2095    /// ```rust
2096    /// proof fn example() {
2097    ///     let xs = seq![1, 2, 3];
2098    ///     let f = |x| x * 2;
2099    ///
2100    ///     assert(xs.take(2).map_values(f) =~= xs.take(1).map_values(f).push(f(xs[1])));
2101    ///     // Left:  [1,2].map(f)          = [2,4]
2102    ///     // Right: [1].map(f).push(f(2)) = [2].push(4)
2103    /// }
2104    /// ```
2105    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    /// If a sequence is a prefix of another sequence,
2119    /// their elements match at all indices within the prefix length.
2120    ///
2121    /// # Example
2122    /// ```rust
2123    /// proof fn example() {
2124    ///     let xs = seq![1, 2, 3];
2125    ///     let prefix = seq![1, 2];
2126    ///     assert(prefix.is_prefix_of(xs));
2127    ///     assert(prefix[0] == xs[0] && prefix[1] == xs[1]);
2128    /// }
2129    /// ```
2130    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    /// If a concatenated sequence (prefix1 + prefix2) is a prefix of another sequence,
2139    /// then prefix1 by itself is also a prefix of that sequence.
2140    ///
2141    /// # Example
2142    /// ```rust
2143    /// proof fn example() {
2144    ///     let xs = seq![1, 2, 3, 4];
2145    ///     let prefix1 = seq![1, 2];
2146    ///     let prefix2 = seq![3];
2147    ///     assert((prefix1 + prefix2).is_prefix_of(xs));
2148    ///     assert(prefix1.is_prefix_of(xs));
2149    /// }
2150    /// ```
2151    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    /// If `prefix1 + [t]` is a prefix of a sequence,
2162    /// `prefix1` is a prefix of `prefix2`,
2163    /// `prefix2` is a prefix of the sequence,
2164    /// `prefix1` and `prefix2` are different, and
2165    /// `prefix1` doesn't contain `t`,
2166    /// then `prefix2` must contain t.
2167    ///
2168    /// # Example
2169    /// ```rust
2170    /// proof fn example() {
2171    ///     let xs = seq![1, 2, 3, 4];
2172    ///     let prefix1 = seq![1];
2173    ///     let prefix2 = seq![1, 2];
2174    ///     let t = 2;
2175    ///     assert((prefix1 + seq![t]).is_prefix_of(xs));
2176    ///     assert(prefix1.is_prefix_of(prefix2));
2177    ///     assert(prefix2.is_prefix_of(xs));
2178    ///     assert(prefix2.contains(t));
2179    /// }
2180    /// ```
2181    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    /// If `prefix1 + [t]` and `prefix2 + [t]` are both prefixes of a sequence,
2198    /// and neither `prefix1` nor `prefix2` contains `t`,
2199    /// then `prefix1` equals `prefix2`.
2200    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    /// If a predicate `p` is true for all elements in a sequence,
2219    /// and `p` is true for an element `e`, then `p` remains true for all elements
2220    /// after pushing `e` to the sequence.
2221    ///
2222    /// # Example
2223    /// ```rust
2224    /// proof fn example() {
2225    ///     let xs = seq![2, 4, 6];
2226    ///     let is_even = |x| x % 2 == 0;
2227    ///     assert(xs.all(is_even));
2228    ///     assert(is_even(8));
2229    ///     assert(xs.push(8).all(is_even));
2230    /// }
2231    /// ```
2232    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    /// Two sequences are equal when concatenated with the same prefix
2247    /// iff those two sequences are equal.
2248    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
2280/// Filtering a sequence and then viewing its elements produces the same result as
2281/// viewing the elements first and then filtering with the corresponding predicate.
2282/// The predicates p and sp must be equivalent under view.
2283///
2284/// # Example
2285/// ```rust
2286/// proof fn example() {
2287///     let s = seq!["hello".to_string(), "world".to_string()];
2288///     let p = |x: String| x.len() > 4;
2289///     let sp = |x: Seq<char>| x.len() > 4;
2290///
2291///     let way1 = s.filter(p).map_values(|x| x.view());
2292///     let way2 = s.map_values(|x| x.view()).filter(sp);
2293///     assert(way1 == way2);
2294/// }
2295/// ```
2296pub 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
2322/// A sequence has exactly one element satisfying a predicate iff
2323/// viewing all elements and filtering with the corresponding predicate
2324/// produces a sequence with exactly one element.
2325///
2326/// # Example
2327/// ```rust
2328/// proof fn example() {
2329///     let s = seq!["hello".to_string(), "world".to_string()];
2330///     let p = |x: String| x.len() == 5;
2331///     let sp = |x: Seq<char>| x.len() == 5;
2332///
2333///     assert(s.exactly_one(p) <==> s.map_values(|x| x.view()).exactly_one(sp));
2334/// }
2335/// ```
2336pub 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    /// Unzips a sequence that contains pairs into two separate sequences.
2352    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    /// Proof of correctness and expected properties of unzip function
2357    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    /// Unzipping a sequence of sequences and then zipping the resulting two sequences
2373    /// back together results in the original sequence of sequences.
2374    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    /// Flattens a sequence of sequences into a single sequence by concatenating
2383    /// subsequences, starting from the first element.
2384    ///
2385    /// ## Example
2386    ///
2387    /// ```rust
2388    /// proof fn flatten_test() {
2389    ///    let seq: Seq<Seq<int>> = seq![seq![1, 2, 3], seq![4, 5, 6], seq![7, 8, 9]];
2390    ///    let flat: Seq<int> = seq.flatten();
2391    ///    reveal_with_fuel(Seq::<Seq<int>>::flatten, 5); //Needed for Verus to unfold the recursive definition of flatten
2392    ///    assert(flat =~= seq![1, 2, 3, 4, 5, 6, 7, 8, 9]);
2393    /// }
2394    /// ```
2395    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    /// Flattens a sequence of sequences into a single sequence by concatenating
2406    /// subsequences in reverse order, i.e. starting from the last element.
2407    /// This is equivalent to a call to `flatten`, but with concatenation operation
2408    /// applied along the oppositive associativity for the sake of proof reasoning in that direction.
2409    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    /// Flattening a sequence of a sequence x, where x has length 1,
2420    /// results in a sequence equivalent to the single element of x
2421    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    /// The length of a flattened sequence of sequences x is greater than or
2433    /// equal to any of the lengths of the elements of x.
2434    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    /// The length of a flattened sequence of sequences x is less than or equal
2452    /// to the length of x multiplied by a number greater than or equal to the
2453    /// length of the longest sequence in x.
2454    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);  //TODO: use math library after imported
2467        }
2468    }
2469
2470    /// Flattening sequences of sequences in order (starting from the beginning)
2471    /// and in reverse order (starting from the end) results in the same sequence.
2472    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            // let s = self.drop_last().flatten();
2482            // let s2 = self.drop_last().flatten_alt();
2483            // assert(s == s2);
2484            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    /// Flattening a sequence of sequences after pushing a new sequence is equivalent to
2495    /// concatenating that sequence to the original flattened result.
2496    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    /// Flattening a sequence containing a single sequence yields that inner sequence.
2519    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
2535/********************************* Extrema in Sequences *********************************/
2536
2537impl Seq<int> {
2538    /// Returns the maximum integer value in a non-empty sequence of integers.
2539    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    /// Proof of correctness and expected properties for max function
2559    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    /// Returns the minimum integer value in a non-empty sequence of integers.
2580    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    /// Proof of correctness and expected properties for min function
2600    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    /// The maximum element in a non-empty sequence is greater than or equal to
2635    /// the maxima of its non-empty subsequences.
2636    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    /// The minimum element in a non-empty sequence is less than or equal to
2647    /// the minima of its non-empty subsequences.
2648    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
2659// Helper function to aid with merge sort
2660spec 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    // TODO: lemma_seq_skip_of_skip and lemma_seq_skip_index2 cause a lot of QIs
2689    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 {  /*assert(rest =~= left);*/
2731            } else if leq(left.first(), right.drop_first().first()) {  //right might be length 1
2732                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
2753/// The maximum of the concatenation of two non-empty sequences is greater than or
2754/// equal to the maxima of its two non-empty subsequences.
2755pub 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
2784/// The minimum of the concatenation of two non-empty sequences is less than or
2785/// equal to the minimum of its two non-empty subsequences.
2786pub 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
2816/************************* Sequence to Multiset Conversion **************************/
2817
2818/// push(a) o to_multiset = to_multiset o insert(a)
2819pub 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
2882/// to_multiset() preserves length
2883pub 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
2900/// to_multiset() contains only the elements of the sequence
2901pub 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        // ==>
2911        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        // <==
2927
2928        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
2958/// Lemma showing that update is equivalent to a remove followed by an insertae
2959pub 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
2968/// The last element of two concatenated sequences, the second one being non-empty, will be the
2969/// last element of the latter sequence.
2970pub 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
2978/// The concatenation of sequences is associative
2979pub 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
2985/// Recursive definition of seq to set conversion
2986spec 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
2996// Helper function showing that the recursive definition of set_to_seq produces a finite set
2997proof 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
3012// Helper function showing that the resulting set contains all elements of the sequence
3013proof 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
3039// Helper function showing that the recursive definition matches the set comprehension one
3040proof 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
3053/// The set obtained from a sequence is finite
3054pub 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
3076/// If sequences a and b don't have duplicates, and there are no
3077/// elements in common between them, then the concatenated sequence
3078/// a + b will not contain duplicates either.
3079pub 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
3089/// Flattening sequences of sequences is distributive over concatenation. That is, concatenating
3090/// the flattening of two sequences of sequences is the same as flattening the
3091/// concatenation of two sequences of sequences.
3092pub 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
3108/// Flattening sequences of sequences in reverse order is distributive over concatentation.
3109/// That is, concatenating the flattening of two sequences of sequences in reverse
3110/// order is the same as flattening the concatenation of two sequences of sequences
3111/// in reverse order.
3112pub 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
3128/// The multiset of a concatenated sequence `a + b` is equivalent to the multiset of the
3129/// concatenated sequence `b + a`.
3130pub 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
3140/// The multiset of a concatenated sequence `a + b` is equivalent to the multiset of just
3141/// sequence `a` added to the multiset of just sequence `b`.
3142pub 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
3157/// Any two sequences that are sorted by a total order and that have the same elements are equal.
3158pub 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
3188// This verified lemma used to be an axiom in the Dafny prelude
3189pub 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
3195// This verified lemma used to be an axiom in the Dafny prelude
3196/// The empty sequence contains nothing
3197pub broadcast proof fn lemma_seq_empty_contains_nothing<A>(x: A)
3198    ensures
3199        !(#[trigger] Seq::<A>::empty().contains(x)),
3200{
3201}
3202
3203// This verified lemma used to be an axiom in the Dafny prelude
3204// Note: Dafny only does one way implication, but theoretically it could go both ways
3205/// A sequence with length 0 is equivalent to the empty sequence
3206pub 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
3212// This verified lemma used to be an axiom in the Dafny prelude
3213/// The concatenation of two sequences contains only the elements
3214/// of the two sequences
3215pub 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
3238// This verified lemma used to be an axiom in the Dafny prelude
3239/// After pushing an element onto a sequence, the sequence contains that element
3240pub 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
3251// This verified lemma used to be an axiom in the Dafny prelude
3252/// The subrange of a sequence contains only the elements within the indices `start` and `stop`
3253/// of the original sequence.
3254pub 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
3272// Definition of a commutative fold_right operator.
3273pub 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
3277// Definition of a commutative fold_left operator.
3278pub 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
3282// For a commutative fold_right operator, any folding order
3283// (i.e., any permutation) produces the same result.
3284pub 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
3321// For a commutative fold_left operator, any folding order
3322// (i.e., any permutation) produces the same result.
3323pub 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
3347/************************** Lemmas about Take/Skip ***************************/
3348
3349// This verified lemma used to be an axiom in the Dafny prelude
3350/// Taking the first `n` elements of a sequence results in a sequence of length `n`,
3351/// as long as `n` is within the bounds of the original sequence.
3352pub 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
3358// This verified lemma used to be an axiom in the Dafny prelude
3359/// The resulting sequence after taking the first `n` elements from sequence `s` contains
3360/// element `x` if and only if `x` is contained in the first `n` elements of `s`.
3361pub 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
3377// This verified lemma used to be an axiom in the Dafny prelude
3378/// If `j` is a valid index less than `n`, then the `j`th element of the sequence `s`
3379/// is the same as `j`th element of the sequence after taking the first `n` elements of `s`.
3380pub 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        //             assert( b.subrange(s, e)[i] == b.take(l)[i + s] );   // either trigger will do
3398    }
3399    // trigger extn equality (verus issue #1257)
3400
3401    assert(a.subrange(s, e) == b.subrange(s, e));
3402}
3403
3404// This verified lemma used to be an axiom in the Dafny prelude
3405/// Skipping the first `n` elements of a sequence gives a sequence of length `n` less than
3406/// the original sequence's length.
3407pub 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
3413// This verified lemma used to be an axiom in the Dafny prelude
3414/// The resulting sequence after skipping the first `n` elements from sequence `s` contains
3415/// element `x` if and only if `x` is contained in `s` before index `n`.
3416pub 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
3430// This verified lemma used to be an axiom in the Dafny prelude
3431/// If `j` is a valid index less than `s.len() - n`, then the `j`th element of the sequence
3432/// `s.skip(n)` is the same as the `j+n`th element of the sequence `s`.
3433pub 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
3439// This verified lemma used to be an axiom in the Dafny prelude
3440/// If `k` is a valid index between `n` (inclusive) and the length of sequence `s` (exclusive),
3441/// then the `k-n`th element of the sequence `s.skip(n)` is the same as the `k`th element of the
3442/// original sequence `s`.
3443pub 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
3449// This verified lemma used to be an axiom in the Dafny prelude
3450/// If `n` is the length of sequence `a`, then taking the first `n` elements of the concatenation
3451/// `a + b` is equivalent to the sequence `a` and skipping the first `n` elements of the concatenation
3452/// `a + b` is equivalent to the sequence `b`.
3453pub 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
3461/************* Lemmas about the Commutability of Take and Skip with Update ************/
3462
3463// This verified lemma used to be an axiom in the Dafny prelude
3464/// If `i` is in the first `n` indices of sequence `s`, updating sequence `s` at index `i` with
3465/// value `v` and then taking the first `n` elements is equivalent to first taking the first `n`
3466/// elements of `s` and then updating index `i` to value `v`.
3467pub 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
3474// This verified lemma used to be an axiom in the Dafny prelude
3475/// If `i` is a valid index after the first `n` indices of sequence `s`, updating sequence `s` at
3476/// index `i` with value `v` and then taking the first `n` elements is equivalent to just taking the first `n`
3477/// elements of `s` without the update.
3478pub 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
3484// This verified lemma used to be an axiom in the Dafny prelude
3485/// If `i` is a valid index after the first `n` indices of sequence `s`, updating sequence `s` at
3486/// index `i` with value `v` and then skipping the first `n` elements is equivalent to skipping the first `n`
3487/// elements of `s` and then updating index `i-n` to value `v`.
3488pub 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
3494// This verified lemma used to be an axiom in the Dafny prelude
3495/// If `i` is a valid index in the first `n` indices of sequence `s`, updating sequence `s` at
3496/// index `i` with value `v` and then skipping the first `n` elements is equivalent to just skipping
3497/// the first `n` elements without the update.
3498pub 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
3504// This verified lemma used to be an axiom in the Dafny prelude
3505/// Pushing element `v` onto the end of sequence `s` and then skipping the first `n` elements is
3506/// equivalent to skipping the first `n` elements of `s` and then pushing `v` onto the end.
3507pub 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
3514// This verified lemma used to be an axiom in the Dafny prelude
3515/// `s.skip(0)` is equivalent to `s`.
3516pub 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
3522// This verified lemma used to be an axiom in the Dafny prelude
3523/// `s.take(0)` is equivalent to the empty sequence.
3524pub 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
3530// This verified lemma used to be an axiom in the Dafny prelude
3531/// If `m + n` is less than or equal to the length of sequence `s`, then skipping the first `m` elements
3532/// and then skipping the first `n` elements of the resulting sequence is equivalent to just skipping
3533/// the first `m + n` elements.
3534pub 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/// Properties of sequences from the Dafny prelude (which were axioms in Dafny, but proven here in Verus)
3541#[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,  //from lemma_seq_contains(s, x),
3546        forall|x: A| !(#[trigger] Seq::<A>::empty().contains(x)),  //from lemma_seq_empty_contains_nothing(x),
3547        forall|s: Seq<A>| #[trigger] s.len() == 0 ==> s =~= Seq::<A>::empty(),  //from lemma_seq_empty_equality(s),
3548        forall|x: Seq<A>, y: Seq<A>, elt: A| #[trigger]
3549            (x + y).contains(elt) <==> x.contains(elt) || y.contains(elt),  //from lemma_seq_concat_contains_all_elements(x, y, elt),
3550        forall|s: Seq<A>, v: A, x: A| #[trigger] s.push(v).contains(x) <==> v == x || s.contains(x),  //from lemma_seq_contains_after_push(s, v, x)
3551        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),  //from lemma_seq_subrange_elements(s, start, stop, x),
3554        forall|s: Seq<A>, n: int| 0 <= n <= s.len() ==> #[trigger] s.take(n).len() == n,  //from lemma_seq_take_len(s, n)
3555        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),  //from lemma_seq_take_contains(s, n, x),
3558        forall|s: Seq<A>, n: int, j: int| 0 <= j < n <= s.len() ==> #[trigger] s.take(n)[j] == s[j],  //from lemma_seq_take_index(s, n, j),
3559        forall|s: Seq<A>, n: int| 0 <= n <= s.len() ==> #[trigger] s.skip(n).len() == s.len() - n,  //from lemma_seq_skip_len(s, n),
3560        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),  //from lemma_seq_skip_contains(s, n, x),
3563        forall|s: Seq<A>, n: int, j: int|
3564            0 <= n && 0 <= j < (s.len() - n) ==> #[trigger] s.skip(n)[j] == s[j + n],  //from lemma_seq_skip_index(s, n, j),
3565        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),  //from lemma_seq_append_take_skip(a, b, n),
3569        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),  //from lemma_seq_take_update_commut1(s, i, v, n),
3571        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),  //from lemma_seq_take_update_commut2(s, i, v, n),
3573        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            ),  //from lemma_seq_skip_update_commut1(s, i, v, n),
3578        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),  //from lemma_seq_skip_update_commut2(s, i, v, n),
3580        forall|s: Seq<A>, v: A, n: int|
3581            0 <= n <= s.len() ==> #[trigger] s.push(v).skip(n) == s.skip(n).push(v),  //from lemma_seq_skip_build_commut(s, v, n),
3582        forall|s: Seq<A>, n: int| n == 0 ==> #[trigger] s.skip(n) == s,  //from lemma_seq_skip_nothing(s, n),
3583        forall|s: Seq<A>, n: int| n == 0 ==> #[trigger] s.take(n) == Seq::<A>::empty(),  //from lemma_seq_take_nothing(s, n),
3584        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            ),  //from lemma_seq_skip_of_skip(s, m, n),
3588        forall|s: Seq<A>, a: A| #[trigger] (s.push(a).to_multiset()) =~= s.to_multiset().insert(a),  //from o_multiset_properties
3589        forall|s: Seq<A>| s.len() == #[trigger] s.to_multiset().len(),  //from to_multiset_ensures
3590        forall|s: Seq<A>, a: A|
3591            s.contains(a) <==> #[trigger] s.to_multiset().count(a)
3592                > 0,  //from to_multiset_ensures
3593{
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/// Prove two sequences `s1` and `s2` are equal by proving that their elements are equal at each index.
3605///
3606/// More precisely, `assert_seqs_equal!` requires:
3607///  * `s1` and `s2` have the same length (`s1.len() == s2.len()`), and
3608///  * for all `i` in the range `0 <= i < s1.len()`, we have `s1[i] == s2[i]`.
3609///
3610/// The property that equality follows from these facts is often called _extensionality_.
3611///
3612/// `assert_seqs_equal!` can handle many trivial-looking
3613/// identities without any additional help:
3614///
3615/// ```rust
3616/// proof fn subrange_concat(s: Seq<u64>, i: int) {
3617///     requires([
3618///         0 <= i && i <= s.len(),
3619///     ]);
3620///
3621///     let t1 = s.subrange(0, i);
3622///     let t2 = s.subrange(i, s.len());
3623///     let t = t1.add(t2);
3624///
3625///     assert_seqs_equal!(s == t);
3626///
3627///     assert(s == t);
3628/// }
3629/// ```
3630///
3631/// In more complex cases, a proof may be required for the equality of each element pair.
3632/// For example,
3633///
3634/// ```rust
3635/// proof fn bitvector_seqs() {
3636///     let s = Seq::<u64>::new(5, |i| i as u64);
3637///     let t = Seq::<u64>::new(5, |i| i as u64 | 0);
3638///
3639///     assert_seqs_equal!(s == t, i => {
3640///         // Need to show that s[i] == t[i]
3641///         // Prove that the elements are equal by appealing to a bitvector solver:
3642///         let j = i as u64;
3643///         assert_bit_vector(j | 0 == j);
3644///         assert(s[i] == t[i]);
3645///     });
3646/// }
3647/// ```
3648#[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
3723// include all the Dafny prelude lemmas
3724pub 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    // Removed the following from group due to bad verification performance
3747    // for `lemma_merge_sorted_with_ensures`
3748    // lemma_seq_skip_of_skip,
3749    group_to_multiset_ensures,
3750}
3751
3752#[doc(hidden)]
3753pub use assert_seqs_equal_internal;
3754pub use assert_seqs_equal;
3755
3756} // verus!