Library Coq.FSets.FMapList
This file proposes an implementation of the non-dependant interface
FMapInterface.S using lists of pairs ordered (increasing) with respect to
left projection.
This lemma isn't part of the spec of Equivb, but is used in FMapAVL
Specification of map
Specification of mapi
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.