# Library CoLoR.Util.FMap.FMapUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2010-01-28
• Pierre-Yves Strub, 2009-04-09
Wrapper for Coq's FMaps definition + additional facts

Set Implicit Arguments.

Module Make (Export XMap : FMapInterface.S).

Module Export XMapProps := Properties XMap.
Module Export XMapFacts := Facts XMap.
Module Export XMapOrdProps := OrdProperties XMap.

In the following, we assume given a type A and a relation eq on A.

Section S.

Variables (A : Type) (eq : relation A).

Lemma remove_empty : forall x, Equal (remove x empty) (@empty A).

Properties of Equiv.

Global Instance Equiv_m' : Proper (inclusion ==> inclusion) (@Equiv A).

Global Instance Equiv_m A : Proper (same ==> same) (@Equiv A).

Lemma Equal_Equiv : Reflexive eq -> Equal << Equiv eq.

Global Instance Equiv_Refl : Reflexive eq -> Reflexive (Equiv eq).

Global Instance Equiv_Sym : Symmetric eq -> Symmetric (Equiv eq).

Global Instance Equiv_Trans : Transitive eq -> Transitive (Equiv eq).

Properties of transpose_neqkey.

Global Instance transpose_neqkey_m' : forall B,
Proper (inclusion ==> Logic.eq ==> impl) (@transpose_neqkey A B).

Global Instance transpose_neqkey_m : forall B,
Proper (same ==> Logic.eq ==> iff) (@transpose_neqkey A B).

forall (x y : A) m, Equal (add k x (add l y m)) (add k x m).

(if eq_dec k l then add k x m else add l y (add k x m)).

Reflexive eq -> transpose_neqkey (Equiv eq) (@add A).

Lemma add_add_eq_Equiv : Reflexive eq -> forall k l, E.eq k l ->
forall x y m, Equiv eq (add k x (add l y m)) (add k x m).

Lemma add_add_Equiv : Reflexive eq -> forall k l x y m,
(if eq_dec k l then add k x m else add l y (add k x m)).

add is a morphism wrt Equiv.

Proper (E.eq ==> eq ==> Equiv eq ==> Equiv eq) (@add A).

Properties of find.

Lemma find_None : forall k m,
find k m = None <-> (forall x:A, ~MapsTo k x m).

Lemma Equiv_MapsTo : forall m m', Equiv eq m m' -> forall k x,
MapsTo k x m -> exists x', MapsTo k x' m' /\ eq x x'.

Lemma Equiv_find_Some : forall m m', Equiv eq m m' -> forall k x,
find k m = Some x -> exists x', find k m' = Some x' /\ eq x x'.

Lemma Equiv_MapsTo' : forall m m', Equiv eq m m' -> forall k x,
MapsTo k x m' -> exists x', MapsTo k x' m /\ eq x' x.

Lemma Equiv_find_Some' : forall m m', Equiv eq m m' -> forall k x,
find k m' = Some x -> exists x', find k m = Some x' /\ eq x' x.

Lemma Equiv_find_None : forall m m', Equiv eq m m' ->
forall k, find k m = None <-> find k m' = None.

Global Instance find_m : Proper (E.eq ==> Equiv eq ==> opt_r eq) (@find A).

Lemma find_empty k : find k empty = @None A.

Properties of Empty and is_empty.

Global Instance Empty_Equiv : Proper (Equiv eq ==> iff) (@Empty A).

Global Instance is_empty_Equiv :
Proper (Equiv eq ==> Logic.eq) (@is_empty A).

Other properties of Equiv.

Lemma Equiv_empty : forall m, Equiv eq empty m <-> Empty m.

Lemma Equiv_add_remove : forall n k x m', ~In k n ->
Equiv eq (add k x n) m' -> Equiv eq n (remove k m').

Lemma Equiv_add : forall n k x m', ~In k n -> Equiv eq (add k x n) m' ->
exists x', eq x x' /\ Add k x' (remove k m') m'.

Properties of fold.

Lemma fold_empty f (i:A) : fold f (@empty A) i = i.

Section fold.

Variables (heq : PreOrder eq)
(B : Type) (eqB : relation B) (heqB : Equivalence eqB).

Global Instance fold_Equiv : forall (f : E.t -> A -> B -> B)
(f_m : Proper (E.eq ==> eq ==> eqB ==> eqB) f)
(hf : transpose_neqkey eqB f),
Proper (Equiv eq ==> eqB ==> eqB) (fold f).

Lemma fold_Equiv_ext : forall (f : E.t -> A -> B -> B)
(f_m : Proper (E.eq ==> eq ==> eqB ==> eqB) f)
(hf : transpose_neqkey eqB f) f',
(forall k k', E.eq k k' -> forall x x', eq x x' ->
forall b b', eqB b b' -> eqB (f k x b) (f' k' x' b')) ->
forall m m', Equiv eq m m' -> forall b b', eqB b b' ->
eqB (fold f m b) (fold f' m' b').

End fold.

Properties of In.

Global Instance In_Equiv' : Proper (E.eq ==> Equiv eq ==> impl) (@In A).

Global Instance In_Equiv : Reflexive eq ->
Proper (E.eq ==> Equiv eq ==> iff) (@In A).

Properties of for_all.

Section for_all.

Variable f : E.t -> A -> bool.

Definition for_all_aux k x b := f k x && b.

Global Instance for_all_aux_m : Proper (E.eq ==> eq ==> Logic.eq) f ->
Proper (E.eq ==> eq ==> Logic.eq ==> Logic.eq) for_all_aux.

Lemma for_all_aux_transp : transpose_neqkey Logic.eq for_all_aux.

Lemma for_all_eq : forall m, for_all f m = fold for_all_aux m true.

Lemma for_all_add : Reflexive eq ->
Proper (E.eq ==> eq ==> Logic.eq) f -> forall k m, ~In k m ->
forall x, for_all f (add k x m) = f k x && for_all f m.

Global Instance for_all_Equiv : PreOrder eq ->
Proper (E.eq ==> eq ==> Logic.eq) f ->
Proper (Equiv eq ==> Logic.eq) (for_all f).

Global Instance for_all_m : Reflexive eq ->
Proper (E.eq ==> eq ==> Logic.eq) f ->
Proper (Equal ==> Logic.eq) (for_all f).

End for_all.

Properties of filter.

Section filter.

Variable f : E.t -> A -> bool.

Definition filter_aux k x m := if f k x then add k x m else m.

Global Instance filter_aux_m : PreOrder eq ->
Proper (E.eq ==> eq ==> Logic.eq) f ->
Proper (E.eq ==> eq ==> Equiv eq ==> Equiv eq) filter_aux.

Lemma filter_aux_transp : Reflexive eq ->
transpose_neqkey (Equiv eq) filter_aux.

Lemma filter_eq : forall m, filter f m = fold filter_aux m empty.

End filter.

Inclusion ordering on maps.

Definition le E F := forall x (T : A), MapsTo x T E -> MapsTo x T F.

Global Instance le_refl : Reflexive le.

Global Instance le_trans : Transitive le.

Global Instance le_Equal : Proper (@Equal A ==> @Equal A ==> impl) le.

Lemma le_add : forall E x T, find x E = None -> le E (add x T E).

Global Instance MapsTo_le :
Proper (Logic.eq ==> Logic.eq ==> le ==> impl) (@MapsTo A).

Global Instance In_le : Proper (Logic.eq ==> le ==> impl) (@In A).

Global Instance add_le : Proper (E.eq ==> Logic.eq ==> le ==> le) (@add A).

End S.

# Module providing results on the domain of a map.

Module Domain (XSet : FSetInterface.S with Module E := XMap.E).

Module Export XSetUtil := FSetUtil.Make XSet.

Import XMap XMapFacts XMapProps XMapOrdProps.

Section S.

Variable A : Type.

## Restriction of an environment to some set of variables.

Definition restrict_fun xs x (T:A) E :=
if XSet.mem x xs then add x T E else E.

Global Instance restrict_fun_e :
Proper (XSet.Equal ==> E.eq ==> Logic.eq ==> Equal ==> Equal)
restrict_fun.

Lemma restrict_fun_transp : forall xs,
transpose_neqkey Equal (restrict_fun xs).

Definition restrict_dom E xs := fold (restrict_fun xs) E empty.

Lemma restrict_dom_empty : forall xs, Equal (restrict_dom empty xs) empty.

Lemma restrict_dom_add : forall xs x T E, ~In x E ->
Equal (restrict_dom (add x T E) xs)
(restrict_fun xs x T (restrict_dom E xs)).

Global Instance restrict_dom_e :
Proper (Equal ==> XSet.Equal ==> Equal) restrict_dom.

Lemma mapsto_restrict_dom : forall E xs x T,
MapsTo x T (restrict_dom E xs) <-> (MapsTo x T E /\ XSet.In x xs).

Global Instance restrict_dom_s :
Proper (le ==> Subset ==> le) restrict_dom.

Lemma restrict_dom_le : forall E xs, le (restrict_dom E xs) E.

Lemma restrict_dom_singleton : forall E x,
Equal (restrict_dom E (singleton x))
match find x E with None => empty | Some T => add x T empty end.

Lemma mapsto_restrict_dom_singleton : forall x T E,
MapsTo x T E -> MapsTo x T (restrict_dom E (singleton x)).

## Domain of a typing environment.

Definition dom_fun x (T:A) xs := XSet.add x xs.

Global Instance dom_fun_e :
Proper (E.eq ==> Logic.eq ==> XSet.Equal ==> XSet.Equal) dom_fun.

Lemma dom_fun_transp : transpose_neqkey XSet.Equal dom_fun.

Definition dom E := fold dom_fun E XSet.empty.

Global Instance dom_e : Proper (Equal ==> XSet.Equal) dom.

Lemma dom_empty : dom empty [=] XSet.empty.

Lemma dom_add_notin : forall x T E,
~In x E -> dom (add x T E) [=] XSet.add x (dom E).

Lemma In_dom : forall x E, XSet.In x (dom E) <-> In x E.

Lemma dom_add : forall x T E, dom (add x T E) [=] XSet.add x (dom E).

End S.

End Domain.

End Make.