# Library Coq.Structures.OrdersLists

Require Export RelationPairs SetoidList Orders.
Set Implicit Arguments.

# Specialization of results about lists modulo.

Module OrderedTypeLists (Import O:OrderedType).
Section ForNotations.
Notation In:=(InA eq).
Notation Inf:=(lelistA lt).
Notation Sort:=(sort lt).
Notation NoDup:=(NoDupA eq).
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, lt x y -> Inf y l -> Inf x l.
Lemma Inf_eq : forall l x y, 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 -> lt a x.
Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l.
Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l.
Lemma Inf_alt :
forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).
Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
End ForNotations.
Hint Resolve ListIn_In Sort_NoDup Inf_lt.
Hint Immediate In_eq Inf_lt.
End OrderedTypeLists.

# Results about keys and data as manipulated in FMaps.

Module KeyOrderedType(Import O:OrderedType).
Module Import MO:=OrderedTypeLists(O).
Section Elt.
Variable elt : Type.
Notation key:=t.
Local Open Scope signature_scope.
Definition eqk : relation (key*elt) := eq @@1.
Definition eqke : relation (key*elt) := eq * Logic.eq.
Definition ltk : relation (key*elt) := lt @@1.
Hint Unfold eqk eqke ltk.
Global Instance eqke_eqk : subrelation eqke eqk.
Global Instance eqk_equiv : Equivalence eqk := _.
Global Instance eqke_equiv : Equivalence eqke := _.
Global Instance ltk_strorder : StrictOrder ltk := _.
Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt).
Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
Lemma InA_eqke_eqk :
forall x m, InA eqke x m -> InA eqk x m.
Hint Resolve InA_eqke_eqk.
Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
Definition In k m := exists e:elt, MapsTo k e m.
Notation Sort := (sort ltk).
Notation Inf := (lelistA ltk).
Hint Unfold MapsTo In.
Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
Lemma In_nil : forall k, In k nil <-> False.
Lemma In_cons : forall k p l,
In k (p::l) <-> eq k (fst p) \/ In k l.
Global Instance MapsTo_compat :
Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
Hint Immediate Inf_eq.
Hint Resolve Inf_lt.
Lemma Sort_Inf_In :
forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
Lemma Sort_Inf_NotIn :
forall l k e, Sort l -> Inf (k,e) l -> ~In k l.
Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
ltk e e' \/ eqk e e'.
Lemma Sort_In_cons_3 :
forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k.
Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
Lemma In_inv_2 : forall k k' e e' l,
InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
Lemma In_inv_3 : forall x x' l,
InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
End Elt.
Hint Unfold eqk eqke ltk.
Hint Extern 2 (eqke ?a ?b) => split.
Hint Resolve ltk_not_eqk ltk_not_eqke.
Hint Resolve InA_eqke_eqk.
Hint Unfold MapsTo In.
Hint Immediate Inf_eq.
Hint Resolve Inf_lt.
Hint Resolve Sort_Inf_NotIn.
Hint Resolve In_inv_2 In_inv_3.
End KeyOrderedType.