vstd_extra/
seq_extra.rs

1//! Extra properties of [`vstd::seq::Seq`](https://verus-lang.github.io/verus/verusdoc/vstd/seq/struct.Seq.html).
2use vstd::prelude::*;
3use vstd::seq::*;
4use vstd::seq_lib::*;
5
6verus! {
7
8/// Splits a tracked sequence at position `n`, leaving `[0, n)` in `s`
9/// and returning `[n, len)`.
10pub proof fn seq_tracked_split_at<T>(tracked s: &mut Seq<T>, n: int) -> (tracked result: Seq<T>)
11    requires
12        0 <= n <= old(s).len(),
13    ensures
14        *final(s) == old(s).subrange(0, n),
15        result == old(s).subrange(n, old(s).len() as int),
16    decreases old(s).len() - n,
17{
18    if n == s.len() {
19        Seq::tracked_empty()
20    } else {
21        let ghost orig = *s;
22        let tracked last = s.tracked_pop();
23        let tracked mut result = seq_tracked_split_at(s, n);
24        result.tracked_push(last);
25        result
26    }
27}
28
29pub broadcast proof fn lemma_seq_add_head_back<T>(s: Seq<T>)
30    requires
31        s.len() > 0,
32    ensures
33        s == #[trigger] seq![s[0]].add(s.drop_first()),
34{
35}
36
37pub broadcast proof fn lemma_seq_push_head<T>(s: Seq<T>, hd: T)
38    ensures
39        #[trigger] seq![hd].add(s) == s.reverse().push(hd).reverse(),
40{
41}
42
43pub broadcast proof fn lemma_seq_drop_pushed_head<T>(s: Seq<T>, hd: T)
44    ensures
45        #[trigger] seq![hd].add(s).drop_first() == s,
46{
47}
48
49pub broadcast proof fn lemma_seq_push_head_take_head<T>(s: Seq<T>, hd: T)
50    ensures
51        #[trigger] seq![hd].add(s)[0] == hd,
52{
53}
54
55} // verus!
56verus! {
57
58/// The result of pushing element `needle` into the sequence `s` contains `needle`.
59pub proof fn lemma_push_contains_same<T>(s: Seq<T>, needle: T)
60    ensures
61        #[trigger] s.push(needle).contains(needle),
62{
63    assert(s.push(needle).last() == needle);
64}
65
66/// If element `needle` is different from `new_elem`, then whether the sequence `s` contains `needle`
67/// after pushing `new_elem` depends on whether `s` contains `needle` before the push.
68pub proof fn lemma_push_contains_different<T>(s: Seq<T>, new_elem: T, needle: T)
69    requires
70        new_elem != needle,
71    ensures
72        #[trigger] s.push(new_elem).contains(needle) == s.contains(needle),
73{
74    if s.contains(needle) {
75        let i = choose|i: int| 0 <= i < s.len() && s[i] == needle;
76        axiom_seq_push_index_different(s, needle, i);
77        assert(0 <= i < s.push(new_elem).len() && s.push(new_elem)[i] == needle);
78    }
79}
80
81/// If the last element of the sequence `s` is different from `needle`, then whether the sequence
82/// `s` contains `needle` after dropping the last element depends on whether `s` contains `needle`
83/// before the drop.
84pub proof fn lemma_drop_last_contains_different<T>(s: Seq<T>, needle: T)
85    requires
86        s.len() > 0,
87        s.last() != needle,
88    ensures
89        #[trigger] s.drop_last().contains(needle) == s.contains(needle),
90{
91    if s.contains(needle) {
92        let i = choose|i: int| 0 <= i < s.len() && s[i] == needle;
93        assert(0 <= i < s.drop_last().len() && s.drop_last()[i] == needle);
94    }
95}
96
97} // verus!
98verus! {
99
100/// Returns true if predicate `f(i,seq[i])` holds for all indices `i`.
101pub open spec fn forall_seq<T>(seq: Seq<T>, f: spec_fn(int, T) -> bool) -> bool {
102    forall|i| #![trigger seq[i]] 0 <= i < seq.len() ==> f(i, seq[i])
103}
104
105pub broadcast group group_forall_seq_lemmas {
106    lemma_forall_seq_push,
107    lemma_seq_all_push,
108    lemma_forall_seq_drop_last,
109    lemma_seq_all_drop_last,
110    lemma_seq_all_add,
111    lemma_seq_all_index,
112}
113
114/// Index `i` of the sequence `s` satisfies `f(i,s[i])` if `forall_seq(s,f)` holds.
115pub proof fn lemma_forall_seq_index<T>(s: Seq<T>, f: spec_fn(int, T) -> bool, i: int)
116    requires
117        forall_seq(s, f),
118        0 <= i < s.len(),
119    ensures
120        f(i, s[i]),
121{
122}
123
124/// Index `i` of the sequence `s` satisfies `f(s[i])` if `s.all(f)` holds.
125/// This proof is required due to the change of trigger by replacing the original `forall_seq_values` with `Seq::all`.
126pub broadcast proof fn lemma_seq_all_index<T>(s: Seq<T>, f: spec_fn(T) -> bool, i: int)
127    requires
128        0 <= i < s.len(),
129        #[trigger] s.all(f),
130    ensures
131        f(#[trigger] (s[i])),
132{
133}
134
135/// `forall_seq(s.push(v),f)` is equivalent to `forall_seq(s,f)` and `f(s.len(),v)`.
136pub broadcast proof fn lemma_forall_seq_push<T>(s: Seq<T>, f: spec_fn(int, T) -> bool, v: T)
137    ensures
138        forall_seq(s, f) && f(s.len() as int, v) <==> #[trigger] forall_seq(s.push(v), f),
139{
140    if forall_seq(s.push(v), f) {
141        assert forall|i| 0 <= i < s.len() implies f(i, s[i]) by {
142            assert(s[i] == s.push(v)[i]);
143        }
144        assert(s.push(v)[s.len() as int] == v);
145    }
146}
147
148/// s.push(v).all(f)` is equivalent to `s.all(f)` and `f(v)`.
149pub broadcast proof fn lemma_seq_all_push<T>(s: Seq<T>, f: spec_fn(T) -> bool, v: T)
150    ensures
151        #[trigger] s.push(v).all(f) <==> s.all(f) && f(v),
152{
153    if s.push(v).all(f) {
154        assert forall|i| 0 <= i < s.len() implies f(s[i]) by {
155            assert(s[i] == s.push(v)[i]);
156        }
157        assert(s.push(v)[s.len() as int] == v);
158    }
159}
160
161/// `forall_seq(s,f)` is equivalent to `forall_seq(s.drop_last(),f)` and `f(s.len() as int - 1, s.last())`.
162pub broadcast proof fn lemma_forall_seq_drop_last<T>(s: Seq<T>, f: spec_fn(int, T) -> bool)
163    requires
164        s.len() > 0,
165    ensures
166        forall_seq(s, f) <==> #[trigger] forall_seq(s.drop_last(), f) && f(
167            s.len() as int - 1,
168            s.last(),
169        ),
170{
171    assert(s == s.drop_last().push(s.last()));
172}
173
174/// `s.all(f)` is equivalent to `s.drop_last().all(f)` and `f(s.last())`.
175pub broadcast proof fn lemma_seq_all_drop_last<T>(s: Seq<T>, f: spec_fn(T) -> bool)
176    requires
177        s.len() > 0,
178    ensures
179        s.all(f) <==> #[trigger] s.drop_last().all(f) && f(s.last()),
180{
181    assert(s == s.drop_last().push(s.last()));
182}
183
184pub broadcast proof fn lemma_seq_all_add<T>(s1: Seq<T>, s2: Seq<T>, f: spec_fn(T) -> bool)
185    ensures
186        s1.all(f) && s2.all(f) <==> #[trigger] (s1 + s2).all(f),
187    decreases s2.len(),
188{
189    if s2.len() == 0 {
190        assert(s1 + s2 == s1);
191    } else {
192        lemma_seq_all_add(s1, s2.drop_last(), f);
193        if s1.all(f) && s2.all(f) {
194            assert((s1 + s2).all(f));
195        }
196        if (s1 + s2).all(f) {
197            assert((s1 + s2).drop_last() == s1 + s2.drop_last());
198            assert(s2 == s2.drop_last().push(s2.last()));
199            assert((s1 + s2).last() == s2.last());
200        }
201    }
202}
203
204/// If `source1` and `source2` are prefixes of `child`, then either `source1` is equal to `source2` or
205/// one of them is a prefix of the other.
206pub proof fn lemma_prefix_of_common_sequence(source1: Seq<nat>, source2: Seq<nat>, child: Seq<nat>)
207    requires
208        source1.is_prefix_of(child),
209        source2.is_prefix_of(child),
210    ensures
211        source1 == source2 || source1.len() < source2.len() && source1.is_prefix_of(source2)
212            || source2.len() < source1.len() && source2.is_prefix_of(source1),
213{
214}
215
216pub broadcast proof fn lemma_seq_to_set_map_contains<T, U>(s: Seq<T>, f: spec_fn(T) -> U, i: int)
217    requires
218        0 <= i < s.len(),
219    ensures
220        #![trigger s.map_values(f), s[i]]
221        (s.map_values(f)).to_set().contains(f(s[i])),
222{
223    assert(s.contains(s[i]));
224    assert(f(s[i]) == s.map_values(f)[i]);
225}
226
227pub broadcast group group_seq_extra_lemmas {
228    lemma_seq_add_head_back,
229    lemma_seq_push_head,
230    lemma_seq_drop_pushed_head,
231    lemma_seq_push_head_take_head,
232    lemma_seq_to_set_map_contains,
233}
234
235} // verus!
vstd_extra/seq_extra.rs

vstd_extra/
seq_extra.rs
