Library Coq.Lists.TheoryList
Some programs and results about lists following CAML Manual
Require Export List.
Local Notation "[ ]" :=
nil (
at level 0).
Local Notation "[ a ; .. ; b ]" := (
a :: .. (
b :: []) ..) (
at level 0).
Section Lists.
Variable A :
Type.
The null function
The Uncons function
The head function
Length of lists
Members of lists
Index of elements
Require Import Le.
Require Import Lt.
Inductive nth_spec :
list A ->
nat ->
A ->
Prop :=
|
nth_spec_O :
forall (
a:
A) (
l:
list A),
nth_spec (
a :: l) 1
a
|
nth_spec_S :
forall (
n:
nat) (
a b:
A) (
l:
list A),
nth_spec l n a ->
nth_spec (
b :: l) (
S n)
a.
Hint Resolve nth_spec_O nth_spec_S.
Inductive fst_nth_spec :
list A ->
nat ->
A ->
Prop :=
|
fst_nth_O :
forall (
a:
A) (
l:
list A),
fst_nth_spec (
a :: l) 1
a
|
fst_nth_S :
forall (
n:
nat) (
a b:
A) (
l:
list A),
a <> b ->
fst_nth_spec l n a ->
fst_nth_spec (
b :: l) (
S n)
a.
Hint Resolve fst_nth_O fst_nth_S.
Lemma fst_nth_nth :
forall (
l:
list A) (
n:
nat) (
a:
A),
fst_nth_spec l n a ->
nth_spec l n a.
Hint Immediate fst_nth_nth.
Lemma nth_lt_O :
forall (
l:
list A) (
n:
nat) (
a:
A),
nth_spec l n a -> 0
< n.
Lemma nth_le_length :
forall (
l:
list A) (
n:
nat) (
a:
A),
nth_spec l n a ->
n <= length l.
Fixpoint Nth_func (
l:
list A) (
n:
nat) :
Exc A :=
match l,
n with
|
a :: _,
S O =>
value a
|
_ :: l',
S (
S p) =>
Nth_func l' (
S p)
|
_,
_ =>
error
end.
Lemma Nth :
forall (
l:
list A) (
n:
nat),
{a : A | nth_spec l n a} + {n = 0
\/ length l < n}.
Lemma Item :
forall (
l:
list A) (
n:
nat),
{a : A | nth_spec l (
S n)
a} + {length l <= n}.
Require Import Minus.
Require Import DecBool.
Fixpoint index_p (
a:
A) (
l:
list A) :
nat ->
Exc nat :=
match l with
|
nil =>
fun p =>
error
|
b :: m =>
fun p =>
ifdec (
eqA_dec a b) (
value p) (
index_p a m (
S p))
end.
Lemma Index_p :
forall (
a:
A) (
l:
list A) (
p:
nat),
{n : nat | fst_nth_spec l (
S n - p)
a} + {AllS (
fun b:
A =>
a <> b)
l}.
Lemma Index :
forall (
a:
A) (
l:
list A),
{n : nat | fst_nth_spec l n a} + {AllS (
fun b:
A =>
a <> b)
l}.
Section Find_sec.
Variables R P :
A ->
Prop.
Inductive InR :
list A ->
Prop :=
|
inR_hd :
forall (
a:
A) (
l:
list A),
R a ->
InR (
a :: l)
|
inR_tl :
forall (
a:
A) (
l:
list A),
InR l ->
InR (
a :: l).
Hint Resolve inR_hd inR_tl.
Definition InR_inv (
l:
list A) :=
match l with
|
nil =>
False
|
b :: m =>
R b \/ InR m
end.
Lemma InR_INV :
forall l:
list A,
InR l ->
InR_inv l.
Lemma InR_cons_inv :
forall (
a:
A) (
l:
list A),
InR (
a :: l) ->
R a \/ InR l.
Lemma InR_or_app :
forall l m:
list A,
InR l \/ InR m ->
InR (
l ++ m).
Lemma InR_app_or :
forall l m:
list A,
InR (
l ++ m) ->
InR l \/ InR m.
Hypothesis RS_dec :
forall a:
A,
{R a} + {P a}.
Fixpoint find (
l:
list A) :
Exc A :=
match l with
|
nil =>
error
|
a :: m =>
ifdec (
RS_dec a) (
value a) (
find m)
end.
Lemma Find :
forall l:
list A,
{a : A | In a l & R a} + {AllS P l}.
Variable B :
Type.
Variable T :
A ->
B ->
Prop.
Variable TS_dec :
forall a:
A,
{c : B | T a c} + {P a}.
Fixpoint try_find (
l:
list A) :
Exc B :=
match l with
|
nil =>
error
|
a :: l1 =>
match TS_dec a with
|
inleft (
exist c _) =>
value c
|
inright _ =>
try_find l1
end
end.
Lemma Try_find :
forall l:
list A,
{c : B | exists2 a : A, In a l & T a c} + {AllS P l}.
End Find_sec.
Section Assoc_sec.
Variable B :
Type.
Fixpoint assoc (
a:
A) (
l:
list (
A * B)) :
Exc B :=
match l with
|
nil =>
error
|
(a', b) :: m =>
ifdec (
eqA_dec a a') (
value b) (
assoc a m)
end.
Inductive AllS_assoc (
P:
A ->
Prop) :
list (
A * B) ->
Prop :=
|
allS_assoc_nil :
AllS_assoc P nil
|
allS_assoc_cons :
forall (
a:
A) (
b:
B) (
l:
list (
A * B)),
P a ->
AllS_assoc P l ->
AllS_assoc P (
(a, b) :: l).
Hint Resolve allS_assoc_nil allS_assoc_cons.
Lemma Assoc :
forall (
a:
A) (
l:
list (
A * B)),
B + {AllS_assoc (
fun a':
A =>
a <> a')
l}.
End Assoc_sec.
End Lists.
Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons :
datatypes.
Hint Immediate fst_nth_nth:
datatypes.