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).


Properties of add.

    Lemma add_transp : transpose_neqkey Equal (@add A).

    Definition add_add_neq := add_transp.

    Lemma add_add_eq : forall k l, E.eq k l ->
      forall (x y : A) m, Equal (add k x (add l y m)) (add k x m).

    Lemma add_add : forall k l (x y : A) m,
      Equal (add k x (add l y m))
      (if eq_dec k l then add k x m else add l y (add k x m)).

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

    Definition add_add_neq_Equiv := add_transp_Equiv.

    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,
      Equiv eq (add k x (add l 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.

    Global Instance add_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.