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.
Section Lists.
Variable A :
Type.
Head and tail
The In predicate
Fixpoint In (
a:
A) (
l:
list A) :
Prop :=
match l with
|
nil =>
False
|
b :: m =>
b = a \/ In a m
end.
End Lists.
Local Notation "[ ]" :=
nil :
list_scope.
Local Notation "[ a ; .. ; b ]" := (
a :: .. (
b :: []) ..) :
list_scope.
Section Facts.
Variable A :
Type.
Discrimination
Destruction
Characterization of In
Inversion
Decidability of In
Discrimination
Concat with nil
app is associative
app commutes with cons
Facts deduced from the result of a concatenation
Compatibility wtih 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} :
Exc A :=
match n,
l with
|
O,
x :: _ =>
value x
|
S n,
_ :: l =>
nth_error l n
|
_,
_ =>
error
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.
Lemma nth_In :
forall (
n:
nat) (
l:
list A) (
d:
A),
n < length l ->
In (
nth n l d)
l.
Lemma nth_overflow :
forall l n d,
length l <= n ->
nth n l d = d.
Lemma nth_indep :
forall l n d d',
n < length l ->
nth n l d = nth n l d'.
Lemma app_nth1 :
forall l l' d n,
n < length l ->
nth n (
l++l')
d = nth n l d.
Lemma app_nth2 :
forall l l' d n,
n >= length l ->
nth n (
l++l')
d = nth (
n-length l)
l' d.
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 occurences of a 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
flat_map
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
Section Bool.
Variable A :
Type.
Variable f :
A ->
bool.
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
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
|
nil =>
(nil, nil)
|
(x,y) :: tl =>
let (
g,
d) :=
split tl in (x::g, y::d)
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
Cutting a list at some position
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
Inductive Exists {
A} (
P:
A->
Prop) :
list A ->
Prop :=
|
Exists_cons_hd :
forall x l,
P x ->
Exists P (
x::l)
|
Exists_cons_tl :
forall x l,
Exists P l ->
Exists P (
x::l).
Hint Constructors Exists.
Lemma Exists_exists :
forall A P (
l:
list A),
Exists P l <-> (exists x, In x l /\ P x).
Lemma Exists_nil :
forall A (
P:
A->
Prop),
Exists P nil <-> False.
Lemma Exists_cons :
forall A (
P:
A->
Prop)
x l,
Exists P (
x::l)
<-> P x \/ Exists P l.
Inductive Forall {
A} (
P:
A->
Prop) :
list A ->
Prop :=
|
Forall_nil :
Forall P nil
|
Forall_cons :
forall x l,
P x ->
Forall P l ->
Forall P (
x::l).
Hint Constructors Forall.
Lemma Forall_forall :
forall A P (
l:
list A),
Forall P l <-> (forall x,
In x l ->
P x).
Lemma Forall_inv :
forall A P (
a:
A)
l,
Forall P (
a :: l) ->
P a.
Lemma Forall_rect :
forall A (
P:
A->
Prop) (
Q :
list A ->
Type),
Q [] -> (
forall b l,
P b ->
Q (
b :: l)) ->
forall l,
Forall P l ->
Q l.
Lemma Forall_impl :
forall A (
P Q :
A ->
Prop), (
forall a,
P a ->
Q a) ->
forall l,
Forall P l ->
Forall Q l.
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.
Definition ForallPairs A (
R :
A ->
A ->
Prop)
l :=
forall a b,
In a l ->
In b l ->
R a b.
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