Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Export SetoidList Morphisms OrdersTac.
Set Implicit Arguments.
Unset Strict Implicit.

NB: This file is here only for compatibility with earlier version of FSets and FMap. Please use Structures/Orders.v directly now.

Ordered types

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.

Arguments LT [X lt eq x y] _.
Arguments EQ [X lt eq x y] _.
Arguments GT [X 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 : core.
  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core.

End MiniOrderedType.

Module Type OrderedType.
  Include MiniOrderedType.

A eq_dec can be deduced from compare below. But adding this redundant field allows seeing an OrderedType as a DecidableType.

  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}.forall x y : t, {eq x y} + {~ eq x y}
  Proof.forall x y : t, {eq x y} + {~ eq x y}
   intros; elim (compare x y); intro H; [ right | left | right ]; auto.x, y:t
H:lt y x
~ eq x y
   assert (~ eq y x); auto.
  Defined.

End MOT_to_OT.

Ordered types properties

Additional properties that can be derived from signature OrderedType.

Module OrderedTypeFacts (Import O: OrderedType).

  Instance eq_equiv : Equivalence eq.Equivalence eq
  Proof.Equivalence eq split; [ exact eq_refl | exact eq_sym | exact eq_trans ]. Qed.

  Lemma lt_antirefl : forall x, ~ lt x x.forall x : t, ~ lt x x
  Proof.forall x : t, ~ lt x x
   intros; intro; absurd (eq x x); auto.
  Qed.

  Instance lt_strorder : StrictOrder lt.StrictOrder lt
  Proof.StrictOrder lt split; [ exact lt_antirefl | exact lt_trans]. Qed.

  Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.forall x y z : t, lt x y -> eq y z -> lt x z
  Proof.forall x y z : t, lt x y -> eq y z -> lt x z
   intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto.x, y, z:t
H:lt x y
H0:eq y z
Heq:eq x z
lt x z
x, y, z:t
H:lt x y
H0:eq y z
Hlt:lt z x
lt x z
   elim (lt_not_eq H); apply eq_trans with z; auto.x, y, z:t
H:lt x y
H0:eq y z
Hlt:lt z x
lt x z
   elim (lt_not_eq (lt_trans Hlt H)); auto.
  Qed.

  Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.forall x y z : t, eq x y -> lt y z -> lt x z
  Proof.forall x y z : t, eq x y -> lt y z -> lt x z
   intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto.x, y, z:t
H:eq x y
H0:lt y z
Heq:eq x z
lt x z
x, y, z:t
H:eq x y
H0:lt y z
Hlt:lt z x
lt x z
   elim (lt_not_eq H0); apply eq_trans with x; auto.x, y, z:t
H:eq x y
H0:lt y z
Hlt:lt z x
lt x z
   elim (lt_not_eq (lt_trans H0 Hlt)); auto.
  Qed.

  Instance lt_compat : Proper (eq==>eq==>iff) lt.Proper (eq ==> eq ==> iff) lt
  Proof.Proper (eq ==> eq ==> iff) lt
  apply proper_sym_impl_iff_2; auto with *.Proper (eq ==> eq ==> impl) lt
  intros x x' Hx y y' Hy H.x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
lt x' y'
  apply eq_lt with x; auto.x, x':t
Hx:eq x x'
y, y':t
Hy:eq y y'
H:lt x y
lt x y'
  apply lt_eq with y; auto.
  Qed.

  Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.forall x y : t, lt x y \/ eq x y \/ lt y x
  Proof.forall x y : t, lt x y \/ eq x y \/ lt y x intros; destruct (compare x y); auto. Qed.

  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.x, y:t
TO.le x y <-> lt x y \/ eq x y
   Proof.x, y:t
TO.le x y <-> lt x y \/ eq x y reflexivity. Qed.
  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.x, y, z:t
~ lt x y -> eq y z -> ~ lt x z Proof.x, y, z:t
~ lt x y -> eq y z -> ~ lt x z order. Qed.
  Lemma eq_le x y z : eq x y -> ~lt y z -> ~lt x z.x, y, z:t
eq x y -> ~ lt y z -> ~ lt x z Proof.x, y, z:t
eq x y -> ~ lt y z -> ~ lt x z order. Qed.
  Lemma neq_eq x y z : ~eq x y -> eq y z -> ~eq x z.x, y, z:t
~ eq x y -> eq y z -> ~ eq x z Proof.x, y, z:t
~ eq x y -> eq y z -> ~ eq x z order. Qed.
  Lemma eq_neq x y z : eq x y -> ~eq y z -> ~eq x z.x, y, z:t
eq x y -> ~ eq y z -> ~ eq x z Proof.x, y, z:t
eq x y -> ~ eq y z -> ~ eq x z order. Qed.
  Lemma le_lt_trans x y z : ~lt y x -> lt y z -> lt x z.x, y, z:t
~ lt y x -> lt y z -> lt x z Proof.x, y, z:t
~ lt y x -> lt y z -> lt x z order. Qed.
  Lemma lt_le_trans x y z : lt x y -> ~lt z y -> lt x z.x, y, z:t
lt x y -> ~ lt z y -> lt x z Proof.x, y, z:t
lt x y -> ~ lt z y -> lt x z order. Qed.
  Lemma le_neq x y : ~lt x y -> ~eq x y -> lt y x.x, y:t
~ lt x y -> ~ eq x y -> lt y x Proof.x, y:t
~ lt x y -> ~ eq x y -> lt y x order. Qed.
  Lemma le_trans x y z : ~lt y x -> ~lt z y -> ~lt z x.x, y, z:t
~ lt y x -> ~ lt z y -> ~ lt z x Proof.x, y, z:t
~ lt y x -> ~ lt z y -> ~ lt z x order. Qed.
  Lemma le_antisym x y : ~lt y x -> ~lt x y -> eq x y.x, y:t
~ lt y x -> ~ lt x y -> eq x y Proof.x, y:t
~ lt y x -> ~ lt x y -> eq x y order. Qed.
  Lemma neq_sym x y : ~eq x y -> ~eq y x.x, y:t
~ eq x y -> ~ eq y x Proof.x, y:t
~ eq x y -> ~ eq y x order. Qed.
  Lemma lt_le x y : lt x y -> ~lt y x.x, y:t
lt x y -> ~ lt y x Proof.x, y:t
lt x y -> ~ lt y x order. Qed.
  Lemma gt_not_eq x y : lt y x -> ~ eq x y.x, y:t
lt y x -> ~ eq x y Proof.x, y:t
lt y x -> ~ eq x y order. Qed.
  Lemma eq_not_lt x y : eq x y -> ~ lt x y.x, y:t
eq x y -> ~ lt x y Proof.x, y:t
eq x y -> ~ lt x y order. Qed.
  Lemma eq_not_gt x y : eq x y -> ~ lt y x.x, y:t
eq x y -> ~ lt y x Proof.x, y:t
eq x y -> ~ lt y x order. Qed.
  Lemma lt_not_gt x y : lt x y -> ~ lt y x.x, y:t
lt x y -> ~ lt y x Proof.x, y:t
lt x y -> ~ lt y x order. Qed.

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

  Lemma elim_compare_eq :
   forall x y : t,
   eq x y -> exists H : eq x y, compare x y = EQ H.forall x y : t,
eq x y -> exists H : eq x y, compare x y = EQ H
  Proof.forall x y : t,
eq x y -> exists H : eq x y, compare x y = EQ H
   intros; case (compare x y); intros H'; try (exfalso; order).x, y:t
H, H':eq x y
exists H0 : eq x y, EQ H' = EQ H0
   exists H'; auto.
  Qed.

  Lemma elim_compare_lt :
   forall x y : t,
   lt x y -> exists H : lt x y, compare x y = LT H.forall x y : t,
lt x y -> exists H : lt x y, compare x y = LT H
  Proof.forall x y : t,
lt x y -> exists H : lt x y, compare x y = LT H
   intros; case (compare x y); intros H'; try (exfalso; order).x, y:t
H, H':lt x y
exists H0 : lt x y, LT H' = LT H0
   exists H'; auto.
  Qed.

  Lemma elim_compare_gt :
   forall x y : t,
   lt y x -> exists H : lt y x, compare x y = GT H.forall x y : t,
lt y x -> exists H : lt y x, compare x y = GT H
  Proof.forall x y : t,
lt y x -> exists H : lt y x, compare x y = GT H
   intros; case (compare x y); intros H'; try (exfalso; order).x, y:t
H, H':lt y x
exists H0 : lt y x, GT H' = GT H0
   exists H'; auto.
  Qed.

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

For compatibility reasons

  Definition eq_dec := eq_dec.

  Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.forall x y : t, {lt x y} + {~ lt x y}
  Proof.forall x y : t, {lt x y} + {~ lt x y}
   intros; elim (compare x y); [ left | right | right ]; auto.
  Defined.

  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.forall x y : t,
eqb x y =
match compare x y with
| EQ _ => true
| _ => false
end
  Proof.forall x y : t,
eqb x y =
match compare x y with
| EQ _ => true
| _ => false
end
  unfold eqb; intros; destruct (eq_dec x y); elim_comp; auto.
  Qed.

(* Specialization of results about lists modulo. *)

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.forall (l : list t) (x y : t),
eq x y -> In x l -> In y l
Proof.forall (l : list t) (x y : t),
eq x y -> In x l -> In y l exact (InA_eqA eq_equiv). Qed.

Lemma ListIn_In : forall l x, List.In x l -> In x l.forall (l : list t) (x : t), List.In x l -> In x l
Proof.forall (l : list t) (x : t), List.In x l -> In x l exact (In_InA eq_equiv). Qed.

Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.forall (l : list t) (x y : t),
lt x y -> Inf y l -> Inf x l
Proof.forall (l : list t) (x y : t),
lt x y -> Inf y l -> Inf x l exact (InfA_ltA lt_strorder). Qed.

Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.forall (l : list t) (x y : t),
eq x y -> Inf y l -> Inf x l
Proof.forall (l : list t) (x y : t),
eq x y -> Inf y l -> Inf x l exact (InfA_eqA eq_equiv lt_compat). Qed.

Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.forall (l : list t) (x a : t),
Sort l -> Inf a l -> In x l -> lt a x
Proof.forall (l : list t) (x a : t),
Sort l -> Inf a l -> In x l -> lt a x exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.

Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l.forall (l : list t) (x : t),
(forall y : t, List.In y l -> lt x y) -> Inf x l
Proof.forall (l : list t) (x : t),
(forall y : t, List.In y l -> lt x y) -> Inf x l exact (@In_InfA t lt). Qed.

Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l.forall (l : list t) (x : t),
(forall y : t, In y l -> lt x y) -> Inf x l
Proof.forall (l : list t) (x : t),
(forall y : t, In y l -> lt x y) -> Inf x l exact (InA_InfA eq_equiv (ltA:=lt)). Qed.

Lemma Inf_alt :
 forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).forall (l : list t) (x : t),
Sort l -> Inf x l <-> (forall y : t, In y l -> lt x y)
Proof.forall (l : list t) (x : t),
Sort l -> Inf x l <-> (forall y : t, In y l -> lt x y) exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed.

Lemma Sort_NoDup : forall l, Sort l -> NoDup l.forall l : list t, Sort l -> NoDup l
Proof.forall l : list t, Sort l -> NoDup l exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed.

End ForNotations.

Hint Resolve ListIn_In Sort_NoDup Inf_lt : core.
Hint Immediate In_eq Inf_lt : core.

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 : core.
  Hint Extern 2 (eqke ?a ?b) => split : core.

   (* eqke is stricter than eqk *)

   Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'.elt:Type
forall x x' : key * elt, eqke x x' -> eqk x x'
   Proof.elt:Type
forall x x' : key * elt, eqke x x' -> eqk x x'
     unfold eqk, eqke; intuition.
   Qed.

  (* ltk ignore the second components *)

   Lemma ltk_right_r : forall x k e e', ltk x (k,e) -> ltk x (k,e').elt:Type
forall (x : key * elt) (k : key) (e e' : elt),
ltk x (k, e) -> ltk x (k, e')
   Proof.elt:Type
forall (x : key * elt) (k : key) (e e' : elt),
ltk x (k, e) -> ltk x (k, e') auto. Qed.

   Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x.elt:Type
forall (x : key * elt) (k : key) (e e' : elt),
ltk (k, e) x -> ltk (k, e') x
   Proof.elt:Type
forall (x : key * elt) (k : key) (e e' : elt),
ltk (k, e) x -> ltk (k, e') x auto. Qed.
   Hint Immediate ltk_right_r ltk_right_l : core.

  (* eqk, eqke are equalities, ltk is a strict order *)

  Lemma eqk_refl : forall e, eqk e e.elt:Type
forall e : key * elt, eqk e e
  Proof.elt:Type
forall e : key * elt, eqk e e auto. Qed.

  Lemma eqke_refl : forall e, eqke e e.elt:Type
forall e : key * elt, eqke e e
  Proof.elt:Type
forall e : key * elt, eqke e e auto. Qed.

  Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e.elt:Type
forall e e' : key * elt, eqk e e' -> eqk e' e
  Proof.elt:Type
forall e e' : key * elt, eqk e e' -> eqk e' e auto. Qed.

  Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e.elt:Type
forall e e' : key * elt, eqke e e' -> eqke e' e
  Proof.elt:Type
forall e e' : key * elt, eqke e e' -> eqke e' e unfold eqke; intuition. Qed.

  Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''.elt:Type
forall e e' e'' : key * elt,
eqk e e' -> eqk e' e'' -> eqk e e''
  Proof.elt:Type
forall e e' e'' : key * elt,
eqk e e' -> eqk e' e'' -> eqk e e'' eauto. Qed.

  Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.elt:Type
forall e e' e'' : key * elt,
eqke e e' -> eqke e' e'' -> eqke e e''
  Proof.elt:Type
forall e e' e'' : key * elt,
eqke e e' -> eqke e' e'' -> eqke e e''
    unfold eqke; intuition; [ eauto | congruence ].
  Qed.

  Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''.elt:Type
forall e e' e'' : key * elt,
ltk e e' -> ltk e' e'' -> ltk e e''
  Proof.elt:Type
forall e e' e'' : key * elt,
ltk e e' -> ltk e' e'' -> ltk e e'' eauto. Qed.

  Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.elt:Type
forall e e' : key * elt, ltk e e' -> ~ eqk e e'
  Proof.elt:Type
forall e e' : key * elt, ltk e e' -> ~ eqk e e' unfold eqk, ltk; auto. Qed.

  Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.elt:Type
forall e e' : key * elt, ltk e e' -> ~ eqke e e'
  Proof.elt:Type
forall e e' : key * elt, ltk e e' -> ~ eqke e e'
    unfold eqke, ltk; intuition; simpl in *; subst.elt:Type
a:key
e':(key * elt)%type
H:lt a (fst e')
H1:eq a (fst e')
False
    exact (lt_not_eq H H1).
  Qed.

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

  Instance eqk_equiv : Equivalence eqk.elt:Type
Equivalence eqk
  Proof.elt:Type
Equivalence eqk constructor; eauto. Qed.

  Instance eqke_equiv : Equivalence eqke.elt:Type
Equivalence eqke
  Proof.elt:Type
Equivalence eqke split; eauto. Qed.

  Instance ltk_strorder : StrictOrder ltk.elt:Type
StrictOrder ltk
  Proof.elt:Type
StrictOrder ltk constructor; eauto.elt:Type
Irreflexive ltk intros x; apply (irreflexivity (x:=fst x)). Qed.

  Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.elt:Type
Proper (eqk ==> eqk ==> iff) ltk
  Proof.elt:Type
Proper (eqk ==> eqk ==> iff) ltk
  intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute.elt:Type
x:key
e:elt
x':key
e':elt
Hxx':eqk (x, e) (x', e')
y:key
f:elt
y':key
f':elt
Hyy':eqk (y, f) (y', f')
(lt x y -> lt x' y') /\ (lt x' y' -> lt x y)
   compute in Hxx'; compute in Hyy'.elt:Type
x:key
e:elt
x':key
e':elt
Hxx':eq x x'
y:key
f:elt
y':key
f':elt
Hyy':eq y y'
(lt x y -> lt x' y') /\ (lt x' y' -> lt x y) rewrite Hxx', Hyy'; auto.
  Qed.

  Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk.elt:Type
Proper (eqke ==> eqke ==> iff) ltk
  Proof.elt:Type
Proper (eqke ==> eqke ==> iff) ltk
  intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute.elt:Type
x:key
e:elt
x':key
e':elt
Hxx':eq (fst (x, e)) (fst (x', e'))
y:key
f:elt
y':key
f':elt
Hyy':eq (fst (y, f)) (fst (y', f'))
(lt x y -> lt x' y') /\ (lt x' y' -> lt x y)
   compute in Hxx'; compute in Hyy'.elt:Type
x:key
e:elt
x':key
e':elt
Hxx':eq x x'
y:key
f:elt
y':key
f':elt
Hyy':eq y y'
(lt x y -> lt x' y') /\ (lt x' y' -> lt x y) rewrite Hxx', Hyy'; auto.
  Qed.

  (* Additional facts *)

  Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'.elt:Type
forall x x' : key * elt, eqk x x' -> ~ ltk x x'
   Proof.elt:Type
forall x x' : key * elt, eqk x x' -> ~ ltk x x'
     unfold eqk, ltk; simpl; auto.
   Qed.

  Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''.elt:Type
forall e e' e'' : key * elt,
ltk e e' -> eqk e' e'' -> ltk e e''
  Proof.elt:Type
forall e e' e'' : key * elt,
ltk e e' -> eqk e' e'' -> ltk e e'' eauto. Qed.

  Lemma eqk_ltk : forall e e' e'', eqk e e' -> ltk e' e'' -> ltk e e''.elt:Type
forall e e' e'' : key * elt,
eqk e e' -> ltk e' e'' -> ltk e e''
  Proof.elt:Type
forall e e' e'' : key * elt,
eqk e e' -> ltk e' e'' -> ltk e e''
      intros (k,e) (k',e') (k'',e'').elt:Type
k:key
e:elt
k':key
e':elt
k'':key
e'':elt
eqk (k, e) (k', e') ->
ltk (k', e') (k'', e'') -> ltk (k, e) (k'', e'')
      unfold ltk, eqk; simpl; eauto.
  Qed.
  Hint Resolve eqk_not_ltk : core.
  Hint Immediate ltk_eqk eqk_ltk : core.

  Lemma InA_eqke_eqk :
     forall x m, InA eqke x m -> InA eqk x m.elt:Type
forall (x : key * elt) (m : list (key * elt)),
InA eqke x m -> InA eqk x m
  Proof.elt:Type
forall (x : key * elt) (m : list (key * elt)),
InA eqke x m -> InA eqk x m
    unfold eqke; induction 1; intuition.
  Qed.
  Hint Resolve InA_eqke_eqk : core.

  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 : core.

  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)

  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.elt:Type
forall (k : key) (l : list (key * elt)),
In k l <-> (exists e : elt, InA eqk (k, e) l)
  Proof.elt:Type
forall (k : key) (l : list (key * elt)),
In k l <-> (exists e : elt, InA eqk (k, e) l)
  firstorder.elt:Type
k:key
l:list (key * elt)
x:elt
H:MapsTo k x l
exists e : elt, InA eqk (k, e) l
elt:Type
k:key
l:list (key * elt)
x:elt
H:InA eqk (k, x) l
In k l
  exists x; auto.elt:Type
k:key
l:list (key * elt)
x:elt
H:InA eqk (k, x) l
In k l
  induction H.elt:Type
k:key
x:elt
y:(key * elt)%type
l:list (key * elt)
H:eqk (k, x) y
In k (y :: l)
elt:Type
k:key
x:elt
y:(key * elt)%type
l:list (key * elt)
H:InA eqk (k, x) l
IHInA:In k l
In k (y :: l)
  destruct y.elt:Type
k:key
x:elt
t0:key
e:elt
l:list (key * elt)
H:eqk (k, x) (t0, e)
In k ((t0, e) :: l)
elt:Type
k:key
x:elt
y:(key * elt)%type
l:list (key * elt)
H:InA eqk (k, x) l
IHInA:In k l
In k (y :: l)
  exists e; auto.elt:Type
k:key
x:elt
y:(key * elt)%type
l:list (key * elt)
H:InA eqk (k, x) l
IHInA:In k l
In k (y :: l)
  destruct IHInA as [e H0].elt:Type
k:key
x:elt
y:(key * elt)%type
l:list (key * elt)
H:InA eqk (k, x) l
e:elt
H0:MapsTo k e l
In k (y :: l)
  exists e; auto.
  Qed.

  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.elt:Type
forall (l : list (key * elt)) (x y : key) (e : elt),
eq x y -> MapsTo x e l -> MapsTo y e l
  Proof.elt:Type
forall (l : list (key * elt)) (x y : key) (e : elt),
eq x y -> MapsTo x e l -> MapsTo y e l
  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *.
  Qed.

  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.elt:Type
forall (l : list (key * elt)) (x y : key),
eq x y -> In x l -> In y l
  Proof.elt:Type
forall (l : list (key * elt)) (x y : key),
eq x y -> In x l -> In y l
  destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto.
  Qed.

  Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.elt:Type
forall (l : list (key * elt)) (x x' : key * elt),
eqk x x' -> Inf x' l -> Inf x l
  Proof.elt:Type
forall (l : list (key * elt)) (x x' : key * elt),
eqk x x' -> Inf x' l -> Inf x l exact (InfA_eqA eqk_equiv ltk_compat). Qed.

  Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.elt:Type
forall (l : list (key * elt)) (x x' : key * elt),
ltk x x' -> Inf x' l -> Inf x l
  Proof.elt:Type
forall (l : list (key * elt)) (x x' : key * elt),
ltk x x' -> Inf x' l -> Inf x l exact (InfA_ltA ltk_strorder). Qed.

  Hint Immediate Inf_eq : core.
  Hint Resolve Inf_lt : core.

  Lemma Sort_Inf_In :
      forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.elt:Type
forall (l : list (key * elt)) (p q : key * elt),
Sort l -> Inf q l -> InA eqk p l -> ltk q p
  Proof.elt:Type
forall (l : list (key * elt)) (p q : key * elt),
Sort l -> Inf q l -> InA eqk p l -> ltk q p
  exact (SortA_InfA_InA eqk_equiv ltk_strorder ltk_compat).
  Qed.

  Lemma Sort_Inf_NotIn :
      forall l k e, Sort l -> Inf (k,e) l ->  ~In k l.elt:Type
forall (l : list (key * elt)) (k : key) (e : elt),
Sort l -> Inf (k, e) l -> ~ In k l
  Proof.elt:Type
forall (l : list (key * elt)) (k : key) (e : elt),
Sort l -> Inf (k, e) l -> ~ In k l
    intros; red; intros.elt:Type
l:list (key * elt)
k:key
e:elt
H:Sort l
H0:Inf (k, e) l
H1:In k l
False
    destruct H1 as [e' H2].elt:Type
l:list (key * elt)
k:key
e:elt
H:Sort l
H0:Inf (k, e) l
e':elt
H2:MapsTo k e' l
False
    elim (@ltk_not_eqk (k,e) (k,e')).elt:Type
l:list (key * elt)
k:key
e:elt
H:Sort l
H0:Inf (k, e) l
e':elt
H2:MapsTo k e' l
ltk (k, e) (k, e')
elt:Type
l:list (key * elt)
k:key
e:elt
H:Sort l
H0:Inf (k, e) l
e':elt
H2:MapsTo k e' l
eqk (k, e) (k, e')
    eapply Sort_Inf_In; eauto.elt:Type
l:list (key * elt)
k:key
e:elt
H:Sort l
H0:Inf (k, e) l
e':elt
H2:MapsTo k e' l
eqk (k, e) (k, e')
    red; simpl; auto.
  Qed.

  Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.elt:Type
forall l : list (key * elt), Sort l -> NoDupA eqk l
  Proof.elt:Type
forall l : list (key * elt), Sort l -> NoDupA eqk l
  exact (SortA_NoDupA eqk_equiv ltk_strorder ltk_compat).
  Qed.

  Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.elt:Type
forall (e : key * elt) (l : list (key * elt))
  (e' : key * elt),
Sort (e :: l) -> InA eqk e' l -> ltk e e'
  Proof.elt:Type
forall (e : key * elt) (l : list (key * elt))
  (e' : key * elt),
Sort (e :: l) -> InA eqk e' l -> ltk e e'
   inversion 1; intros; eapply Sort_Inf_In; eauto.
  Qed.

  Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
      ltk e e' \/ eqk e e'.elt:Type
forall (l : list (key * elt)) (e e' : key * elt),
Sort (e :: l) ->
InA eqk e' (e :: l) -> ltk e e' \/ eqk e e'
  Proof.elt:Type
forall (l : list (key * elt)) (e e' : key * elt),
Sort (e :: l) ->
InA eqk e' (e :: l) -> ltk e e' \/ eqk e e'
    inversion_clear 2; auto.elt:Type
l:list (key * elt)
e, e':(key * elt)%type
H:Sort (e :: l)
H1:InA eqk e' l
ltk e e' \/ eqk e e'
    left; apply Sort_In_cons_1 with l; auto.
  Qed.

  Lemma Sort_In_cons_3 :
    forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k.elt:Type
forall (x : key) (l : list (key * elt)) (k : key)
  (e : elt), Sort ((k, e) :: l) -> In x l -> ~ eq x k
  Proof.elt:Type
forall (x : key) (l : list (key * elt)) (k : key)
  (e : elt), Sort ((k, e) :: l) -> In x l -> ~ eq x k
    inversion_clear 1; red; intros.elt:Type
x:key
l:list (key * elt)
k:key
e:elt
H0:Sort l
H1:Inf (k, e) l
H:In x l
H2:eq x k
False
    destruct (Sort_Inf_NotIn H0 H1 (In_eq H2 H)).
  Qed.

  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.elt:Type
forall (k k' : key) (e : elt) (l : list (key * elt)),
In k ((k', e) :: l) -> eq k k' \/ In k l
  Proof.elt:Type
forall (k k' : key) (e : elt) (l : list (key * elt)),
In k ((k', e) :: l) -> eq k k' \/ In k l
    inversion 1.elt:Type
k, k':key
e:elt
l:list (key * elt)
H:In k ((k', e) :: l)
x:elt
H0:MapsTo k x ((k', e) :: l)
eq k k' \/ In k l
    inversion_clear H0; eauto.elt:Type
k, k':key
e:elt
l:list (key * elt)
H:In k ((k', e) :: l)
x:elt
H1:eqke (k, x) (k', e)
eq k k' \/ In k l
    destruct H1; simpl in *; intuition.
  Qed.

  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.elt:Type
forall (k k' : key) (e e' : elt)
  (l : list (key * elt)),
InA eqk (k, e) ((k', e') :: l) ->
~ eq k k' -> InA eqk (k, e) l
  Proof.elt:Type
forall (k k' : key) (e e' : elt)
  (l : list (key * elt)),
InA eqk (k, e) ((k', e') :: l) ->
~ eq k k' -> InA eqk (k, e) l
   inversion_clear 1; compute in H0; intuition.
  Qed.

  Lemma In_inv_3 : forall x x' l,
      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.elt:Type
forall (x x' : key * elt) (l : list (key * elt)),
InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l
  Proof.elt:Type
forall (x x' : key * elt) (l : list (key * elt)),
InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l
   inversion_clear 1; compute in H0; intuition.
  Qed.

 End Elt.

 Hint Unfold eqk eqke ltk : core.
 Hint Extern 2 (eqke ?a ?b) => split : core.
 Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
 Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core.
 Hint Immediate eqk_sym eqke_sym : core.
 Hint Resolve eqk_not_ltk : core.
 Hint Immediate ltk_eqk eqk_ltk : core.
 Hint Resolve InA_eqke_eqk : core.
 Hint Unfold MapsTo In : core.
 Hint Immediate Inf_eq : core.
 Hint Resolve Inf_lt : core.
 Hint Resolve Sort_Inf_NotIn : core.
 Hint Resolve In_inv_2 In_inv_3 : core.

End KeyOrderedType.