Struct SeqCopy item path

An empty sequence (i.e., a sequence of length 0).

Construct a sequence s of length len where entry s[i] is given by f(i).

The length of a sequence.

0 <= i < self.len(),

Gets the value at the given index i.

If i is not in the range [0, self.len()), then the resulting value is meaningless and arbitrary.

0 <= i < self.len(),

{ self.index(i) }

[] operator, synonymous with index

Appends the value a to the end of the sequence. This always increases the length of the sequence by 1. This often requires annotating the type of the element literal in the sequence, e.g., 10int.

§Example

proof fn push_test() {
    assert(seq![10int, 11, 12].push(13) =~= seq![10, 11, 12, 13]);
}

0 <= i < self.len(),

Updates the sequence at the given index, replacing the element with the given value, and leaves all other entries unchanged.

§Example

proof fn update_test() {
    let s = seq![10, 11, 12, 13, 14];
    let t = s.update(2, -5);
    assert(t =~= seq![10, 11, -5, 13, 14]);
}

0 <= start_inclusive <= end_exclusive <= self.len(),

Returns a sequence for the given subrange.

§Example

proof fn subrange_test() {
    let s = seq![10int, 11, 12, 13, 14];
    //                      ^-------^
    //           0      1   2   3   4   5
    let sub = s.subrange(2, 4);
    assert(sub =~= seq![12, 13]);
}

{ self.subrange(0, n) }

Returns a sequence containing only the first n elements of the original sequence

{ self.subrange(n, self.len() as int) }

Returns a sequence without the first n elements of the original sequence

Concatenates the sequences.

§Example

proof fn add_test() {
    assert(seq![10int, 11].add(seq![12, 13, 14])
            =~= seq![10, 11, 12, 13, 14]);
}

{ self.add(rhs) }

+ operator, synonymous with add

0 < self.len(),

{ self[self.len() as int - 1] }

Returns the last element of the sequence.

0 < self.len(),

{ self[0] }

Returns the first element of the sequence.

{ Seq::new(self.len(), |i: int| f(i, self[i])) }

Applies the function f to each element of the sequence, and returns the resulting sequence. The int parameter of f is the index of the element being mapped.

{ Seq::new(self.len(), |i: int| f(self[i])) }

Applies the function f to each element of the sequence, and returns the resulting sequence.

{ self.map_values(f).flatten() }

Applies the function f to each element of the sequence, producing a sequence of sequences, and then concatenates (flattens) those into a single flat sequence of B.

§Example

fn example() {
    let s = seq![1, 2, 3];
    let result = s.flat_map(|x| seq![x, x]);
    assert_eq!(result, seq![1, 1, 2, 2, 3, 3]);
}
``

{ self.len() <= other.len() && (self =~= other.subrange(0, self.len() as int)) }

Is true if the calling sequence is a prefix of the given sequence ‘other’.

§Example

proof fn prefix_test() {
    let pre: Seq<int> = seq![1, 2, 3];
    let whole: Seq<int> = seq![1, 2, 3, 4, 5];
    assert(pre.is_prefix_of(whole));
}

{
    self.len() <= other.len()
        && (self
            =~= other.subrange((other.len() - self.len()) as int, other.len() as int))
}

Is true if the calling sequence is a suffix of the given sequence ‘other’.

§Example

proof fn suffix_test() {
    let end: Seq<int> = seq![3, 4, 5];
    let whole: Seq<int> = seq![1, 2, 3, 4, 5];
    assert(end.is_suffix_of(whole));
}

total_ordering(leq),

Sorts the sequence according to the given leq function

§Example

{{#include ../../../../examples/multiset.rs:sorted_by_leq}}

{ forall |i: int| 0 <= i < self.len() ==> #[trigger] pred(self[i]) }

Tests if all elements in the sequence satisfy the predicate.

§Example

fn example() {
    let s = seq![2, 4, 6, 8];
    assert!(s.all(|x| x % 2 == 0));
}

{ exists |i: int| 0 <= i < self.len() && #[trigger] pred(self[i]) }

Tests if any element in the sequence satisfies the predicate.

§Example

fn example() {
    let s = seq![1, 2, 3, 4];
    assert!(s.any(|x| x > 3));
}

{ self.filter(pred).len() == 1 }

Checks that exactly one element in the sequence satisfies the given predicate.

§Example

fn example() {
    let s = seq![1, 2, 3];
    assert!(s.exactly_one(|x| x == 2));
}

{
    if self.len() == 0 {
        self
    } else {
        let subseq = self.drop_last().filter(pred);
        if pred(self.last()) { subseq.push(self.last()) } else { subseq }
    }
}

Returns the sequence containing only the elements of the original sequence such that pred(element) is true.

§Example

proof fn filter_test() {
   let seq: Seq<int> = seq![1, 2, 3, 4, 5];
   let even: Seq<int> = seq.filter(|x| x % 2 == 0);
   reveal_with_fuel(Seq::<int>::filter, 6); //Needed for Verus to unfold the recursive definition of filter
   assert(even =~= seq![2, 4]);
}

self.len() > 0,

{
    if self.len() > 1 {
        if leq(self[0], self.subrange(1, self.len() as int).max_via(leq)) {
            self.subrange(1, self.len() as int).max_via(leq)
        } else {
            self[0]
        }
    } else {
        self[0]
    }
}

Returns the maximum value in a non-empty sequence, given sorting function leq

self.len() > 0,

{
    if self.len() > 1 {
        let subseq = self.subrange(1, self.len() as int);
        let elt = subseq.min_via(leq);
        if leq(elt, self[0]) { elt } else { self[0] }
    } else {
        self[0]
    }
}

Returns the minimum value in a non-empty sequence, given sorting function leq

{ choose |i: int| 0 <= i < self.len() && self[i] == needle }

Returns an index where needle appears in the sequence. Returns an arbitrary value if the sequence does not contain the needle.

For an element that occurs at least once in a sequence, if its first occurence is at index i, Some(i) is returned. Otherwise, None is returned

For an element that occurs at least once in a sequence, if its last occurence is at index i, Some(i) is returned. Otherwise, None is returned

self.len() >= 1,

{ self.subrange(0, self.len() as int - 1) }

Drops the last element of a sequence and returns a sequence whose length is thereby 1 smaller.

If the input sequence is empty, the result is meaningless and arbitrary.

0 < b.len(),

(a + b).drop_last() == a + b.drop_last(),

Dropping the last element of a concatenation of a and b is equivalent to skipping the last element of b and then concatenating a and b

{
    forall |i, j| {
        (0 <= i < self.len() && 0 <= j < self.len() && i != j) ==> self[i] != self[j]
    }
}

returns true if the sequence has no duplicate elements

{
    forall |i: int, j: int| {
        0 <= i < self.len() && 0 <= j < other.len() ==> self[i] != other[j]
    }
}

Returns true if two sequences are disjoint

{ Set::new(|a: A| self.contains(a)) }

Converts a sequence into a set

Converts a sequence into a multiset

forall |a: A| #[trigger] (self.push(a).to_multiset()) =~= self.to_multiset().insert(a),

forall |i: int| {
    0 <= i < self.len()
        ==> (#[trigger] (self.remove(i).to_multiset())
            =~= self.to_multiset().remove(self[i]))
},

self.len() == #[trigger] self.to_multiset().len(),

forall |a: A| self.contains(a) <==> #[trigger] self.to_multiset().count(a) > 0,

Proof of function to_multiset() correctness

0 <= i <= self.len(),

{ self.subrange(0, i).push(a) + self.subrange(i, self.len() as int) }

Insert item a at index i, shifting remaining elements (if any) to the right

0 <= pos <= self.len(),

self.insert(pos, elt).len() == self.len() + 1,

forall |i: int| 0 <= i < pos ==> #[trigger] self.insert(pos, elt)[i] == self[i],

forall |i: int| pos <= i < self.len() ==> self.insert(pos, elt)[i + 1] == self[i],

self.insert(pos, elt)[pos] == elt,

Proof of correctness and expected properties of insert function

0 <= i < self.len(),

{ self.subrange(0, i) + self.subrange(i + 1, self.len() as int) }

Remove item at index i, shifting remaining elements to the left

0 <= i < self.len(),

self.remove(i).len() == self.len() - 1,

forall |index: int| 0 <= index < i ==> #[trigger] self.remove(i)[index] == self[index],

forall |index: int| {
    i <= index < self.len() - 1 ==> #[trigger] self.remove(i)[index] == self[index + 1]
},

Proof of function remove() correctness

{
    let index = self.index_of_first(val);
    match index {
        Some(i) => self.remove(i),
        None => self,
    }
}

If a given element occurs at least once in a sequence, the sequence without its first occurrence is returned. Otherwise the same sequence is returned.

{
    if self.len() == 0 {
        Seq::empty()
    } else {
        Seq::new(self.len(), |i: int| self[self.len() - 1 - i])
    }
}

Returns the sequence that is in reverse order to a given sequence.

self.len() == other.len(),

{
    if self.len() != other.len() {
        Seq::empty()
    } else if self.len() == 0 {
        Seq::empty()
    } else {
        Seq::new(self.len(), |i: int| (self[i], other[i]))
    }
}

Zips two sequences of equal length into one sequence that consists of pairs. If the two sequences are different lengths, returns an empty sequence

{ if self.len() == 0 { b } else { f(self.drop_last().fold_left(b, f), self.last()) } }

Folds the sequence to the left, applying f to perform the fold.

Equivalent to Iterator::fold in Rust.

Given a sequence s = [x0, x1, x2, ..., xn], applying this function s.fold_left(b, f) returns f(...f(f(b, x0), x1), ..., xn).

{
    if self.len() == 0 {
        b
    } else {
        self.subrange(1, self.len() as int).fold_left_alt(f(b, self[0]), f)
    }
}

Equivalent to Self::fold_left but defined by breaking off the leftmost element when recursing, rather than the rightmost. See Self::lemma_fold_left_alt that proves equivalence.

0 <= k <= self.len(),

self
    .subrange(k, self.len() as int)
    .fold_left((#[trigger] self.subrange(0, k).fold_left(b, f)), f)
    == self.fold_left(b, f),

A lemma that proves how Self::fold_left distributes over splitting a sequence.

self.fold_left(b, f) == self.fold_left_alt(b, f),

Self::fold_left and Self::fold_left_alt are equivalent.

self.reverse().fold_left(v, f) == self.fold_right(|a: A, b: B| f(b, a), v),

Self::fold_left on the reversed sequence is equivalent to Self::fold_right on the original sequence with corresponding folding operator

{ if self.len() == 0 { b } else { self.drop_last().fold_right(f, f(self.last(), b)) } }

Folds the sequence to the right, applying f to perform the fold.

Equivalent to DoubleEndedIterator::rfold in Rust.

Given a sequence s = [x0, x1, x2, ..., xn], applying this function s.fold_right(b, f) returns f(x0, f(x1, f(x2, ..., f(xn, b)...))).

{
    if self.len() == 0 {
        b
    } else {
        f(self[0], self.subrange(1, self.len() as int).fold_right_alt(f, b))
    }
}

Equivalent to Self::fold_right but defined by breaking off the leftmost element when recursing, rather than the rightmost. See Self::lemma_fold_right_alt that proves equivalence.

0 <= k <= self.len(),

self
    .subrange(0, k)
    .fold_right(f, (#[trigger] self.subrange(k, self.len() as int).fold_right(f, b)))
    == self.fold_right(f, b),

A lemma that proves how Self::fold_right distributes over splitting a sequence.

self.fold_right(f, b) == self.fold_right_alt(f, b),

Self::fold_right and Self::fold_right_alt are equivalent.

self.reverse().fold_right(f, v) == self.fold_left(v, |b: B, a: A| f(a, b)),

Self::fold_right on the reversed sequence is equivalent to Self::fold_left on the original sequence with corresponding folding operator

self.no_duplicates(),

forall |x: A| self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1,

Given a sequence with no duplicates, each element occurs only once in its conversion to a multiset

forall |x: A| self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1,

self.no_duplicates(),

If, in a sequence’s conversion to a multiset, each element occurs only once, the sequence has no duplicates.

self.reverse().to_multiset() =~= self.to_multiset(),

Conversion of a sequence to multiset is equivalent to conversion of its reversion to multiset

0 < self.len(),

#[trigger] self.drop_last().push(self.last()) =~= self,

The concatenation of two subsequences derived from a non-empty sequence, the first obtained from skipping the last element, the second consisting only of the last element, is the original sequence.

forall |i: int| 0 <= i < self.len() ==> #[trigger] f(#[trigger] self[i]),

forall |x: A| #[trigger] self.contains(x) ==> #[trigger] f(x),

If a predicate is true at every index of a sequence, it is true for every member of the sequence as a collection. Useful for converting quantifiers between the two forms to satisfy a precondition in the latter form.

forall |x: A| #[trigger] self.contains(x) ==> #[trigger] f(x),

forall |i: int| 0 <= i < self.len() ==> #[trigger] f(self[i]),

If a predicate is true for every member of a sequence as a collection, it is true at every index of the sequence. Useful for converting quantifiers between the two forms to satisfy a precondition in the latter form.

0 <= pos <= self.len(),

self.subrange(0, pos) + self.subrange(pos, self.len() as int) =~= self,

A sequence that is sliced at the pos-th element, concatenated with that same sequence sliced from the pos-th element, is equal to the original unsliced sequence.

0 <= a <= b <= self.len(),

new == self.subrange(a, b),

a <= pos < b,

pos - a < new.len(),

new[pos - a] == self[pos],

Any element in a slice is included in the original sequence.

0 <= s1 <= e1 <= self.len(),

0 <= s2 <= e2 <= e1 - s1,

self.subrange(s1, e1).subrange(s2, e2) =~= self.subrange(s1 + s2, s1 + e2),

A slice (from s2..e2) of a slice (from s1..e1) of a sequence is equal to just a slice (s1+s2..s1+e2) of the original sequence.

self.no_duplicates(),

self.len() == self.to_set().len(),

A sequence of unique items, when converted to a set, produces a set with matching length

self.to_set().len() <= self.len(),

The cardinality of a set of elements is always less than or equal to that of the full sequence of elements.

self.to_set().len() == 0 <==> self.len() == 0,

A sequence is of length 0 if and only if its conversion to a set results in the empty set.

self.to_set().len() == self.len(),

self.no_duplicates(),

A sequence with cardinality equal to its set has no duplicates. Inverse property of that shown in lemma unique_seq_to_set

#[trigger] self.to_set().map(f) =~= self.map_values(f).to_set(),

Mapping a function over a sequence and converting to a set is the same as mapping it over the sequence converted to a set.

#[trigger] (sq + seq![elt]).to_set() =~= sq.to_set().insert(elt),

Appending an element to a sequence and converting to set, is equal to converting to set and inserting it.

0 <= off,

off + vs.len() <= self.len(),

{
    Seq::new(
        self.len(),
        |i: int| if off <= i < off + vs.len() { vs[i - off] } else { self[i] },
    )
}

Update a subrange of a sequence starting at off to values vs. Expects that the updated subrange off up to off+vs.len() fits in the existing sequence.

0 <= i < self.len() ==> ((self.skip(i)).skip(1) =~= #[trigger] self.skip(i + 1)),

Skipping i elements and then 1 more is equivalent to skipping i + 1 elements.

§Example

proof fn example() {
    let s = seq![1, 2, 3, 4];
    s.lemma_seq_skip_skip(2);
    assert(s.skip(2).skip(1) =~= s.skip(3));
}

self.contains(elem),

0 <= idx < self.len() && self[idx] == elem,

If an element is contained in a sequence, then there exists an index where that element appears.

§Example

proof fn example() {
    let s = seq![10, 20, 30];
    assert(s.contains(20));
    let idx = s.lemma_contains_to_index(20);
    assert(s[idx] == 20);
}

self.len() > 0,

pred(self[0]) && self.skip(1).all(|x| pred(x)),

self.all(|x| pred(x)),

If a predicate holds for the first element and for all elements in the tail, then it holds for the entire sequence.

§Example

proof fn example() {
    let s = seq![2, 4, 6, 8];
    let is_even = |x| x % 2 == 0;
    assert(is_even(s[0]));
    assert(s.skip(1).all(is_even));
    s.lemma_all_from_head_tail(is_even);
    assert(s.all(is_even));
}

self.any(|x| pred(x)),

!pred(self[0]) ==> self.skip(1).any(|x| pred(x)),

If a predicate holds for any element in the sequence and does not hold for the first element, then the predicate must hold for some element in the tail.

§Example

proof fn example() {
    let s = seq![1, 4, 6, 8];
    let is_even = |x| x % 2 == 0;
    assert(s.any(is_even));
    assert(!is_even(s[0]));
    s.lemma_any_tail(is_even);
    assert(s.skip(1).any(is_even));
}

{
    if self.len() == 0 {
        seen
    } else if seen.contains(self[0]) {
        self.skip(1).remove_duplicates(seen)
    } else {
        self.skip(1).remove_duplicates(seen + seq![self[0]])
    }
}

Removes duplicate elements from a sequence, maintaining the order of first appearance. Takes a seen sequence parameter to track previously encountered elements.

§Example

fn example() {
    let s = seq![1, 2, 1, 3, 2, 4];
    let seen = seq![];
    let result = s.remove_duplicates(seen);
    assert_eq!(result, seq![1, 2, 3, 4]);

    let seen2 = seq![2, 3];
    let result2 = s.remove_duplicates(seen2);
    assert_eq!(result2, seq![1, 4]);
}

forall |x| {
    (self + seen).contains(x) <==> #[trigger] self.remove_duplicates(seen).contains(x)
},

#[trigger] self.remove_duplicates(seen).len() <= self.len() + seen.len(),

Properties of remove_duplicates:

• The output contains x if and only if x was in the input sequence or seen set
• The output length is at most the sum of input and seen lengths

§Example

proof fn example() {
    let s = seq![1, 2, 1, 3];
    let seen = seq![2];
    s.lemma_remove_duplicates_properties(seen);
    assert(s.remove_duplicates(seen).contains(1));
    assert(s.remove_duplicates(seen).contains(3));
    assert(!s.remove_duplicates(seen).contains(2));
    assert(s.remove_duplicates(seen).len() <= s.len() + seen.len());
}

0 <= i < self.len(),

self.remove_duplicates(seen)
    == self.skip(i).remove_duplicates(self.take(i).remove_duplicates(seen)),

Shows that removing duplicates from a sequence is equivalent to:

1. First removing duplicates from the prefix up to index i (with the given seen set)
2. Using that result as the new seen set for removing duplicates from the suffix after i

§Example

proof fn example() {
    let s = seq![1, 2, 1, 3, 2, 4];
    let seen = seq![];
    s.lemma_remove_duplicates_append_index(seen, 2);
    assert(s.remove_duplicates(seen)
        =~= seq![1, 3, 2, 4].remove_duplicates(seq![1, 2].remove_duplicates(seen)));
}

(self + seen).contains(x)
    ==> (self + seq![x]).remove_duplicates(seen) == self.remove_duplicates(seen),

!(self + seen).contains(x)
    ==> (self + seq![x]).remove_duplicates(seen)
        == self.remove_duplicates(seen) + seq![x],

When appending an element x to a sequence:

• If x is in self + seen, removing duplicates equals removing duplicates from self
• If x is not in (self + seen), removing duplicates equals removing duplicates from self, concatenated with [x]

§Example

proof fn example() {
    let s1 = seq![1, 2];
    let seen = seq![];
    assert!(!s1.contains(3));
    lemma_remove_duplicates_append(s1, 3, seen);
    assert((s1 + seq![3]).remove_duplicates(seen) =~= s1.remove_duplicates(seen) + seq![3]);
}

self.all(|x: A| !pred(x)),

self.filter(pred).len() == 0,

If all elements in a sequence fail the predicate, filtering by that predicate yields an empty sequence

§Example

proof fn example() {
    let s = seq![1, 2, 3];
    let pred = |x| x > 5;
    lemma_all_neg_filter_empty(s, pred);
    assert(s.filter(pred).len() == 0);
}

{
    if self.len() == 0 {
        Seq::empty()
    } else {
        let rest = self.drop_last();
        match f(self.last()) {
            Option::Some(s) => rest.filter_map(f) + seq![s],
            Option::None => rest.filter_map(f),
        }
    }
}

Applies an Option-returning function to each element, keeping only successful (Some) results

§Example

let s = seq![1, 2, 3];
let f = |x| if x % 2 == 0 { Some(x * 2) } else { None };
assert(s.filter_map(f) =~= seq![4]);

#[trigger] self.filter(p).contains(elem),

self.contains(elem),

If an element exists in the filtered sequence, it must exist in the original sequence

#[trigger] self.filter_map(f).contains(elt),

exists |t: A| #[trigger] self.contains(t) && f(t) == Some(elt),

If an element exists in filter_map’s output, there must be an input element that mapped to it

0 <= k < xs.len(),

xs.take(k + 1) =~= xs.take(k) + seq![xs[k]],

Taking k+1 elements is the same as taking k elements plus the kth element

§Example

let s = seq![1, 2, 3];
lemma_take_plus_one(s, 1);
seq![1, 2] == seq![1] + seq![2]

seq![a].filter_map(f)
    =~= match f(a) {
        Option::Some(b) => seq![b],
        Option::None => Seq::empty(),
    },

filter_map on a single element sequence either produces a new single element sequence (if f returns Some) or an empty sequence (if f returns None)

0 <= i < self.len(),

#[trigger] self.take(i + 1).filter_map(f)
    =~= self.take(i).filter_map(f)
        + (match f(self[i]) {
            Option::Some(s) => seq![s],
            Option::None => Seq::empty(),
        }),

filter_map of take(i+1) equals filter_map of take(i) plus maybe the mapped i’th element

§Example

let s = seq![1, 2, 3];
let f = |x| if x % 2 == 0 { Some(x * 2) } else { None };
s.lemma_filter_map_take_succ(s, f, 1);
assert(s.take(2).filter_map(f) == s.take(1).filter_map(f) + seq![f(s[1]).unwrap()]);
assert(s.take(2).filter_map(f) == seq![] + seq![4]);

{
    if self.len() == 0 {
        Seq::empty()
    } else {
        let rest = self.drop_first().filter(p);
        let first = self.first();
        if p(first) { seq![first] + rest } else { rest }
    }
}

An alternative implementation of filter that processes the sequence recursively from left to right, in contrast to the standard filter which processes from right to left.

#[trigger] (seq![x] + self).filter(p)
    == (if p(x) { seq![x] } else { Seq::empty() }) + self.filter(p),

When filtering (x + sequence), if x satisfies the predicate, x is prepended to the filtered sequence. Otherwise, only the filtered sequence remains.

§Example

proof fn filter_prepend_test() {
    let s = seq![2, 3, 4];
    let is_even = |x: int| x % 2 == 0;
    let with_five = seq![5] + s;
    assert(with_five.filter(is_even) =~= seq![2, 4]); // 5 filtered out
    let with_six = seq![6] + s;
    assert(with_six.filter(is_even) =~= seq![6, 2, 4]); // 6 included
}

self.filter(p) =~= self.filter_alt(p),

The filter() and filter_alt() methods produce equivalent results for any sequence

self.is_prefix_of(ys),

self.filter(p).is_prefix_of(ys.filter(p)),

Filtering preserves the prefix relationship between sequences.

§Example

proof fn filter_monotone_test() {
    let s = seq![1, 2, 3];
    let ys = seq![1, 2, 3, 4, 5];
    let is_even = |x: int| x % 2 == 0;
    assert(s.is_prefix_of(ys));
    assert(s.filter(is_even).is_prefix_of(ys.filter(is_even)));
    assert(s.filter(is_even) =~= seq![2]);
    assert(ys.filter(is_even) =~= seq![2, 4]);
}

0 <= i <= self.len(),

self.filter(p).len() >= self.take(i).filter(p).len(),

The length of filter(take(i)) is never greater than the length of filter(entire_sequence).

§Example

proof fn filter_take_len_test() {
    let s = seq![1, 2, 3, 4, 5];
    let is_even = |x: int| x % 2 == 0;
    let i = 3;
    assert(s.take(i) =~= seq![1, 2, 3]);
    assert(s.take(i).filter(is_even) =~= seq![2]);
    assert(s.filter(is_even) =~= seq![2, 4]);
    assert(s.filter(is_even).len() >= s.take(i).filter(is_even).len());
}

#[trigger] self.push(elem).filter(p).len()
    == self.filter(p).len() + (if p(elem) { 1int } else { 0int }),

Filtering a prefix of a sequence produces the same number or fewer elements as filtering the entire sequence.

§Example

proof fn filter_take_len_test() {
    let s = seq![1, 2, 3, 4, 5];
    let is_even = |x: int| x % 2 == 0;
    assert(s.filter(is_even).len() >= s.take(3).filter(is_even).len());
}

0 <= i < self.len(),

self.contains(#[trigger] self[i]),

If an index i is valid for a sequence (0 ≤ i < len), then the element at that index is contained in the sequence.

0 <= i < self.len(),

#[trigger] self.take(i + 1) =~= self.take(i).push(self[i]),

Taking i+1 elements from a sequence is equivalent to taking i elements and then pushing the element at index i.

#[trigger] self.take(self.len() as int) == self,

Taking the full length of a sequence returns the sequence itself.

0 <= i < self.len(),

#[trigger] self.take(i + 1).any(p) <==> self.take(i).any(p) || p(self[i]),

Taking i+1 elements and checking if any element satisfies predicate p is equivalent to: either taking i elements and checking if any satisfies p, OR checking if the i-th element satisfies p.

§Example

proof fn take_any_succ_test() {
    let s = seq![1, 2, 3];
    let is_even = |x| x % 2 == 0;
    let i = 1;
    assert(s.take(i + 1).any(is_even) == (s.take(i).any(is_even) || is_even(s[i])));
}

injective(f),

self.no_duplicates() <==> self.map_values(f).no_duplicates(),

A sequence has no duplicates iff mapping an injective function over it produces a sequence with no duplicates.

§Example

proof fn no_duplicates_injective_test() {
    let s = seq![1, 2];
    let f = |x| x + 1;  // injective function
    assert(s.no_duplicates() == s.map_values(f).no_duplicates());
}

self.map_values(f).push(f(x)) =~= #[trigger] self.push(x).map_values(f),

Pushing an element and then mapping a function over a sequence is equivalent to mapping the function over the sequence and then pushing the function applied to that element.

§Example

proof fn push_map_test() {
    let s = seq![1, 2];
    let f = |x| x + 1;
    assert(s.push(3).map_values(f) =~= s.map_values(f).push(f(3)));
}

#[trigger] self.push(elem).to_set() =~= self.to_set().insert(elem),

Converting a sequence to a set after pushing an element is equivalent to converting to a set first and then inserting that element.

§Example

proof fn push_to_set_test() {
    let s = seq![1, 2];
    assert(s.push(3).to_set() =~= s.to_set().insert(3));
}

#[trigger] self.push(elem).filter(pred)
    == if pred(elem) { self.filter(pred).push(elem) } else { self.filter(pred) },

Filtering a sequence after pushing an element is equivalent to: if the element satisfies the predicate, filter the sequence and push the element otherwise, just filter the sequence without the element.

§Example

proof fn filter_push_test() {
    let s = seq![1, 2];
    let is_even = |x| x % 2 == 0;
    assert(s.push(4).filter(is_even) == s.filter(is_even).push(4));
    assert(s.push(3).filter(is_even) == s.filter(is_even));
}

0 <= i < self.len(),

self.len() == b.len(),

self.zip_with(b).contains((self[i], b[i])),

If two sequences have the same length and i is a valid index, then the pair (a[i], b[i]) is contained in their zip.

§Example

proof fn zip_contains_test() {
    let a = seq![1, 2];
    let b = seq!["a", "b"];
    assert(a.zip_with(b).contains((a[0], b[0])));
    assert(a.zip_with(b).contains((a[1], b[1])));
}

self.len() == b.len(),

self.zip_with(b).all(|p: (A, B)| f(p.0, p.1))
    <==> forall |i: int| 0 <= i < self.len() ==> f(self[i], b[i]),

Proves equivalence between checking a predicate over zipped sequences and checking corresponding elements by index. Requires sequences of equal length.

§Example

proof fn example() {
    let xs = seq![1, 2];
    let ys = seq![2, 3];
    let f = |x, y| x < y;
    assert(xs.zip_with(ys).all(|(x, y)| f(x, y)) <==>
           forall|i| 0 <= i < xs.len() ==> f(xs[i], ys[i]));
    // We can now prove specific index relationships
    assert(xs[0] < ys[0]); // 1 < 2
    assert(xs[1] < ys[1]); // 2 < 3
}

self.push(elem).flat_map(f) =~= self.flat_map(f) + f(elem),

flat_mapping after pushing an element is the same as flat_mapping first and then appending f of that element.

§Example

proof fn example() {
    let xs = seq![1, 2];
    let f = |x| seq![x, x + 1];
    assert(xs.push(3).flat_map(f) =~= xs.flat_map(f) + f(3));
    // xs.push(3).flat_map(f)    = [1,2,2,3,3,4]
    // xs.flat_map(f) + f(3)     = [1,2,2,3] + [3,4]
}

0 <= i < self.len(),

#[trigger] self.take(i + 1).flat_map(f) =~= self.take(i).flat_map(f) + f(self[i]),

flat_mapping a sequence up to index i+1 is equivalent to flat_mapping up to index i and appending f of the element at index i.

§Example

proof fn example() {
    let xs = seq![1, 2, 3];
    let f = |x| seq![x, x + 1];

    assert(xs.take(2).flat_map(f) =~= xs.take(1).flat_map(f) + f(xs[1]));
    // xs.take(2).flat_map(f)        = [1,2,2,3]
    // xs.take(1).flat_map(f) + f(2) = [1,2] + [2,3]
}

#[trigger] self.len() == 1,

#[trigger] self.flat_map(f) == f(self[0]),

flat_mapping a sequence with a single element is equivalent to applying the function f to that element.

0 <= i < self.len(),

#[trigger] self.take(i + 1).map_values(f) =~= self.take(i).map_values(f).push(f(self[i])),

Mapping a sequence’s first i+1 elements equals mapping its first i elements plus f of the i-th element.

§Example

proof fn example() {
    let xs = seq![1, 2, 3];
    let f = |x| x * 2;

    assert(xs.take(2).map_values(f) =~= xs.take(1).map_values(f).push(f(xs[1])));
    // Left:  [1,2].map(f)          = [2,4]
    // Right: [1].map(f).push(f(2)) = [2].push(4)
}

#[trigger] prefix.is_prefix_of(self),

forall |i: int| 0 <= i < prefix.len() ==> prefix[i] == self[i],

If a sequence is a prefix of another sequence, their elements match at all indices within the prefix length.

§Example

proof fn example() {
    let xs = seq![1, 2, 3];
    let prefix = seq![1, 2];
    assert(prefix.is_prefix_of(xs));
    assert(prefix[0] == xs[0] && prefix[1] == xs[1]);
}

#[trigger] (prefix1 + prefix2).is_prefix_of(self),

prefix1.is_prefix_of(self),

If a concatenated sequence (prefix1 + prefix2) is a prefix of another sequence, then prefix1 by itself is also a prefix of that sequence.

§Example

proof fn example() {
    let xs = seq![1, 2, 3, 4];
    let prefix1 = seq![1, 2];
    let prefix2 = seq![3];
    assert((prefix1 + prefix2).is_prefix_of(xs));
    assert(prefix1.is_prefix_of(xs));
}

#[trigger] (prefix1 + seq![t]).is_prefix_of(self),

#[trigger] prefix1.is_prefix_of(prefix2),

prefix2.is_prefix_of(self),

prefix1 != prefix2,

!prefix1.contains(t),

prefix2.contains(t),

If prefix1 + [t] is a prefix of a sequence, prefix1 is a prefix of prefix2, prefix2 is a prefix of the sequence, prefix1 and prefix2 are different, and prefix1 doesn’t contain t, then prefix2 must contain t.

§Example

proof fn example() {
    let xs = seq![1, 2, 3, 4];
    let prefix1 = seq![1];
    let prefix2 = seq![1, 2];
    let t = 2;
    assert((prefix1 + seq![t]).is_prefix_of(xs));
    assert(prefix1.is_prefix_of(prefix2));
    assert(prefix2.is_prefix_of(xs));
    assert(prefix2.contains(t));
}

#[trigger] (prefix1 + seq![t]).is_prefix_of(self),

#[trigger] (prefix2 + seq![t]).is_prefix_of(self),

!prefix1.contains(t),

!prefix2.contains(t),

prefix1 == prefix2,

If prefix1 + [t] and prefix2 + [t] are both prefixes of a sequence, and neither prefix1 nor prefix2 contains t, then prefix1 equals prefix2.

self.all(p),

p(elem),

#[trigger] self.push(elem).all(p),

If a predicate p is true for all elements in a sequence, and p is true for an element e, then p remains true for all elements after pushing e to the sequence.

§Example

proof fn example() {
    let xs = seq![2, 4, 6];
    let is_even = |x| x % 2 == 0;
    assert(xs.all(is_even));
    assert(is_even(8));
    assert(xs.push(8).all(is_even));
}

(self + s1 == self + s2) <==> (s1 == s2),

Two sequences are equal when concatenated with the same prefix iff those two sequences are equal.

Unzips a sequence that contains pairs into two separate sequences.

self.unzip().0.len() == self.unzip().1.len(),

self.unzip().0.len() == self.len(),

self.unzip().1.len() == self.len(),

forall |i: int| {
    0 <= i < self.len()
        ==> (#[trigger] self.unzip().0[i], #[trigger] self.unzip().1[i]) == self[i]
},

Proof of correctness and expected properties of unzip function

self.unzip().0.zip_with(self.unzip().1) =~= self,

Unzipping a sequence of sequences and then zipping the resulting two sequences back together results in the original sequence of sequences.

{
    if self.len() == 0 {
        Seq::empty()
    } else {
        self.first().add(self.drop_first().flatten())
    }
}

Flattens a sequence of sequences into a single sequence by concatenating subsequences, starting from the first element.

§Example

proof fn flatten_test() {
   let seq: Seq<Seq<int>> = seq![seq![1, 2, 3], seq![4, 5, 6], seq![7, 8, 9]];
   let flat: Seq<int> = seq.flatten();
   reveal_with_fuel(Seq::<Seq<int>>::flatten, 5); //Needed for Verus to unfold the recursive definition of flatten
   assert(flat =~= seq![1, 2, 3, 4, 5, 6, 7, 8, 9]);
}

{
    if self.len() == 0 {
        Seq::empty()
    } else {
        self.drop_last().flatten_alt().add(self.last())
    }
}

Flattens a sequence of sequences into a single sequence by concatenating subsequences in reverse order, i.e. starting from the last element. This is equivalent to a call to flatten, but with concatenation operation applied along the oppositive associativity for the sake of proof reasoning in that direction.

self.len() == 1 ==> self.flatten() == self.first(),

Flattening a sequence of a sequence x, where x has length 1, results in a sequence equivalent to the single element of x

0 <= i < self.len(),

self.flatten_alt().len() >= self[i].len(),

The length of a flattened sequence of sequences x is greater than or equal to any of the lengths of the elements of x.

forall |i: int| 0 <= i < self.len() ==> (#[trigger] self[i]).len() <= j,

self.flatten_alt().len() <= self.len() * j,

The length of a flattened sequence of sequences x is less than or equal to the length of x multiplied by a number greater than or equal to the length of the longest sequence in x.

self.flatten() =~= self.flatten_alt(),

Flattening sequences of sequences in order (starting from the beginning) and in reverse order (starting from the end) results in the same sequence.

#[trigger] self.push(elem).flatten() =~= self.flatten() + elem,

Flattening a sequence of sequences after pushing a new sequence is equivalent to concatenating that sequence to the original flattened result.

#[trigger] self.len() == 1,

#[trigger] self.flatten() == self[0],

Flattening a sequence containing a single sequence yields that inner sequence.

0 < self.len(),

{
    if self.len() == 1 {
        self[0]
    } else if self.len() == 0 {
        0
    } else {
        let later_max = self.drop_first().max();
        if self[0] >= later_max { self[0] } else { later_max }
    }
}

Returns the maximum integer value in a non-empty sequence of integers.

forall |x: int| self.contains(x) ==> x <= self.max(),

forall |i: int| 0 <= i < self.len() ==> self[i] <= self.max(),

self.len() == 0 || self.contains(self.max()),

Proof of correctness and expected properties for max function

0 < self.len(),

{
    if self.len() == 1 {
        self[0]
    } else if self.len() == 0 {
        0
    } else {
        let later_min = self.drop_first().min();
        if self[0] <= later_min { self[0] } else { later_min }
    }
}

Returns the minimum integer value in a non-empty sequence of integers.

forall |x: int| self.contains(x) ==> self.min() <= x,

forall |i: int| 0 <= i < self.len() ==> self.min() <= self[i],

self.len() == 0 || self.contains(self.min()),

Proof of correctness and expected properties for min function

0 <= from < to <= self.len(),

self.subrange(from, to).max() <= self.max(),

The maximum element in a non-empty sequence is greater than or equal to the maxima of its non-empty subsequences.

0 <= from < to <= self.len(),

self.subrange(from, to).min() >= self.min(),

The minimum element in a non-empty sequence is less than or equal to the minima of its non-empty subsequences.

Returns the argument unchanged.

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.