Library ListUtil
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
This page has been generated by coqdoc