# Library Coq.FSets.FMapList

# Finite map library

This file proposes an implementation of the non-dependant interface FMapInterface.S using lists of pairs ordered (increasing) with respect to left projection.
Require Import FMapInterface.
Module Raw (X:OrderedType).
Module Import MX := OrderedTypeFacts X.
Module Import PX := KeyOrderedType 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 ltk := (ltk (elt:=elt)).
Notation MapsTo := (MapsTo (elt:=elt)).
Notation In := (In (elt:=elt)).
Notation Sort := (sort ltk).
Notation Inf := (lelistA (ltk)).

# 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_sorted : Sort 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:Sort m) x, In x m -> mem x m = true.
Lemma mem_2 : forall m (Hm:Sort 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:Sort m) x e, MapsTo x e m -> find x m = Some e.

# add

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_Inf : forall (m:t elt)(x x':key)(e e':elt),
Inf ( x' , e' ) m -> ltk ( x' , e' ) ( x , e ) -> Inf ( x' , e' ) (add x e m).
Hint Resolve add_Inf.
Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m).

# remove

Lemma remove_1 : forall m (Hm:Sort m) x y, X.eq x y -> ~ In y (remove x m).
Lemma remove_2 : forall m (Hm:Sort m) x y e,
~ X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
Lemma remove_3 : forall m (Hm:Sort m) x y e,
MapsTo y e (remove x m) -> MapsTo y e m.
Lemma remove_Inf : forall (m:t elt)(Hm : Sort m)(x x':key)(e':elt),
Inf ( x' , e' ) m -> Inf ( x' , e' ) (remove x m).
Hint Resolve remove_Inf.
Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (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_3 : forall m (Hm:Sort m), sort ltk (elements m).
Lemma elements_3w : forall m (Hm:Sort m), NoDupA eqk (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 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 equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp,
Equivb cmp m m' -> equal cmp m m' = true.
Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp,
equal cmp m m' = true -> Equivb cmp m m'.
This lemma isn't part of the spec of Equivb, but is used in FMapAVL
Lemma equal_cons : forall cmp l1 l2 x y, Sort (x :: l1) -> Sort (y :: l2) ->
eqk x y -> cmp (snd x) (snd y) = true ->
(Equivb cmp l1 l2 <-> Equivb cmp (x :: l1) (y :: l2)).
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_lelistA : forall (m: t elt)(x:key)(e:elt)(e':elt')(f:elt->elt'),
lelistA (@ltk elt) ( x , e ) m ->
lelistA (@ltk elt') ( x , e' ) (map f m).
Hint Resolve map_lelistA.
Lemma map_sorted : forall (m: t elt)(Hm : sort (@ltk elt) m)(f:elt -> elt'),
sort (@ltk 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_lelistA : forall (m: t elt)(x:key)(e:elt)(f:key->elt->elt'),
lelistA (@ltk elt) ( x , e ) m ->
lelistA (@ltk elt') ( x , f x e ) (mapi f m).
Hint Resolve mapi_lelistA.
Lemma mapi_sorted : forall m (Hm : sort (@ltk elt) m)(f: key ->elt -> elt'),
sort (@ltk elt') (mapi f m).
End Elt2.
Section Elt3.

# map2

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.