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' l2The [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 qCorrectness 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