Library Coq.FSets.FMapWeakList
Finite map library
This file proposes an implementation of the non-dependent interface
FMapInterface.WS
using lists of pairs, unordered but without redundancy.
Require
Import
FunInd
FMapInterface
.
Set Implicit Arguments
.
Module
Raw
(
X
:
DecidableType
).
Module
Import
PX
:=
KeyDecidableType
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
MapsTo
:= (
MapsTo
(
elt
:=
elt
)).
Notation
In
:= (
In
(
elt
:=
elt
)).
Notation
NoDupA
:= (
NoDupA
eqk
).
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
:
core
.
Lemma
empty_NoDup
:
NoDupA
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
=>
if
X.eq_dec
k
k'
then
true
else
mem
k
l
end
.
Lemma
mem_1
:
forall
m
(
Hm
:
NoDupA
m
)
x
,
In
x
m
->
mem
x
m
=
true
.
Lemma
mem_2
:
forall
m
(
Hm
:
NoDupA
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'
=>
if
X.eq_dec
k
k'
then
Some
x
else
find
k
s'
end
.
Lemma
find_2
:
forall
m
x
e
,
find
x
m
=
Some
e
->
MapsTo
x
e
m
.
Lemma
find_1
:
forall
m
(
Hm
:
NoDupA
m
)
x
e
,
MapsTo
x
e
m
->
find
x
m
=
Some
e
.
Lemma
find_eq
:
forall
m
(
Hm
:
NoDupA
m
)
x
x'
,
X.eq
x
x'
->
find
x
m
=
find
x'
m
.
add
Function
add
(
k
:
key
) (
x
:
elt
) (
s
:
t
elt
) {
struct
s
} :
t
elt
:=
match
s
with
|
nil
=>
(
k
,
x
)
::
nil
|
(
k'
,
y
)
::
l
=>
if
X.eq_dec
k
k'
then
(
k
,
x
)
::
l
else
(
k'
,
y
)
::
add
k
x
l
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_3'
:
forall
m
x
y
e
e'
,
~
X.eq
x
y
->
InA
eqk
(
y
,
e
)
(
add
x
e'
m
)
->
InA
eqk
(
y
,
e
)
m
.
Lemma
add_NoDup
:
forall
m
(
Hm
:
NoDupA
m
)
x
e
,
NoDupA
(
add
x
e
m
).
Lemma
add_eq
:
forall
m
(
Hm
:
NoDupA
m
)
x
a
e
,
X.eq
x
a
->
find
x
(
add
a
e
m
)
=
Some
e
.
Lemma
add_not_eq
:
forall
m
(
Hm
:
NoDupA
m
)
x
a
e
,
~
X.eq
x
a
->
find
x
(
add
a
e
m
)
=
find
x
m
.
remove
Function
remove
(
k
:
key
) (
s
:
t
elt
) {
struct
s
} :
t
elt
:=
match
s
with
|
nil
=>
nil
|
(
k'
,
x
)
::
l
=>
if
X.eq_dec
k
k'
then
l
else
(
k'
,
x
)
::
remove
k
l
end
.
Lemma
remove_1
:
forall
m
(
Hm
:
NoDupA
m
)
x
y
,
X.eq
x
y
->
~
In
y
(
remove
x
m
).
Lemma
remove_2
:
forall
m
(
Hm
:
NoDupA
m
)
x
y
e
,
~
X.eq
x
y
->
MapsTo
y
e
m
->
MapsTo
y
e
(
remove
x
m
).
Lemma
remove_3
:
forall
m
(
Hm
:
NoDupA
m
)
x
y
e
,
MapsTo
y
e
(
remove
x
m
)
->
MapsTo
y
e
m
.
Lemma
remove_3'
:
forall
m
(
Hm
:
NoDupA
m
)
x
y
e
,
InA
eqk
(
y
,
e
)
(
remove
x
m
)
->
InA
eqk
(
y
,
e
)
m
.
Lemma
remove_NoDup
:
forall
m
(
Hm
:
NoDupA
m
)
x
,
NoDupA
(
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_3w
:
forall
m
(
Hm
:
NoDupA
m
),
NoDupA
(
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
Definition
check
(
cmp
:
elt
->
elt
->
bool
)(
k
:
key
)(
e
:
elt
)(
m'
:
t
elt
) :=
match
find
k
m'
with
|
None
=>
false
|
Some
e'
=>
cmp
e
e'
end
.
Definition
submap
(
cmp
:
elt
->
elt
->
bool
)(
m
m'
:
t
elt
) :
bool
:=
fold
(
fun
k
e
b
=>
andb
(
check
cmp
k
e
m'
)
b
)
m
true
.
Definition
equal
(
cmp
:
elt
->
elt
->
bool
)(
m
m'
:
t
elt
) :
bool
:=
andb
(
submap
cmp
m
m'
) (
submap
(
fun
e'
e
=>
cmp
e
e'
)
m'
m
).
Definition
Submap
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
)
.
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
submap_1
:
forall
m
(
Hm
:
NoDupA
m
)
m'
(
Hm'
:
NoDupA
m'
)
cmp
,
Submap
cmp
m
m'
->
submap
cmp
m
m'
=
true
.
Lemma
submap_2
:
forall
m
(
Hm
:
NoDupA
m
)
m'
(
Hm'
:
NoDupA
m'
)
cmp
,
submap
cmp
m
m'
=
true
->
Submap
cmp
m
m'
.
Specification of
equal
Lemma
equal_1
:
forall
m
(
Hm
:
NoDupA
m
)
m'
(
Hm'
:
NoDupA
m'
)
cmp
,
Equivb
cmp
m
m'
->
equal
cmp
m
m'
=
true
.
Lemma
equal_2
:
forall
m
(
Hm
:
NoDupA
m
)
m'
(
Hm'
:
NoDupA
m'
)
cmp
,
equal
cmp
m
m'
=
true
->
Equivb
cmp
m
m'
.
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_NoDup
:
forall
m
(
Hm
:
NoDupA
(@
eqk
elt
)
m
)(
f
:
elt
->
elt'
),
NoDupA
(@
eqk
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_NoDup
:
forall
m
(
Hm
:
NoDupA
(@
eqk
elt
)
m
)(
f
:
key
->
elt
->
elt'
),
NoDupA
(@
eqk
elt'
) (
mapi
f
m
).
End
Elt2
.
Section
Elt3
.
Variable
elt
elt'
elt''
:
Type
.
Notation
oee'
:= (
option
elt
*
option
elt'
)%
type
.
Definition
combine_l
(
m
:
t
elt
)(
m'
:
t
elt'
) :
t
oee'
:=
mapi
(
fun
k
e
=>
(
Some
e
,
find
k
m'
)
)
m
.
Definition
combine_r
(
m
:
t
elt
)(
m'
:
t
elt'
) :
t
oee'
:=
mapi
(
fun
k
e'
=>
(
find
k
m
,
Some
e'
)
)
m'
.
Definition
fold_right_pair
(
A
B
C
:
Type
)(
f
:
A
->
B
->
C
->
C
) :=
List.fold_right
(
fun
p
=>
f
(
fst
p
) (
snd
p
)).
Definition
combine
(
m
:
t
elt
)(
m'
:
t
elt'
) :
t
oee'
:=
let
l
:=
combine_l
m
m'
in
let
r
:=
combine_r
m
m'
in
fold_right_pair
(
add
(
elt
:=
oee'
))
r
l
.
Lemma
fold_right_pair_NoDup
:
forall
l
r
(
Hl
:
NoDupA
(
eqk
(
elt
:=
oee'
))
l
)
(
Hl
:
NoDupA
(
eqk
(
elt
:=
oee'
))
r
),
NoDupA
(
eqk
(
elt
:=
oee'
)) (
fold_right_pair
(
add
(
elt
:=
oee'
))
r
l
).
Hint Resolve
fold_right_pair_NoDup
:
core
.
Lemma
combine_NoDup
:
forall
m
(
Hm
:
NoDupA
(@
eqk
elt
)
m
)
m'
(
Hm'
:
NoDupA
(@
eqk
elt'
)
m'
),
NoDupA
(@
eqk
oee'
) (
combine
m
m'
).
Definition
at_least_left
(
o
:
option
elt
)(
o'
:
option
elt'
) :=
match
o
with
|
None
=>
None
|
_
=>
Some
(
o
,
o'
)
end
.
Definition
at_least_right
(
o
:
option
elt
)(
o'
:
option
elt'
) :=
match
o'
with
|
None
=>
None
|
_
=>
Some
(
o
,
o'
)
end
.
Lemma
combine_l_1
:
forall
m
(
Hm
:
NoDupA
(@
eqk
elt
)
m
)
m'
(
Hm'
:
NoDupA
(@
eqk
elt'
)
m'
)(
x
:
key
),
find
x
(
combine_l
m
m'
)
=
at_least_left
(
find
x
m
) (
find
x
m'
).
Lemma
combine_r_1
:
forall
m
(
Hm
:
NoDupA
(@
eqk
elt
)
m
)
m'
(
Hm'
:
NoDupA
(@
eqk
elt'
)
m'
)(
x
:
key
),
find
x
(
combine_r
m
m'
)
=
at_least_right
(
find
x
m
) (
find
x
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
:
NoDupA
(@
eqk
elt
)
m
)
m'
(
Hm'
:
NoDupA
(@
eqk
elt'
)
m'
)(
x
:
key
),
find
x
(
combine
m
m'
)
=
at_least_one
(
find
x
m
) (
find
x
m'
).
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
.
Definition
map2
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''
))
nil
m1
.
Lemma
map2_NoDup
:
forall
m
(
Hm
:
NoDupA
(@
eqk
elt
)
m
)
m'
(
Hm'
:
NoDupA
(@
eqk
elt'
)
m'
),
NoDupA
(@
eqk
elt''
) (
map2
m
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
:
NoDupA
(@
eqk
elt
)
m
)
m'
(
Hm'
:
NoDupA
(@
eqk
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
:
NoDupA
(@
eqk
elt
)
m
)
m'
(
Hm'
:
NoDupA
(@
eqk
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
:
NoDupA
(@
eqk
elt
)
m
)
m'
(
Hm'
:
NoDupA
(@
eqk
elt'
)
m'
)(
x
:
key
),
In
x
(
map2
m
m'
)
->
In
x
m
\/
In
x
m'
.
End
Elt3
.
End
Raw
.
Module
Make
(
X
:
DecidableType
) <:
WS
with
Module
E
:=
X
.
Module
Raw
:=
Raw
X
.
Module
E
:=
X
.
Definition
key
:=
E.t
.
Record
slist
(
elt
:
Type
) :=
{
this
:>
Raw.t
elt
;
NoDup
:
NoDupA
(@
Raw.PX.eqk
elt
)
this
}.
Definition
t
(
elt
:
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_NoDup
elt
).
Definition
is_empty
m
:
bool
:=
Raw.is_empty
(
this
m
).
Definition
add
x
e
m
:
t
elt
:=
Build_slist
(
Raw.add_NoDup
(
NoDup
m
)
x
e
).
Definition
find
x
m
:
option
elt
:=
Raw.find
x
(
this
m
).
Definition
remove
x
m
:
t
elt
:=
Build_slist
(
Raw.remove_NoDup
(
NoDup
m
)
x
).
Definition
mem
x
m
:
bool
:=
Raw.mem
x
(
this
m
).
Definition
map
f
m
:
t
elt'
:=
Build_slist
(
Raw.map_NoDup
(
NoDup
m
)
f
).
Definition
mapi
(
f
:
key
->
elt
->
elt'
)
m
:
t
elt'
:=
Build_slist
(
Raw.mapi_NoDup
(
NoDup
m
)
f
).
Definition
map2
f
m
(
m'
:
t
elt'
) :
t
elt''
:=
Build_slist
(
Raw.map2_NoDup
f
(
NoDup
m
) (
NoDup
m'
)).
Definition
elements
m
:
list
(
key
*
elt
) := @
Raw.elements
elt
(
this
m
).
Definition
cardinal
m
:=
length
(
this
m
).
Definition
fold
(
A
:
Type
)(
f
:
key
->
elt
->
A
->
A
)
m
(
i
:
A
) :
A
:= @
Raw.fold
elt
A
f
(
this
m
)
i
.
Definition
equal
cmp
m
m'
:
bool
:= @
Raw.equal
elt
cmp
(
this
m
) (
this
m'
).
Definition
MapsTo
x
e
m
:
Prop
:=
Raw.PX.MapsTo
x
e
(
this
m
).
Definition
In
x
m
:
Prop
:=
Raw.PX.In
x
(
this
m
).
Definition
Empty
m
:
Prop
:=
Raw.Empty
(
this
m
).
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
(
this
m
) (
this
m'
).
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
.
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_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
.