Library Coq.Structures.DecidableType
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)
Types with decidable Equalities (but no ordering)
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.