vstd::seq_lib

Function lemma_exactly_one_view

Source 
pub proof fn lemma_exactly_one_view<S: View>(
    s: Seq<S>,
    p: FnSpec<(S,), bool>,
    sp: FnSpec<(S::V,), bool>,
)
Expand description
requires
forall |s: S| p(s) <==> sp(s.view()),
injective(|x: S| x.view()),
ensures
s.exactly_one(p) <==> s.map_values(|x: S| x.view()).exactly_one(sp),

A sequence has exactly one element satisfying a predicate iff viewing all elements and filtering with the corresponding predicate produces a sequence with exactly one element.

§Example

proof fn example() {
    let s = seq!["hello".to_string(), "world".to_string()];
    let p = |x: String| x.len() == 5;
    let sp = |x: Seq<char>| x.len() == 5;

    assert(s.exactly_one(p) <==> s.map_values(|x| x.view()).exactly_one(sp));
}