Library Coq.Structures.EqualitiesFacts
Require
Import
Equalities
Bool
SetoidList
RelationPairs
.
Set Implicit Arguments
.
Keys and datas used in the future MMaps
Module
KeyDecidableType
(
D
:
DecidableType
).
Local Open
Scope
signature_scope
.
Definition
eqk
{
elt
} :
relation
(
key
*
elt
) :=
D.eq
@@1
.
Definition
eqke
{
elt
} :
relation
(
key
*
elt
) :=
D.eq
*
Logic.eq
.
Hint Unfold
eqk
eqke
:
core
.
eqk, eqke are equalities
Instance
eqk_equiv
{
elt
} :
Equivalence
(@
eqk
elt
) :=
_
.
Instance
eqke_equiv
{
elt
} :
Equivalence
(@
eqke
elt
) :=
_
.
eqke is stricter than eqk
Instance
eqke_eqk
{
elt
} :
subrelation
(@
eqke
elt
) (@
eqk
elt
).
Alternative definitions of eqke and eqk
Lemma
eqke_def
{
elt
}
k
k'
(
e
e'
:
elt
) :
eqke
(
k
,
e
)
(
k'
,
e'
)
=
(
D.eq
k
k'
/\
e
=
e'
)
.
Lemma
eqke_def'
{
elt
} (
p
q
:
key
*
elt
) :
eqke
p
q
=
(
D.eq
(
fst
p
) (
fst
q
)
/\
snd
p
=
snd
q
)
.
Lemma
eqke_1
{
elt
}
k
k'
(
e
e'
:
elt
) :
eqke
(
k
,
e
)
(
k'
,
e'
)
->
D.eq
k
k'
.
Lemma
eqke_2
{
elt
}
k
k'
(
e
e'
:
elt
) :
eqke
(
k
,
e
)
(
k'
,
e'
)
->
e
=
e'
.
Lemma
eqk_def
{
elt
}
k
k'
(
e
e'
:
elt
) :
eqk
(
k
,
e
)
(
k'
,
e'
)
=
D.eq
k
k'
.
Lemma
eqk_def'
{
elt
} (
p
q
:
key
*
elt
) :
eqk
p
q
=
D.eq
(
fst
p
) (
fst
q
).
Lemma
eqk_1
{
elt
}
k
k'
(
e
e'
:
elt
) :
eqk
(
k
,
e
)
(
k'
,
e'
)
->
D.eq
k
k'
.
Hint Resolve
eqke_1
eqke_2
eqk_1
:
core
.
Lemma
InA_eqke_eqk
{
elt
}
p
(
m
:
list
(
key
*
elt
)) :
InA
eqke
p
m
->
InA
eqk
p
m
.
Hint Resolve
InA_eqke_eqk
:
core
.
Lemma
InA_eqk_eqke
{
elt
}
p
(
m
:
list
(
key
*
elt
)) :
InA
eqk
p
m
->
exists
q
,
eqk
p
q
/\
InA
eqke
q
m
.
Lemma
InA_eqk
{
elt
}
p
q
(
m
:
list
(
key
*
elt
)) :
eqk
p
q
->
InA
eqk
p
m
->
InA
eqk
q
m
.
Definition
MapsTo
{
elt
} (
k
:
key
)(
e
:
elt
):=
InA
eqke
(
k
,
e
)
.
Definition
In
{
elt
}
k
m
:=
exists
e
:
elt
,
MapsTo
k
e
m
.
Hint Unfold
MapsTo
In
:
core
.
Lemma
In_alt
{
elt
}
k
(
l
:
list
(
key
*
elt
)) :
In
k
l
<->
exists
e
,
InA
eqk
(
k
,
e
)
l
.
Lemma
In_alt'
{
elt
} (
l
:
list
(
key
*
elt
))
k
e
:
In
k
l
<->
InA
eqk
(
k
,
e
)
l
.
Lemma
In_alt2
{
elt
}
k
(
l
:
list
(
key
*
elt
)) :
In
k
l
<->
Exists
(
fun
p
=>
D.eq
k
(
fst
p
))
l
.
Lemma
In_nil
{
elt
}
k
:
In
k
(@
nil
(
key
*
elt
))
<->
False
.
Lemma
In_cons
{
elt
}
k
p
(
l
:
list
(
key
*
elt
)) :
In
k
(
p
::
l
)
<->
D.eq
k
(
fst
p
)
\/
In
k
l
.
Instance
MapsTo_compat
{
elt
} :
Proper
(
D.eq
==>
Logic.eq
==>
equivlistA
eqke
==>
iff
) (@
MapsTo
elt
).
Instance
In_compat
{
elt
} :
Proper
(
D.eq
==>
equivlistA
eqk
==>
iff
) (@
In
elt
).
Lemma
MapsTo_eq
{
elt
} (
l
:
list
(
key
*
elt
))
x
y
e
:
D.eq
x
y
->
MapsTo
x
e
l
->
MapsTo
y
e
l
.
Lemma
In_eq
{
elt
} (
l
:
list
(
key
*
elt
))
x
y
:
D.eq
x
y
->
In
x
l
->
In
y
l
.
Lemma
In_inv
{
elt
}
k
k'
e
(
l
:
list
(
key
*
elt
)) :
In
k
(
(
k'
,
e
)
::
l
)
->
D.eq
k
k'
\/
In
k
l
.
Lemma
In_inv_2
{
elt
}
k
k'
e
e'
(
l
:
list
(
key
*
elt
)) :
InA
eqk
(
k
,
e
)
(
(
k'
,
e'
)
::
l
)
->
~
D.eq
k
k'
->
InA
eqk
(
k
,
e
)
l
.
Lemma
In_inv_3
{
elt
}
x
x'
(
l
:
list
(
key
*
elt
)) :
InA
eqke
x
(
x'
::
l
)
->
~
eqk
x
x'
->
InA
eqke
x
l
.
Hint Extern
2 (
eqke
?
a
?
b
) =>
split
:
core
.
Hint Resolve
InA_eqke_eqk
:
core
.
Hint Resolve
In_inv_2
In_inv_3
:
core
.
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
.
And also for pairs of UsualDecidableTypeFull
Module
PairUsualDecidableTypeFull
(
D1
D2
:
UsualDecidableTypeFull
)
<:
UsualDecidableTypeFull
.
Module
M
:=
PairUsualDecidableType
D1
D2
.
Include
Backport_DT
(
M
).
Include
HasEqDec2Bool
.
End
PairUsualDecidableTypeFull
.