Struct vstd::seq::Seq

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(),

[] 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]);
}

DEPRECATED: use =~= or =~~= instead. Returns true if the two sequences are pointwise equal, i.e., they have the same length and the corresponding values are equal at each index. This is equivalent to the sequences being actually equal by axiom_seq_ext_equal.

To prove that two sequences are equal via extensionality, it may be easier to use the general-purpose =~= or =~~= or to use the assert_seqs_equal! macro, rather than using .ext_equal directly.

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]);
}

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

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]);
}

+ operator, synonymous with add

0 < self.len(),

Returns the last element of the sequence.

0 < self.len(),

Returns the first element of the sequence.

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.

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.

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));
}

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 ../../../rust_verify/example/multiset.rs:sorted_by_leq}}

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,

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

self.len() > 0,

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

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,

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

returns true if the sequence has no duplicate elements

Returns true if two sequences are disjoint

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),

self.len() == 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(),

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(),

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

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.

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

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

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

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).

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.

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

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

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)...))).

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.

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

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

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

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

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.

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]);
}

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.

0 < self.len(),

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(),

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.