Library Coq.FSets.FMapList
Finite map library
This file proposes an implementation of the non-dependant interface
FMapInterface.S
using lists of pairs ordered (increasing) with respect to left projection.
Require
Import
FMapInterface
.
Set Implicit Arguments
.
Module
Raw
(
X
:
OrderedType
).
Module
Import
MX
:=
OrderedTypeFacts
X
.
Module
Import
PX
:=
KeyOrderedType
X
.
Definition
key
:=
X.t
.
Definition
t
(
elt
:
Type
) :=
list
(
X.t
*
elt
).
Section
Elt
.
Variable
elt
:
Type
.
Notation
eqk
:= (
eqk
(
elt
:=
elt
)).
Notation
eqke
:= (
eqke
(
elt
:=
elt
)).
Notation
ltk
:= (
ltk
(
elt
:=
elt
)).
Notation
MapsTo
:= (
MapsTo
(
elt
:=
elt
)).
Notation
In
:= (
In
(
elt
:=
elt
)).
Notation
Sort
:= (
sort
ltk
).
Notation
Inf
:= (
lelistA
(
ltk
)).
empty
Definition
empty
:
t
elt
:=
nil
.
Definition
Empty
m
:=
forall
(
a
:
key
)(
e
:
elt
) ,
~
MapsTo
a
e
m
.
Lemma
empty_1
:
Empty
empty
.
Hint Resolve
empty_1
.
Lemma
empty_sorted
:
Sort
empty
.
is_empty
Definition
is_empty
(
l
:
t
elt
) :
bool
:=
if
l
then
true
else
false
.
Lemma
is_empty_1
:
forall
m
,
Empty
m
->
is_empty
m
=
true
.
Lemma
is_empty_2
:
forall
m
,
is_empty
m
=
true
->
Empty
m
.
mem
Function
mem
(
k
:
key
) (
s
:
t
elt
) {
struct
s
} :
bool
:=
match
s
with
|
nil
=>
false
|
(
k´
,
_
)
::
l
=>
match
X.compare
k
k´
with
|
LT
_
=>
false
|
EQ
_
=>
true
|
GT
_
=>
mem
k
l
end
end
.
Lemma
mem_1
:
forall
m
(
Hm
:
Sort
m
)
x
,
In
x
m
->
mem
x
m
=
true
.
Lemma
mem_2
:
forall
m
(
Hm
:
Sort
m
)
x
,
mem
x
m
=
true
->
In
x
m
.
find
Function
find
(
k
:
key
) (
s
:
t
elt
) {
struct
s
} :
option
elt
:=
match
s
with
|
nil
=>
None
|
(
k´
,
x
)
::
s´
=>
match
X.compare
k
k´
with
|
LT
_
=>
None
|
EQ
_
=>
Some
x
|
GT
_
=>
find
k
s´
end
end
.
Lemma
find_2
:
forall
m
x
e
,
find
x
m
=
Some
e
->
MapsTo
x
e
m
.
Lemma
find_1
:
forall
m
(
Hm
:
Sort
m
)
x
e
,
MapsTo
x
e
m
->
find
x
m
=
Some
e
.
add
Function
add
(
k
:
key
) (
x
:
elt
) (
s
:
t
elt
) {
struct
s
} :
t
elt
:=
match
s
with
|
nil
=>
(
k
,
x
)
::
nil
|
(
k´
,
y
)
::
l
=>
match
X.compare
k
k´
with
|
LT
_
=>
(
k
,
x
)
::
s
|
EQ
_
=>
(
k
,
x
)
::
l
|
GT
_
=>
(
k´
,
y
)
::
add
k
x
l
end
end
.
Lemma
add_1
:
forall
m
x
y
e
,
X.eq
x
y
->
MapsTo
y
e
(
add
x
e
m
).
Lemma
add_2
:
forall
m
x
y
e
e´
,
~
X.eq
x
y
->
MapsTo
y
e
m
->
MapsTo
y
e
(
add
x
e´
m
).
Lemma
add_3
:
forall
m
x
y
e
e´
,
~
X.eq
x
y
->
MapsTo
y
e
(
add
x
e´
m
) ->
MapsTo
y
e
m
.
Lemma
add_Inf
:
forall
(
m
:
t
elt
)(
x
x´
:
key
)(
e
e´
:
elt
),
Inf
(
x´
,
e´
)
m
->
ltk
(
x´
,
e´
)
(
x
,
e
)
->
Inf
(
x´
,
e´
)
(
add
x
e
m
).
Hint Resolve
add_Inf
.
Lemma
add_sorted
:
forall
m
(
Hm
:
Sort
m
)
x
e
,
Sort
(
add
x
e
m
).
remove
Function
remove
(
k
:
key
) (
s
:
t
elt
) {
struct
s
} :
t
elt
:=
match
s
with
|
nil
=>
nil
|
(
k´
,
x
)
::
l
=>
match
X.compare
k
k´
with
|
LT
_
=>
s
|
EQ
_
=>
l
|
GT
_
=>
(
k´
,
x
)
::
remove
k
l
end
end
.
Lemma
remove_1
:
forall
m
(
Hm
:
Sort
m
)
x
y
,
X.eq
x
y
->
~
In
y
(
remove
x
m
).
Lemma
remove_2
:
forall
m
(
Hm
:
Sort
m
)
x
y
e
,
~
X.eq
x
y
->
MapsTo
y
e
m
->
MapsTo
y
e
(
remove
x
m
).
Lemma
remove_3
:
forall
m
(
Hm
:
Sort
m
)
x
y
e
,
MapsTo
y
e
(
remove
x
m
) ->
MapsTo
y
e
m
.
Lemma
remove_Inf
:
forall
(
m
:
t
elt
)(
Hm
:
Sort
m
)(
x
x´
:
key
)(
e´
:
elt
),
Inf
(
x´
,
e´
)
m
->
Inf
(
x´
,
e´
)
(
remove
x
m
).
Hint Resolve
remove_Inf
.
Lemma
remove_sorted
:
forall
m
(
Hm
:
Sort
m
)
x
,
Sort
(
remove
x
m
).
elements
Definition
elements
(
m
:
t
elt
) :=
m
.
Lemma
elements_1
:
forall
m
x
e
,
MapsTo
x
e
m
->
InA
eqke
(
x
,
e
)
(
elements
m
).
Lemma
elements_2
:
forall
m
x
e
,
InA
eqke
(
x
,
e
)
(
elements
m
) ->
MapsTo
x
e
m
.
Lemma
elements_3
:
forall
m
(
Hm
:
Sort
m
),
sort
ltk
(
elements
m
).
Lemma
elements_3w
:
forall
m
(
Hm
:
Sort
m
),
NoDupA
eqk
(
elements
m
).
fold
Function
fold
(
A
:
Type
)(
f
:
key
->
elt
->
A
->
A
)(
m
:
t
elt
) (
acc
:
A
) {
struct
m
} :
A
:=
match
m
with
|
nil
=>
acc
|
(
k
,
e
)
::
m´
=>
fold
f
m´
(
f
k
e
acc
)
end
.
Lemma
fold_1
:
forall
m
(
A
:
Type
)(
i
:
A
)(
f
:
key
->
elt
->
A
->
A
),
fold
f
m
i
=
fold_left
(
fun
a
p
=>
f
(
fst
p
) (
snd
p
)
a
) (
elements
m
)
i
.
equal
Function
equal
(
cmp
:
elt
->
elt
->
bool
)(
m
m´
:
t
elt
) {
struct
m
} :
bool
:=
match
m
,
m´
with
|
nil
,
nil
=>
true
|
(
x
,
e
)
::
l
,
(
x´
,
e´
)
::
l´
=>
match
X.compare
x
x´
with
|
EQ
_
=>
cmp
e
e´
&&
equal
cmp
l
l´
|
_
=>
false
end
|
_
,
_
=>
false
end
.
Definition
Equivb
cmp
m
m´
:=
(
forall
k
,
In
k
m
<->
In
k
m´
)
/\
(
forall
k
e
e´
,
MapsTo
k
e
m
->
MapsTo
k
e´
m´
->
cmp
e
e´
=
true
)
.
Lemma
equal_1
:
forall
m
(
Hm
:
Sort
m
)
m´
(
Hm´
:
Sort
m´
)
cmp
,
Equivb
cmp
m
m´
->
equal
cmp
m
m´
=
true
.
Lemma
equal_2
:
forall
m
(
Hm
:
Sort
m
)
m´
(
Hm
:
Sort
m´
)
cmp
,
equal
cmp
m
m´
=
true
->
Equivb
cmp
m
m´
.
This lemma isn't part of the spec of
Equivb
, but is used in
FMapAVL
Lemma
equal_cons
:
forall
cmp
l1
l2
x
y
,
Sort
(
x
::
l1
) ->
Sort
(
y
::
l2
) ->
eqk
x
y
->
cmp
(
snd
x
) (
snd
y
)
=
true
->
(
Equivb
cmp
l1
l2
<->
Equivb
cmp
(
x
::
l1
) (
y
::
l2
)).
Variable
elt´
:
Type
.
map
and
mapi
Fixpoint
map
(
f
:
elt
->
elt´
) (
m
:
t
elt
) :
t
elt´
:=
match
m
with
|
nil
=>
nil
|
(
k
,
e
)
::
m´
=>
(
k
,
f
e
)
::
map
f
m´
end
.
Fixpoint
mapi
(
f
:
key
->
elt
->
elt´
) (
m
:
t
elt
) :
t
elt´
:=
match
m
with
|
nil
=>
nil
|
(
k
,
e
)
::
m´
=>
(
k
,
f
k
e
)
::
mapi
f
m´
end
.
End
Elt
.
Section
Elt2
.
Variable
elt
elt´
:
Type
.
Specification of
map
Lemma
map_1
:
forall
(
m
:
t
elt
)(
x
:
key
)(
e
:
elt
)(
f
:
elt
->
elt´
),
MapsTo
x
e
m
->
MapsTo
x
(
f
e
) (
map
f
m
).
Lemma
map_2
:
forall
(
m
:
t
elt
)(
x
:
key
)(
f
:
elt
->
elt´
),
In
x
(
map
f
m
) ->
In
x
m
.
Lemma
map_lelistA
:
forall
(
m
:
t
elt
)(
x
:
key
)(
e
:
elt
)(
e´
:
elt´
)(
f
:
elt
->
elt´
),
lelistA
(@
ltk
elt
)
(
x
,
e
)
m
->
lelistA
(@
ltk
elt´
)
(
x
,
e´
)
(
map
f
m
).
Hint Resolve
map_lelistA
.
Lemma
map_sorted
:
forall
(
m
:
t
elt
)(
Hm
:
sort
(@
ltk
elt
)
m
)(
f
:
elt
->
elt´
),
sort
(@
ltk
elt´
) (
map
f
m
).
Specification of
mapi
Lemma
mapi_1
:
forall
(
m
:
t
elt
)(
x
:
key
)(
e
:
elt
)(
f
:
key
->
elt
->
elt´
),
MapsTo
x
e
m
->
exists
y
,
X.eq
y
x
/\
MapsTo
x
(
f
y
e
) (
mapi
f
m
).
Lemma
mapi_2
:
forall
(
m
:
t
elt
)(
x
:
key
)(
f
:
key
->
elt
->
elt´
),
In
x
(
mapi
f
m
) ->
In
x
m
.
Lemma
mapi_lelistA
:
forall
(
m
:
t
elt
)(
x
:
key
)(
e
:
elt
)(
f
:
key
->
elt
->
elt´
),
lelistA
(@
ltk
elt
)
(
x
,
e
)
m
->
lelistA
(@
ltk
elt´
)
(
x
,
f
x
e
)
(
mapi
f
m
).
Hint Resolve
mapi_lelistA
.
Lemma
mapi_sorted
:
forall
m
(
Hm
:
sort
(@
ltk
elt
)
m
)(
f
:
key
->
elt
->
elt´
),
sort
(@
ltk
elt´
) (
mapi
f
m
).
End
Elt2
.
Section
Elt3
.
map2
Variable
elt
elt´
elt´´
:
Type
.
Variable
f
:
option
elt
->
option
elt´
->
option
elt´´
.
Definition
option_cons
(
A
:
Type
)(
k
:
key
)(
o
:
option
A
)(
l
:
list
(
key
*
A
)) :=
match
o
with
|
Some
e
=>
(
k
,
e
)
::
l
|
None
=>
l
end
.
Fixpoint
map2_l
(
m
:
t
elt
) :
t
elt´´
:=
match
m
with
|
nil
=>
nil
|
(
k
,
e
)
::
l
=>
option_cons
k
(
f
(
Some
e
)
None
) (
map2_l
l
)
end
.
Fixpoint
map2_r
(
m´
:
t
elt´
) :
t
elt´´
:=
match
m´
with
|
nil
=>
nil
|
(
k
,
e´
)
::
l´
=>
option_cons
k
(
f
None
(
Some
e´
)) (
map2_r
l´
)
end
.
Fixpoint
map2
(
m
:
t
elt
) :
t
elt´
->
t
elt´´
:=
match
m
with
|
nil
=>
map2_r
|
(
k
,
e
)
::
l
=>
fix
map2_aux
(
m´
:
t
elt´
) :
t
elt´´
:=
match
m´
with
|
nil
=>
map2_l
m
|
(
k´
,
e´
)
::
l´
=>
match
X.compare
k
k´
with
|
LT
_
=>
option_cons
k
(
f
(
Some
e
)
None
) (
map2
l
m´
)
|
EQ
_
=>
option_cons
k
(
f
(
Some
e
) (
Some
e´
)) (
map2
l
l´
)
|
GT
_
=>
option_cons
k´
(
f
None
(
Some
e´
)) (
map2_aux
l´
)
end
end
end
.
Notation
oee´
:= (
option
elt
*
option
elt´
)%
type
.
Fixpoint
combine
(
m
:
t
elt
) :
t
elt´
->
t
oee´
:=
match
m
with
|
nil
=>
map
(
fun
e´
=>
(
None
,
Some
e´
)
)
|
(
k
,
e
)
::
l
=>
fix
combine_aux
(
m´
:
t
elt´
) :
list
(
key
*
oee´
) :=
match
m´
with
|
nil
=>
map
(
fun
e
=>
(
Some
e
,
None
)
)
m
|
(
k´
,
e´
)
::
l´
=>
match
X.compare
k
k´
with
|
LT
_
=>
(
k
,(
Some
e
,
None
))
::
combine
l
m´
|
EQ
_
=>
(
k
,(
Some
e
,
Some
e´
))
::
combine
l
l´
|
GT
_
=>
(
k´
,(
None
,
Some
e´
))
::
combine_aux
l´
end
end
end
.
Definition
fold_right_pair
(
A
B
C
:
Type
)(
f
:
A
->
B
->
C
->
C
)(
l
:
list
(
A
*
B
))(
i
:
C
) :=
List.fold_right
(
fun
p
=>
f
(
fst
p
) (
snd
p
))
i
l
.
Definition
map2_alt
m
m´
:=
let
m0
:
t
oee´
:=
combine
m
m´
in
let
m1
:
t
(
option
elt´´
) :=
map
(
fun
p
=>
f
(
fst
p
) (
snd
p
))
m0
in
fold_right_pair
(
option_cons
(
A
:=
elt´´
))
m1
nil
.
Lemma
map2_alt_equiv
:
forall
m
m´
,
map2_alt
m
m´
=
map2
m
m´
.
Lemma
combine_lelistA
:
forall
m
m´
(
x
:
key
)(
e
:
elt
)(
e´
:
elt´
)(
e´´
:
oee´
),
lelistA
(@
ltk
elt
)
(
x
,
e
)
m
->
lelistA
(@
ltk
elt´
)
(
x
,
e´
)
m´
->
lelistA
(@
ltk
oee´
)
(
x
,
e´´
)
(
combine
m
m´
).
Hint Resolve
combine_lelistA
.
Lemma
combine_sorted
:
forall
m
(
Hm
:
sort
(@
ltk
elt
)
m
)
m´
(
Hm´
:
sort
(@
ltk
elt´
)
m´
),
sort
(@
ltk
oee´
) (
combine
m
m´
).
Lemma
map2_sorted
:
forall
m
(
Hm
:
sort
(@
ltk
elt
)
m
)
m´
(
Hm´
:
sort
(@
ltk
elt´
)
m´
),
sort
(@
ltk
elt´´
) (
map2
m
m´
).
Definition
at_least_one
(
o
:
option
elt
)(
o´
:
option
elt´
) :=
match
o
,
o´
with
|
None
,
None
=>
None
|
_
,
_
=>
Some
(
o
,
o´
)
end
.
Lemma
combine_1
:
forall
m
(
Hm
:
sort
(@
ltk
elt
)
m
)
m´
(
Hm´
:
sort
(@
ltk
elt´
)
m´
) (
x
:
key
),
find
x
(
combine
m
m´
)
=
at_least_one
(
find
x
m
) (
find
x
m´
).
Definition
at_least_one_then_f
(
o
:
option
elt
)(
o´
:
option
elt´
) :=
match
o
,
o´
with
|
None
,
None
=>
None
|
_
,
_
=>
f
o
o´
end
.
Lemma
map2_0
:
forall
m
(
Hm
:
sort
(@
ltk
elt
)
m
)
m´
(
Hm´
:
sort
(@
ltk
elt´
)
m´
) (
x
:
key
),
find
x
(
map2
m
m´
)
=
at_least_one_then_f
(
find
x
m
) (
find
x
m´
).
Specification of
map2
Lemma
map2_1
:
forall
m
(
Hm
:
sort
(@
ltk
elt
)
m
)
m´
(
Hm´
:
sort
(@
ltk
elt´
)
m´
)(
x
:
key
),
In
x
m
\/
In
x
m´
->
find
x
(
map2
m
m´
)
=
f
(
find
x
m
) (
find
x
m´
).
Lemma
map2_2
:
forall
m
(
Hm
:
sort
(@
ltk
elt
)
m
)
m´
(
Hm´
:
sort
(@
ltk
elt´
)
m´
)(
x
:
key
),
In
x
(
map2
m
m´
) ->
In
x
m
\/
In
x
m´
.
End
Elt3
.
End
Raw
.
Module
Make
(
X
:
OrderedType
) <:
S
with
Module
E
:=
X
.
Module
Raw
:=
Raw
X
.
Module
E
:=
X
.
Definition
key
:=
E.t
.
Record
slist
(
elt
:
Type
) :=
{
this
:>
Raw.t
elt
;
sorted
:
sort
(@
Raw.PX.ltk
elt
)
this
}.
Definition
t
(
elt
:
Type
) :
Type
:=
slist
elt
.
Section
Elt
.
Variable
elt
elt´
elt´´
:
Type
.
Implicit
Types
m
:
t
elt
.
Implicit
Types
x
y
:
key
.
Implicit
Types
e
:
elt
.
Definition
empty
:
t
elt
:=
Build_slist
(
Raw.empty_sorted
elt
).
Definition
is_empty
m
:
bool
:=
Raw.is_empty
m
.(
this
).
Definition
add
x
e
m
:
t
elt
:=
Build_slist
(
Raw.add_sorted
m
.(
sorted
)
x
e
).
Definition
find
x
m
:
option
elt
:=
Raw.find
x
m
.(
this
).
Definition
remove
x
m
:
t
elt
:=
Build_slist
(
Raw.remove_sorted
m
.(
sorted
)
x
).
Definition
mem
x
m
:
bool
:=
Raw.mem
x
m
.(
this
).
Definition
map
f
m
:
t
elt´
:=
Build_slist
(
Raw.map_sorted
m
.(
sorted
)
f
).
Definition
mapi
(
f
:
key
->
elt
->
elt´
)
m
:
t
elt´
:=
Build_slist
(
Raw.mapi_sorted
m
.(
sorted
)
f
).
Definition
map2
f
m
(
m´
:
t
elt´
) :
t
elt´´
:=
Build_slist
(
Raw.map2_sorted
f
m
.(
sorted
)
m´
.(
sorted
)).
Definition
elements
m
:
list
(
key
*
elt
) := @
Raw.elements
elt
m
.(
this
).
Definition
cardinal
m
:=
length
m
.(
this
).
Definition
fold
(
A
:
Type
)(
f
:
key
->
elt
->
A
->
A
)
m
(
i
:
A
) :
A
:= @
Raw.fold
elt
A
f
m
.(
this
)
i
.
Definition
equal
cmp
m
m´
:
bool
:= @
Raw.equal
elt
cmp
m
.(
this
)
m´
.(
this
).
Definition
MapsTo
x
e
m
:
Prop
:=
Raw.PX.MapsTo
x
e
m
.(
this
).
Definition
In
x
m
:
Prop
:=
Raw.PX.In
x
m
.(
this
).
Definition
Empty
m
:
Prop
:=
Raw.Empty
m
.(
this
).
Definition
Equal
m
m´
:=
forall
y
,
find
y
m
=
find
y
m´
.
Definition
Equiv
(
eq_elt
:
elt
->
elt
->
Prop
)
m
m´
:=
(
forall
k
,
In
k
m
<->
In
k
m´
)
/\
(
forall
k
e
e´
,
MapsTo
k
e
m
->
MapsTo
k
e´
m´
->
eq_elt
e
e´
)
.
Definition
Equivb
cmp
m
m´
:
Prop
:= @
Raw.Equivb
elt
cmp
m
.(
this
)
m´
.(
this
).
Definition
eq_key
: (
key
*
elt
) -> (
key
*
elt
) ->
Prop
:= @
Raw.PX.eqk
elt
.
Definition
eq_key_elt
: (
key
*
elt
) -> (
key
*
elt
) ->
Prop
:= @
Raw.PX.eqke
elt
.
Definition
lt_key
: (
key
*
elt
) -> (
key
*
elt
) ->
Prop
:= @
Raw.PX.ltk
elt
.
Lemma
MapsTo_1
:
forall
m
x
y
e
,
E.eq
x
y
->
MapsTo
x
e
m
->
MapsTo
y
e
m
.
Lemma
mem_1
:
forall
m
x
,
In
x
m
->
mem
x
m
=
true
.
Lemma
mem_2
:
forall
m
x
,
mem
x
m
=
true
->
In
x
m
.
Lemma
empty_1
:
Empty
empty
.
Lemma
is_empty_1
:
forall
m
,
Empty
m
->
is_empty
m
=
true
.
Lemma
is_empty_2
:
forall
m
,
is_empty
m
=
true
->
Empty
m
.
Lemma
add_1
:
forall
m
x
y
e
,
E.eq
x
y
->
MapsTo
y
e
(
add
x
e
m
).
Lemma
add_2
:
forall
m
x
y
e
e´
,
~
E.eq
x
y
->
MapsTo
y
e
m
->
MapsTo
y
e
(
add
x
e´
m
).
Lemma
add_3
:
forall
m
x
y
e
e´
,
~
E.eq
x
y
->
MapsTo
y
e
(
add
x
e´
m
) ->
MapsTo
y
e
m
.
Lemma
remove_1
:
forall
m
x
y
,
E.eq
x
y
->
~
In
y
(
remove
x
m
).
Lemma
remove_2
:
forall
m
x
y
e
,
~
E.eq
x
y
->
MapsTo
y
e
m
->
MapsTo
y
e
(
remove
x
m
).
Lemma
remove_3
:
forall
m
x
y
e
,
MapsTo
y
e
(
remove
x
m
) ->
MapsTo
y
e
m
.
Lemma
find_1
:
forall
m
x
e
,
MapsTo
x
e
m
->
find
x
m
=
Some
e
.
Lemma
find_2
:
forall
m
x
e
,
find
x
m
=
Some
e
->
MapsTo
x
e
m
.
Lemma
elements_1
:
forall
m
x
e
,
MapsTo
x
e
m
->
InA
eq_key_elt
(
x
,
e
)
(
elements
m
).
Lemma
elements_2
:
forall
m
x
e
,
InA
eq_key_elt
(
x
,
e
)
(
elements
m
) ->
MapsTo
x
e
m
.
Lemma
elements_3
:
forall
m
,
sort
lt_key
(
elements
m
).
Lemma
elements_3w
:
forall
m
,
NoDupA
eq_key
(
elements
m
).
Lemma
cardinal_1
:
forall
m
,
cardinal
m
=
length
(
elements
m
).
Lemma
fold_1
:
forall
m
(
A
:
Type
) (
i
:
A
) (
f
:
key
->
elt
->
A
->
A
),
fold
f
m
i
=
fold_left
(
fun
a
p
=>
f
(
fst
p
) (
snd
p
)
a
) (
elements
m
)
i
.
Lemma
equal_1
:
forall
m
m´
cmp
,
Equivb
cmp
m
m´
->
equal
cmp
m
m´
=
true
.
Lemma
equal_2
:
forall
m
m´
cmp
,
equal
cmp
m
m´
=
true
->
Equivb
cmp
m
m´
.
End
Elt
.
Lemma
map_1
:
forall
(
elt
elt´
:
Type
)(
m
:
t
elt
)(
x
:
key
)(
e
:
elt
)(
f
:
elt
->
elt´
),
MapsTo
x
e
m
->
MapsTo
x
(
f
e
) (
map
f
m
).
Lemma
map_2
:
forall
(
elt
elt´
:
Type
)(
m
:
t
elt
)(
x
:
key
)(
f
:
elt
->
elt´
),
In
x
(
map
f
m
) ->
In
x
m
.
Lemma
mapi_1
:
forall
(
elt
elt´
:
Type
)(
m
:
t
elt
)(
x
:
key
)(
e
:
elt
)
(
f
:
key
->
elt
->
elt´
),
MapsTo
x
e
m
->
exists
y
,
E.eq
y
x
/\
MapsTo
x
(
f
y
e
) (
mapi
f
m
).
Lemma
mapi_2
:
forall
(
elt
elt´
:
Type
)(
m
:
t
elt
)(
x
:
key
)
(
f
:
key
->
elt
->
elt´
),
In
x
(
mapi
f
m
) ->
In
x
m
.
Lemma
map2_1
:
forall
(
elt
elt´
elt´´
:
Type
)(
m
:
t
elt
)(
m´
:
t
elt´
)
(
x
:
key
)(
f
:
option
elt
->
option
elt´
->
option
elt´´
),
In
x
m
\/
In
x
m´
->
find
x
(
map2
f
m
m´
)
=
f
(
find
x
m
) (
find
x
m´
).
Lemma
map2_2
:
forall
(
elt
elt´
elt´´
:
Type
)(
m
:
t
elt
)(
m´
:
t
elt´
)
(
x
:
key
)(
f
:
option
elt
->
option
elt´
->
option
elt´´
),
In
x
(
map2
f
m
m´
) ->
In
x
m
\/
In
x
m´
.
End
Make
.
Module
Make_ord
(
X
:
OrderedType
)(
D
:
OrderedType
) <:
Sord
with
Module
Data
:=
D
with
Module
MapS.E
:=
X
.
Module
Data
:=
D
.
Module
MapS
:=
Make
(
X
).
Import
MapS
.
Module
MD
:=
OrderedTypeFacts
(
D
).
Import
MD
.
Definition
t
:=
MapS.t
D.t
.
Definition
cmp
e
e´
:=
match
D.compare
e
e´
with
EQ
_
=>
true
|
_
=>
false
end
.
Fixpoint
eq_list
(
m
m´
:
list
(
X.t
*
D.t
)) :
Prop
:=
match
m
,
m´
with
|
nil
,
nil
=>
True
|
(
x
,
e
)
::
l
,
(
x´
,
e´
)
::
l´
=>
match
X.compare
x
x´
with
|
EQ
_
=>
D.eq
e
e´
/\
eq_list
l
l´
|
_
=>
False
end
|
_
,
_
=>
False
end
.
Definition
eq
m
m´
:=
eq_list
m
.(
this
)
m´
.(
this
).
Fixpoint
lt_list
(
m
m´
:
list
(
X.t
*
D.t
)) :
Prop
:=
match
m
,
m´
with
|
nil
,
nil
=>
False
|
nil
,
_
=>
True
|
_
,
nil
=>
False
|
(
x
,
e
)
::
l
,
(
x´
,
e´
)
::
l´
=>
match
X.compare
x
x´
with
|
LT
_
=>
True
|
GT
_
=>
False
|
EQ
_
=>
D.lt
e
e´
\/
(
D.eq
e
e´
/\
lt_list
l
l´
)
end
end
.
Definition
lt
m
m´
:=
lt_list
m
.(
this
)
m´
.(
this
).
Lemma
eq_equal
:
forall
m
m´
,
eq
m
m´
<->
equal
cmp
m
m´
=
true
.
Lemma
eq_1
:
forall
m
m´
,
Equivb
cmp
m
m´
->
eq
m
m´
.
Lemma
eq_2
:
forall
m
m´
,
eq
m
m´
->
Equivb
cmp
m
m´
.
Lemma
eq_refl
:
forall
m
:
t
,
eq
m
m
.
Lemma
eq_sym
:
forall
m1
m2
:
t
,
eq
m1
m2
->
eq
m2
m1
.
Lemma
eq_trans
:
forall
m1
m2
m3
:
t
,
eq
m1
m2
->
eq
m2
m3
->
eq
m1
m3
.
Lemma
lt_trans
:
forall
m1
m2
m3
:
t
,
lt
m1
m2
->
lt
m2
m3
->
lt
m1
m3
.
Lemma
lt_not_eq
:
forall
m1
m2
:
t
,
lt
m1
m2
->
~
eq
m1
m2
.
Ltac
cmp_solve
:=
unfold
eq
,
lt
;
simpl
;
try
Raw.MX.elim_comp
;
auto
.
Definition
compare
:
forall
m1
m2
,
Compare
lt
eq
m1
m2
.
End
Make_ord
.