Library Coq.FSets.FMapWeakList
This file proposes an implementation of the non-dependant interface
FMapInterface.WS using lists of pairs, unordered but without redundancy.
Specification of equal
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
Lemma mapi_1 :
forall (
m:t
elt)(
x:key)(e:elt)(f:key->elt->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)(f:key->elt->elt'),
In x (
mapi f m) ->
In x m.
Lemma mapi_NoDup :
forall m (
Hm :
NoDupA (@
eqk elt)
m)(
f:
key->elt->elt'),
NoDupA (@
eqk elt') (
mapi f m).
End Elt2.
Section Elt3.
Variable elt elt' elt'' :
Type.
Notation oee' := (
option elt *
option elt')%type.
Definition combine_l (
m:t
elt)(
m':t
elt') :
t oee' :=
mapi (
fun k e => (
Some e,
find k m'))
m.
Definition combine_r (
m:t
elt)(
m':t
elt') :
t oee' :=
mapi (
fun k e' => (
find k m,
Some e'))
m'.
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 combine (
m:t
elt)(
m':t
elt') :
t oee' :=
let l :=
combine_l m m' in
let r :=
combine_r m m' in
fold_right_pair (
add (
elt:=oee'))
l r.
Lemma fold_right_pair_NoDup :
forall l r (
Hl:
NoDupA (
eqk (
elt:=oee'))
l)
(
Hl:
NoDupA (
eqk (
elt:=oee'))
r),
NoDupA (
eqk (
elt:=oee')) (
fold_right_pair (
add (
elt:=oee'))
l r).
Hint Resolve fold_right_pair_NoDup.
Lemma combine_NoDup :
forall m (
Hm:NoDupA (@
eqk elt)
m)
m' (
Hm':NoDupA (@
eqk elt')
m'),
NoDupA (@
eqk oee') (
combine m m').
Definition at_least_left (
o:option
elt)(
o':option
elt') :=
match o with
|
None =>
None
|
_ =>
Some (
o,o')
end.
Definition at_least_right (
o:option
elt)(
o':option
elt') :=
match o' with
|
None =>
None
|
_ =>
Some (
o,o')
end.
Lemma combine_l_1 :
forall m (
Hm:NoDupA (@
eqk elt)
m)
m' (
Hm':NoDupA (@
eqk elt')
m')(
x:key),
find x (
combine_l m m') =
at_least_left (
find x m) (
find x m').
Lemma combine_r_1 :
forall m (
Hm:NoDupA (@
eqk elt)
m)
m' (
Hm':NoDupA (@
eqk elt')
m')(
x:key),
find x (
combine_r m m') =
at_least_right (
find x m) (
find x 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:NoDupA (@
eqk elt)
m)
m' (
Hm':NoDupA (@
eqk elt')
m')(
x:key),
find x (
combine m m') =
at_least_one (
find x m) (
find x m').
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.
Definition map2 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_NoDup :
forall m (
Hm:NoDupA (@
eqk elt)
m)
m' (
Hm':NoDupA (@
eqk elt')
m'),
NoDupA (@
eqk elt'') (
map2 m 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:NoDupA (@
eqk elt)
m)
m' (
Hm':NoDupA (@
eqk 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:NoDupA (@
eqk elt)
m)
m' (
Hm':NoDupA (@
eqk 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:NoDupA (@
eqk elt)
m)
m' (
Hm':NoDupA (@
eqk elt')
m')(
x:key),
In x (
map2 m m') ->
In x m \/
In x m'.
End Elt3.
End Raw.
Module Make (
X:
DecidableType) <:
WS with Module E:=X.
Module Raw :=
Raw X.
Module E :=
X.
Definition key :=
E.t.
Record slist (
elt:Type) :=
{
this :>
Raw.t elt;
NoDup :
NoDupA (@
Raw.PX.eqk elt)
this}.
Definition t (
elt: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_NoDup elt).
Definition is_empty m :
bool :=
Raw.is_empty m.(
this).
Definition add x e m :
t elt :=
Build_slist (
Raw.add_NoDup m.(
NoDup)
x e).
Definition find x m :
option elt :=
Raw.find x m.(
this).
Definition remove x m :
t elt :=
Build_slist (
Raw.remove_NoDup m.(
NoDup)
x).
Definition mem x m :
bool :=
Raw.mem x m.(
this).
Definition map f m :
t elt' :=
Build_slist (
Raw.map_NoDup m.(
NoDup)
f).
Definition mapi (
f:key->elt->elt')
m :
t elt' :=
Build_slist (
Raw.mapi_NoDup m.(
NoDup)
f).
Definition map2 f m (
m':t
elt') :
t elt'' :=
Build_slist (
Raw.map2_NoDup f m.(
NoDup)
m'.(
NoDup)).
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.
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_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.