# Library Coq.Structures.DecidableType

Require Export SetoidList.
Require Equalities.
Set Implicit Arguments.
NB: This file is here only for compatibility with earlier version of FSets and FMap. Please use Structures/Equalities.v directly now.

# Types with Equalities, and nothing more (for subtyping purpose)

Module Type EqualityType := Equalities.EqualityTypeOrig.

# Types with decidable Equalities (but no ordering)

Module Type DecidableType := Equalities.DecidableTypeOrig.

# Additional notions about keys and datas used in FMap

Module KeyDecidableType(D:DecidableType).
Import D.
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').
Hint Unfold eqk eqke.
Hint Extern 2 (eqke ?a ?b) => split.
Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'.
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''.
Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
Hint Immediate eqk_sym eqke_sym.
Global Instance eqk_equiv : Equivalence eqk.
Global Instance eqke_equiv : Equivalence eqke.
Lemma InA_eqke_eqk :
forall x m, InA eqke x m -> InA eqk x m.
Hint Resolve InA_eqke_eqk.
Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
Definition In k m := exists e:elt, MapsTo k e m.
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 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.
Hint Extern 2 (eqke ?a ?b) => split.
Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
Hint Immediate eqk_sym eqke_sym.
Hint Resolve InA_eqke_eqk.
Hint Unfold MapsTo In.
Hint Resolve In_inv_2 In_inv_3.
End KeyDecidableType.