Library Coq.Structures.OrdersLists

Require Export RelationPairs SetoidList Orders EqualitiesFacts.

Set Implicit Arguments.

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.
Hint Immediate In_eq Inf_lt.

End OrderedTypeLists.

Results about keys and data as manipulated in the future MMaps.

Module KeyOrderedType(O:OrderedType).
Include KeyDecidableType(O).
Local Open Scope signature_scope.

Definition ltk {elt} : relation (key*elt) := O.lt @@1.

Hint Unfold ltk.

Instance ltk_strorder {elt} : StrictOrder (@ltk elt) := _.

Instance ltk_compat {elt} : Proper (eqk==>eqk==>iff) (@ltk elt).

Instance ltk_compat' {elt} : Proper (eqke==>eqke==>iff) (@ltk elt).

Instance pair_compat {elt} : Proper (O.eq==>Logic.eq==>eqke) (@pair key elt).

Section Elt.
Variable elt : Type.
Implicit Type p q : key*elt.
Implicit Type l m : list (key*elt).

Lemma ltk_not_eqk p q : ltk p q -> ~ eqk p q.

Lemma ltk_not_eqke p q : ltk p q -> ~eqke p q.

Notation Sort := (sort ltk).
Notation Inf := (lelistA ltk).

Lemma Inf_eq l x x' : eqk x x' -> Inf x' l -> Inf x l.

Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l.

Hint Immediate Inf_eq.
Hint Resolve Inf_lt.

Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p.

Lemma Sort_Inf_NotIn l k e : Sort l -> Inf (k,e) l -> ~In k l.

Lemma Sort_NoDupA l : Sort l -> NoDupA eqk l.

Lemma Sort_In_cons_1 l p q : Sort (p::l) -> InA eqk q l -> ltk p q.

Lemma Sort_In_cons_2 l p q : Sort (p::l) -> InA eqk q (p::l) ->
ltk p q \/ eqk p q.

Lemma Sort_In_cons_3 x l k e :
Sort ((k,e)::l) -> In x l -> ~O.eq x k.

End Elt.

Hint Resolve ltk_not_eqk ltk_not_eqke.
Hint Immediate Inf_eq.
Hint Resolve Inf_lt.
Hint Resolve Sort_Inf_NotIn.

End KeyOrderedType.