let ((lemma_splitAt_append (#a:Type) (n:nat) (l:list a)):(Lemma ((requires <=(n, length l))) ((ensures (let  (l1, l2) = splitAt n l in /\(==(append l1 l2, l), =(length l1, n))))))):match n with 0  -> () | _  -> match l with []  -> () | (Prims.Cons x xs)  -> lemma_splitAt_append (-(n, 1)) xs

If we [append] the two lists produced using a [splitAt], then we get back the original list

let ((lemma_append_splitAt (#t:Type) (l1:list t) (l2:list t)):(Lemma ((ensures (==(splitAt (length l1) (append l1 l2), ((FStar.Pervasives.Native.Mktuple2 l1 l2)))))))):match l1 with []  -> () | _  -> lemma_append_splitAt (tl l1) l2

If we [splitAt] the point at which two lists have been [append]ed, then we get back the original lists.

let ((lemma_splitAt (#t:Type) (l:list t) (l1:list t) (l2:list t) (n:n:nat:{<=(n, length l)})):(Lemma (<==>(==(splitAt n l, ((FStar.Pervasives.Native.Mktuple2 l1 l2))), /\(==(l, @(l1, l2)), =(length l1, n)))))):lemma_splitAt_append n l; lemma_append_splitAt l1 l2

Fully characterize behavior of [splitAt] in terms of more standard list concepts

let ((lemma_splitAt_index_hd (#t:Type) (n:nat) (l:list t)):(Lemma ((requires (<(n, length l)))) ((ensures (let  (l1, l2) = splitAt n l in splitAt_length n l; /\(>(length l2, 0), ==(hd l2, index l n))))))):let  (Prims.Cons x xs) = l in match n with 0  -> () | _  -> lemma_splitAt_index_hd (-(n, 1)) (tl l)

The [hd] of the second list returned via [splitAt] is the [n]th element of the original list

let ((lemma_splitAt_shorten_left (#t:Type) (l1:list t) (l2:list t) (i:i:nat:{/\(<=(i, length l1), <=(i, length l2))}) (j:j:nat:{<=(j, i)})):(Lemma ((requires (==(fst (splitAt i l1), fst (splitAt i l2))))) ((ensures (==(fst (splitAt j l1), fst (splitAt j l2))))))):match j with 0  -> () | _  -> lemma_splitAt_shorten_left (tl l1) (tl l2) (-(i, 1)) (-(j, 1))

If two lists have the same left prefix, then shorter left prefixes are also the same.

let ((lemma_splitAt_reindex_left (#t:Type) (i:nat) (l:list t) (j:nat)):(Lemma ((requires /\(<=(i, length l), <(j, i)))) ((ensures (let  (left, right) = splitAt i l in splitAt_length i l; /\(<(j, length left), ==(index left j, index l j))))))):match (FStar.Pervasives.Native.Mktuple2 i j) with (1, _)|
 (_, 0)  -> () | _  -> lemma_splitAt_reindex_left (-(i, 1)) (tl l) (-(j, 1))

Doing an [index] on the left-part of a [splitAt] is same as doing it on the original list

let ((lemma_splitAt_reindex_right (#t:Type) (i:nat) (l:list t) (j:nat)):(Lemma ((requires /\(<=(i, length l), <(+(j, i), length l)))) ((ensures (let  (left, right) = splitAt i l in splitAt_length i l; /\(<(j, length right), ==(index right j, index l (+(j, i))))))))):match i with 0  -> () | _  -> lemma_splitAt_reindex_right (-(i, 1)) (tl l) j

Doing an [index] on the right-part of a [splitAt] is same as doing it on the original list, but shifted

 Properties of split3

let ((lemma_split3_append (#t:Type) (l:list t) (n:n:nat:{<(n, length l)})):(Lemma ((requires True)) ((ensures (let  (a, b, c) = split3 l n in ==(l, append a ((Prims.Cons b c)))))))):lemma_splitAt_append n l

The 3 pieces returned via [split3] can be joined together via an [append] and a [cons]

let ((lemma_split3_index (#t:Type) (l:list t) (n:n:nat:{<(n, length l)})):(Lemma ((requires True)) ((ensures (let  (a, b, c) = split3 l n in ==(b, index l n)))))):lemma_splitAt_index_hd n l

let ((lemma_split3_length (#t:Type) (l:list t) (n:n:nat:{<(n, length l)})):(Lemma ((requires True)) ((ensures (let  (a, b, c) = split3 l n in /\(=(length a, n), =(length c, -(-(length l, n), 1)))))))):splitAt_length n l

let ((lemma_split3_on_same_leftprefix (#t:Type) (l1:list t) (l2:list t) (n:n:nat:{/\(<(n, length l1), <(n, length l2))})):(Lemma ((requires (==(fst (splitAt (+(n, 1)) l1), fst (splitAt (+(n, 1)) l2))))) ((ensures (let  (a1, b1, c1) = split3 l1 n in let  (a2, b2, c2) = split3 l2 n in /\(==(a1, a2), ==(b1, b2))))))):let  (a1, b1, c1) = split3 l1 n in let  (a2, b2, c2) = split3 l2 n in lemma_split3_append l1 n; lemma_split3_append l2 n; lemma_split3_length l1 n; lemma_split3_length l2 n; append_l_cons b1 c1 a1; append_l_cons b2 c2 a2; let  (x1, y1) = splitAt (+(n, 1)) l1 in let  (x2, y2) = splitAt (+(n, 1)) l2 in lemma_splitAt_append (+(n, 1)) l1; lemma_splitAt_append (+(n, 1)) l2; splitAt_length (+(n, 1)) l1; splitAt_length (+(n, 1)) l2; append_length_inv_head x1 y1 (append a1 (Prims.Cons b1 (Prims.Nil ))) c1; append_length_inv_head x2 y2 (append a2 (Prims.Cons b2 (Prims.Nil ))) c2; append_length_inv_tail a1 (Prims.Cons b1 (Prims.Nil )) a2 (Prims.Cons b2 (Prims.Nil )); ()

If we [split3] on lists with the same left prefix, we get the same element and left prefix.

let ((lemma_split3_unsnoc (#t:Type) (l:list t) (n:n:nat:{<(n, length l)})):(Lemma ((requires (<>(n, -(length l, 1))))) ((ensures (let  (a, b, c) = split3 l n in lemma_split3_length l n; /\(>(length c, 0), (let  (xs, x) = unsnoc l in let  (ys, y) = unsnoc c in ==(append a ((Prims.Cons b ys)), xs)))))))):match n with 0  -> () | _  -> lemma_split3_unsnoc (tl l) (-(n, 1))

If we perform an [unsnoc] on a list, then the left part is the same as an [append]+[cons] on the list after [split3].

let ((lemma_unsnoc_split3 (#t:Type) (l:list t) (i:i:nat:{<(i, length l)})):(Lemma ((requires (<>(i, -(length l, 1))))) ((ensures (let  (xs, x) = unsnoc l in /\(<(i, length xs), (let  (a0, b0, c0) = split3 l i in let  (a1, b1, c1) = split3 xs i in /\(==(a0, a1), ==(b0, b1))))))))):let  (xs, x) = unsnoc l in lemma_unsnoc_length l; let  (a0, b0, c0) = split3 l i in let  (a1, b1, c1) = split3 xs i in splitAt_length_total xs; lemma_splitAt_shorten_left xs l (length xs) (+(i, 1)); lemma_split3_on_same_leftprefix l xs i

Doing [unsnoc] and [split3] in either order leads to the same left part, and element.

let ((lemma_split3_r_hd (#t:Type) (l:list t) (i:i:nat:{<(i, length l)})):(Lemma ((ensures (let  (a, b, c) = split3 l i in lemma_split3_length l i; ==>(>(length c, 0), /\(<(+(i, 1), length l), ==(hd c, index l (+(i, 1)))))))))):match i with 0  -> () | _  -> lemma_split3_r_hd (tl l) (-(i, 1))

module FStar.List.Pure.Properties