# Finite map library

This file proposes an implementation of the non-dependant interface FMapInterface.WS using lists of pairs, unordered but without redundancy.

Require Import FMapInterface.

Module Raw (X:DecidableType).

Module Import PX := KeyDecidableType X.

Definition key := X.t.
Definition t (elt:Type) := list (X.t * elt).

Section Elt.

Variable elt : Type.

Notation eqk := (eqk (elt:=elt)).
Notation eqke := (eqke (elt:=elt)).
Notation MapsTo := (MapsTo (elt:=elt)).
Notation In := (In (elt:=elt)).
Notation NoDupA := (NoDupA eqk).

# empty

Definition empty : t elt := nil.

Definition Empty m := forall (a : key)(e:elt), ~ MapsTo a e m.

Lemma empty_1 : Empty empty.

Hint Resolve empty_1.

Lemma empty_NoDup : NoDupA empty.

# is_empty

Definition is_empty (l : t elt) : bool := if l then true else false.

Lemma is_empty_1 :forall m, Empty m -> is_empty m = true.

Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.

# mem

Lemma mem_1 : forall m (Hm:NoDupA m) x, In x m -> mem x m = true.

Lemma mem_2 : forall m (Hm:NoDupA m) x, mem x m = true -> In x m.

# find

Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.

Lemma find_1 : forall m (Hm:NoDupA m) x e,
MapsTo x e m -> find x m = Some e.

Lemma find_eq : forall m (Hm:NoDupA m) x x',
X.eq x x' -> find x m = find x' m.

Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).

Lemma add_2 : forall m x y e e',
~ X.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).

Lemma add_3 : forall m x y e e',
~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.

Lemma add_3' : forall m x y e e',
~ X.eq x y -> InA eqk (y,e) (add x e' m) -> InA eqk (y,e) m.

Lemma add_NoDup : forall m (Hm:NoDupA m) x e, NoDupA (add x e m).

Lemma add_eq : forall m (Hm:NoDupA m) x a e,
X.eq x a -> find x (add a e m) = Some e.

Lemma add_not_eq : forall m (Hm:NoDupA m) x a e,
~X.eq x a -> find x (add a e m) = find x m.

# remove

Lemma remove_1 : forall m (Hm:NoDupA m) x y, X.eq x y -> ~ In y (remove x m).

Lemma remove_2 : forall m (Hm:NoDupA m) x y e,
~ X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).

Lemma remove_3 : forall m (Hm:NoDupA m) x y e,
MapsTo y e (remove x m) -> MapsTo y e m.

Lemma remove_3' : forall m (Hm:NoDupA m) x y e,
InA eqk (y,e) (remove x m) -> InA eqk (y,e) m.

Lemma remove_NoDup : forall m (Hm:NoDupA m) x, NoDupA (remove x m).

# elements

Definition elements (m: t elt) := m.

Lemma elements_1 : forall m x e, MapsTo x e m -> InA eqke (x,e) (elements m).

Lemma elements_2 : forall m x e, InA eqke (x,e) (elements m) -> MapsTo x e m.

Lemma elements_3w : forall m (Hm:NoDupA m), NoDupA (elements m).

# fold

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.

# equal

Definition check (cmp : elt -> elt -> bool)(k:key)(e:elt)(m': t elt) :=
match find k m' with
| None => false
| Some e' => cmp e e'
end.

Definition submap (cmp : elt -> elt -> bool)(m m' : t elt) : bool :=
fold (fun k e b => andb (check cmp k e m') b) m true.

Definition equal (cmp : elt -> elt -> bool)(m m' : t elt) : bool :=
andb (submap cmp m m') (submap (fun e' e => cmp e e') m' m).

Definition Submap cmp m m' :=
(forall k, In k m -> In k m') /\
(forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).

Definition Equivb cmp m m' :=
(forall k, In k m <-> In k m') /\
(forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).

Lemma submap_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp,
Submap cmp m m' -> submap cmp m m' = true.

Lemma submap_2 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp,
submap cmp m m' = true -> Submap cmp m m'.

Specification of equal

Lemma equal_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp,
Equivb cmp m m' -> equal cmp m m' = true.

Lemma equal_2 : forall m (Hm:NoDupA m) m' (Hm':NoDupA m') cmp,
equal cmp m m' = true -> Equivb cmp m m'.

Variable elt':Type.

# map and mapi

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

Lemma map_1 : forall (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 (m:t elt)(x:key)(f:elt->elt'),
In x (map f m) -> In x m.

Lemma map_NoDup : forall m (Hm : NoDupA (@eqk elt) m)(f:elt->elt'),
NoDupA (@eqk elt') (map f m).

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

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.