Pure total operations on lists
This module defines all pure and total operations on lists that can be used in specifications.
Base operationsval isEmpty:Unidentified product: [list 'a] (Tot bool)[isEmpty l] returns [true] if and only if [l] is empty
val hd:Unidentified product: [l:l:list 'a:{Cons? l}] (Tot 'a)[hd l] returns the first element of [l]. Requires [l] to be nonempty, at type-checking time. Named as in: OCaml, F#, Coq
val tail:Unidentified product: [l:l:list 'a:{Cons? l}] (Tot (list 'a))[tail l] returns [l] without its first element. Requires, at type-checking time, that [l] be nonempty. Similar to: tl in OCaml, F#, Coq
val tl:Unidentified product: [l:l:list 'a:{Cons? l}] (Tot (list 'a))[tl l] returns [l] without its first element. Requires, at type-checking time, that [l] be nonempty. Named as in: OCaml, F#, Coq
val last:Unidentified product: [l:l:list 'a:{Cons? l}] (Tot 'a)[last l] returns the last element of [l]. Requires, at type-checking time, that [l] be nonempty. Named as in: Haskell
val init:Unidentified product: [l:l:list 'a:{Cons? l}] (Tot (list 'a))[init l] returns [l] without its last element. Requires, at type-checking time, that [l] be nonempty. Named as in: Haskell
val length:Unidentified product: [list 'a] (Tot nat)[length l] returns the total number of elements in [l]. Named as in: OCaml, F#, Coq
val nth:Unidentified product: [list 'a] Unidentified product: [nat] (Tot (option 'a))[nth l n] returns the [n]-th element in list [l] (with the first element being the 0-th) if [l] is long enough, or [None] otherwise. Named as in: OCaml, F#, Coq
val index:Unidentified product: [#a:Type] Unidentified product: [l:list a] Unidentified product: [i:i:nat:{<(i, length l)}] (Tot a)[index l n] returns the [n]-th element in list [l] (with the first element being the 0-th). Requires, at type-checking time, that [l] be of length at least [n+1].
val count:Unidentified product: [#a:eqtype] Unidentified product: [a] Unidentified product: [list a] (Tot nat)[count x l] returns the number of occurrences of [x] in [l]. Requires, at type-checking time, the type of [a] to have equality defined. Similar to: [List.count_occ] in Coq.
val rev_acc:Unidentified product: [list 'a] Unidentified product: [list 'a] (Tot (list 'a))[rev_acc l1 l2] appends the elements of [l1] to the beginning of [l2], in reverse order. It is equivalent to [append (rev l1) l2], but is tail-recursive. Similar to: [List.rev_append] in OCaml, Coq.
val rev:Unidentified product: [list 'a] (Tot (list 'a))[rev l] returns the list [l] in reverse order. Named as in: OCaml, F#, Coq.
val append:Unidentified product: [list 'a] Unidentified product: [list 'a] (Tot (list 'a))[append l1 l2] appends the elements of [l2] to the end of [l1]. Named as: OCaml, F#. Similar to: [List.app] in Coq.
let (op_At x y):append x yDefines notation [@] for [append], as in OCaml, F# .
val snoc:Unidentified product: [(*(list 'a, 'a))] (Tot (list 'a))[snoc (l, x)] adds [x] to the end of the list [l].
Note: We use an uncurried [snoc (l, x)] instead of the curried
[snoc l x]. This is intentional. If [snoc] takes a pair instead
of 2 arguments, it allows for a better pattern on
[lemma_unsnoc_snoc], which connects [snoc] and [unsnoc]. In
particular, if we had two arguments, then either the pattern would
either be too restrictive or would lead to over-triggering. More
context for this can be seen in the (collapsed and uncollapsed)
comments at https://github.com/FStarLang/FStar/pull/1560 val flatten:Unidentified product: [list (list 'a)] (Tot (list 'a))[flatten l], where [l] is a list of lists, returns the list of the elements of the lists in [l], preserving their order. Named as in: OCaml, Coq.
val map:Unidentified product: [(Unidentified product: ['a] (Tot 'b))] Unidentified product: [list 'a] (Tot (list 'b))[map f l] applies [f] to each element of [l] and returns the list of results, in the order of the original elements in [l]. Requires, at type-checking time, [f] to be a pure total function. Named as in: OCaml, Coq, F#
val mapi_init:Unidentified product: [(Unidentified product: [int] Unidentified product: ['a] (Tot 'b))] Unidentified product: [list 'a] Unidentified product: [int] (Tot (list 'b))[mapi_init f n l] applies, for each [k], [f (n+k)] to the [k]-th element of [l] and returns the list of results, in the order of the original elements in [l]. Requires, at type-checking time, [f] to be a pure total function.
val mapi:Unidentified product: [(Unidentified product: [int] Unidentified product: ['a] (Tot 'b))] Unidentified product: [list 'a] (Tot (list 'b))[mapi f l] applies, for each [k], [f k] to the [k]-th element of [l] and returns the list of results, in the order of the original elements in [l]. Requires, at type-checking time, [f] to be a pure total function. Named as in: OCaml
val concatMap:Unidentified product: [(Unidentified product: ['a] (Tot (list 'b)))] Unidentified product: [list 'a] (Tot (list 'b))[concatMap f l] applies [f] to each element of [l] and returns the concatenation of the results, in the order of the original elements of [l]. This is equivalent to [flatten (map f l)]. Requires, at type-checking time, [f] to be a pure total function.
val fold_left:Unidentified product: [(Unidentified product: ['a] Unidentified product: ['b] (Tot 'a))] Unidentified product: ['a] Unidentified product: [l:list 'b] (Tot 'a (decreases l))[fold_left f x [y1; y2; ...; yn]] computes (f (... (f x y1) y2) ... yn). Requires, at type-checking time, [f] to be a pure total function. Named as in: OCaml, Coq.
val fold_right:Unidentified product: [(Unidentified product: ['a] Unidentified product: ['b] (Tot 'b))] Unidentified product: [list 'a] Unidentified product: ['b] (Tot 'b)[fold_right f [x1; x2; ...; xn] y] computes (f x1 (f x2 (... (f xn y)) ... )). Requires, at type-checking time, [f] to be a pure total function. Named as in: OCaml, Coq
let ((fold_right_gtot (#a:Type) (#b:Type) (l:list a) (f:Unidentified product: [a] Unidentified product: [b] (GTot b)) (x:b)):(GTot b)):match l with [] -> x | (Prims.Cons hd tl) -> f hd (fold_right_gtot tl f x)[fold_right_gtot] is just like [fold_right], except f is a ghost function *
val fold_left2:Unidentified product: [f:(Unidentified product: ['a] Unidentified product: ['b] Unidentified product: ['c] (Tot 'a))] Unidentified product: [accu:'a] Unidentified product: [l1:(list 'b)] Unidentified product: [l2:(list 'c)] (Pure 'a ((requires (==(length l1, length l2)))) ((ensures ((fun _ -> True)))) (decreases l1))[fold_left2 f x [y1; y2; ...; yn] [z1; z2; ...; zn]] computes (f (... (f x y1 z1) y2 z2) ... yn zn). Requires, at type-checking time, [f] to be a pure total function, and the lists [y1; y2; ...; yn] and [z1; z2; ...; zn] to have the same lengths. Named as in: OCaml
List searching *val mem:Unidentified product: [#a:eqtype] Unidentified product: [a] Unidentified product: [list a] (Tot bool)[mem x l] returns [true] if, and only if, [x] appears as an element of [l]. Requires, at type-checking time, the type of elements of [l] to have decidable equality. Named as in: OCaml. See also: List.In in Coq, which is propositional.
Propositional membership (as in Coq). Does not require decidable
equality. let ((memP (#a:Type) (x:a) (l:list a)):(Tot Type0)):match l with [] -> False | (Prims.Cons y q) -> \/(==(x, y), memP x q)[memP x l] holds if, and only if, [x] appears as an element of [l]. Similar to: List.In in Coq.
let contains:mem[contains x l] returns [true] if, and only if, [x] appears as an element of [l]. Requires, at type-checking time, the type of elements of [l] to have decidable equality. It is equivalent to: [mem x l]. TODO: should we rather swap the order of arguments?
val existsb:Unidentified product: [#a:Type] Unidentified product: [f:(Unidentified product: [a] (Tot bool))] Unidentified product: [list a] (Tot bool)[existsb f l] returns [true] if, and only if, there exists some element [x] in [l] such that [f x] holds.
val find:Unidentified product: [#a:Type] Unidentified product: [f:(Unidentified product: [a] (Tot bool))] Unidentified product: [list a] (Tot (option (x:a:{f x})))[find f l] returns [Some x] for some element [x] appearing in [l] such that [f x] holds, or [None] only if no such [x] exists.
Filtering elements of a list [l] through a Boolean pure total
predicate [f] let ((mem_filter_spec (#a:Type) (f:(Unidentified product: [a] (Tot bool))) (m:list a) (u:option (x:unit:{hasEq a}))):(Tot Type0)):match u with None -> True | (Some z) -> forall x.{:pattern } ==>(mem x m, f x)We would like to have a postcondition for [filter f l] saying that, for any element [x] of [filter f l], [f x] holds. To this end, we need to use [mem] as defined above, which would require the underlying type [a] of list elements to have decidable equality. However, we would still like to define [filter] on all element types, even those that do not have decidable equality. Thus, we define our postcondition as [mem_filter_spec f m u] below, where [m] is the intended [filter f l] and [u] indicates whether [a] has decidable equality ([None] if not). Requires, at type-checking time, [f] to be a pure total function.
val filter:Unidentified product: [#a:Type] Unidentified product: [f:(Unidentified product: [a] (Tot bool))] Unidentified product: [l:list a] (Tot (m:list a:{forall u.{:pattern } mem_filter_spec f m u}))[filter f l] returns [l] with all elements [x] such that [f x] does not hold removed. Requires, at type-checking time, [f] to be a pure total function. Named as in: OCaml, Coq
val mem_filter:#a:eqtype -> f:(Unidentified product: [a] (Tot bool)) -> l:list a -> x:a -> (Lemma ((requires (mem #a x (filter f l)))) ((ensures (f x))))Postcondition on [filter f l] for types with decidable equality: for any element [x] of [filter f l], [f x] holds. Requires, at type-checking time, [f] to be a pure total function.
val mem_filter_forall:#a:eqtype -> f:(Unidentified product: [a] (Tot bool)) -> l:list a -> (Lemma ((requires True)) ((ensures (forall x.{:pattern } ==>(mem #a x (filter f l), f x)))) (Prims.Cons (SMTPat (filter f l)) (Prims.Nil )))Postcondition on [filter f l] for types with decidable equality, stated with [forall]: for any element [x] of [filter f l], [f x] holds. Requires, at type-checking time, [f] to be a pure total function.
val for_all:Unidentified product: [(Unidentified product: ['a] (Tot bool))] Unidentified product: [list 'a] (Tot bool)[for_all f l] returns [true] if, and only if, for all elements [x] appearing in [l], [f x] holds. Requires, at type-checking time, [f] to be a pure total function. Named as in: OCaml. Similar to: List.forallb in Coq
let ((for_all_mem (#a:eqtype) (f:(Unidentified product: [a] (Tot bool))) (l:list a)):(Lemma (<==>(for_all f l, (forall x.{:pattern } ==>(mem x l, f x)))))):match l with [] -> () | (Prims.Cons _ q) -> for_all_mem f qSpecification for [for_all f l] vs. mem
val collect:Unidentified product: [(Unidentified product: ['a] (Tot (list 'b)))] Unidentified product: [list 'a] (Tot (list 'b))[collect f l] applies [f] to each element of [l] and returns the concatenation of the results, in the order of the original elements of [l]. It is equivalent to [flatten (map f l)]. Requires, at type-checking time, [f] to be a pure total function. TODO: what is the difference with [concatMap]?
val tryFind:Unidentified product: [(Unidentified product: ['a] (Tot bool))] Unidentified product: [list 'a] (Tot (option 'a))[tryFind f l] returns [Some x] for some element [x] appearing in [l] such that [f x] holds, or [None] only if no such [x] exists. Requires, at type-checking time, [f] to be a pure total function. Contrary to [find], [tryFind] provides no postcondition on its result.
val tryPick:Unidentified product: [(Unidentified product: ['a] (Tot (option 'b)))] Unidentified product: [list 'a] (Tot (option 'b))[tryPick f l] returns [y] for some element [x] appearing in [l] such that [f x = Some y] for some y, or [None] only if [f x = None] for all elements [x] of [l]. Requires, at type-checking time, [f] to be a pure total function.
val choose:Unidentified product: [(Unidentified product: ['a] (Tot (option 'b)))] Unidentified product: [list 'a] (Tot (list 'b))[choose f l] returns the list of [y] for all elements [x] appearing in [l] such that [f x = Some y] for some [y]. Requires, at type-checking time, [f] to be a pure total function.
val partition:Unidentified product: [f:(Unidentified product: ['a] (Tot bool))] Unidentified product: [list 'a] (Tot (*(list 'a, list 'a)))[partition f l] returns the pair of lists [(l1, l2)] where all elements [x] of [l] are in [l1] if [f x] holds, and in [l2] otherwise. Both [l1] and [l2] retain the original order of [l]. Requires, at type-checking time, [f] to be a pure total function.
val subset:Unidentified product: [#a:eqtype] Unidentified product: [list a] Unidentified product: [list a] (Tot bool)[subset la lb] is true if and only if all the elements from [la] are also in [lb]. Requires, at type-checking time, the type of elements of [la] and [lb] to have decidable equality.
val noRepeats:Unidentified product: [#a:eqtype] Unidentified product: [list a] (Tot bool)[noRepeats l] returns [true] if, and only if, no element of [l] appears in [l] more than once. Requires, at type-checking time, the type of elements of [la] and [lb] to have decidable equality.
val no_repeats_p:Unidentified product: [#a:Type] Unidentified product: [list a] (Tot prop)[no_repeats_p l] valid if, and only if, no element of [l] appears in [l] more than once.
List of tuples *val assoc:Unidentified product: [#a:eqtype] Unidentified product: [#b:Type] Unidentified product: [a] Unidentified product: [list (*(a, b))] (Tot (option b))[assoc x l] returns [Some y] where [(x, y)] is the first element of [l] whose first element is [x], or [None] only if no such element exists. Requires, at type-checking time, the type of [x] to have decidable equality. Named as in: OCaml.
val split:Unidentified product: [list (*('a, 'b))] (Tot (*(list 'a, list 'b)))[split] takes a list of pairs [(x1, y1), ..., (xn, yn)] and returns the pair of lists ([x1, ..., xn], [y1, ..., yn]). Named as in: OCaml
let unzip:split[unzip] takes a list of pairs [(x1, y1), ..., (xn, yn)] and returns the pair of lists ([x1, ..., xn], [y1, ..., yn]). Named as in: Haskell
val unzip3:Unidentified product: [list (*(*('a, 'b), 'c))] (Tot (*(*(list 'a, list 'b), list 'c)))[unzip3] takes a list of triples [(x1, y1, z1), ..., (xn, yn, zn)] and returns the triple of lists ([x1, ..., xn], [y1, ..., yn], [z1, ..., zn]). Named as in: Haskell
Splitting a list at some index *let ((splitAt (#a:Type) (n:nat) (l:list a)):*(list a, list a)):if =(n, 0) then (FStar.Pervasives.Native.Mktuple2 (Prims.Nil ) l) else match l with [] -> (FStar.Pervasives.Native.Mktuple2 (Prims.Nil ) l) | (Prims.Cons x xs) -> let (l1, l2) = splitAt (-(n, 1)) xs in (FStar.Pervasives.Native.Mktuple2 (Prims.Cons x l1) l2)[splitAt] takes a natural number n and a list and returns a pair of the maximal prefix of l of size smaller than n and the rest of the list
val unsnoc:Unidentified product: [#a:Type] Unidentified product: [l:l:list a:{>(length l, 0)}] (Tot (*(list a, a)))[unsnoc] is an inverse of [snoc]. It splits a list into all-elements-except-last and last element.
val split3:Unidentified product: [#a:Type] Unidentified product: [l:list a] Unidentified product: [i:i:nat:{<(i, length l)}] (Tot (*(*(list a, a), list a)))[split3] splits a list into 3 parts. This allows easy access to the part of the list before and after the element, as well as the element itself.
Sorting (implemented as quicksort) *val partition_length:Unidentified product: [f:(Unidentified product: ['a] (Tot bool))] Unidentified product: [l:list 'a] (Lemma ((requires True)) ((ensures (=(+(length (fst (partition f l)), length (snd (partition f l))), length l)))))[partition] splits a list [l] into two lists, the sum of whose lengths is the length of [l].
val bool_of_compare:Unidentified product: [#a:Type] Unidentified product: [(Unidentified product: [a] Unidentified product: [a] (Tot int))] Unidentified product: [a] Unidentified product: [a] (Tot bool)[bool_of_compare] turns a comparison function into a strict order. More precisely, [bool_of_compare compare x y] returns true if, and only if, [compare x y] is positive. Inspired from OCaml, where polymorphic comparison using both the [compare] function and the (>) infix operator are such that [compare x y] is positive if, and only if, x > y. Requires, at type-checking time, [compare] to be a pure total function.
val compare_of_bool:Unidentified product: [#a:eqtype] Unidentified product: [(Unidentified product: [a] Unidentified product: [a] (Tot bool))] Unidentified product: [a] Unidentified product: [a] (Tot int)[compare_of_bool] turns a strict order into a comparison function. More precisely, [compare_of_bool rel x y] returns a positive number if, and only if, x rel y holds. Inspired from OCaml, where polymorphic comparison using both the [compare] function and the (>) infix operator are such that [compare x y] is positive if, and only if, x > y. Requires, at type-checking time, [rel] to be a pure total function.
val sortWith:Unidentified product: [(Unidentified product: ['a] Unidentified product: ['a] (Tot int))] Unidentified product: [l:list 'a] (Tot (list 'a) (decreases (length l)))[sortWith compare l] returns the list [l'] containing the elements of [l] sorted along the comparison function [compare], in such a way that if [compare x y > 0], then [x] appears before [y] in [l']. Requires, at type-checking time, [compare] to be a pure total function.
A l1 is a strict prefix of l2.