# Library Coq.Lists.TheoryList

Some programs and results about lists following CAML Manual

Require Export List.
Section Lists.

Variable A : Type.

The null function

Definition Isnil (l:list A) : Prop := nil = l.

Lemma Isnil_nil : Isnil nil.
Hint Resolve Isnil_nil.

Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l).

Hint Resolve Isnil_nil not_Isnil_cons.

Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}.

The Uncons function

Lemma Uncons :
forall l:list A, {a : A & {m : list A | a :: m = l}} + {Isnil l}.

Lemma Hd :
forall l:list A, {a : A | exists m : list A, a :: m = l} + {Isnil l}.

Lemma Tl :
forall l:list A,
{m : list A | (exists a : A, a :: m = l) \/ Isnil l /\ Isnil m}.

Length of lists

Fixpoint Length_l (l:list A) (n:nat) {struct l} : nat :=
match l with
| nil => n
| _ :: m => Length_l m (S n)
end.

Lemma Length_l_pf : forall (l:list A) (n:nat), {m : nat | n + length l = m}.

Lemma Length : forall l:list A, {m : nat | length l = m}.

Members of lists
Inductive In_spec (a:A) : list A -> Prop :=
| in_hd : forall l:list A, In_spec a (a :: l)
| in_tl : forall (l:list A) (b:A), In a l -> In_spec a (b :: l).
Hint Resolve in_hd in_tl.
Hint Unfold In.
Hint Resolve in_cons.

Theorem In_In_spec : forall (a:A) (l:list A), In a l <-> In_spec a l.

Inductive AllS (P:A -> Prop) : list A -> Prop :=
| allS_nil : AllS P nil
| allS_cons : forall (a:A) (l:list A), P a -> AllS P l -> AllS P (a :: l).
Hint Resolve allS_nil allS_cons.

Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}.

Fixpoint mem (a:A) (l:list A) {struct l} : bool :=
match l with
| nil => false
| b :: m => if eqA_dec a b then true else mem a m
end.

Hint Unfold In.
Lemma Mem : forall (a:A) (l:list A), {In a l} + {AllS (fun b:A => b <> a) l}.

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) {struct l} : 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) {struct l} : 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)) {struct l} :
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 allS_nil allS_cons:
datatypes.
Hint Immediate fst_nth_nth: datatypes.