module FStar.List.Tot.Properties

Properties of pure total operations on lists

This module states and proves some properties about pure and total operations on lists.

let (llist a (n:nat)):l:list a:{=(length l, n)}

A list indexed by its length *

 Properties about mem *
val mem_empty:Unidentified product: [#a:eqtype] Unidentified product: [x:a] (Lemma ((requires (mem x (Prims.Nil )))) ((ensures False)))

The empty list has no elements

val mem_existsb:Unidentified product: [#a:eqtype] Unidentified product: [f:(Unidentified product: [a] (Tot bool))] Unidentified product: [xs:list a] (Lemma ((ensures (<==>(existsb f xs, (exists x:a.{:pattern } (/\(=(f x, true), mem x xs))))))))

Full specification for [existsb]: [existsb f xs] holds if, and only if, there exists an element [x] of [xs] such that [f x] holds.

 Properties about rev *
val rev_mem:Unidentified product: [#a:eqtype] Unidentified product: [l:list a] Unidentified product: [x:a] (Lemma ((requires True)) ((ensures (<==>(mem x (rev l), mem x l)))))

A list and its reversed have the same elements

 Properties about append *
let ((lemma_append_last (#a:Type) (l1:list a) (l2:list a)):(Lemma ((requires (>(length l2, 0)))) ((ensures (==(last (@(l1, l2)), last l2)))))):match l1 with []  -> () | (Prims.Cons _ l1')  -> lemma_append_last l1' l2

The [last] element of a list remains the same, even after that list is [append]ed to another list.

 Properties mixing rev and append *
 Properties about snoc 
 Reverse induction principle *
 Properties about iterators *
 Properties about unsnoc 
val lemma_unsnoc_snoc:Unidentified product: [#a:Type] Unidentified product: [l:l:list a:{>(length l, 0)}] (Lemma ((requires True)) ((ensures (==(snoc (unsnoc l), l)))) (Prims.Cons (SMTPat (snoc (unsnoc l))) (Prims.Nil )))

[unsnoc] is the inverse of [snoc]

val lemma_snoc_unsnoc:Unidentified product: [#a:Type] Unidentified product: [lx:(*(list a, a))] (Lemma ((requires True)) ((ensures (==(unsnoc (snoc lx), lx)))) (decreases (length (fst (lx)))) (Prims.Cons (SMTPat (unsnoc (snoc lx))) (Prims.Nil )))

[snoc] is the inverse of [unsnoc]

val lemma_unsnoc_length:Unidentified product: [#a:Type] Unidentified product: [l:l:list a:{>(length l, 0)}] (Lemma ((requires True)) ((ensures (==(length (fst (unsnoc l)), -(length l, 1))))))

Doing an [unsnoc] gives us a list that is shorter in length by 1

let ((lemma_unsnoc_append (#a:Type) (l1:list a) (l2:list a)):(Lemma ((requires (>(length l2, 0)))) ((ensures (let  (as, a) = unsnoc (@(l1, l2)) in let  (bs, b) = unsnoc l2 in /\(==(as, @(l1, bs)), ==(a, b))))))):match l1 with []  -> () | (Prims.Cons _ l1')  -> lemma_unsnoc_append l1' l2

[unsnoc] followed by [append] can be connected to the same vice-versa.

let ((lemma_unsnoc_is_last (#t:Type) (l:list t)):(Lemma ((requires (>(length l, 0)))) ((ensures (/\(==(snd (unsnoc l), last l), ==(snd (unsnoc l), index l (-(length l, 1))))))))):match l with [_]  -> () | _  -> lemma_unsnoc_is_last (tl l)

[unsnoc] gives you [last] element, which is [index]ed at [length l - 1]

let ((lemma_unsnoc_index (#t:Type) (l:list t) (i:nat)):(Lemma ((requires (/\(>(length l, 0), <(i, -(length l, 1)))))) ((ensures (/\(<(i, length (fst (unsnoc l))), ==(index (fst (unsnoc l)) i, index l i))))))):match i with 0  -> () | _  -> lemma_unsnoc_index (tl l) (-(i, 1))

[index]ing on the left part of an [unsnoc]d list is the same as indexing the original list.

 Definition and properties about [split_using] 
let ((split_using (#t:Type) (l:list t) (x:x:t:{memP x l})):(GTot (r:(*(list t, list t))))):match l with [_]  -> (FStar.Pervasives.Native.Mktuple2 (Prims.Nil ) l) | (Prims.Cons a as)  -> if FStar.StrongExcludedMiddle.strong_excluded_middle (==(a, x)) then ((FStar.Pervasives.Native.Mktuple2 (Prims.Nil ) l)) else (let  (l1', l2') = split_using as x in (FStar.Pervasives.Native.Mktuple2 (Prims.Cons a l1') l2'))

[split_using] splits a list at the first instance of finding an element in it.

NOTE: Uses [strong_excluded_middle] axiom. 
 Definition of [index_of] 
let ((index_of (#t:Type) (l:list t) (x:x:t:{memP x l})):(GTot (i:nat:{/\(<(i, length l), ==(index l i, x))}))):match l with [_]  -> 0 | (Prims.Cons a as)  -> if FStar.StrongExcludedMiddle.strong_excluded_middle (==(a, x)) then (0) else (+(1, index_of as x))

[index_of l x] gives the index of the leftmost [x] in [l].

NOTE: Uses [strong_excluded_middle] axiom. 
 Properties about partition *
val partition_mem:Unidentified product: [#a:eqtype] Unidentified product: [f:(Unidentified product: [a] (Tot bool))] Unidentified product: [l:list a] Unidentified product: [x:a] (Lemma ((requires True)) ((ensures (let  (l1, l2) = partition f l in =(mem x l, (||(mem x l1, mem x l2)))))))

If [partition f l = (l1, l2)], then for any [x], [x] is in [l] if and only if [x] is in either one of [l1] or [l2]

val partition_mem_forall:Unidentified product: [#a:eqtype] Unidentified product: [f:(Unidentified product: [a] (Tot bool))] Unidentified product: [l:list a] (Lemma ((requires True)) ((ensures (let  (l1, l2) = partition f l in (forall x.{:pattern } =(mem x l, (||(mem x l1, mem x l2))))))))

Same as [partition_mem], but using [forall]

val partition_mem_p_forall:Unidentified product: [#a:eqtype] Unidentified product: [p:(Unidentified product: [a] (Tot bool))] Unidentified product: [l:list a] (Lemma ((requires True)) ((ensures (let  (l1, l2) = partition p l in /\((forall x.{:pattern } ==>(mem x l1, p x)), (forall x.{:pattern } ==>(mem x l2, not (p x))))))))

If [partition f l = (l1, l2)], then for any [x], if [x] is in [l1] (resp. [l2]), then [f x] holds (resp. does not hold)

val partition_count:Unidentified product: [#a:eqtype] Unidentified product: [f:(Unidentified product: [a] (Tot bool))] Unidentified product: [l:list a] Unidentified product: [x:a] (Lemma ((requires True)) ((ensures (=(count x l, (+(count x (fst (partition f l)), count x (snd (partition f l)))))))))

If [partition f l = (l1, l2)], then the number of occurrences of any [x] in [l] is the same as the sum of the number of occurrences in [l1] and [l2].

val partition_count_forall:Unidentified product: [#a:eqtype] Unidentified product: [f:(Unidentified product: [a] (Tot bool))] Unidentified product: [l:list a] (Lemma ((requires True)) ((ensures (forall x.{:pattern } =(count x l, (+(count x (fst (partition f l)), count x (snd (partition f l)))))))))

Same as [partition_count], but using [forall]

 Correctness of quicksort *
val sortWith_permutation:Unidentified product: [#a:eqtype] Unidentified product: [f:(Unidentified product: [a] Unidentified product: [a] (Tot int))] Unidentified product: [l:list a] (Lemma ((requires True)) ((ensures (forall x.{:pattern } =(count x l, count x (sortWith f l))))) (decreases (length l)))

Correctness of [sortWith], part 1/2: the number of occurrences of any [x] in [sortWith f l] is the same as the number of occurrences in [l].

val sorted:Unidentified product: [(Unidentified product: ['a] Unidentified product: ['a] (Tot bool))] Unidentified product: [list 'a] (Tot bool)

[sorted f l] holds if, and only if, any two consecutive elements [x], [y] of [l] are such that [f x y] holds.

typeabbrev 

[f] is a total order if, and only if, it is reflexive, anti-symmetric, transitive and total.

val append_sorted:Unidentified product: [#a:eqtype] Unidentified product: [f:(Unidentified product: [a] Unidentified product: [a] (Tot bool))] Unidentified product: [l1:l1:list a:{sorted f l1}] Unidentified product: [l2:l2:list a:{sorted f l2}] Unidentified product: [pivot:a] (Lemma ((requires (/\(/\(total_order #a f, (forall y.{:pattern } ==>(mem y l1, not (f pivot y)))), (forall y.{:pattern } ==>(mem y l2, f pivot y)))))) ((ensures (sorted f (@(l1, ((Prims.Cons pivot l2))))))) (Prims.Cons (SMTPat (sorted f (@(l1, ((Prims.Cons pivot l2)))))) (Prims.Nil )))

Correctness of the merging of two sorted lists around a pivot.

val sortWith_sorted:Unidentified product: [#a:eqtype] Unidentified product: [f:(Unidentified product: [a] Unidentified product: [a] (Tot int))] Unidentified product: [l:list a] (Lemma ((requires (total_order #a (bool_of_compare f)))) ((ensures (/\((sorted (bool_of_compare f) (sortWith f l)), (forall x.{:pattern } =(mem x l, mem x (sortWith f l))))))) (decreases (length l)))

Correctness of [sortWith], part 2/2: the elements of [sortWith f l] are sorted according to comparison function [f], and the elements of [sortWith f l] are the elements of [l].

let ((mem_memP (#a:eqtype) (x:a) (l:list a)):(Lemma ((ensures (<==>(mem x l, memP x l)))))):match l with []  -> () | (Prims.Cons a q)  -> mem_memP x q

Correctness of [mem] for types with decidable equality. TODO: replace [mem] with [memP] in relevant lemmas and define the right SMTPat to automatically recover lemmas about [mem] for types with decidable equality

let ((lemma_index_memP (#t:Type) (l:list t) (i:i:nat:{<(i, length l)})):(Lemma ((ensures (memP index l i l))) (Prims.Cons (SMTPat (memP index l i l)) (Prims.Nil )))):match i with 0  -> () | _  -> lemma_index_memP (tl l) (-(i, 1))

If an element can be [index]ed, then it is a [memP] of the list.

val memP_empty:Unidentified product: [#a:Type] Unidentified product: [x:a] (Lemma ((requires (memP x (Prims.Nil )))) ((ensures False)))

The empty list has no elements.

val memP_existsb:Unidentified product: [#a:Type] Unidentified product: [f:(Unidentified product: [a] (Tot bool))] Unidentified product: [xs:list a] (Lemma ((ensures (<==>(existsb f xs, (exists x:a.{:pattern } (/\(=(f x, true), memP x xs))))))))

Full specification for [existsb]: [existsb f xs] holds if, and only if, there exists an element [x] of [xs] such that [f x] holds.

let ((noRepeats_nil (#a:eqtype)):(Lemma ((ensures (noRepeats #a (Prims.Nil )))))):()

Properties of [noRepeats]

 Properties of [assoc] 
 Properties of [fold_left] 
 Properties of [strict_prefix_of] 
 Properties of << with lists 
 Properties about find 
 Properties of init and last