# Library Coq.Structures.EqualitiesFacts

Require Import Equalities Bool SetoidList RelationPairs.

Set Implicit Arguments.

# Keys and datas used in the future MMaps

Module KeyDecidableType(D:DecidableType).

Local Open Scope signature_scope.

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

Hint Unfold eqk eqke.

eqk, eqke are equalities

Instance eqk_equiv {elt} : Equivalence (@eqk elt) := _.

Instance eqke_equiv {elt} : Equivalence (@eqke elt) := _.

eqke is stricter than eqk

Instance eqke_eqk {elt} : subrelation (@eqke elt) (@eqk elt).

Alternative definitions of eqke and eqk

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

Hint Resolve eqke_1 eqke_2 eqk_1.

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

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.

Hint Unfold MapsTo In.

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.

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

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.

Hint Extern 2 (eqke ?a ?b) => split.
Hint Resolve InA_eqke_eqk.
Hint Resolve In_inv_2 In_inv_3.

End KeyDecidableType.

# PairDecidableType

From two decidable types, we can build a new DecidableType over their cartesian product.

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

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

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

Instance eq_equiv : Equivalence eq := _.

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

End PairDecidableType.

Similarly for pairs of UsualDecidableType

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

End PairUsualDecidableType.