Struct Seq 

pub struct Seq<A> { /* private fields */ }

Seq<A> is a sequence type for specifications. To use a “sequence” in compiled code, use an exec type like vec::Vec that has Seq<A> as its specification type.

An object seq: Seq<A> has a length, given by seq.len(), and a value at each i for 0 <= i < seq.len(), given by seq[i].

Sequences can be constructed in a few different ways:

• Seq::empty construct an empty sequence (len() == 0)
• Seq::new construct a sequence of a given length, initialized according to a given function mapping indices i to values A.
• The seq! macro, to construct small sequences of a fixed size (analagous to the std::vec! macro).
• By manipulating an existing sequence with Seq::push, Seq::update, or Seq::add.

To prove that two sequences are equal, it is usually easiest to use the extensional equality operator =~=.

Implementations

impl<A> Seq<A>

pub fn empty() -> Seq<A>

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

pub fn new(len: nat, f: FnSpec<(int,), A>) -> Seq<A>

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

pub fn len(self) -> nat

The length of a sequence.

pub fn index(self, i: int) -> A

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.

pub fn spec_index(self, i: int) -> A

[] operator, synonymous with index

pub fn spec_index_range_full(self) -> Seq<A>

[..] operator, which returns the original Seq

pub fn spec_index_range_from<I>(self, i: I) -> Seq<A>

where I: Integer,

[i..] operator, synonymous with skip

pub fn spec_index_range_to<J>(self, j: J) -> Seq<A>

where J: Integer,

[..j] operator, synonymous with take

pub fn spec_index_range_to_inclusive<J>(self, j: J) -> Seq<A>

where J: Integer,

[..=j] operator, synonymous with take on j + 1

pub fn spec_index_range<I, J>(self, i: I, j: J) -> Seq<A>

where I: Integer, J: Integer,

[i..j] operator, synonymous with subrange

pub fn spec_index_range_inclusive<I, J>(self, i: I, j: J) -> Seq<A>

where I: Integer, J: Integer,

[i..=j] operator, synonymous with subrange on j + 1

pub fn push(self, a: A) -> Seq<A>

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

pub fn update(self, i: int, a: A) -> Seq<A>

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

pub fn subrange(self, start_inclusive: int, end_exclusive: int) -> Seq<A>

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[2..4];
    assert(sub =~= seq![12, 13]);
}

pub fn take(self, n: int) -> Seq<A>

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

pub fn skip(self, n: int) -> Seq<A>

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

pub fn add(self, rhs: Seq<A>) -> Seq<A>

Concatenates the sequences.

Example

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

pub fn spec_add(self, rhs: Seq<A>) -> Seq<A>

+ operator, synonymous with add

pub fn last(self) -> A

Returns the last element of the sequence.

pub fn first(self) -> A

Returns the first element of the sequence.

pub fn tracked_empty() -> Seq<A>

Create an empty sequence

pub fn tracked_insert(&mut self, i: int, v: A)

Insert a tracked element into a sequence

Example

proof fn insert_test(tracked &mut s: Seq<int>, tracked v: int)
    requires
        old(s)@ == seq![0, 1, 2]
    ensures
        final(s)@ == seq![0, 1, v, 2]
{
    s.tracked_insert(2, v)
}

pub fn tracked_remove(&mut self, i: int) -> A

Remove a tracked element from a sequence

pub fn tracked_borrow(&self, i: int) -> &A

Obtain a tracked borrow into an element of a sequence

pub fn tracked_borrow_mut(&mut self, i: int) -> &mut A

Obtain a tracked mutable borrow into an element of a sequence

pub fn tracked_push(&mut self, v: A)

Push a tracked value into the end of a sequence

pub fn tracked_push_front(&mut self, v: A)

Push a tracked value into the beginning of a sequence

pub fn tracked_pop(&mut self) -> A

Pop a tracked value from the end of a sequence

pub fn tracked_pop_front(&mut self) -> A

Pop a tracked value from the beginning of a sequence

pub fn tracked_split_at(&mut self, i: int) -> Seq<A>

Split a tracked sequence around an index

impl<A> Seq<A>

pub fn map<B>(self, f: FnSpec<(int, A), B>) -> Seq<B>

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.

pub fn map_values<B>(self, f: FnSpec<(A,), B>) -> Seq<B>

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

pub fn flat_map<B>(self, f: FnSpec<(A,), Seq<B>>) -> Seq<B>

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

pub fn as_ref(&self) -> Seq<&A>

Add a reference (&) to each element of the sequence

pub fn lemma_as_ref_index(self, i: int)

pub fn is_prefix_of(self, other: Seq<A>) -> bool

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

pub fn is_suffix_of(self, other: Seq<A>) -> bool

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

pub fn sort_by(self, leq: FnSpec<(A, A), bool>) -> Seq<A>

Sorts the sequence according to the given leq function

Example

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

pub fn all(self, pred: FnSpec<(A,), bool>) -> bool

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

pub fn any(self, pred: FnSpec<(A,), bool>) -> bool

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

pub fn exactly_one(self, pred: FnSpec<(A,), bool>) -> bool

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

pub fn lemma_sort_by_ensures(self, leq: FnSpec<(A, A), bool>)

pub fn filter(self, pred: FnSpec<(A,), bool>) -> Seq<A>

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

pub fn lemma_filter_len(self, pred: FnSpec<(A,), bool>)

pub fn lemma_filter_pred(self, pred: FnSpec<(A,), bool>, i: int)

pub fn lemma_filter_contains(self, pred: FnSpec<(A,), bool>, i: int)

pub fn filter_lemma(self, pred: FnSpec<(A,), bool>)

👎Deprecated:

Use broadcast use group_filter_ensures instead

pub fn filter_distributes_over_add( a: Seq<A>, b: Seq<A>, pred: FnSpec<(A,), bool>, )

pub fn filter_index(self, pred: FnSpec<(int,), bool>) -> Seq<A>

Returns the sequence containing each element at index i of the original sequence such that pred(i) is true.

Example

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

Note that the predicate can also refer to elements of the sequence:

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

pub fn filter_index_range(self, pred: FnSpec<(int,), bool>) -> bool

Every resulting value of filter_index came from self at an acceptable index

pub fn filter_index_domain(self, pred: FnSpec<(int,), bool>) -> bool

Every value in self at an acceptable index is in the result of filter_index

pub fn lemma_filter_index(self, pred: FnSpec<(int,), bool>)

Properties of filter_index

pub fn filter_index_ext(self, p: FnSpec<(int,), bool>, q: FnSpec<(int,), bool>)

filter_index depends only on the predicate’s values on the valid index range, so two pointwise-equal (but distinct) predicate closures yield the same result.

pub fn lemma_filter_index_head(self, pred: FnSpec<(int,), bool>)

Head decomposition for filter_index to better match its use in loops

pub fn add_empty_left(a: Seq<A>, b: Seq<A>)

pub fn add_empty_right(a: Seq<A>, b: Seq<A>)

pub fn push_distributes_over_add(a: Seq<A>, b: Seq<A>, elt: A)

pub fn max_via(self, leq: FnSpec<(A, A), bool>) -> A

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

pub fn min_via(self, leq: FnSpec<(A, A), bool>) -> A

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

pub fn contains(self, needle: A) -> bool

pub fn index_of(self, needle: A) -> int

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

pub fn index_of_first(self, needle: A) -> Option<int>

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

pub fn index_of_first_ensures(self, needle: A)

pub fn index_of_last(self, needle: A) -> Option<int>

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

pub fn index_of_last_ensures(self, needle: A)

pub fn drop_last(self) -> Seq<A>

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.

pub fn drop_last_distributes_over_add(a: Seq<A>, b: Seq<A>)

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

pub fn drop_first(self) -> Seq<A>

pub fn no_duplicates(self) -> bool

returns true if the sequence has no duplicate elements

pub fn disjoint(self, other: Seq<A>) -> bool

Returns true if two sequences are disjoint

pub fn to_set(self) -> Set<A>

Converts a sequence into a set

pub fn to_set_ensures(self)

pub fn to_iset(self) -> ISet<A>

pub fn to_multiset(self) -> Multiset<A>

Converts a sequence into a multiset

pub fn to_multiset_ensures(self)

Proof of function to_multiset() correctness

pub fn insert(self, i: int, a: A) -> Seq<A>

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

pub fn insert_ensures(self, pos: int, elt: A)

Proof of correctness and expected properties of insert function

pub fn remove(self, i: int) -> Seq<A>

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

pub fn remove_ensures(self, i: int)

Proof of function remove() correctness

pub fn remove_value(self, val: A) -> Seq<A>

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.

pub fn reverse(self) -> Seq<A>

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

pub fn zip_with<B>(self, other: Seq<B>) -> Seq<(A, B)>

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

pub fn zip_truncate<B>(self, other: Seq<B>) -> Seq<(A, B)>

Truncates both sequences to the minimum length, then zips them.

pub fn fold_left<B>(self, b: B, f: FnSpec<(B, A), B>) -> B

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

pub fn fold_left_alt<B>(self, b: B, f: FnSpec<(B, A), B>) -> B

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.

pub fn lemma_fold_left_split<B>(self, b: B, f: FnSpec<(B, A), B>, k: int)

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

pub fn lemma_fold_left_alt<B>(self, b: B, f: FnSpec<(B, A), B>)

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

pub fn lemma_reverse_fold_left<B>(self, v: B, f: FnSpec<(B, A), B>)

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

pub fn fold_right<B>(self, f: FnSpec<(A, B), B>, b: B) -> 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)...))).

pub fn fold_right_alt<B>(self, f: FnSpec<(A, B), B>, b: B) -> 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.

pub fn lemma_fold_right_split<B>(self, f: FnSpec<(A, B), B>, b: B, k: int)

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

pub fn lemma_fold_right_commute_one<B>(self, a: A, f: FnSpec<(A, B), B>, v: B)

pub fn lemma_fold_right_alt<B>(self, f: FnSpec<(A, B), B>, b: B)

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

pub fn lemma_reverse_fold_right<B>(self, v: B, f: FnSpec<(A, B), B>)

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

pub fn lemma_multiset_has_no_duplicates(self)

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

pub fn lemma_multiset_has_no_duplicates_conv(self)

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

pub fn lemma_reverse_to_multiset(self)

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

pub fn lemma_add_last_back(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.

pub fn lemma_indexing_implies_membership(self, f: FnSpec<(A,), bool>)

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.

pub fn lemma_membership_implies_indexing(self, f: FnSpec<(A,), bool>)

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.

pub fn lemma_split_at(self, pos: int)

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.

pub fn lemma_element_from_slice(self, new: Seq<A>, a: int, b: int, pos: int)

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

pub fn lemma_slice_of_slice(self, s1: int, e1: int, s2: int, e2: int)

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.

pub fn unique_seq_to_set(self)

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

pub fn lemma_cardinality_of_set(self)

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

pub fn lemma_cardinality_of_empty_set_is_0(self)

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

pub fn lemma_no_dup_set_cardinality(self)

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

pub fn lemma_to_set_map_commutes<B>(self, f: FnSpec<(A,), B>)

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

pub fn lemma_to_iset_map_commutes<B>(self, f: FnSpec<(A,), B>)

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

pub fn lemma_to_set_insert_commutes(sq: Seq<A>, elt: A)

Appending an element to a sequence and converting to a Set is equal to converting to a Set and inserting the element.

pub fn lemma_to_iset_insert_commutes(sq: Seq<A>, elt: A)

Appending an element to a sequence and converting to an ISet is equal to converting to an ISet and inserting the element.

pub fn update_subrange_with(self, off: int, vs: Seq<A>) -> Seq<A>

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.

pub fn lemma_seq_skip_skip(self, i: int)

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[2..][1..] =~= s[3..]);
}

pub fn lemma_contains_to_index(self, elem: A) -> int

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

pub fn lemma_all_from_head_tail(self, pred: FnSpec<(A,), bool>)

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[1..].all(is_even));
    s.lemma_all_from_head_tail(is_even);
    assert(s.all(is_even));
}

pub fn lemma_any_tail(self, pred: FnSpec<(A,), bool>)

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[1..].any(is_even));
}

pub fn remove_duplicates(self, seen: Seq<A>) -> Seq<A>

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

pub fn lemma_remove_duplicates_properties(self, seen: Seq<A>)

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

pub fn lemma_remove_duplicates_append_index(self, i: int, seen: Seq<A>)

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

pub fn lemma_remove_duplicates_append(self, x: A, seen: Seq<A>)

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

pub fn lemma_all_neg_filter_empty(self, pred: FnSpec<(A,), bool>)

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

pub fn filter_map<B>(self, f: FnSpec<(A,), Option<B>>) -> Seq<B>

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

pub fn lemma_filter_contains_rev(self, p: FnSpec<(A,), bool>, elem: A)

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

pub fn lemma_filter_map_contains<B>(self, f: FnSpec<(A,), Option<B>>, elt: B)

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

pub fn lemma_take_succ(xs: Seq<A>, k: int)

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]

pub fn lemma_filter_map_singleton<B>(a: A, f: FnSpec<(A,), Option<B>>)

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)

pub fn lemma_filter_map_take_succ<B>(self, f: FnSpec<(A,), Option<B>>, i: int)

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[..2].filter_map(f) == s[..1].filter_map(f) + seq![f(s[1]).unwrap()]);
assert(s[..2].filter_map(f) == seq![] + seq![4]);

pub fn filter_alt(self, p: FnSpec<(A,), bool>) -> Seq<A>

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.

pub fn lemma_filter_prepend(self, x: A, p: FnSpec<(A,), bool>)

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
}

pub fn lemma_filter_eq_filter_alt(self, p: FnSpec<(A,), bool>)

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

pub fn lemma_filter_monotone(self, ys: Seq<A>, p: FnSpec<(A,), bool>)

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

pub fn lemma_filter_take_len(self, p: FnSpec<(A,), bool>, i: int)

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[..i] =~= seq![1, 2, 3]);
    assert(s[..i].filter(is_even) =~= seq![2]);
    assert(s.filter(is_even) =~= seq![2, 4]);
    assert(s.filter(is_even).len() >= s[..i].filter(is_even).len());
}

pub fn lemma_filter_len_push(self, p: FnSpec<(A,), bool>, elem: A)

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[..3].filter(is_even).len());
}

pub fn lemma_index_contains(self, i: int)

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

pub fn lemma_take_succ_push(self, i: int)

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

pub fn lemma_take_len(self)

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

pub fn lemma_take_any_succ(self, p: FnSpec<(A,), bool>, i: int)

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[..i + 1].any(is_even) == (s[..i].any(is_even) || is_even(s[i])));
}

pub fn lemma_no_duplicates_injective<B>(self, f: FnSpec<(A,), B>)

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

pub fn lemma_push_map_commute<B>(self, f: FnSpec<(A,), B>, x: A)

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

pub fn lemma_push_to_set_commute(self, elem: A)

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

pub fn lemma_filter_push(self, elem: A, pred: FnSpec<(A,), bool>)

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

pub fn lemma_zip_with_contains_index<B>(self, b: Seq<B>, i: int)

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

pub fn lemma_zip_with_uncurry_all<B>(self, b: Seq<B>, f: FnSpec<(A, B), bool>)

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
}

pub fn lemma_flat_map_push<B>(self, f: FnSpec<(A,), Seq<B>>, elem: A)

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

pub fn lemma_flat_map_take_append<B>(self, f: FnSpec<(A,), Seq<B>>, i: int)

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[..2].flat_map(f) =~= xs[..1].flat_map(f) + f(xs[1]));
    // xs[..2].flat_map(f)        = [1,2,2,3]
    // xs[..1].flat_map(f) + f(2) = [1,2] + [2,3]
}

pub fn lemma_flat_map_singleton<B>(self, f: FnSpec<(A,), Seq<B>>)

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

pub fn lemma_map_take_succ<B>(self, f: FnSpec<(A,), B>, i: int)

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[..2].map_values(f) =~= xs[..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)
}

pub fn lemma_prefix_index_eq(self, prefix: Seq<A>)

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

pub fn lemma_prefix_concat(self, prefix1: Seq<A>, prefix2: Seq<A>)

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

pub fn lemma_prefix_chain_contains(self, prefix1: Seq<A>, prefix2: Seq<A>, t: A)

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

pub fn lemma_prefix_append_unique(self, prefix1: Seq<A>, prefix2: Seq<A>, t: A)

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

pub fn lemma_all_push(self, p: FnSpec<(A,), bool>, elem: A)

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

pub fn lemma_concat_injective(self, s1: Seq<A>, s2: Seq<A>)

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

pub fn group_seq_extra()

impl<A> Seq<&A>

pub fn unref(self) -> Seq<A>

Dereference each element of the sequence

impl<A, B> Seq<(&A, &B)>

pub fn unref(self) -> Seq<(A, B)>

Dereference each element of each tuple in the sequence

impl<A, B> Seq<(A, B)>

pub fn unzip(self) -> (Seq<A>, Seq<B>)

Unzips a sequence that contains pairs into two separate sequences.

pub fn unzip_ensures(self)

Proof of correctness and expected properties of unzip function

pub fn lemma_zip_of_unzip(self)

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

impl<A> Seq<Seq<A>>

pub fn flatten(self) -> Seq<A>

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

pub fn flatten_alt(self) -> Seq<A>

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.

pub fn lemma_flatten_one_element(self)

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

pub fn lemma_flatten_length_ge_single_element_length(self, i: int)

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

pub fn lemma_flatten_length_le_mul(self, j: int)

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.

pub fn lemma_flatten_and_flatten_alt_are_equivalent(self)

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

pub fn lemma_flatten_push(self, elem: Seq<A>)

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

pub fn lemma_flatten_singleton(self)

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

pub fn group_seq_flatten()

impl Seq<int>

pub fn max(self) -> int

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

pub fn max_ensures(self)

Proof of correctness and expected properties for max function

pub fn min(self) -> int

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

pub fn min_ensures(self)

Proof of correctness and expected properties for min function

pub fn sort(self) -> Seq<int>

pub fn lemma_sort_ensures(self)

pub fn lemma_subrange_max(self, from: int, to: int)

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

pub fn lemma_subrange_min(self, from: int, to: int)

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

Trait Implementations

impl ExecSpecType for Seq<char>

Impls for shared traits

type ExecOwnedType = String

Owned version of the exec type.

type ExecRefType<'a> = &'a str

Reference version of the exec type.

impl<T, const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<Seq<T>> for Size<HAS_MIN, MIN, HAS_MAX, MAX>

open spec fn apply(&self, value: Seq<T>) -> bool

{ size_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value.len()) }