Library Coq.Lists.List
Basics: definition of polymorphic lists and some operations
The definition of
list is now in
Init/Datatypes,
as well as the definitions of
length and
app
Open Scope list_scope.
Standard notations for lists.
In a special module to avoid conflicts.
Head and tail
The In predicate
Generic facts
Discrimination
Destruction
Facts about In
Characterization of
In
Inversion
Decidability of In
Facts about app
Discrimination
Concat with nil
app is associative
app commutes with cons
Facts deduced from the result of a concatenation
Compatibility with other operations
Operations on the elements of a list
Section Elts.
Variable A :
Type.
Fixpoint nth (
n:
nat) (
l:
list A) (
default:
A) {
struct l} :
A :=
match n,
l with
|
O,
x :: l' =>
x
|
O,
other =>
default
|
S m,
[] =>
default
|
S m,
x :: t =>
nth m t default
end.
Fixpoint nth_ok (
n:
nat) (
l:
list A) (
default:
A) {
struct l} :
bool :=
match n,
l with
|
O,
x :: l' =>
true
|
O,
other =>
false
|
S m,
[] =>
false
|
S m,
x :: t =>
nth_ok m t default
end.
Lemma nth_in_or_default :
forall (
n:
nat) (
l:
list A) (
d:
A),
{In (
nth n l d)
l} + {nth n l d = d}.
Lemma nth_S_cons :
forall (
n:
nat) (
l:
list A) (
d a:
A),
In (
nth n l d)
l -> In (
nth (
S n) (
a :: l)
d) (
a :: l).
Fixpoint nth_error (
l:
list A) (
n:
nat) {
struct n} :
option A :=
match n,
l with
|
O,
x :: _ =>
Some x
|
S n,
_ :: l =>
nth_error l n
|
_,
_ =>
None
end.
Definition nth_default (
default:
A) (
l:
list A) (
n:
nat) :
A :=
match nth_error l n with
|
Some x =>
x
|
None =>
default
end.
Lemma nth_default_eq :
forall n l (
d:
A),
nth_default d l n = nth n l d.
Results about nth
Results about nth_error
Results directly relating nth and nth_error
Last element of a list
last l d returns the last element of the list
l,
or the default value
d if
l is empty.
removelast l remove the last element of l
Counting occurrences of an element
Compatibility of count_occ with operations on list
Compatibility with other operations
An alternative tail-recursive definition for reverse
Reverse Induction Principle on Lists
Decidable equality on lists
Applying functions to the elements of a list
Map
map and count of occurrences
flat_map
Definition flat_map (
f:
A -> list B) :=
fix flat_map (
l:
list A) :
list B :=
match l with
|
nil =>
nil
|
cons x t =>
(f x)++(flat_map t)
end.
Lemma in_flat_map :
forall (
f:
A->list B)(
l:
list A)(
y:
B),
In y (
flat_map f l)
<-> exists x, In x l /\ In y (
f x).
End Map.
Lemma flat_map_concat_map :
forall A B (
f :
A -> list B)
l,
flat_map f l = concat (
map f l).
Lemma concat_map :
forall A B (
f :
A -> B)
l,
map f (
concat l)
= concat (
map (
map f)
l).
Lemma map_id :
forall (
A :
Type) (
l :
list A),
map (
fun x =>
x)
l = l.
Lemma map_map :
forall (
A B C:
Type)(
f:
A->B)(
g:
B->C)
l,
map g (
map f l)
= map (
fun x =>
g (
f x))
l.
Lemma map_ext_in :
forall (
A B :
Type)(
f g:
A->B)
l,
(forall a,
In a l -> f a = g a) -> map f l = map g l.
Lemma ext_in_map :
forall (
A B :
Type)(
f g:
A->B)
l,
map f l = map g l -> forall a,
In a l -> f a = g a.
Lemma map_ext_in_iff :
forall (
A B :
Type)(
f g:
A->B)
l,
map f l = map g l <-> forall a,
In a l -> f a = g a.
Lemma map_ext :
forall (
A B :
Type)(
f g:
A->B),
(forall a,
f a = g a) -> forall l,
map f l = map g l.
Left-to-right iterator on lists
Right-to-left iterator on lists
(list_power x y) is y^x, or the set of sequences of elts of y
indexed by elts of x, sorted in lexicographic order.
Boolean operations over lists
find whether a boolean function can be satisfied by an
elements of the list.
find whether a boolean function is satisfied by
all the elements of a list.
filter
find
partition
Fixpoint partition (
l:
list A) :
list A * list A :=
match l with
|
nil =>
(nil, nil)
|
x :: tl =>
let (
g,
d) :=
partition tl in
if f x then (x::g,d) else (g,x::d)
end.
Theorem partition_cons1 a l l1 l2:
partition l = (l1, l2) ->
f a = true ->
partition (
a::l)
= (a::l1, l2).
Theorem partition_cons2 a l l1 l2:
partition l = (l1, l2) ->
f a=false ->
partition (
a::l)
= (l1, a::l2).
Theorem partition_length l l1 l2:
partition l = (l1, l2) ->
length l = length l1 + length l2.
Theorem partition_inv_nil (
l :
list A):
partition l = ([], []) <-> l = [].
Theorem elements_in_partition l l1 l2:
partition l = (l1, l2) ->
forall x:
A,
In x l <-> In x l1 \/ In x l2.
End Bool.
Section Filtering.
Variables (
A :
Type).
Lemma filter_map :
forall (
f g :
A -> bool) (
l :
list A),
filter f l = filter g l <-> map f l = map g l.
Lemma filter_ext_in :
forall (
f g :
A -> bool) (
l :
list A),
(forall a,
In a l -> f a = g a) -> filter f l = filter g l.
Lemma ext_in_filter :
forall (
f g :
A -> bool) (
l :
list A),
filter f l = filter g l -> (forall a,
In a l -> f a = g a).
Lemma filter_ext_in_iff :
forall (
f g :
A -> bool) (
l :
list A),
filter f l = filter g l <-> (forall a,
In a l -> f a = g a).
Lemma filter_ext :
forall (
f g :
A -> bool),
(forall a,
f a = g a) -> forall l,
filter f l = filter g l.
End Filtering.
Operations on lists of pairs or lists of lists
split derives two lists from a list of pairs
Fixpoint split (
l:
list (
A*B)) :
list A * list B :=
match l with
|
[] =>
([], [])
|
(x,y) :: tl =>
let (
left,
right) :=
split tl in (x::left, y::right)
end.
Lemma in_split_l :
forall (
l:
list (
A*B))(
p:
A*B),
In p l -> In (
fst p) (
fst (
split l)).
Lemma in_split_r :
forall (
l:
list (
A*B))(
p:
A*B),
In p l -> In (
snd p) (
snd (
split l)).
Lemma split_nth :
forall (
l:
list (
A*B))(
n:
nat)(
d:
A*B),
nth n l d = (nth n (
fst (
split l)) (
fst d)
, nth n (
snd (
split l)) (
snd d)
).
Lemma split_length_l :
forall (
l:
list (
A*B)),
length (
fst (
split l))
= length l.
Lemma split_length_r :
forall (
l:
list (
A*B)),
length (
snd (
split l))
= length l.
combine is the opposite of split.
Lists given to combine are meant to be of same length.
If not, combine stops on the shorter list
Fixpoint combine (
l :
list A) (
l' :
list B) :
list (
A*B) :=
match l,
l' with
|
x::tl,
y::tl' =>
(x,y)::(combine tl tl')
|
_,
_ =>
nil
end.
Lemma split_combine :
forall (
l:
list (
A*B)),
let (
l1,
l2) :=
split l in combine l1 l2 = l.
Lemma combine_split :
forall (
l:
list A)(
l':
list B),
length l = length l' ->
split (
combine l l')
= (l,l').
Lemma in_combine_l :
forall (
l:
list A)(
l':
list B)(
x:
A)(
y:
B),
In (x,y) (
combine l l')
-> In x l.
Lemma in_combine_r :
forall (
l:
list A)(
l':
list B)(
x:
A)(
y:
B),
In (x,y) (
combine l l')
-> In y l'.
Lemma combine_length :
forall (
l:
list A)(
l':
list B),
length (
combine l l')
= min (
length l) (
length l').
Lemma combine_nth :
forall (
l:
list A)(
l':
list B)(
n:
nat)(
x:
A)(
y:
B),
length l = length l' ->
nth n (
combine l l')
(x,y) = (nth n l x, nth n l' y).
list_prod has the same signature as combine, but unlike
combine, it adds every possible pairs, not only those at the
same position.
Miscellaneous operations on lists
Length order of lists
Cutting a list at some position
Section Cutting.
Variable A :
Type.
Fixpoint firstn (
n:
nat)(
l:
list A) :
list A :=
match n with
| 0 =>
nil
|
S n =>
match l with
|
nil =>
nil
|
a::l =>
a::(firstn n l)
end
end.
Lemma firstn_nil n:
firstn n [] = [].
Lemma firstn_cons n a l:
firstn (
S n) (
a::l)
= a :: (firstn n l).
Lemma firstn_all l:
firstn (
length l)
l = l.
Lemma firstn_all2 n:
forall (
l:
list A),
(length l) <= n -> firstn n l = l.
Lemma firstn_O l:
firstn 0
l = [].
Lemma firstn_le_length n:
forall l:
list A,
length (
firstn n l)
<= n.
Lemma firstn_length_le:
forall l:
list A,
forall n:
nat,
n <= length l -> length (
firstn n l)
= n.
Lemma firstn_app n:
forall l1 l2,
firstn n (
l1 ++ l2)
= (firstn n l1) ++ (firstn (
n - length l1)
l2).
Lemma firstn_app_2 n:
forall l1 l2,
firstn (
(length l1) + n) (
l1 ++ l2)
= l1 ++ firstn n l2.
Lemma firstn_firstn:
forall l:
list A,
forall i j :
nat,
firstn i (
firstn j l)
= firstn (
min i j)
l.
Fixpoint skipn (
n:
nat)(
l:
list A) :
list A :=
match n with
| 0 =>
l
|
S n =>
match l with
|
nil =>
nil
|
a::l =>
skipn n l
end
end.
Lemma firstn_skipn_comm :
forall m n l,
firstn m (
skipn n l)
= skipn n (
firstn (
n + m)
l).
Lemma skipn_firstn_comm :
forall m n l,
skipn m (
firstn n l)
= firstn (
n - m) (
skipn m l).
Lemma skipn_O :
forall l,
skipn 0
l = l.
Lemma skipn_nil :
forall n,
skipn n (
[] :
list A)
= [].
Lemma skipn_cons n a l:
skipn (
S n) (
a::l)
= skipn n l.
Lemma skipn_none :
forall l,
skipn (
length l)
l = [].
Lemma skipn_all2 n:
forall l,
length l <= n -> skipn n l = [].
Lemma firstn_skipn :
forall n l,
firstn n l ++ skipn n l = l.
Lemma firstn_length :
forall n l,
length (
firstn n l)
= min n (
length l).
Lemma skipn_length n :
forall l,
length (
skipn n l)
= length l - n.
Lemma skipn_all l:
skipn (
length l)
l = nil.
Lemma skipn_app n :
forall l1 l2,
skipn n (
l1 ++ l2)
= (skipn n l1) ++ (skipn (
n - length l1)
l2).
Lemma firstn_skipn_rev:
forall x l,
firstn x l = rev (
skipn (
length l - x) (
rev l)).
Lemma firstn_rev:
forall x l,
firstn x (
rev l)
= rev (
skipn (
length l - x)
l).
Lemma skipn_rev:
forall x l,
skipn x (
rev l)
= rev (
firstn (
length l - x)
l).
Lemma removelast_firstn :
forall n l,
n < length l ->
removelast (
firstn (
S n)
l)
= firstn n l.
Lemma firstn_removelast :
forall n l,
n < length l ->
firstn n (
removelast l)
= firstn n l.
End Cutting.
Combining pairs of lists of possibly-different lengths
Predicate for List addition/removal (no need for decidability)
Effective computation of a list without duplicates
Alternative characterisations of being without duplicates,
thanks to nth_error and nth
Having NoDup hypotheses bring more precise facts about incl.
NoDup and map
NB: the reciprocal result holds only for injective functions,
see FinFun.v
Sequence of natural numbers
seq computes the sequence of len contiguous integers
that starts at start. For instance, seq 2 3 is 2::3::4::nil.
Existential and universal predicates over lists
Variable A:
Type.
Section One_predicate.
Variable P:
A->Prop.
Inductive Exists :
list A -> Prop :=
|
Exists_cons_hd :
forall x l,
P x -> Exists (
x::l)
|
Exists_cons_tl :
forall x l,
Exists l -> Exists (
x::l).
Hint Constructors Exists :
core.
Lemma Exists_exists (
l:
list A) :
Exists l <-> (exists x, In x l /\ P x).
Lemma Exists_nil :
Exists nil <-> False.
Lemma Exists_cons x l:
Exists (
x::l)
<-> P x \/ Exists l.
Lemma Exists_dec l:
(forall x:
A,
{P x} + { ~ P x }) ->
{Exists l} + {~ Exists l}.
Inductive Forall :
list A -> Prop :=
|
Forall_nil :
Forall nil
|
Forall_cons :
forall x l,
P x -> Forall l -> Forall (
x::l).
Hint Constructors Forall :
core.
Lemma Forall_forall (
l:
list A):
Forall l <-> (forall x,
In x l -> P x).
Lemma Forall_inv :
forall (
a:
A)
l,
Forall (
a :: l)
-> P a.
Lemma Forall_rect :
forall (
Q :
list A -> Type),
Q [] -> (forall b l,
P b -> Q (
b :: l)
) -> forall l,
Forall l -> Q l.
Lemma Forall_dec :
(forall x:
A,
{P x} + { ~ P x }) ->
forall l:
list A,
{Forall l} + {~ Forall l}.
End One_predicate.
Theorem Forall_inv_tail
:
forall (
P :
A -> Prop) (
x0 :
A) (
xs :
list A),
Forall P (
x0 :: xs)
-> Forall P xs.
Theorem Exists_impl
:
forall (
P Q :
A -> Prop),
(forall x :
A,
P x -> Q x) -> forall xs :
list A,
Exists P xs -> Exists Q xs.
Lemma Forall_Exists_neg (
P:
A->Prop)(
l:
list A) :
Forall (
fun x =>
~ P x)
l <-> ~(Exists P l).
Lemma Exists_Forall_neg (
P:
A->Prop)(
l:
list A) :
(forall x,
P x \/ ~P x) ->
Exists (
fun x =>
~ P x)
l <-> ~(Forall P l).
Lemma neg_Forall_Exists_neg (
P:
A->Prop) (
l:
list A) :
(forall x:
A,
{P x} + { ~ P x }) ->
~ Forall P l ->
Exists (
fun x =>
~ P x)
l.
Lemma Forall_Exists_dec (
P:
A->Prop) :
(forall x:
A,
{P x} + { ~ P x }) ->
forall l:
list A,
{Forall P l} + {Exists (
fun x =>
~ P x)
l}.
Lemma Forall_impl :
forall (
P Q :
A -> Prop),
(forall a,
P a -> Q a) ->
forall l,
Forall P l -> Forall Q l.
End Exists_Forall.
Hint Constructors Exists :
core.
Hint Constructors Forall :
core.
Section Forall2.
Forall2: stating that elements of two lists are pairwise related.
ForallPairs : specifies that a certain relation should
always hold when inspecting all possible pairs of elements of a list.
ForallOrdPairs : we still check a relation over all pairs
of elements of a list, but now the order of elements matters.
ForallPairs implies ForallOrdPairs. The reverse implication is true
only when R is symmetric and reflexive.
Inversion of predicates over lists based on head symbol
Ltac is_list_constr c :=
match c with
|
nil =>
idtac
| (
_::_) =>
idtac
|
_ =>
fail
end.
Ltac invlist f :=
match goal with
|
H:
f ?
l |-
_ =>
is_list_constr l;
inversion_clear H;
invlist f
|
H:
f _ ?
l |-
_ =>
is_list_constr l;
inversion_clear H;
invlist f
|
H:
f _ _ ?
l |-
_ =>
is_list_constr l;
inversion_clear H;
invlist f
|
H:
f _ _ _ ?
l |-
_ =>
is_list_constr l;
inversion_clear H;
invlist f
|
H:
f _ _ _ _ ?
l |-
_ =>
is_list_constr l;
inversion_clear H;
invlist f
|
_ =>
idtac
end.
Exporting hints and tactics