# Library ListUtil

 List utility stuff

Require Import List TheoryList.

Set Implicit Arguments.

Section ListUtil.
Variable A : Set.

Theorem nth_spec_implies_In : forall v (ls : list A) n,
nth_spec ls n v
-> In v ls.

Section eq_dec.
Variable eq_dec : forall (x y : A), {x = y} + {x <> y}.

Definition In_eq_dec : forall (x : A) (ls : list A), {In x ls} + {~In x ls}.

Definition incl_eq_dec : forall (ls1 ls2 : list A), {incl ls1 ls2} + {~incl ls1 ls2}.
End eq_dec.

Section AllS.
Variable f : A -> Prop.

Theorem AllS_In : forall ls, AllS f ls
-> forall x, In x ls
-> f x.

Theorem AllS_deduce : forall ls,
(forall x, In x ls
-> f x)
-> AllS f ls.

Hypothesis f_dec : forall x, {f x} + {~f x}.

Definition AllS_dec : forall (ls : list A), {AllS f ls} + {~AllS f ls}.

Definition AllS_dec_some : forall (ls : list A), {AllS f ls} + {~AllS f ls /\ ls <> nil}.

Theorem AllS_not : forall ls,
~AllS f ls
-> ls = nil \/ exists x, In x ls /\ ~f x.

Theorem AllS_not_dec : forall ls,
~AllS f ls
-> {x : A | In x ls /\ ~f x} + {ls = nil} .
End AllS.
End ListUtil.

Hint Resolve nth_spec_implies_In.

Index