Library Coq.FSets.FMapAVL
FMapAVL
This module implements maps using AVL trees.
It follows the implementation from Ocaml's standard library.
See the comments at the beginning of FSetAVL for more details.
Notations and helper lemma about pairs
Notation "s #1" := (
fst s) (
at level 9,
format "s '#1'") :
pair_scope.
Notation "s #2" := (
snd s) (
at level 9,
format "s '#2'") :
pair_scope.
The Raw functor
Functor of pure functions + separate proofs of invariant
preservation
Module Raw (
Import I:
Int)(
X:
OrderedType).
Local Open Scope pair_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope Int_scope.
Definition key :=
X.t.
Hint Transparent key :
core.
Trees
Trees
The fifth field of
Node is the height of the tree
Basic functions on trees: height and cardinal
Membership
The
mem function is deciding membership. It exploits the
bst property
to achieve logarithmic complexity.
Helper functions
create l x r creates a node, assuming
l and
r
to be balanced and
|height l - height r| <= 2.
bal l x e r acts as create, but performs one step of
rebalancing if necessary, i.e. assumes |height l - height r| <= 3.
Extraction of minimum binding
Morally,
remove_min is to be applied to a non-empty tree
t = Node l x e r h. Since we can't deal here with
assert false
for
t=Leaf, we pre-unpack
t (and forget about
h).
Merging two trees
merge t1 t2 builds the union of
t1 and
t2 assuming all elements
of
t1 to be smaller than all elements of
t2, and
|height t1 - height t2| <= 2.
join
Same as
bal but does not assume anything regarding heights of
l
and
r.
Splitting
split x m returns a triple
(l, o, r) where
- l is the set of elements of m that are < x
- r is the set of elements of m that are > x
- o is the result of find x m.
Record triple :=
mktriple {
t_left:
t;
t_opt:
option elt;
t_right:
t }.
Notation "<< l , b , r >>" := (
mktriple l b r) (
at level 9).
Fixpoint split x m :
triple :=
match m with
|
Leaf =>
<< Leaf, None, Leaf >>
|
Node l y d r h =>
match X.compare x y with
|
LT _ =>
let (
ll,
o,
rl) :=
split x l in << ll, o, join rl y d r >>
|
EQ _ =>
<< l, Some d, r >>
|
GT _ =>
let (
rl,
o,
rr) :=
split x r in << join l y d rl, o, rr >>
end
end.
Concatenation
Same as
merge but does not assume anything about heights.
Elements
elements_tree_aux acc t catenates the elements of
t in infix
order to the list
acc
then elements is an instantiation with an empty acc
Enumeration of the elements of a tree
cons m e adds the elements of tree m on the head of
enumeration e.
One step of comparison of elements
Comparison of left tree, middle element, then right tree
Initial continuation
The complete comparison
Optimized map2
Suggestion by B. Gregoire: a
map2 function with specialized
arguments that allows bypassing some tree traversal. Instead of one
f0 of type
key -> option elt -> option elt' -> option elt'',
we ask here for:
- f which is a specialisation of f0 when first option isn't None
- mapl treats a tree elt with f0 when second option is None
- mapr treats a tree elt' with f0 when first option is None
The idea is that
mapl and
mapr can be instantaneous (e.g.
the identity or some constant function).
Map2
The
map2 function of the Map interface can be implemented
via
map2_opt and
map_option.
Binary search trees
lt_tree x s: all elements in
s are smaller than
x
(resp. greater for
gt_tree)
bst t : t is a binary search tree
Correctness proofs, isolated in a sub-module
Module Proofs.
Module MX :=
OrderedTypeFacts X.
Module PX :=
KeyOrderedType X.
Module L :=
FMapList.Raw X.
Functional Scheme mem_ind :=
Induction for mem Sort Prop.
Functional Scheme find_ind :=
Induction for find Sort Prop.
Functional Scheme bal_ind :=
Induction for bal Sort Prop.
Functional Scheme add_ind :=
Induction for add Sort Prop.
Functional Scheme remove_min_ind :=
Induction for remove_min Sort Prop.
Functional Scheme merge_ind :=
Induction for merge Sort Prop.
Functional Scheme remove_ind :=
Induction for remove Sort Prop.
Functional Scheme concat_ind :=
Induction for concat Sort Prop.
Functional Scheme split_ind :=
Induction for split Sort Prop.
Functional Scheme map_option_ind :=
Induction for map_option Sort Prop.
Functional Scheme map2_opt_ind :=
Induction for map2_opt Sort Prop.
Automation and dedicated tactics.
Hint Constructors tree MapsTo In bst :
core.
Hint Unfold lt_tree gt_tree :
core.
Tactic Notation "factornode"
ident(
l)
ident(
x)
ident(
d)
ident(
r)
ident(
h)
"as"
ident(
s) :=
set (
s:=
Node l x d r h)
in *;
clearbody s;
clear l x d r h.
A tactic for cleaning hypothesis after use of functional induction.
Ltac clearf :=
match goal with
|
H : (@
Logic.eq (
Compare _ _ _ _)
_ _) |-
_ =>
clear H;
clearf
|
H : (@
Logic.eq (
sumbool _ _)
_ _) |-
_ =>
clear H;
clearf
|
_ =>
idtac
end.
A tactic to repeat inversion_clear on all hyps of the
form (f (Node ...))
Ltac inv f :=
match goal with
|
H:
f (
Leaf _) |-
_ =>
inversion_clear H;
inv f
|
H:
f _ (
Leaf _) |-
_ =>
inversion_clear H;
inv f
|
H:
f _ _ (
Leaf _) |-
_ =>
inversion_clear H;
inv f
|
H:
f _ _ _ (
Leaf _) |-
_ =>
inversion_clear H;
inv f
|
H:
f (
Node _ _ _ _ _) |-
_ =>
inversion_clear H;
inv f
|
H:
f _ (
Node _ _ _ _ _) |-
_ =>
inversion_clear H;
inv f
|
H:
f _ _ (
Node _ _ _ _ _) |-
_ =>
inversion_clear H;
inv f
|
H:
f _ _ _ (
Node _ _ _ _ _) |-
_ =>
inversion_clear H;
inv f
|
_ =>
idtac
end.
Ltac inv_all f :=
match goal with
|
H:
f _ |-
_ =>
inversion_clear H;
inv f
|
H:
f _ _ |-
_ =>
inversion_clear H;
inv f
|
H:
f _ _ _ |-
_ =>
inversion_clear H;
inv f
|
H:
f _ _ _ _ |-
_ =>
inversion_clear H;
inv f
|
_ =>
idtac
end.
Helper tactic concerning order of elements.
Ltac order :=
match goal with
|
U:
lt_tree _ ?
s,
V:
In _ ?
s |-
_ =>
generalize (
U _ V);
clear U;
order
|
U:
gt_tree _ ?
s,
V:
In _ ?
s |-
_ =>
generalize (
U _ V);
clear U;
order
|
_ =>
MX.order
end.
Ltac intuition_in :=
repeat (
intuition;
inv In;
inv MapsTo).
Ltac join_tac :=
intros ?
l;
induction l as [| ?
ll _ ?
lx ?
ld ?
lr ?
Hlr ?
lh];
[ |
intros ?
x ?
d ?
r;
induction r as [| ?
rl ?
Hrl ?
rx ?
rd ?
rr _ ?
rh];
unfold join;
[ |
destruct (
gt_le_dec lh (
rh+2))
as [?
GT|?
LE];
[
match goal with |-
context [
bal ?
u ?
v ?
w ?
z ] =>
replace (
bal u v w z)
with (
bal ll lx ld (
join lr x d (
Node rl rx rd rr rh))); [ |
auto]
end
|
destruct (
gt_le_dec rh (
lh+2))
as [?
GT'|?
LE'];
[
match goal with |-
context [
bal ?
u ?
v ?
w ?
z ] =>
replace (
bal u v w z)
with (
bal (
join (
Node ll lx ld lr lh)
x d rl)
rx rd rr); [ |
auto]
end
| ] ] ] ];
intros.
Section Elt.
Variable elt:
Type.
Implicit Types m r :
t elt.
Basic results about MapsTo, In, lt_tree, gt_tree, height
Facts about
MapsTo and
In.
Results about lt_tree and gt_tree
Lemma lt_leaf :
forall x,
lt_tree x (
Leaf elt).
Lemma gt_leaf :
forall x,
gt_tree x (
Leaf elt).
Lemma lt_tree_node :
forall x y l r e h,
lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (
Node l y e r h).
Lemma gt_tree_node :
forall x y l r e h,
gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (
Node l y e r h).
Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node :
core.
Lemma lt_left :
forall x y l r e h,
lt_tree x (
Node l y e r h)
-> lt_tree x l.
Lemma lt_right :
forall x y l r e h,
lt_tree x (
Node l y e r h)
-> lt_tree x r.
Lemma gt_left :
forall x y l r e h,
gt_tree x (
Node l y e r h)
-> gt_tree x l.
Lemma gt_right :
forall x y l r e h,
gt_tree x (
Node l y e r h)
-> gt_tree x r.
Hint Resolve lt_left lt_right gt_left gt_right :
core.
Lemma lt_tree_not_in :
forall x m,
lt_tree x m -> ~ In x m.
Lemma lt_tree_trans :
forall x y,
X.lt x y -> forall m,
lt_tree x m -> lt_tree y m.
Lemma gt_tree_not_in :
forall x m,
gt_tree x m -> ~ In x m.
Lemma gt_tree_trans :
forall x y,
X.lt y x -> forall m,
gt_tree x m -> gt_tree y m.
Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans :
core.
Lemma mem_1 :
forall m x,
bst m -> In x m -> mem x m = true.
Lemma mem_2 :
forall m x,
mem x m = true -> In x m.
Lemma find_1 :
forall m x e,
bst m -> 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 find_iff :
forall m x e,
bst m ->
(find x m = Some e <-> MapsTo x e m).
Lemma find_in :
forall m x,
find x m <> None -> In x m.
Lemma in_find :
forall m x,
bst m -> In x m -> find x m <> None.
Lemma find_in_iff :
forall m x,
bst m ->
(find x m <> None <-> In x m).
Lemma not_find_iff :
forall m x,
bst m ->
(find x m = None <-> ~In x m).
Lemma find_find :
forall m m' x,
find x m = find x m' <->
(forall d,
find x m = Some d <-> find x m' = Some d).
Lemma find_mapsto_equiv :
forall m m' x,
bst m -> bst m' ->
(find x m = find x m' <->
(forall d,
MapsTo x d m <-> MapsTo x d m')).
Lemma find_in_equiv :
forall m m' x,
bst m -> bst m' ->
find x m = find x m' ->
(In x m <-> In x m').
Extraction of minimum binding
Notation eqk := (
PX.eqk (
elt:=
elt)).
Notation eqke := (
PX.eqke (
elt:=
elt)).
Notation ltk := (
PX.ltk (
elt:=
elt)).
Lemma elements_aux_mapsto :
forall (
s:
t elt)
acc x e,
InA eqke (x,e) (
elements_aux acc s)
<-> MapsTo x e s \/ InA eqke (x,e) acc.
Lemma elements_mapsto :
forall (
s:
t elt)
x e,
InA eqke (x,e) (
elements s)
<-> MapsTo x e s.
Lemma elements_in :
forall (
s:
t elt)
x,
L.PX.In x (
elements s)
<-> In x s.
Lemma elements_aux_sort :
forall (
s:
t elt)
acc,
bst s -> sort ltk acc ->
(forall x e y,
InA eqke (x,e) acc -> In y s -> X.lt y x) ->
sort ltk (
elements_aux acc s).
Lemma elements_sort :
forall s :
t elt,
bst s -> sort ltk (
elements s).
Hint Resolve elements_sort :
core.
Lemma elements_nodup :
forall s :
t elt,
bst s -> NoDupA eqk (
elements s).
Lemma elements_aux_cardinal :
forall (
m:
t elt)
acc, (
length acc + cardinal m)%
nat = length (
elements_aux acc m).
Lemma elements_cardinal :
forall (
m:
t elt),
cardinal m = length (
elements m).
Lemma elements_app :
forall (
s:
t elt)
acc,
elements_aux acc s = elements s ++ acc.
Lemma elements_node :
forall (
t1 t2:
t elt)
x e z l,
elements t1 ++ (x,e) :: elements t2 ++ l =
elements (
Node t1 x e t2 z)
++ l.
Comparison
flatten_e e returns the list of elements of the enumeration
e
i.e. the list of elements actually compared
Proof of correction for the comparison
Variable cmp :
elt->elt->bool.
Definition IfEq b l1 l2 :=
L.equal cmp l1 l2 = b.
Lemma cons_IfEq :
forall b x1 x2 d1 d2 l1 l2,
X.eq x1 x2 -> cmp d1 d2 = true ->
IfEq b l1 l2 ->
IfEq b (
(x1,d1)::l1) (
(x2,d2)::l2).
Lemma equal_end_IfEq :
forall e2,
IfEq (
equal_end e2)
nil (
flatten_e e2).
Lemma equal_more_IfEq :
forall x1 d1 (
cont:
enumeration elt -> bool)
x2 d2 r2 e2 l,
IfEq (
cont (
cons r2 e2))
l (
elements r2 ++ flatten_e e2)
->
IfEq (
equal_more cmp x1 d1 cont (
More x2 d2 r2 e2)) (
(x1,d1)::l)
(
flatten_e (
More x2 d2 r2 e2)).
Lemma equal_cont_IfEq :
forall m1 cont e2 l,
(forall e,
IfEq (
cont e)
l (
flatten_e e)
) ->
IfEq (
equal_cont cmp m1 cont e2) (
elements m1 ++ l) (
flatten_e e2).
Lemma equal_IfEq :
forall (
m1 m2:
t elt),
IfEq (
equal cmp m1 m2) (
elements m1) (
elements m2).
Definition Equivb 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 Equivb_elements :
forall s s',
Equivb s s' <-> L.Equivb cmp (
elements s) (
elements s').
Lemma equal_Equivb :
forall (
s s':
t elt),
bst s -> bst s' ->
(equal cmp s s' = true <-> Equivb s s').
End Elt.
Section Map.
Variable elt elt' :
Type.
Variable f :
elt -> elt'.
Lemma map_1 :
forall (
m:
t elt)(
x:
key)(
e:
elt),
MapsTo x e m -> MapsTo x (
f e) (
map f m).
Lemma map_2 :
forall (
m:
t elt)(
x:
key),
In x (
map f m)
-> In x m.
Lemma map_bst :
forall m,
bst m -> bst (
map f m).
End Map.
Section Mapi.
Variable elt elt' :
Type.
Variable f :
key -> elt -> elt'.
Lemma mapi_1 :
forall (
m:
tree elt)(
x:
key)(
e:
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),
In x (
mapi f m)
-> In x m.
Lemma mapi_bst :
forall m,
bst m -> bst (
mapi f m).
End Mapi.
Section Map_option.
Variable elt elt' :
Type.
Variable f :
key -> elt -> option elt'.
Hypothesis f_compat :
forall x x' d,
X.eq x x' -> f x d = f x' d.
Lemma map_option_2 :
forall (
m:
t elt)(
x:
key),
In x (
map_option f m)
-> exists d, MapsTo x d m /\ f x d <> None.
Lemma map_option_bst :
forall m,
bst m -> bst (
map_option f m).
Hint Resolve map_option_bst :
core.
Ltac nonify e :=
replace e with (@
None elt)
by
(
symmetry;
rewrite not_find_iff;
auto;
intro;
order).
Lemma map_option_find :
forall (
m:
t elt)(
x:
key),
bst m ->
find x (
map_option f m)
=
match (
find x m)
with Some d =>
f x d |
None =>
None end.
End Map_option.
Section Map2_opt.
Variable elt elt' elt'' :
Type.
Variable f0 :
key -> option elt -> option elt' -> option elt''.
Variable f :
key -> elt -> option elt' -> option elt''.
Variable mapl :
t elt -> t elt''.
Variable mapr :
t elt' -> t elt''.
Hypothesis f0_f :
forall x d o,
f x d o = f0 x (
Some d)
o.
Hypothesis mapl_bst :
forall m,
bst m -> bst (
mapl m).
Hypothesis mapr_bst :
forall m',
bst m' -> bst (
mapr m').
Hypothesis mapl_f0 :
forall x m,
bst m ->
find x (
mapl m)
=
match find x m with Some d =>
f0 x (
Some d)
None |
None =>
None end.
Hypothesis mapr_f0 :
forall x m',
bst m' ->
find x (
mapr m')
=
match find x m' with Some d' =>
f0 x None (
Some d') |
None =>
None end.
Hypothesis f0_compat :
forall x x' o o',
X.eq x x' -> f0 x o o' = f0 x' o o'.
Notation map2_opt := (
map2_opt f mapl mapr).
Lemma map2_opt_2 :
forall m m' y,
bst m -> bst m' ->
In y (
map2_opt m m')
-> In y m \/ In y m'.
Lemma map2_opt_bst :
forall m m',
bst m -> bst m' ->
bst (
map2_opt m m').
Hint Resolve map2_opt_bst :
core.
Ltac map2_aux :=
match goal with
|
H :
In ?
x _ \/ In ?
x ?
m,
H' :
find ?
x ?
m = find ?
x ?
m',
B:
bst ?
m,
B':
bst ?
m' |-
_ =>
destruct H; [
intuition_in;
order |
rewrite <-(
find_in_equiv B B' H');
auto ]
end.
Ltac nonify t :=
match t with (
find ?
y (
map2_opt ?
m ?
m')) =>
replace t with (@
None elt'');
[ |
symmetry;
rewrite not_find_iff;
auto;
intro;
destruct (@
map2_opt_2 m m' y);
auto;
order ]
end.
Lemma map2_opt_1 :
forall m m' y,
bst m -> bst m' ->
In y m \/ In y m' ->
find y (
map2_opt m m')
= f0 y (
find y m) (
find y m').
End Map2_opt.
Section Map2.
Variable elt elt' elt'' :
Type.
Variable f :
option elt -> option elt' -> option elt''.
Lemma map2_bst :
forall m m',
bst m -> bst m' -> bst (
map2 f m m').
Lemma map2_1 :
forall m m' y,
bst m -> bst m' ->
In y m \/ In y m' -> find y (
map2 f m m')
= f (
find y m) (
find y m').
Lemma map2_2 :
forall m m' y,
bst m -> bst m' ->
In y (
map2 f m m')
-> In y m \/ In y m'.
End Map2.
End Proofs.
End Raw.
Encapsulation
Now, in order to really provide a functor implementing
S, we
need to encapsulate everything into a type of balanced binary search trees.
Module IntMake (
I:
Int)(
X:
OrderedType) <:
S with Module E :=
X.
Module E :=
X.
Module Raw :=
Raw I X.
Import Raw.Proofs.
#[
universes(
template)]
Record bst (
elt:
Type) :=
Bst {
this :>
Raw.tree elt;
is_bst :
Raw.bst this}.
Definition t :=
bst.
Definition key :=
E.t.
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 :=
Bst (
empty_bst elt).
Definition is_empty m :
bool :=
Raw.is_empty (
this m).
Definition add x e m :
t elt :=
Bst (
add_bst x e (
is_bst m)).
Definition remove x m :
t elt :=
Bst (
remove_bst x (
is_bst m)).
Definition mem x m :
bool :=
Raw.mem x (
this m).
Definition find x m :
option elt :=
Raw.find x (
this m).
Definition map f m :
t elt' :=
Bst (
map_bst f (
is_bst m)).
Definition mapi (
f:
key->elt->elt')
m :
t elt' :=
Bst (
mapi_bst f (
is_bst m)).
Definition map2 f m (
m':
t elt') :
t elt'' :=
Bst (
map2_bst f (
is_bst m) (
is_bst m')).
Definition elements m :
list (
key*elt) :=
Raw.elements (
this m).
Definition cardinal m :=
Raw.cardinal (
this m).
Definition fold (
A:
Type) (
f:
key->elt->A->A)
m i :=
Raw.fold (
A:=
A)
f (
this m)
i.
Definition equal cmp m m' :
bool :=
Raw.equal cmp (
this m) (
this m').
Definition MapsTo x e m :
Prop :=
Raw.MapsTo x e (
this m).
Definition In x m :
Prop :=
Raw.In0 x (
this m).
Definition Empty m :
Prop :=
Empty (
this m).
Definition eq_key :
(key*elt) -> (key*elt) -> Prop := @
PX.eqk elt.
Definition eq_key_elt :
(key*elt) -> (key*elt) -> Prop := @
PX.eqke elt.
Definition lt_key :
(key*elt) -> (key*elt) -> Prop := @
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 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 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).
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 :=
Equiv (
Cmp cmp).
Lemma Equivb_Equivb :
forall cmp m m',
Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'.
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 IntMake.
Module IntMake_ord (
I:
Int)(
X:
OrderedType)(
D :
OrderedType) <:
Sord with Module Data :=
D
with Module MapS.E :=
X.
Module Data :=
D.
Module Import MapS :=
IntMake(
I)(
X).
Module LO :=
FMapList.Make_ord(
X)(
D).
Module R :=
Raw.
Module P :=
Raw.Proofs.
Definition t :=
MapS.t D.t.
Definition cmp e e' :=
match D.compare e e' with EQ _ =>
true |
_ =>
false end.
One step of comparison of elements
Comparison of left tree, middle element, then right tree
Initial continuation
The complete comparison
Correctness of this comparison
The dependent-style compare