Library Coq.Lists.List
Basics: definition of polymorphic lists and some operations
Section Lists.
Variable A :
Type.
Inductive list :
Type :=
|
nil :
list
|
cons :
A ->
list ->
list.
Infix "::" :=
cons (
at level 60,
right associativity) :
list_scope.
Open Scope list_scope.
Head and tail
Definition head (
l:list) :=
match l with
|
nil =>
error
|
x ::
_ =>
value x
end.
Definition hd (
default:A) (
l:list) :=
match l with
|
nil =>
default
|
x ::
_ =>
x
end.
Definition tail (
l:list) :
list :=
match l with
|
nil =>
nil
|
a ::
m =>
m
end.
Length of lists
The In predicate
Fixpoint In (
a:A) (
l:list) {
struct l} :
Prop :=
match l with
|
nil =>
False
|
b ::
m =>
b =
a \/
In a m
end.
Concatenation of two lists
Fixpoint app (
l m:list) {
struct l} :
list :=
match l with
|
nil =>
m
|
a ::
l1 =>
a ::
app l1 m
end.
Infix "++" :=
app (
right associativity,
at level 60) :
list_scope.
End Lists.
Exporting list notations and tactics
Implicit Arguments nil [
A].
Infix "::" :=
cons (
at level 60,
right associativity) :
list_scope.
Infix "++" :=
app (
right associativity,
at level 60) :
list_scope.
Open Scope list_scope.
Delimit Scope list_scope with list.
Section Facts.
Variable A :
Type.
Discrimination
Theorem nil_cons :
forall (
x:A) (
l:list
A),
nil <>
x ::
l.
Destruction
Characterization of In
Theorem in_eq :
forall (
a:A) (
l:list
A),
In a (
a ::
l).
Theorem in_cons :
forall (
a b:A) (
l:list
A),
In b l ->
In b (
a ::
l).
Theorem in_nil :
forall a:A, ~
In a nil.
Lemma In_split :
forall x (
l:list
A),
In x l ->
exists l1,
exists l2,
l =
l1++x::l2.
Inversion
Theorem in_inv :
forall (
a b:A) (
l:list
A),
In b (
a ::
l) ->
a =
b \/
In b l.
Decidability of In
Theorem In_dec :
(
forall x y:A, {
x =
y} + {
x <>
y}) ->
forall (
a:A) (
l:list
A), {
In a l} + {~
In a l}.
Discrimination
Concat with nil
app is associative
Theorem app_ass :
forall l m n:list
A, (
l ++
m) ++
n =
l ++
m ++
n.
Hint Resolve app_ass.
Theorem ass_app :
forall l m n:list
A,
l ++
m ++
n = (
l ++
m) ++
n.
app commutes with cons
Theorem app_comm_cons :
forall (
x y:list
A) (
a:A),
a :: (
x ++
y) = (
a ::
x) ++
y.
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,
nil =>
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,
nil =>
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_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.
Fixpoint last (
l:list
A) (
d:A) {
struct l} :
A :=
match l with
|
nil =>
d
|
a ::
nil =>
a
|
a ::
l =>
last l d
end.
removelast l remove the last element of l
Counting occurences of a element
Hypotheses eqA_dec :
forall x y :
A, {
x =
y}+{x <>
y}.
Fixpoint count_occ (
l :
list A) (
x :
A){
struct l} :
nat :=
match l with
|
nil => 0
|
y ::
tl =>
let n :=
count_occ tl x in
if eqA_dec y x then S n else n
end.
Compatibility of count_occ with operations on list
Compatibility with other operations
An alternative tail-recursive definition for reverse
Reverse Induction Principle on Lists
Some facts about Permutation
Permutation over lists is a equivalence relation
Compatibility with others operations on lists
Theorem Permutation_in :
forall (
l l' :
list A) (
x :
A),
Permutation l l' ->
In x l ->
In x l'.
Lemma Permutation_app_tail :
forall (
l l' tl :
list A),
Permutation l l' ->
Permutation (
l++tl) (
l'++tl).
Lemma Permutation_app_head :
forall (
l tl tl' :
list A),
Permutation tl tl' ->
Permutation (
l++tl) (
l++tl').
Theorem Permutation_app :
forall (
l m l' m' :
list A),
Permutation l l' ->
Permutation m m' ->
Permutation (
l++m) (
l'++m').
Theorem Permutation_app_swap :
forall (
l l' :
list A),
Permutation (
l++l') (
l'++l).
Theorem Permutation_cons_app :
forall (
l l1 l2:list
A)
a,
Permutation l (
l1 ++
l2) ->
Permutation (
a ::
l) (
l1 ++
a ::
l2).
Hint Resolve Permutation_cons_app.
Theorem Permutation_length :
forall (
l l' :
list A),
Permutation l l' ->
length l =
length l'.
Theorem Permutation_rev :
forall (
l :
list A),
Permutation l (
rev l).
Theorem Permutation_ind_bis :
forall P :
list A ->
list A ->
Prop,
P (@
nil A) (@
nil A) ->
(
forall x l l',
Permutation l l' ->
P l l' ->
P (
x ::
l) (
x ::
l')) ->
(
forall x y l l',
Permutation l l' ->
P l l' ->
P (
y ::
x ::
l) (
x ::
y ::
l')) ->
(
forall l l' l'',
Permutation l l' ->
P l l' ->
Permutation l' l'' ->
P l' l'' ->
P l l'') ->
forall l l',
Permutation l l' ->
P l l'.
Ltac break_list l x l' H :=
destruct l as [|x
l'];
simpl in *;
injection H;
intros;
subst;
clear H.
Theorem Permutation_app_inv :
forall (
l1 l2 l3 l4:list
A)
a,
Permutation (
l1++a::l2) (
l3++a::l4) ->
Permutation (
l1++l2) (
l3 ++
l4).
Theorem Permutation_cons_inv :
forall l l' a,
Permutation (
a::l) (
a::l') ->
Permutation l l'.
Theorem Permutation_cons_app_inv :
forall l l1 l2 a,
Permutation (
a ::
l) (
l1 ++
a ::
l2) ->
Permutation l (
l1 ++
l2).
Theorem Permutation_app_inv_l :
forall l l1 l2,
Permutation (
l ++
l1) (
l ++
l2) ->
Permutation l1 l2.
Theorem Permutation_app_inv_r :
forall l l1 l2,
Permutation (
l1 ++
l) (
l2 ++
l) ->
Permutation l1 l2.
End Permutation.
Decidable equality on lists
Hypotheses eqA_dec :
forall (
x y :
A), {
x =
y}+{x <>
y}.
Lemma list_eq_dec :
forall l l':list
A, {
l =
l'} + {
l <>
l'}.
End ListOps.
Applying functions to the elements of a list
flat_map
Definition flat_map (
f:A ->
list B) :=
fix flat_map (
l:list
A) {
struct l} :
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 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 :
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
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)) {
struct l }:
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){
struct l} :
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.
Miscelenous 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.
Exporting hints and tactics