Library Coq.Logic.DecidableType
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.
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.