Library Coq.Structures.EqualitiesFacts
Require
Import
Equalities
Bool
SetoidList
RelationPairs
.
Keys and datas used in FMap
Module
KeyDecidableType
(
Import
D
:
DecidableType
).
Section
Elt
.
Variable
elt
:
Type
.
Notation
key
:=
t
.
Local
Open
Scope
signature_scope
.
Definition
eqk
:
relation
(
key
*
elt
) :=
eq
@@1
.
Definition
eqke
:
relation
(
key
*
elt
) :=
eq
*
Logic.eq
.
Hint Unfold
eqk
eqke
.
Global Instance
eqke_eqk
:
subrelation
eqke
eqk
.
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
In_alt2
:
forall
k
l
,
In
k
l
<->
Exists
(
fun
p
=>
eq
k
(
fst
p
))
l
.
Lemma
In_nil
:
forall
k
,
In
k
nil
<->
False
.
Lemma
In_cons
:
forall
k
p
l
,
In
k
(
p
::
l
)
<->
eq
k
(
fst
p
)
\/
In
k
l
.
Global Instance
MapsTo_compat
:
Proper
(
eq
==>
Logic.eq
==>
equivlistA
eqke
==>
iff
)
MapsTo
.
Global Instance
In_compat
:
Proper
(
eq
==>
equivlistA
eqk
==>
iff
)
In
.
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
InA_eqke_eqk
.
Hint Unfold
MapsTo
In
.
Hint Resolve
In_inv_2
In_inv_3
.
End
KeyDecidableType
.
PairDecidableType
From two decidable types, we can build a new DecidableType over their cartesian product.
Module
PairDecidableType
(
D1
D2
:
DecidableType
) <:
DecidableType
.
Definition
t
:= (
D1.t
*
D2.t
)%
type
.
Definition
eq
:= (
D1.eq
*
D2.eq
)%
signature
.
Instance
eq_equiv
:
Equivalence
eq
:=
_
.
Definition
eq_dec
:
forall
x
y
,
{
eq
x
y
}+{
~
eq
x
y
}
.
End
PairDecidableType
.
Similarly for pairs of UsualDecidableType
Module
PairUsualDecidableType
(
D1
D2
:
UsualDecidableType
) <:
UsualDecidableType
.
Definition
t
:= (
D1.t
*
D2.t
)%
type
.
Definition
eq
:= @
eq
t
.
Instance
eq_equiv
:
Equivalence
eq
:=
_
.
Definition
eq_dec
:
forall
x
y
,
{
eq
x
y
}+{
~
eq
x
y
}
.
End
PairUsualDecidableType
.