What to expect of a standard library about lists?

This page collects various data about what to expect of a standard library about lists.

Dictionary of concepts between stdlib, std++, ext-lib, mathcomp, with comparison with ocaml

In progress, started 23/10/24 for stdlib

	List.v	std++	ext-lib	mathcomp
basics
file name	List.v	list.v	List.v	seq.v
all refers to Datatypes.list, but possibly renamed	list	list	list	seq
first constructor	nil	nil	nil	nil/Nil
second constructor	cons	cons	cons	cons/Cons
notation first constructor	[]	[]	[]	[::]
notation second constructor	a::l	a::l	a::l	a::l
notations for finite lists	[a1;...;an]	[a1;...;an]	[a1;...;an]	[::a1;...;an]
naming tradition	ocaml	haskell
basic predicates
belonging as a Prop	In (recursive)	elem_of_list (inductive)
exists on bool	existsb		anyb
forall on bool	forallb		allb
exists, inductive in Prop	Exists
forall, inductive in Prop	Forall
lifting of a relation, inductive in Prop	Forall2	list_equiv
being extended with one element, in Prop, inductive in Prop	Add
having no duplicates, in Prop, inductive in Prop	NoDup (dep on In)	NoDup (dep on elem_of_list)
being lexicographically compared, with accumulator, inductive	ListCompareSpec
forall of a relation on pairs, in Prop	ForallPairs
forall of a relation on ordered pairs, inductive in Prop	ForallOrdPairs
of smaller length, in Prop	lel
inclusion, in Prop	Incl
to be prefix, in Prop		prefix
to be suffix, in Prop		suffix
basic combinators
functoriality	map	list_fmap
functoriality with concatenation	flat_map
functoriality through traversable	--		mapT_list
functoriality with filtering	--	list_omap	mapT_list
functoriality with position	--	imap
functoriality with boolean mask	--	mask
bifunctoriality with position	--	imap2
monadic functoriality	--	mapM
iteration	fold_right	foldr
iteration (tail-recursive)	fold_left	foldl
lifting of boolean equality	(Scheme)		list_eqb
lifting of decidable equality	list_eq_dec
injection from option		option_list
partial projection to option		maybe_list_singleton
basic functions
length	length (in Init)
append	append (in Init)
head (with a default value)	hd
head (with optional result)	hd_error
tail (returning [] on [])	tl	tail
nth (with a default value)	nth/nth_default
nth (with optional result)	nth_error	list_lookup
applying function to element at position	--	list_alter
applying function to sublist of some length at position	--	sublist_alter
replacing element at position	--	list_insert
last (with a default value)	last
last (with optional result)	--	last
remove last (returning [] on [])	removelast
remove at position	--	list_delete
reversal	rev
reversal, tail-recursive, with accumulator	rev_append
reversal, tail-recursive	rev'	reverse
monadic bind		list_bind
concatenation	concat	list_join
power set	list_power
permutations		permutations
splitting lists of pairs into pairs of lists	split
combining pairs of lists into lists of pairs (dropping mismatches)	combine
product of lists	List_prod
taking nth first elements	firstn	take	firstn	take
dropping nth first elements	skipn	drop
taking sublist of some length from some position (in option)		sublist_lookup
constant list of a given length	repeat	replicate
overriding a sublist	--	list_inserts
resizing, padding with a default if necessary	--	resize
partition according to a list of length	--	reshape
sum of a list of natural numbers	list_sum
max of a list of natural numbers	list_max
interval [n;...;n+p]	seq
rotate left-to-right by a number		rotate
predicates assuming a boolean equality
belonging as a boolean				mem_seq
functions referring to a boolean predicate
filtering over a boolean predicate	filter	list_filter
finding first satisfying a boolean predicate with optional result	find
partition according to a predicate	partition
functions assuming decidability of equality
remove an element	remove/remove'
count number of occurrences	count_occ/count_occ'
remove duplicates	nodup
decidable exists	Exists_dec/Forall_Exists_dec
decidable forall	Forall_dec
decidable belonging	in_dec
functions assuming a ternary comparison function
ternary lexicographic comparison	list_compare
misc
		rotate_take
		zipped_map

Notes:

• stdlib has nth_ok n l a : bool which says that n <= length l. Is that worth?
• stdlib has two definitions of nth with a default, one going through nth with optional result; are they both as useful?
• to be continued for std++, extlib, mathcomp
• mathcomp encapsulates boolean equality as an "eqType"
• std++ encapsulates decidable equality as an "EqDecision"

A comparison of statements involving firstn available in stdlib, std++, ext-lib, mathcomp

As of 29/08/24 (taken here)

statement	List.v	std++	ext-lib	mathcomp
(name of the function)	firstn	take	firstn	take
firstn n [] = []	firstn_nil	take_nil		take0
firstn 0 l = []	firstn_0
n = 0 -> firstn n l = []			firstn_0
firstn (S n) (a::l) = a :: (firstn n l)	firstn_cons
0 < n -> firstn n (a :: b) = a :: firstn (n - 1) b			firstn_cons
firstn n0 (x :: s) = if n0 is S n then x :: firstn n s else []				take_cons
firstn i l ++ lastn i l = l	firstn_lastn	take_drop		cat_take_drop
nth_error n = Some x -> firstn (S n) l = firstn n l ++ [x]		take_S_r
nth_error (firstn n l) i = if i <? n then nth_error l i else None	nth_error_firstn
nth i (firstn n l) d = if i <? n then nth i l d else d	nth_firstn
i < n -> nth_error i (firstn n l) = nth_error i l		lookup_take		nth_take
n < length l -> firstn (S n) s = firstn n l :: nth_error l n				take_nth
firstn (length l) l = l	firstn_all			take_size
length l <= n -> firstn n l = l	firstn_all2	take_ge	firstn_all	take_oversize
length (firstn n l) = min n (length l)		take_length		size_take_min
length (firstn n s) = if n <? length s then n else length s				size_take
length (firstn n l) <= n	length_firstn_le	take_length_le
length l <= n -> length (firstn n l) = length l		take_length_ge
n <= length l -> length (firstn n l) = n	length_firstn_eq			size_takel
firstn i (firstn j l) = firstn (min i j) l	firstn_firstn	take_take
firstn (min i j) l = firstn i (firstn j l)				take_min
firstn n (firstn n l) = firstn n l		take_idemp
i <= j -> firstn i (firstn j l) = firstn i l				take_takel
j <= i -> firstn i (firstn j l) = firstn j l				take_taker
firstn i (firstn j s) = firstn j (firstn i s)				takeC
firstn (length l) (l ++ k) = l		take_app
n = length l -> firstn n (l ++ k) = l		take_app_alt
n <= length l -> firstn n (l ++ k) = firstn n l		take_app_le	firstn_app_L	takel_cat
n = length l1 -> firstn n ((l1 ++ l2) ++ l3) = l1		take_app3_alt
firstn n (l1 ++ l2) = (firstn n l1) ++ (firstn (n - length l1) l2)	firstn_app
firstn n (s1 ++ s2) = if n < length s1 then firstn n s1 else s1 ++ firstn (n - length s1) s2				take_size_cat
length a <= n -> firstn n (a ++ b) = a ++ firstn (n - length a) b			firstn_app_R
firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2	firstn_app_2
i <= j -> firstn i (repeat x j) = repeat x i				take_nseq