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.