(************************************************************************)
(*         *   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 RelationPairs SetoidList Orders EqualitiesFacts.

Set Implicit Arguments.
Unset Strict Implicit.

Module OrderedTypeLists (O:OrderedType).

Notation In:=(InA O.eq).
Notation Inf:=(lelistA O.lt).
Notation Sort:=(sort O.lt).
Notation NoDup:=(NoDupA O.eq).

Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
forall (l : list O.t) (x y : O.t),
x = y -> In x l -> In y l
Proof.
forall (l : list O.t) (x y : O.t),
x = y -> In x l -> In y l intros.
l:list O.t
x, y:O.t
H:x = y
H0:In x l
In y l rewrite <- H; auto. Qed.

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

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

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

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

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

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

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

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

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

End OrderedTypeLists.

Module KeyOrderedType(O:OrderedType).
 Include KeyDecidableType(O). (* provides eqk, eqke *)

 Notation key:=O.t.
 Local Open Scope signature_scope.

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

 Hint Unfold ltk : core.

 (* ltk is a strict order *)

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

 Instance ltk_compat {elt} : Proper (eqk==>eqk==>iff) (@ltk elt).
elt:Type
Proper (eqk ==> eqk ==> iff) ltk
 Proof.
elt:Type
Proper (eqk ==> eqk ==> iff) ltk unfold eqk, ltk; auto with *. Qed.

 Instance ltk_compat' {elt} : Proper (eqke==>eqke==>iff) (@ltk elt).
elt:Type
Proper (eqke ==> eqke ==> iff) ltk
 Proof.
elt:Type
Proper (eqke ==> eqke ==> iff) ltk eapply subrelation_proper; eauto with *. Qed.

 (* Additional facts *)

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

 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.
elt:Type
p, q:(key * elt)%type
ltk p q -> ~ eqk p q
  Proof.
elt:Type
p, q:(key * elt)%type
ltk p q -> ~ eqk p q
  intros LT EQ; rewrite EQ in LT.
elt:Type
p, q:(key * elt)%type
LT:ltk q q
EQ:eqk p q
False
  elim (StrictOrder_Irreflexive _ LT).
  Qed.

  Lemma ltk_not_eqke p q : ltk p q -> ~eqke p q.
elt:Type
p, q:(key * elt)%type
ltk p q -> ~ eqke p q
  Proof.
elt:Type
p, q:(key * elt)%type
ltk p q -> ~ eqke p q
  intros LT EQ; rewrite EQ in LT.
elt:Type
p, q:(key * elt)%type
LT:ltk q q
EQ:eqke p q
False
  elim (StrictOrder_Irreflexive _ LT).
  Qed.

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

  Lemma Inf_eq l x x' : eqk x x' -> Inf x' l -> Inf x l.
elt:Type
l:list (key * elt)
x, x':(key * elt)%type
eqk x x' -> Inf x' l -> Inf x l
  Proof.
elt:Type
l:list (key * elt)
x, x':(key * elt)%type
eqk x x' -> Inf x' l -> Inf x l now intros <-. Qed.

  Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l.
elt:Type
l:list (key * elt)
x, x':(key * elt)%type
ltk x x' -> Inf x' l -> Inf x l
  Proof.
elt:Type
l:list (key * elt)
x, x':(key * elt)%type
ltk x x' -> Inf x' l -> Inf x l apply InfA_ltA; auto with *. Qed.

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

  Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p.
elt:Type
l:list (key * elt)
p, q:(key * elt)%type
Sort l -> Inf q l -> InA eqk p l -> ltk q p
  Proof.
elt:Type
l:list (key * elt)
p, q:(key * elt)%type
Sort l -> Inf q l -> InA eqk p l -> ltk q p apply SortA_InfA_InA; auto with *. Qed.

  Lemma Sort_Inf_NotIn l k e : Sort l -> Inf (k,e) l ->  ~In k l.
elt:Type
l:list (key * elt)
k:key
e:elt
Sort l -> Inf (k, e) l -> ~ In k l
  Proof.
elt:Type
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')
    repeat red; reflexivity.
  Qed.

  Lemma Sort_NoDupA l : Sort l -> NoDupA eqk l.
elt:Type
l:list (key * elt)
Sort l -> NoDupA eqk l
  Proof.
elt:Type
l:list (key * elt)
Sort l -> NoDupA eqk l apply SortA_NoDupA; auto with *. Qed.

  Lemma Sort_In_cons_1 l p q : Sort (p::l) -> InA eqk q l -> ltk p q.
elt:Type
l:list (key * elt)
p, q:(key * elt)%type
Sort (p :: l) -> InA eqk q l -> ltk p q
  Proof.
elt:Type
l:list (key * elt)
p, q:(key * elt)%type
Sort (p :: l) -> InA eqk q l -> ltk p q
   intros; invlist sort; eapply Sort_Inf_In; eauto.
  Qed.

  Lemma Sort_In_cons_2 l p q : Sort (p::l) -> InA eqk q (p::l) ->
      ltk p q \/ eqk p q.
elt:Type
l:list (key * elt)
p, q:(key * elt)%type
Sort (p :: l) ->
InA eqk q (p :: l) -> ltk p q \/ eqk p q
  Proof.
elt:Type
l:list (key * elt)
p, q:(key * elt)%type
Sort (p :: l) ->
InA eqk q (p :: l) -> ltk p q \/ eqk p q
    intros; invlist InA; auto with relations.
elt:Type
l:list (key * elt)
p, q:(key * elt)%type
H:Sort (p :: l)
H1:InA eqk q l
ltk p q \/ eqk p q
    left; apply Sort_In_cons_1 with l; auto with relations.
  Qed.

  Lemma Sort_In_cons_3 x l k e :
    Sort ((k,e)::l) -> In x l -> ~O.eq x k.
elt:Type
x:key
l:list (key * elt)
k:key
e:elt
Sort ((k, e) :: l) -> In x l -> ~ O.eq x k
  Proof.
elt:Type
x:key
l:list (key * elt)
k:key
e:elt
Sort ((k, e) :: l) -> In x l -> ~ O.eq x k
    intros; invlist sort; red; intros.
elt:Type
x:key
l:list (key * elt)
k:key
e:elt
H0:In x l
H1:Sort l
H2:Inf (k, e) l
H:O.eq x k
False
    eapply Sort_Inf_NotIn; eauto using In_eq.
  Qed.

 End Elt.

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

End KeyOrderedType.