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
.