Library Coq.FSets.FMapPositive
An implementation of FMapInterface.S 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.
Even if positive can be seen as an ordered type with respect to the
usual order (see OrderedTypeEx), we use here a lexicographic order
over bits, which is more natural here (lower bits are considered first).
Module PositiveOrderedTypeBits <:
UsualOrderedType.
Definition t:=positive.
Definition eq:=@eq
positive.
Definition eq_refl := @
refl_equal t.
Definition eq_sym := @
sym_eq t.
Definition eq_trans := @
trans_eq t.
Fixpoint bits_lt (
p q:positive) {
struct p } :
Prop :=
match p,
q with
|
xH,
xI _ =>
True
|
xH,
_ =>
False
|
xO p,
xO q =>
bits_lt p q
|
xO _,
_ =>
True
|
xI p,
xI q =>
bits_lt p q
|
xI _,
_ =>
False
end.
Definition lt:=bits_lt.
Lemma bits_lt_trans :
forall x y z :
positive,
bits_lt x y ->
bits_lt y z ->
bits_lt x z.
Lemma lt_trans :
forall x y z :
t,
lt x y ->
lt y z ->
lt x z.
Lemma bits_lt_antirefl :
forall x :
positive, ~
bits_lt x x.
Lemma lt_not_eq :
forall x y :
t,
lt x y -> ~
eq x y.
Definition compare :
forall x y :
t,
Compare lt eq x y.
Lemma eq_dec (
x y:
positive): {
x =
y} + {
x <>
y}.
End PositiveOrderedTypeBits.
Other positive stuff
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) {
struct j} :
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').
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) {
struct m} :
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) {
struct m} :
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) {
struct m} :
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) {
struct m1} :
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) {
struct m1} :
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.