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
Fixpoint map (
f:elt ->
elt') (
m:t
elt) {
struct m} :
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) {
struct m} :
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
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)) {
struct m } :
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)) {
struct m} :
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.