Module Environment

From Coq Require Import FSets.FMapPositive.
From Coq Require Import FSets.FMapFacts.
From Coq Require Import ZArith.ZArith.
From Coq Require Import Classes.EquivDec.

From Velus Require Import Common.CommonTactics.
From Velus Require Import Common.CommonList.
From Velus Require Import Common.

Module Env.

  Include PositiveMap.
  Include PositiveMapAdditionalFacts.
  Module Props := FMapFacts.OrdProperties PositiveMap.

  Section Extra.

    Context {A: Type}.

    Lemma add_comm:
      forall x y a b (m: t A),
        x <> y ->
        add x a (add y b m) = add y b (add x a m).

    Lemma in_dec:
      forall x (m: t A),
        In x m \/ ~In x m.

    Remark option_map_map:
      forall {A B C} (f: A -> B) (g: B -> C) o,
        option_map g (option_map f o) = option_map (fun x => g (f x)) o.

    Lemma xmapi_xmapi:
      forall {B C} (f: ident -> A -> B) (g: ident -> B -> C) (m: t A) x,
        xmapi g (xmapi f m x) x =
        xmapi (fun x (v : A) => g x (f x v)) m x.

    Lemma mapi_mapi:
      forall {B C} (f: positive -> A -> B) (g: positive -> B -> C) (m: t A),
        mapi g (mapi f m) = mapi (fun x v => g x (f x v)) m.

    Lemma map_map:
      forall {B C} (f: A -> B) (g: B -> C) (m: t A),
        map g (map f m) = map (fun x => g (f x)) m.

    Fact xmapi_ext : forall {B} (f g : positive -> A -> B) (m : t A) p,
        (forall p x, f p x = g p x) ->
        xmapi f m p = xmapi g m p.

    Lemma map_ext: forall {B} (f g : A -> B) (m: t A),
        (forall x, f x = g x) ->
        map f m = map g m.

    Definition adds_with {B} (f: B -> A) (xs: list (positive * B)) (m: t A) : t A :=
      fold_left (fun env (xv: positive * B) =>
                   let (x, v) := xv in
                   add x (f v) env) xs m.

    Definition from_list_with {B} (f: B -> A) (xs: list (positive * B)) : t A :=
      adds_with f xs (@empty A).

    Definition adds' (xs: list (positive * A)) (m: t A) : t A :=
      fold_left (fun env (xv: positive * A) =>
                   let (x , v) := xv in
                   add x v env) xs m.

    Definition from_list (xs: list (positive * A)) : t A :=
      adds' xs (@empty A).

    Definition adds_opt (xs: list positive) (vos : list (option A)) (e : t A) : t A :=
      fold_right (fun (xvo: positive * option A) env =>
                    match xvo with
                    | (x, Some v) => add x v env
                    | _ => env end) e (combine xs vos).

    Definition adds (xs: list positive) (vs : list A) (m : t A) : t A :=
      adds' (combine xs vs) m.

    Lemma adds'_is_adds_with_identity:
      forall xs m,
        adds' xs m = adds_with (fun x => x) xs m.

    Section AddsWith.

      Context {B: Type}.
      Variable f: B -> A.

      Lemma adds_with_app:
        forall xs ys s,
          adds_with f ys (adds_with f xs s) = adds_with f (xs ++ ys) s.

      Lemma find_adds_with_spec:
        forall x xvs s,
          (InMembers x xvs ->
           forall s', find x (adds_with f xvs s) = find x (adds_with f xvs s'))
          /\ (~ InMembers x xvs ->
             find x (adds_with f xvs s) = find x s).

      Lemma gsso_with:
      forall x xvs m,
        ~ InMembers x xvs ->
        find x (adds_with f xvs m) = find x m.

      Lemma find_adds_with_spec_Some:
        forall xvs x a m,
          find x (adds_with f xvs m) = Some a ->
          (exists b, List.In (x, b) xvs /\ f b = a)
          \/ (~ InMembers x xvs /\ find x m = Some a).

      Lemma find_gsso_with:
        forall xvs x y a m,
          x <> y ->
          find x (adds_with f ((y, a) :: xvs) m) = find x (adds_with f xvs m).

      Lemma find_gsss_with:
      forall x a xvs m,
        ~ InMembers x xvs ->
        find x (adds_with f ((x, a) :: xvs) m) = Some (f a).

      Lemma In_find_adds_with:
        forall x a xvs m,
          NoDupMembers xvs ->
          List.In (x, a) xvs ->
          find x (adds_with f xvs m) = Some (f a).

      Lemma adds_with_cons:
        forall xvs x b m,
          ~ InMembers x xvs ->
          adds_with f ((x, b) :: xvs) m = add x (f b) (adds_with f xvs m).

    End AddsWith.

    Lemma adds'_app:
      forall xs ys s,
        adds' ys (adds' xs s) = adds' (xs ++ ys) s.

    Lemma gsso':
      forall x xvs m,
        ~ InMembers x xvs ->
        find x (adds' xvs m) = find x m.

    Corollary gsso:
      forall x xs (vs: list A) m,
        ~ List.In x xs ->
        find x (adds xs vs m) = find x m.

    Lemma from_list_find_In:
      forall xvs x a,
        find x (from_list xvs) = Some a ->
        List.In (x, a) xvs.

    Lemma find_gsso':
      forall xvs x y a m,
        x <> y ->
        find x (adds' ((y, a) :: xvs) m) = find x (adds' xvs m).

    Corollary find_gsso:
      forall x y xs (vs: list A) m,
        x <> y ->
        find x (adds (y :: xs) vs m) = find x (adds xs (tl vs) m).

    Lemma find_gsss':
      forall x a xvs m,
        ~ InMembers x xvs ->
        find x (adds' ((x, a) :: xvs) m) = Some a.

    Corollary find_gsss:
      forall x a xs (vs: list A) m,
        ~ List.In x xs ->
        find x (adds (x :: xs) (a :: vs) m) = Some a.

    Lemma In_find_adds':
      forall x a xvs m,
        NoDupMembers xvs ->
        List.In (x, a) xvs ->
        find x (adds' xvs m) = Some a.

    Corollary In_find_adds:
      forall x a xs vs m,
        NoDup xs ->
        List.In (x, a) (combine xs vs) ->
        find x (adds xs vs m) = Some a.

    Lemma In_adds_spec':
      forall x xvs (m: t A),
        In x (adds' xvs m) <-> (InMembers x xvs \/ In x m).

    Lemma find_adds'_In:
      forall x y xvs (m: t A),
        find x (adds' xvs m) = Some y -> (List.In (x, y) xvs \/ find x m = Some y).

    Lemma find_adds'_nIn: forall x xvs (m : t A),
        find x (adds' xvs m) = None <-> (not (InMembers x xvs) /\ find x m = None).

    Corollary In_adds_spec:
      forall x xs vs (m: t A),
        length xs = length vs ->
        (In x (adds xs vs m) <-> (List.In x xs \/ In x m)).

    Lemma adds_opt_nil_nil:
      forall e,
        adds_opt List.nil List.nil e = e.

    Lemma adds_opt_nil_l:
      forall e vs,
        adds_opt List.nil vs e = e.

    Lemma adds_nil_nil:
      forall e,
        adds List.nil List.nil e = e.

    Lemma adds_nil_l:
      forall e vs,
        adds List.nil vs e = e.

    Lemma adds'_cons:
      forall xvs x (a: A) m,
        ~ InMembers x xvs ->
        adds' ((x, a) :: xvs) m = add x a (adds' xvs m).

    Corollary adds_cons_cons:
      forall xs x (a: A) vs m,
        ~ List.In x xs ->
        adds (x :: xs) (a :: vs) m = add x a (adds xs vs m).

    Lemma find_In_from_list:
      forall x (v : A) xs,
        List.In (x, v) xs ->
        NoDupMembers xs ->
        find x (from_list xs) = Some v.

    Lemma In_from_list:
      forall x (xs : list (ident * A)),
        In x (from_list xs) <-> InMembers x xs.

    Lemma In_find:
      forall x (s: t A),
        In x s <-> (exists v, find x s = Some v).

    Corollary find_In:
      forall x (s: t A) v,
        find x s = Some v ->
        In x s.

    Lemma elements_In:
      forall x (a: A) m,
        List.In (x, a) (elements m) -> In x m.

    Lemma Equiv_orel {R : relation A} :
      forall S T, Env.Equiv R S T <-> (forall x, (orel R) (Env.find x S) (Env.find x T)).

    Lemma NoDupMembers_NoDupA:
      forall {A} (xs: list (positive * A)),
        NoDupMembers xs <-> SetoidList.NoDupA (@eq_key A) xs.

    Lemma InA_map_fst:
      forall {A} x xs y,
        SetoidList.InA eq x (List.map (@fst positive A) xs)
        <-> SetoidList.InA (@eq_key A) (x, y) xs.

    Lemma NoDupA_map_fst:
      forall {A} xs,
        SetoidList.NoDupA eq (List.map (@fst positive A) xs)
        <-> SetoidList.NoDupA (@eq_key A) xs.

    Lemma NoDupMembers_elements:
      forall m,
        NoDupMembers (@elements A m).

    Lemma elements_add:
      forall x (v: A) m,
        ~ In x m ->
        Permutation.Permutation (elements (add x v m)) ((x,v) :: elements m).

    Lemma In_Members:
      forall x (m : t A),
        In x m <-> InMembers x (elements m).

    Lemma elements_adds:
      forall xs m,
        NoDupMembers (elements m++xs) ->
        Permutation.Permutation (elements (adds' xs m)) (elements m++xs).

    Lemma Equiv_empty:
      forall m eq,
        (forall x, find x m = None) ->
        Equiv eq m (empty A).

    Lemma find_adds_opt_spec_Some:
      forall xs vs x a m,
        length xs = length vs ->
        find x (adds_opt xs vs m) = Some a ->
        List.In (x, Some a) (combine xs vs)
        \/ find x m = Some a.

    Lemma find_gsso_opt:
      forall x x' xs (vs: list (option A)) S,
        x <> x' ->
        find x (adds_opt (x' :: xs) vs S) = find x (adds_opt xs (tl vs) S).

    Lemma find_gsss_opt:
      forall x v xs (vs: list (option A)) S,
        find x (adds_opt (x :: xs) (Some v :: vs) S) = Some v.

    Lemma find_In_gsso_opt:
      forall x ys (vs: list (option A)) env,
        ~ List.In x ys ->
        find x (adds_opt ys vs env) = find x env.

    Lemma adds_opt_cons_cons:
      forall xs x (v: A) vs e,
        adds_opt (x :: xs) (Some v :: vs) e = add x v (adds_opt xs vs e).

    Lemma adds_opt_cons_cons':
      forall xs x (v: A) vs e,
        ~ List.In x xs ->
        adds_opt (x :: xs) (Some v :: vs) e = adds_opt xs vs (add x v e).

    Lemma adds_opt_cons_cons_None:
      forall xs x (vs: list (option A)) e,
        adds_opt (x :: xs) (None :: vs) e = adds_opt xs vs e.

    Lemma In_adds_opt_In:
      forall xs vos x,
        In x (adds_opt xs vos (empty _)) ->
        List.In x xs.

    Lemma adds_opt_is_adds:
      forall xs vs (m: t A),
        NoDup xs ->
        adds_opt xs (List.map (@Some A) vs) m = adds xs vs m.

    Lemma add_not_Leaf:
      forall x v S, add x v S <> Leaf A.

    Lemma add_remove_comm:
      forall x x' (v: A) m,
        x <> x' ->
        remove x' (add x v m) = add x v (remove x' m).

    Lemma remove_comm:
      forall x x' (m : t A),
        remove x (remove x' m) = remove x' (remove x m).

    Lemma adds_opt_mono:
      forall x (env: t A) ys rvos,
        In x env ->
        Forall (fun x => ~(x = None)) rvos ->
        In x (adds_opt ys rvos env).

    Global Instance find_Proper (R : relation A) `{Equivalence A R}:
      Proper (eq ==> Env.Equiv R ==> orel R) (@Env.find A).

    Global Instance find_eq_Proper:
      Proper (eq ==> Env.Equiv eq ==> eq) (@Env.find A).

    Lemma omap_find:
      forall xs (env : Env.t A),
        Forall (fun x => Env.In x env) xs ->
        exists vs, omap (fun x => Env.find x env) xs = Some vs
              /\ Forall2 (fun x v => Env.find x env = Some v) xs vs.

    Lemma elements_from_list_incl : forall xs,
        incl (elements (from_list xs)) xs.

    Lemma find_env_from_list':
      forall x (v: A) xs s,
        find x (adds' xs s) = Some v
        -> List.In (x, v) xs \/ (~InMembers x xs /\ find x s = Some v).

  End Extra.


  Section Equiv.

    Context {A} (R : relation A).

    Lemma find_Some_orel `{Reflexive _ R} :
      forall env x v,
        find x env = Some v ->
        orel R (find x env) (Some v).

    Lemma orel_find_Some:
      forall env x v,
        orel R (find x env) (Some v) ->
        exists v', R v' v /\ find x env = Some v'.

    Global Add Parametric Morphism `{Equivalence _ R} : (@In A)
        with signature (eq ==> Equiv R ==> iff)
          as In_Equiv.

    Global Instance Equiv_Reflexive `{Reflexive A R} : Reflexive (Equiv R).

    Global Instance Equiv_Transitive `{Transitive A R} :
      Transitive (Equiv R).

    Global Instance Equiv_Symmetric `{Symmetric _ R} : Symmetric (Equiv R).

    Global Add Parametric Relation `{Equivalence _ R} : (t A) (Equiv R)
        reflexivity proved by Equiv_Reflexive
        symmetry proved by Equiv_Symmetric
        transitivity proved by Equiv_Transitive
      as Equivalence_Equiv.

    Global Add Parametric Morphism `{Equivalence _ R} : (Equiv R)
        with signature (Equiv R ==> Equiv R ==> iff)
          as Equiv_Equiv.

    Lemma add_remove:
      forall env x (v : A),
        Env.find x env = Some v ->
        Env.Equal env (Env.add x v (Env.remove x env)).

    Lemma Equal_add_both:
      forall x (v : A) env1 env2,
        Env.Equal env1 env2 ->
        Env.Equal (Env.add x v env1) (Env.add x v env2).

  End Equiv.


  Existing Instance Equivalence_Equiv.


  Section EnvRefines.

    Import Relation_Definitions Basics.

    Context {A : Type}
            (R : relation A).

    Definition refines (env1 env2 : Env.t A) : Prop :=
      forall x v, Env.find x env1 = Some v ->
             exists v', R v v' /\ Env.find x env2 = Some v'.

    Global Typeclasses Opaque refines.

    Lemma refines_empty:
      forall env, refines (empty A) env.

    Lemma refines_refl `{Reflexive _ R} : reflexive _ refines.

    Lemma refines_trans `{Transitive _ R} : transitive _ refines.

    Global Add Parametric Relation `{Reflexive _ R} `{Transitive _ R}
      : _ refines
        reflexivity proved by refines_refl
        transitivity proved by refines_trans
          as env_refines_preorder.

    Global Add Parametric Morphism `{Reflexive _ R} `{Transitive _ R} : refines
        with signature (refines --> refines ++> impl)
          as refines_refines1.

    Global Add Parametric Morphism `{Reflexive _ R} `{Transitive _ R} : refines
        with signature (refines ++> refines --> flip impl)
          as refines_refines2.

    Lemma refines_add `{Reflexive _ R} :
      forall env x v,
        ~ In x env ->
        refines env (add x v env).

    Lemma refines_add_both:
      forall env1 env2 x v1 v2,
        refines env1 env2 ->
        R v1 v2 ->
        refines (add x v1 env1) (add x v2 env2).

    Global Add Morphism (@In A)
        with signature (eq ==> refines ++> impl)
          as In_refines.

    Global Add Morphism (@In A)
        with signature (eq ==> refines --> flip impl)
          as In_refines_flip.

    Global Instance refines_Proper `{Reflexive _ R} `{Transitive _ R} :
      Proper (flip refines ==> refines ==> impl) refines.

    Global Instance add_refines_Proper `{Reflexive _ R}:
      Proper (@eq ident ==> @eq A ==> refines ==> refines) (@add A).

    Lemma Equiv_refines' `{Symmetric _ R}:
      forall env1 env2,
        Equiv R env1 env2 ->
        refines env1 env2.

    Lemma Equiv_refines `{Equivalence _ R}:
      forall env1 env2,
        Equiv R env1 env2 <-> (refines env1 env2 /\ refines env2 env1).

    Global Add Parametric Morphism `{Equivalence _ R} : refines
        with signature (Equiv R ==> Equiv R ==> iff)
          as refines_Equiv.

    Global Add Parametric Morphism `{Equivalence _ R} : refines
        with signature (Equiv R ==> Equiv R ==> flip impl)
          as refines_Equiv_flip_impl.

    Global Instance equiv_refines `{Equivalence _ R} :
      PartialOrder (Equiv R) refines.

    Lemma refines_add_right `{Reflexive _ R} `{Transitive _ R}:
      forall env1 env2 x v,
        refines env1 env2 ->
        ~ In x env1 ->
        refines env1 (add x v env2).

    Lemma refines_remove `{Reflexive _ R}:
      forall env x,
        refines (remove x env) env.

    Lemma refines_remove_both:
      forall env1 env2 x,
        refines env1 env2 ->
        refines (remove x env1) (remove x env2).

    Lemma refines_add_remove:
      forall env1 env2 x v,
        refines env1 env2 ->
        refines (remove x env1) (add x v env2).

    Lemma find_add:
      forall {x v} {env : t A},
        find x env = Some v ->
        Equal env (add x v env).

    Lemma refines_orel_find `{Reflexive _ R} `{Transitive _ R}:
      forall env1 env2 x,
        refines env1 env2 ->
        In x env1 ->
        orel R (find x env1) (find x env2).

    Lemma refines_find_add_left `{Reflexive _ R}:
      forall x v env,
        find x env = Some v ->
        refines (add x v env) env.

    Lemma refines_find_add_right `{Reflexive _ R}:
      forall x v env,
        find x env = Some v ->
        refines env (add x v env).

    Lemma refines_add_left `{Reflexive _ R} `{Transitive _ R}:
      forall x v1 v2 env1 env2,
        refines env1 env2 ->
        find x env2 = Some v2 ->
        R v1 v2 ->
        refines (add x v1 env1) env2.

  End EnvRefines.

  Existing Instance env_refines_preorder.
  Existing Instance Equivalence_Equiv.

  Hint Immediate refines_empty.
  Hint Extern 4 (refines _ (add ?x _ _) (add ?x _ _)) => apply refines_add.

  Lemma Equal_Equiv {A}:
    relation_equivalence Equal (Equiv (@eq A)).

  Add Parametric Morphism {A}: (@Equiv A)
      with signature (subrelation ==> eq ==> eq ==> impl)
        as Equiv_subrelation.

  Global Instance subrelation_Equiv {A} (R1 R2 : relation A):
    subrelation R1 R2 ->
    subrelation (Equiv R1) (Equiv R2).

  Global Instance Equal_subrelation_Equiv {A} (R : relation A) `{Reflexive _ R}:
    subrelation Equal (Equiv R).

  Global Instance Equiv_subrelation_Equal {A}:
    subrelation (Equiv (@eq A)) Equal.

  Global Instance refines_Equal_Proper {A}:
    Proper (@Equal A ==> @Equal A ==> iff) (refines eq).

  Section RefinesAdds.
    Context {V : Type}.

    Fact refines_adds' : forall (xs : list (ident * V)) H H',
        refines eq H H' ->
        refines eq (adds' xs H) (adds' xs H').

    Lemma refines_adds : forall ids (vs : list V) H,
        Forall (fun id => ~In id H) ids ->
        refines eq H (adds ids vs H).

    Lemma refines_adds_opt:
      forall {A} xs m1 m2 (vos1 vos2 : list (option A)),
        refines eq m2 m1 ->
        Forall2 (fun vo1 vo2 => forall v, vo2 = Some v -> vo1 = Some v) vos1 vos2 ->
        NoDup xs ->
        Forall (fun x => ~Env.In x m2) xs ->
        refines eq (Env.adds_opt xs vos2 m2) (Env.adds_opt xs vos1 m1).
  End RefinesAdds.

  Lemma In_add1 {A : Type}:
    forall x (v : A) env,
      In x (add x v env).

  Lemma In_add2 {A : Type}:
    forall x y (v : A) env,
      In y env ->
      In y (add x v env).

  Hint Immediate In_add1.
  Hint Extern 4 (In ?x (add ?y ?v ?env)) => apply In_add2.
  Hint Extern 4 (refines _ ?x ?x) => reflexivity.
  Hint Immediate eq_Transitive.

  Section EnvDom.

    Context { V : Type }.

    Definition dom (env : Env.t V) (dom : list ident) :=
      forall x, Env.In x env <-> List.In x dom.

    Lemma dom_use:
      forall {env xs},
        dom env xs ->
        forall x, Env.In x env <-> List.In x xs.

    Lemma dom_intro:
      forall env xs,
        (forall x, Env.In x env <-> List.In x xs) ->
        dom env xs.

    Lemma dom_add_cons:
      forall env xs x v,
        dom env xs ->
        dom (add x v env) (x :: xs).

    Lemma dom_empty:
      dom (empty V) List.nil.

    Import Permutation.

    Global Add Parametric Morphism (E : relation V) `{Equivalence _ E} : dom
        with signature (Equiv E ==> @Permutation ident ==> iff)
          as dom_Equiv_Permutation.

    Corollary dom_Permutation : forall d l1 l2,
        Permutation l1 l2 ->
        dom d l1 <-> dom d l2.

    Lemma dom_equal_empty:
      forall M, dom M List.nil <-> Equal M (empty V).

    Lemma dom_from_list_map_fst:
      forall (xs : list (ident * V)) ys,
        NoDupMembers xs ->
        ys = List.map fst xs ->
        dom (from_list xs) ys.

    Lemma dom_elements: forall (e : t V),
        dom e (List.map fst (elements e)).

    Lemma dom_Perm : forall e xs ys,
        NoDup xs ->
        NoDup ys ->
        dom e xs ->
        dom e ys ->
        Permutation xs ys.

    Global Opaque dom.
  End EnvDom.

  Hint Extern 4 (dom ?env (?xs ++ nil)) => rewrite app_nil_r.
  Hint Immediate dom_empty.

  Add Parametric Morphism {A} (R: relation A) `{Equivalence _ R} : (@add A)
      with signature (eq ==> R ==> Equiv R ==> Equiv R)
        as add_Equiv.

  Add Parametric Morphism {A} : (@dom A)
      with signature (eq ==> same_elements ==> iff)
        as dom_same_elements.

  Lemma uniquify_dom:
    forall {A} (env : Env.t A) xs,
      dom env xs ->
      exists ys, dom env ys /\ NoDup ys.

  Lemma find_not_In_dom:
    forall {A} (H : Env.t A) xs x,
      dom H xs ->
      ~List.In x xs ->
      find x H = None.

  Lemma dom_cons_remove:
    forall {A} (env : @t A) x xs,
      dom env xs ->
      dom (remove x env) (filter (nequiv_decb x) xs).

  Section DomAdds.

    Context { V : Type }.

    Fact dom_adds' : forall (xs : list (ident * V)) H d,
        dom H d ->
        dom (adds' xs H) ((List.map fst xs)++d).

    Lemma dom_adds : forall ids (vs : list V) H d,
        length ids = length vs ->
        dom H d ->
        dom (adds ids vs H) (ids++d).

    Lemma adds_MapsTo : forall ids (vs : list V) H n d d',
        length ids = length vs ->
        n < length ids ->
        NoDup ids ->
        Env.MapsTo (nth n ids d) (nth n vs d') (Env.adds ids vs H).
  End DomAdds.

  Section EnvDomUpperBound.

    Context { V : Type }.

    Definition dom_ub (env : t V) (dom : list ident) :=
      forall x, In x env -> List.In x dom.

    Lemma dom_ub_use:
      forall {env xs},
        dom_ub env xs ->
        forall x, In x env -> List.In x xs.

    Lemma dom_ub_intro:
      forall env xs,
        (forall x, In x env -> List.In x xs) ->
        dom_ub env xs.

    Lemma dom_dom_ub:
    forall H d,
      Env.dom H d ->
      dom_ub H d.

    Lemma dom_ub_empty:
      forall d, dom_ub (empty V) d.

    Lemma dom_ub_app:
      forall H xs ys,
        dom_ub H xs ->
        dom_ub H (xs ++ ys).

    Global Opaque dom_ub.
  End EnvDomUpperBound.

  Lemma refines_dom_ub_dom:
    forall {A R} (H H' : Env.t A) d,
      refines R H H' ->
      dom H d ->
      dom_ub H' d ->
      dom H' d.

  Lemma dom_ub_cons:
    forall {V} x xs (env: t V),
      dom_ub env xs ->
      dom_ub env (x::xs).

  Lemma dom_ub_add:
    forall {V} x v xs (env: t V),
      dom_ub env xs ->
      dom_ub (add x v env) (x::xs).

  Lemma dom_Forall_not_In:
    forall {A} (H : Env.t A) xs ys,
      dom H xs ->
      Forall (fun x => ~List.In x xs) ys ->
      forall y, List.In y ys -> ~(In y H).

  Section EnvDomLowerBound.

    Context { V : Type }.

    Definition dom_lb (env : t V) (dom : list ident) :=
      forall x, List.In x dom -> In x env.

    Lemma dom_lb_cons : forall (env : t V) (id : ident) (xs : list ident),
        dom_lb env (id::xs) <-> (In id env /\ dom_lb env xs).

    Lemma dom_lb_use:
      forall {env xs},
        dom_lb env xs ->
        forall x, List.In x xs -> In x env.

    Lemma dom_lb_intro:
      forall env xs,
        (forall x, List.In x xs -> In x env) ->
        dom_lb env xs.

    Lemma dom_dom_lb:
    forall H d,
      dom H d ->
      dom_lb H d.

    Lemma dom_lb_nil:
      forall E, dom_lb E nil.

    Lemma dom_lb_add_cons:
      forall x xs v H,
        dom_lb H xs ->
        dom_lb (add x v H) (x :: xs).

    Lemma dom_lb_app:
      forall H xs ys,
        dom_lb H (xs ++ ys) ->
        dom_lb H xs.

    Global Opaque dom_lb.
  End EnvDomLowerBound.

  Hint Resolve dom_lb_nil.

  Lemma dom_lb_ub_dom:
    forall {A} (H : t A) d,
      dom_lb H d ->
      dom_ub H d ->
      dom H d.

  Hint Resolve dom_lb_ub_dom.

  Section EnvRestrict.
    Context {V : Type}.

    Definition restrict (H : Env.t V) (xs : list ident) : Env.t V :=
      List.fold_right (fun id H' => match (Env.find id H) with
                                 | None => H'
                                 | Some v => add id v H'
                                 end) (empty V) xs.

    Lemma restrict_dom_ub : forall xs (H : Env.t V),
        dom_ub (restrict H xs) xs.

    Lemma restrict_refines : forall R xs (H : Env.t V),
        Reflexive R ->
        Transitive R ->
        refines R (restrict H xs) H.

    Lemma dom_lb_restrict_dom : forall xs (H : Env.t V),
        dom_lb H xs ->
        dom (restrict H xs) xs.

    Lemma restrict_find : forall xs (H : Env.t V) id v,
        List.In id xs ->
        find id H = Some v ->
        find id (restrict H xs) = Some v.
  End EnvRestrict.

  Section adds_opt'.
    Import List.ListNotations.
    Definition adds_opt' {A : Type} (xos: list (option positive))
               (vs : list A) (e : Env.t A) : Env.t A :=
      fold_right (fun (xov: option positive * A) env =>
                    match xov with
                    | (Some x, v) => Env.add x v env
                    | _ => env end) e (combine xos vs).

    Lemma find_adds_opt'_spec_Some:
      forall {A} xs vs x (a : A) m,
        length xs = length vs ->
        Env.find x (adds_opt' xs vs m) = Some a ->
        List.In (Some x, a) (combine xs vs)
        \/ Env.find x m = Some a.

    Lemma find_gsso_opt':
      forall {A}x x' xs (vs: list A) S,
        Some x <> x' ->
        Env.find x (adds_opt' (x' :: xs) vs S) =
        Env.find x (adds_opt' xs (tl vs) S).

    Lemma find_gsss_opt':
      forall {A} x v xs (vs: list A) S,
        Env.find x (adds_opt' (Some x :: xs) (v :: vs) S) = Some v.

    Lemma find_In_gsso_opt':
      forall {A} x ys (vs: list A) env,
        ~ Ino x ys ->
        Env.find x (adds_opt' ys vs env) = Env.find x env.

    Lemma adds_opt'_cons_Some:
      forall {A} xs x (v: A) vs e,
        adds_opt' (Some x :: xs) (v :: vs) e =
        Env.add x v (adds_opt' xs vs e).

    Lemma adds_opt'_cons_None:
      forall {A} xs (v : A) vs e,
        adds_opt' (None :: xs) (v :: vs) e = adds_opt' xs vs e.

    Lemma adds_opt'_app :
      forall {A} xs (vs : list A) xs' vs' m,
        length xs = length vs ->
        adds_opt' (xs ++ xs') (vs ++ vs') m
        = adds_opt' xs vs (adds_opt' xs' vs' m).

    Lemma adds_opt'_nil:
      forall {A} vs (e : Env.t A),
        adds_opt' [] vs e = e.

    Lemma adds_opt'_nil':
      forall {A} xs (e : Env.t A),
        adds_opt' xs [] e = e.

    Lemma adds_opt'_None:
      forall {A B} xs vs (e : Env.t A),
        adds_opt' (List.map (fun _ : B => None) xs) vs e = e.

    Lemma find_adds_opt'_disj:
      forall {A} (x : ident) xs xs' vs vs' (e : Env.t A),
        (forall x, Ino x xs -> ~ Ino x xs') ->
        Ino x xs ->
        Env.find x (adds_opt' xs vs e)
        = Env.find x (adds_opt' xs vs (adds_opt' xs' vs' e)).

    Lemma find_permute_adds_opt':
      forall {A} (x : ident) xs xs' vs vs' (e : Env.t A),
        (forall x, Ino x xs -> ~ Ino x xs') ->
        Env.find x (adds_opt' xs vs (adds_opt' xs' vs' e))
        = Env.find x (adds_opt' xs' vs' (adds_opt' xs vs e)).

    Lemma find_adds_opt'_ino:
      forall {A} (x : ident) xs vs (e : Env.t A),
        length xs = length vs ->
        Ino x xs ->
        Env.find x (adds_opt' xs vs e)
        = Env.find x (adds_opt' xs vs (Env.empty A)).

    Lemma In_find_adds_opt':
      forall {A} (x : ident) (v : A) xs vs m,
        NoDupo xs ->
        List.In (Some x, v) (combine xs vs) ->
        Env.find x (adds_opt' xs vs m) = Some v.

    Lemma adds_opt'_adds: forall {A} xs (vs : list A) m,
        NoDup xs ->
        length xs = length vs ->
        Equal (adds_opt' (List.map Some xs) vs m) (adds xs vs m).

    Lemma adds_opt'_ignore: forall {A} xs1 xs2 (vs1 vs2 : list A) m,
        length xs1 = length vs1 ->
        length xs2 = length vs2 ->
        (forall x, Ino x xs2 -> Ino x xs1) ->
        Env.Equal (adds_opt' xs1 vs1 (adds_opt' xs2 vs2 m)) (adds_opt' xs1 vs1 m).

    Lemma adds_opt'_refines: forall {A} xs1 (vs : list A) m,
        length xs1 = length vs ->
        Forall (fun x => forall id, x = Some id -> ~In id m) xs1 ->
        Env.refines eq m (adds_opt' xs1 vs m).

    Lemma adds_opt'_dom : forall {A} ys xs (vs : list A) m,
        length ys = length vs ->
        Env.dom m xs ->
        Env.dom (adds_opt' ys vs m) (xs ++ map_filter id ys).
  End adds_opt'.

  Section union.
    Context {A : Type}.

    Definition union (m1 : t A) (m2 : t A) :=
      adds' (elements m2) m1.

    Lemma union_find_None : forall m1 m2 x,
        find x (union m1 m2) = None <->
        find x m1 = None /\ find x m2 = None.

    Lemma union_find1 : forall m1 m2 x y,
        find x m1 = Some y ->
        find x m2 = Some y ->
        find x (union m1 m2) = Some y.

    Lemma union_find2 : forall m1 m2 x y,
        find x m1 = Some y ->
        find x m2 = None ->
        find x (union m1 m2) = Some y.

    Lemma union_find3 : forall m1 m2 x y,
        find x m1 = None ->
        find x m2 = Some y ->
        find x (union m1 m2) = Some y.

    Lemma union_find4 : forall m1 m2 x y,
        find x (union m1 m2) = Some y ->
        find x m1 = Some y \/ find x m2 = Some y.

    Lemma union_refines1 : forall m m',
        refines eq m m' ->
        refines eq m (union m m').

    Lemma union_refines2 : forall m m1 m2,
        refines eq m m1 ->
        refines eq m m2 ->
        refines eq m (union m1 m2).

    Lemma union_dom : forall m1 m2 xs ys zs,
        dom m1 (xs ++ ys) ->
        dom m2 (xs ++ zs) ->
        dom (union m1 m2) (xs ++ ys ++ zs).

    Fact dom_In_nIn : forall (m m' : t A) xs ys x,
        dom m xs ->
        dom m' (xs ++ ys) ->
        In x m' ->
        ~In x m ->
        (~List.In x xs /\ List.In x ys).

    Lemma union_refines3 : forall m m1 m2 xs ys zs,
        NoDup (ys ++ zs) ->
        dom m xs ->
        dom m1 (xs ++ ys) ->
        dom m2 (xs ++ zs) ->
        refines eq m m1 ->
        refines eq m m2 ->
        refines eq m1 (union m1 m2).

    Lemma union_refines4 : forall m m1 m2 xs ys zs,
        NoDup (ys ++ zs) ->
        dom m xs ->
        dom m1 (xs ++ ys) ->
        dom m2 (xs ++ zs) ->
        refines eq m m1 ->
        refines eq m m2 ->
        refines eq m2 (union m1 m2).

  End union.

  Section diff.
    Context {V : Type}.

    Definition diff (a b : Env.t V) :=
      fold (fun k _ a => Env.remove k a) b a.

    Lemma diff_spec : forall a b x v,
        MapsTo x v (diff a b) <->
        MapsTo x v a /\ ~In x b.

    Corollary diff_In_iff : forall a b x,
        In x (diff a b) <->
        In x a /\ ~In x b.

    Lemma diff_empty : forall a b,
        Env.Empty b ->
        Env.Equal (diff a b) a.

    Lemma diff_remove : forall a b x x' y',
        find x' (diff a (remove x b)) = Some y' ->
        x <> x' /\ Env.find x' (diff a b) = Some y' \/ x = x'.
  End diff.

  Section find_pred.
    Context {V : Type}.
    Variable P : key -> V -> bool.

    Definition find_pred (m : Env.t V) : option (key * V) :=
      fold (fun k v acc => if P k v then Some (k, v) else acc) m None.

    Lemma find_pred_spec : forall m k v,
        find_pred m = Some (k, v) ->
        MapsTo k v m /\ P k v = true.
  End find_pred.


  Module Notations.
    Notation "e1 ≈ e2" := (Equal e1 e2)
                             (at level 70, no associativity) : env_scope.

    Notation "e1 ≈⟨ R ⟩ e2" := (Equiv R e1 e2)
                                  (at level 70, no associativity,
                                   format "e1 '[' ≈⟨ R ⟩ ']' e2") : env_scope.

    Notation "e1 ⊑⟨ ee ⟩ e2" := (refines ee e1 e2)
                                  (at level 70, no associativity,
                                   format "e1 '[' ⊑⟨ ee ⟩ ']' e2") : env_scope.
    Notation "e1 ⊑ e2" := (refines eq e1 e2)
                            (at level 70, no associativity) : env_scope.

  End Notations.

End Env.

Open Scope env_scope.