Require Export SetoidList Morphisms OrdersTac.
Set Implicit Arguments.

Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type :=
  | LT : lt x y -> Compare lt eq x y
  | EQ : eq x y -> Compare lt eq x y
  | GT : lt y x -> Compare lt eq x y.


Module Type MiniOrderedType.

  Parameter Inline t : Type.

  Parameter Inline eq : t -> t -> Prop.
  Parameter Inline lt : t -> t -> Prop.

  Axiom eq_refl : forall x : t, eq x x.
  Axiom eq_sym : forall x y : t, eq x y -> eq y x.
  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.

  Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
  Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.

  Parameter compare : forall x y : t, Compare lt eq x y.

  Hint Immediate eq_sym.
  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.

End MiniOrderedType.

Module Type OrderedType.
  Include MiniOrderedType.

  Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }.

End OrderedType.

Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType.
  Include O.

  Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.

End MOT_to_OT.

Module OrderedTypeFacts (Import O: OrderedType).

  Instance eq_equiv : Equivalence eq.

  Lemma lt_antirefl : forall x, ~ lt x x.

  Instance lt_strorder : StrictOrder lt.

  Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.

  Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.

  Instance lt_compat : Proper (eq==>eq==>iff) lt.

  Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.

  Module TO.
   Definition t := t.
   Definition eq := eq.
   Definition lt := lt.
   Definition le x y := lt x y \/ eq x y.
  End TO.
  Module IsTO.
   Definition eq_equiv := eq_equiv.
   Definition lt_strorder := lt_strorder.
   Definition lt_compat := lt_compat.
   Definition lt_total := lt_total.
   Lemma le_lteq x y : TO.le x y <-> lt x y \/ eq x y.
  End IsTO.
  Module OrderTac := !MakeOrderTac TO IsTO.
  Ltac order := OrderTac.order.

  Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z.
  Lemma eq_le x y z : eq x y -> ~lt y z -> ~lt x z.
  Lemma neq_eq x y z : ~eq x y -> eq y z -> ~eq x z.
  Lemma eq_neq x y z : eq x y -> ~eq y z -> ~eq x z.
  Lemma le_lt_trans x y z : ~lt y x -> lt y z -> lt x z.
  Lemma lt_le_trans x y z : lt x y -> ~lt z y -> lt x z.
  Lemma le_neq x y : ~lt x y -> ~eq x y -> lt y x.
  Lemma le_trans x y z : ~lt y x -> ~lt z y -> ~lt z x.
  Lemma le_antisym x y : ~lt y x -> ~lt x y -> eq x y.
  Lemma neq_sym x y : ~eq x y -> ~eq y x.
  Lemma lt_le x y : lt x y -> ~lt y x.
  Lemma gt_not_eq x y : lt y x -> ~ eq x y.
  Lemma eq_not_lt x y : eq x y -> ~ lt x y.
  Lemma eq_not_gt x y : eq x y -> ~ lt y x.
  Lemma lt_not_gt x y : lt x y -> ~ lt y x.

  Hint Resolve gt_not_eq eq_not_lt.
  Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq.
  Hint Resolve eq_not_gt lt_antirefl lt_not_gt.

  Lemma elim_compare_eq :
   forall x y : t,
   eq x y -> exists H : eq x y, compare x y = EQ H.

  Lemma elim_compare_lt :
   forall x y : t,
   lt x y -> exists H : lt x y, compare x y = LT H.

  Lemma elim_compare_gt :
   forall x y : t,
   lt y x -> exists H : lt y x, compare x y = GT H.

  Ltac elim_comp :=
    match goal with
      | |- ?e => match e with
           | context ctx [ compare ?a ?b ] =>
                let H := fresh in
                (destruct (compare a b) as [H|H|H]; try order)
         end
    end.

  Ltac elim_comp_eq x y :=
    elim (elim_compare_eq (x:=x) (y:=y));
     [ intros _1 _2; rewrite _2; clear _1 _2 | auto ].

  Ltac elim_comp_lt x y :=
    elim (elim_compare_lt (x:=x) (y:=y));
     [ intros _1 _2; rewrite _2; clear _1 _2 | auto ].

  Ltac elim_comp_gt x y :=
    elim (elim_compare_gt (x:=x) (y:=y));
     [ intros _1 _2; rewrite _2; clear _1 _2 | auto ].

  Definition eq_dec := eq_dec.

  Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.

  Definition eqb x y : bool := if eq_dec x y then true else false.

  Lemma eqb_alt :
    forall x y, eqb x y = match compare x y with EQ _ => true | _ => false end.


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 OrderedTypeFacts.

Module KeyOrderedType(O:OrderedType).
 Import O.
 Module MO:=OrderedTypeFacts(O).
 Import MO.

 Section Elt.
 Variable elt : Type.
 Notation key:=t.

  Definition eqk (p p´:key*elt) := eq (fst p) (fst p´).
  Definition eqke (p p´:key*elt) :=
          eq (fst p) (fst p´) /\ (snd p) = (snd p´).
  Definition ltk (p p´:key*elt) := lt (fst p) (fst p´).

  Hint Unfold eqk eqke ltk.
  Hint Extern 2 (eqke ?a ?b) => split.


   Lemma eqke_eqk : forall x x´, eqke x x´ -> eqk x x´.


   Lemma ltk_right_r : forall x k e e´, ltk x (k,e) -> ltk x (k,e´).

   Lemma ltk_right_l : forall x k e e´, ltk (k,e) x -> ltk (k,e´) x.
   Hint Immediate ltk_right_r ltk_right_l.


  Lemma eqk_refl : forall e, eqk e e.

  Lemma eqke_refl : forall e, eqke e e.

  Lemma eqk_sym : forall e e´, eqk e e´ -> eqk e´ e.

  Lemma eqke_sym : forall e e´, eqke e e´ -> eqke e´ e.

  Lemma eqk_trans : forall e e´ e´´, eqk e e´ -> eqk e´ e´´ -> eqk e e´´.

  Lemma eqke_trans : forall e e´ e´´, eqke e e´ -> eqke e´ e´´ -> eqke e e´´.

  Lemma ltk_trans : forall e e´ e´´, ltk e e´ -> ltk e´ e´´ -> ltk e e´´.

  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´.

  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
  Hint Immediate eqk_sym eqke_sym.

  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 ltk_compat´ : Proper (eqke==>eqke==>iff) ltk.


  Lemma eqk_not_ltk : forall x x´, eqk x x´ -> ~ltk x x´.

  Lemma ltk_eqk : forall e e´ e´´, ltk e e´ -> eqk e´ e´´ -> ltk e e´´.

  Lemma eqk_ltk : forall e e´ e´´, eqk e e´ -> ltk e´ e´´ -> ltk e e´´.
  Hint Resolve eqk_not_ltk.
  Hint Immediate ltk_eqk eqk_ltk.

  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 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 eqk_trans eqke_trans eqk_refl eqke_refl.
 Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
 Hint Immediate eqk_sym eqke_sym.
 Hint Resolve eqk_not_ltk.
 Hint Immediate ltk_eqk eqk_ltk.
 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.