Require Import Equalities Bool SetoidList RelationPairs.

Set Implicit Arguments.

Module KeyDecidableType(D:DecidableType).

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

 Definition eqk {elt} : relation (key*elt) := D.eq @@1.
 Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq.

 #[global]
 Hint Unfold eqk eqke : core.

#[global]
 Instance eqk_equiv {elt} : Equivalence (@eqk elt) := _.

#[global]
 Instance eqke_equiv {elt} : Equivalence (@eqke elt) := _.

#[global]
 Instance eqke_eqk {elt} : subrelation (@eqke elt) (@eqk elt).

 Lemma eqke_def {elt} k k' (e e':elt) :
  eqke (k,e) (k',e') = (D.eq k k' /\ e = e').

 Lemma eqke_def' {elt} (p q:key*elt) :
  eqke p q = (D.eq (fst p) (fst q) /\ snd p = snd q).

 Lemma eqke_1 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> D.eq k k'.

 Lemma eqke_2 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> e=e'.

 Lemma eqk_def {elt} k k' (e e':elt) : eqk (k,e) (k',e') = D.eq k k'.

 Lemma eqk_def' {elt} (p q:key*elt) : eqk p q = D.eq (fst p) (fst q).

 Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'.

 #[global]
 Hint Resolve eqke_1 eqke_2 eqk_1 : core.


 Lemma InA_eqke_eqk {elt} p (m:list (key*elt)) :
   InA eqke p m -> InA eqk p m.
 #[global]
 Hint Resolve InA_eqke_eqk : core.

 Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) :
  InA eqk p m -> exists q, eqk p q /\ InA eqke q m.

 Lemma InA_eqk {elt} p q (m:list (key*elt)) :
   eqk p q -> InA eqk p m -> InA eqk q m.

 Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e).
 Definition In {elt} k m := exists e:elt, MapsTo k e m.

 #[global]
 Hint Unfold MapsTo In : core.


 Lemma In_alt {elt} k (l:list (key*elt)) :
   In k l <-> exists e, InA eqk (k,e) l.

 Lemma In_alt' {elt} (l:list (key*elt)) k e :
   In k l <-> InA eqk (k,e) l.

 Lemma In_alt2 {elt} k (l:list (key*elt)) :
   In k l <-> Exists (fun p => D.eq k (fst p)) l.

 Lemma In_nil {elt} k : In k (@nil (key*elt)) <-> False.

 Lemma In_cons {elt} k p (l:list (key*elt)) :
   In k (p::l) <-> D.eq k (fst p) \/ In k l.

#[global]
 Instance MapsTo_compat {elt} :
   Proper (D.eq==>Logic.eq==>equivlistA eqke==>iff) (@MapsTo elt).

#[global]
 Instance In_compat {elt} : Proper (D.eq==>equivlistA eqk==>iff) (@In elt).

 Lemma MapsTo_eq {elt} (l:list (key*elt)) x y e :
   D.eq x y -> MapsTo x e l -> MapsTo y e l.

 Lemma In_eq {elt} (l:list (key*elt)) x y :
   D.eq x y -> In x l -> In y l.

 Lemma In_inv {elt} k k' e (l:list (key*elt)) :
   In k ((k',e) :: l) -> D.eq k k' \/ In k l.

 Lemma In_inv_2 {elt} k k' e e' (l:list (key*elt)) :
   InA eqk (k, e) ((k', e') :: l) -> ~ D.eq k k' -> InA eqk (k, e) l.

 Lemma In_inv_3 {elt} x x' (l:list (key*elt)) :
   InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.

 #[global]
 Hint Extern 2 (eqke ?a ?b) => split : core.
 #[global]
 Hint Resolve InA_eqke_eqk : core.
 #[global]
 Hint Resolve In_inv_2 In_inv_3 : core.

End KeyDecidableType.

Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.

 Definition t := (D1.t * D2.t)%type.

 Definition eq := (D1.eq * D2.eq)%signature.

#[global]
 Instance eq_equiv : Equivalence eq := _.

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

End PairDecidableType.

Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
 Definition t := (D1.t * D2.t)%type.
 Definition eq := @eq t.
#[global]
 Instance eq_equiv : Equivalence eq := _.
 Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.

End PairUsualDecidableType.

Module PairUsualDecidableTypeFull (D1 D2:UsualDecidableTypeFull)
  <: UsualDecidableTypeFull.

 Module M := PairUsualDecidableType D1 D2.
 Include Backport_DT (M).
 Include HasEqDec2Bool.

End PairUsualDecidableTypeFull.