Library Coq.FSets.FMapPositive
FMapPositive : an implementation of FMapInterface for positive keys.
This file is an adaptation to the FMap framework of a work by
Xavier Leroy and Sandrine Blazy (used for building certified compilers).
Keys are of type positive, and maps are binary trees: the sequence
of binary digits of a positive number corresponds to a path in such a tree.
This is quite similar to the IntMap library, except that no path
compression is implemented, and that the current file is simple enough to be
self-contained.
First, some stuff about positive
The module of maps over positive keys
elements
cardinal
Fixpoint cardinal (
m :
t A) :
nat :=
match m with
|
Leaf => 0%
nat
|
Node l None r => (
cardinal l + cardinal r)%
nat
|
Node l (
Some _)
r =>
S (
cardinal l + cardinal r)
end.
Section CompcertSpec.
Theorem gempty:
forall (
i:
positive),
find i empty = None.
Theorem gss:
forall (
i:
positive) (
x:
A) (
m:
t A),
find i (
add i x m)
= Some x.
Lemma gleaf :
forall (
i :
positive),
find i (
Leaf :
t A)
= None.
Theorem gso:
forall (
i j:
positive) (
x:
A) (
m:
t A),
i <> j ->
find i (
add j x m)
= find i m.
Lemma rleaf :
forall (
i :
positive),
remove i (
Leaf :
t A)
= Leaf.
Theorem grs:
forall (
i:
positive) (
m:
t A),
find i (
remove i m)
= None.
Theorem gro:
forall (
i j:
positive) (
m:
t A),
i <> j ->
find i (
remove j m)
= find i m.
Lemma xelements_correct:
forall (
m:
t A) (
i j :
positive) (
v:
A),
find i m = Some v ->
List.In (append j i, v) (
xelements m j).
Theorem elements_correct:
forall (
m:
t A) (
i:
positive) (
v:
A),
find i m = Some v ->
List.In (i, v) (
elements m).
Fixpoint xfind (
i j :
positive) (
m :
t A) :
option A :=
match i,
j with
|
_,
xH =>
find i m
|
xO ii,
xO jj =>
xfind ii jj m
|
xI ii,
xI jj =>
xfind ii jj m
|
_,
_ =>
None
end.
Lemma xfind_left :
forall (
j i :
positive) (
m1 m2 :
t A) (
o :
option A) (
v :
A),
xfind i (
append j (
xO xH))
m1 = Some v ->
xfind i j (
Node m1 o m2)
= Some v.
Lemma xelements_ii :
forall (
m:
t A) (
i j :
positive) (
v:
A),
List.In (xI i, v) (
xelements m (
xI j)) ->
List.In (i, v) (
xelements m j).
Lemma xelements_io :
forall (
m:
t A) (
i j :
positive) (
v:
A),
~List.In (xI i, v) (
xelements m (
xO j)).
Lemma xelements_oo :
forall (
m:
t A) (
i j :
positive) (
v:
A),
List.In (xO i, v) (
xelements m (
xO j)) ->
List.In (i, v) (
xelements m j).
Lemma xelements_oi :
forall (
m:
t A) (
i j :
positive) (
v:
A),
~List.In (xO i, v) (
xelements m (
xI j)).
Lemma xelements_ih :
forall (
m1 m2:
t A) (
o:
option A) (
i :
positive) (
v:
A),
List.In (xI i, v) (
xelements (
Node m1 o m2)
xH) ->
List.In (i, v) (
xelements m2 xH).
Lemma xelements_oh :
forall (
m1 m2:
t A) (
o:
option A) (
i :
positive) (
v:
A),
List.In (xO i, v) (
xelements (
Node m1 o m2)
xH) ->
List.In (i, v) (
xelements m1 xH).
Lemma xelements_hi :
forall (
m:
t A) (
i :
positive) (
v:
A),
~List.In (xH, v) (
xelements m (
xI i)).
Lemma xelements_ho :
forall (
m:
t A) (
i :
positive) (
v:
A),
~List.In (xH, v) (
xelements m (
xO i)).
Lemma find_xfind_h :
forall (
m:
t A) (
i:
positive),
find i m = xfind i xH m.
Lemma xelements_complete:
forall (
i j :
positive) (
m:
t A) (
v:
A),
List.In (i, v) (
xelements m j) ->
xfind i j m = Some v.
Theorem elements_complete:
forall (
m:
t A) (
i:
positive) (
v:
A),
List.In (i, v) (
elements m) ->
find i m = Some v.
Lemma cardinal_1 :
forall (
m:
t A),
cardinal m = length (
elements m).
End CompcertSpec.
Definition MapsTo (
i:
positive)(
v:
A)(
m:
t A) :=
find i m = Some v.
Definition In (
i:
positive)(
m:
t A) :=
exists e:A, MapsTo i e m.
Definition Empty m :=
forall (
a :
positive)(
e:
A) ,
~ MapsTo a e m.
Definition eq_key (
p p':
positive*A) :=
E.eq (
fst p) (
fst p').
Definition eq_key_elt (
p p':
positive*A) :=
E.eq (
fst p) (
fst p')
/\ (snd p) = (snd p').
Definition lt_key (
p p':
positive*A) :=
E.lt (
fst p) (
fst p').
Global Instance eqk_equiv :
Equivalence eq_key.
Global Instance eqke_equiv :
Equivalence eq_key_elt.
Global Instance ltk_strorder :
StrictOrder lt_key.
Lemma mem_find :
forall m x,
mem x m = match find x m with None =>
false |
_ =>
true end.
Lemma Empty_alt :
forall m,
Empty m <-> forall a,
find a m = None.
Lemma Empty_Node :
forall l o r,
Empty (
Node l o r)
<-> o=None /\ Empty l /\ Empty r.
Section FMapSpec.
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.
Variable m m' m'' :
t A.
Variable x y z :
key.
Variable e e' :
A.
Lemma MapsTo_1 :
E.eq x y ->
MapsTo x e m ->
MapsTo y e m.
Lemma find_1 :
MapsTo x e m ->
find x m = Some e.
Lemma find_2 :
find x m = Some e ->
MapsTo x e m.
Lemma empty_1 :
Empty empty.
Lemma is_empty_1 :
Empty m ->
is_empty m = true.
Lemma is_empty_2 :
is_empty m = true ->
Empty m.
Lemma add_1 :
E.eq x y ->
MapsTo y e (
add x e m).
Lemma add_2 :
~ E.eq x y ->
MapsTo y e m ->
MapsTo y e (
add x e' m).
Lemma add_3 :
~ E.eq x y ->
MapsTo y e (
add x e' m) ->
MapsTo y e m.
Lemma remove_1 :
E.eq x y ->
~ In y (
remove x m).
Lemma remove_2 :
~ E.eq x y ->
MapsTo y e m ->
MapsTo y e (
remove x m).
Lemma remove_3 :
MapsTo y e (
remove x m) ->
MapsTo y e m.
Lemma elements_1 :
MapsTo x e m ->
InA eq_key_elt (x,e) (
elements m).
Lemma elements_2 :
InA eq_key_elt (x,e) (
elements m) ->
MapsTo x e m.
Lemma xelements_bits_lt_1 :
forall p p0 q m v,
List.In (p0,v) (
xelements m (
append p (
xO q))) ->
E.bits_lt p0 p.
Lemma xelements_bits_lt_2 :
forall p p0 q m v,
List.In (p0,v) (
xelements m (
append p (
xI q))) ->
E.bits_lt p p0.
Lemma xelements_sort :
forall p,
sort lt_key (
xelements m p).
Lemma elements_3 :
sort lt_key (
elements m).
Lemma elements_3w :
NoDupA eq_key (
elements m).
End FMapSpec.
map and mapi
Variable B :
Type.
Section Mapi.
Variable f :
positive ->
A ->
B.
Fixpoint xmapi (
m :
t A) (
i :
positive) :
t B :=
match m with
|
Leaf => @
Leaf B
|
Node l o r =>
Node (
xmapi l (
append i (
xO xH)))
(
option_map (
f i)
o)
(
xmapi r (
append i (
xI xH)))
end.
Definition mapi m :=
xmapi m xH.
End Mapi.
Definition map (
f :
A ->
B)
m :=
mapi (
fun _ =>
f)
m.
End A.
Lemma xgmapi:
forall (
A B:
Type) (
f:
positive ->
A ->
B) (
i j :
positive) (
m:
t A),
find i (
xmapi f m j)
= option_map (
f (
append j i)) (
find i m).
Theorem gmapi:
forall (
A B:
Type) (
f:
positive ->
A ->
B) (
i:
positive) (
m:
t A),
find i (
mapi f m)
= option_map (
f i) (
find i 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 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.
Section map2.
Variable A B C :
Type.
Variable f :
option A ->
option B ->
option C.
Implicit Arguments Leaf [
A].
Fixpoint xmap2_l (
m :
t A) :
t C :=
match m with
|
Leaf =>
Leaf
|
Node l o r =>
Node (
xmap2_l l) (
f o None) (
xmap2_l r)
end.
Lemma xgmap2_l :
forall (
i :
positive) (
m :
t A),
f None None = None ->
find i (
xmap2_l m)
= f (
find i m)
None.
Fixpoint xmap2_r (
m :
t B) :
t C :=
match m with
|
Leaf =>
Leaf
|
Node l o r =>
Node (
xmap2_r l) (
f None o) (
xmap2_r r)
end.
Lemma xgmap2_r :
forall (
i :
positive) (
m :
t B),
f None None = None ->
find i (
xmap2_r m)
= f None (
find i m).
Fixpoint _map2 (
m1 :
t A)(
m2 :
t B) :
t C :=
match m1 with
|
Leaf =>
xmap2_r m2
|
Node l1 o1 r1 =>
match m2 with
|
Leaf =>
xmap2_l m1
|
Node l2 o2 r2 =>
Node (
_map2 l1 l2) (
f o1 o2) (
_map2 r1 r2)
end
end.
Lemma gmap2:
forall (
i:
positive)(
m1:
t A)(
m2:
t B),
f None None = None ->
find i (
_map2 m1 m2)
= f (
find i m1) (
find i m2).
End map2.
Definition map2 (
elt elt' elt'':
Type)(
f:
option elt->
option elt'->
option elt'') :=
_map2 (
fun o1 o2 =>
match o1,
o2 with None,
None =>
None |
_,
_ =>
f o1 o2 end).
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'.
Section Fold.
Variables A B :
Type.
Variable f :
positive ->
A ->
B ->
B.
Fixpoint xfoldi (
m :
t A) (
v :
B) (
i :
positive) :=
match m with
|
Leaf =>
v
|
Node l (
Some x)
r =>
xfoldi r (
f i x (
xfoldi l v (
append i 2))) (
append i 3)
|
Node l None r =>
xfoldi r (
xfoldi l v (
append i 2)) (
append i 3)
end.
Lemma xfoldi_1 :
forall m v i,
xfoldi m v i = fold_left (
fun a p =>
f (
fst p) (
snd p)
a) (
xelements m i)
v.
Definition fold m i :=
xfoldi m i 1.
End Fold.
Lemma fold_1 :
forall (
A:
Type)(
m:
t A)(
B:
Type)(
i :
B) (
f :
key ->
A ->
B ->
B),
fold f m i = fold_left (
fun a p =>
f (
fst p) (
snd p)
a) (
elements m)
i.
Fixpoint equal (
A:
Type)(
cmp :
A ->
A ->
bool)(
m1 m2 :
t A) :
bool :=
match m1,
m2 with
|
Leaf,
_ =>
is_empty m2
|
_,
Leaf =>
is_empty m1
|
Node l1 o1 r1,
Node l2 o2 r2 =>
(match o1,
o2 with
|
None,
None =>
true
|
Some v1,
Some v2 =>
cmp v1 v2
|
_,
_ =>
false
end)
&& equal cmp l1 l2 && equal cmp r1 r2
end.
Definition Equal (
A:
Type)(
m m':
t A) :=
forall y,
find y m = find y m'.
Definition Equiv (
A:
Type)(
eq_elt:
A->
A->
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 (
A:
Type)(
cmp:
A->
A->
bool) :=
Equiv (
Cmp cmp).
Lemma equal_1 :
forall (
A:
Type)(
m m':
t A)(
cmp:
A->
A->
bool),
Equivb cmp m m' ->
equal cmp m m' = true.
Lemma equal_2 :
forall (
A:
Type)(
m m':
t A)(
cmp:
A->
A->
bool),
equal cmp m m' = true ->
Equivb cmp m m'.
End PositiveMap.
Here come some additionnal facts about this implementation.
Most are facts that cannot be derivable from the general interface.