Library Coq.Structures.OrdersLists
Specialization of results about lists modulo.
Module OrderedTypeLists (
O:
OrderedType).
Lemma In_eq :
forall l x y,
eq x y -> In x l -> In y l.
Lemma ListIn_In :
forall l x,
List.In x l -> In x l.
Lemma Inf_lt :
forall l x y,
O.lt x y -> Inf y l -> Inf x l.
Lemma Inf_eq :
forall l x y,
O.eq x y -> Inf y l -> Inf x l.
Lemma Sort_Inf_In :
forall l x a,
Sort l -> Inf a l -> In x l -> O.lt a x.
Lemma ListIn_Inf :
forall l x,
(forall y,
List.In y l -> O.lt x y) -> Inf x l.
Lemma In_Inf :
forall l x,
(forall y,
In y l -> O.lt x y) -> Inf x l.
Lemma Inf_alt :
forall l x,
Sort l -> (Inf x l <-> (forall y,
In y l -> O.lt x y)).
Lemma Sort_NoDup :
forall l,
Sort l -> NoDup l.
Hint Resolve ListIn_In Sort_NoDup Inf_lt :
core.
Hint Immediate In_eq Inf_lt :
core.
End OrderedTypeLists.
Results about keys and data as manipulated in the future MMaps.