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 mapi_elements {B} (f : _ -> A -> B) : forall m,
        Env.elements (Env.mapi f m) = List.map (fun '(x, y) => (x, f x y)) (Env.elements 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.

    Lemma map_Equiv {B} {Ra: A -> A -> Prop} {Rb: B -> B -> Prop} : forall (f : A -> B) (m1 m2: t A),
        (forall x y, Ra x y -> Rb (f x) (f y)) ->
        Env.Equiv Ra m1 m2 ->
        Env.Equiv Rb (Env.map f m1) (Env.map f m2).

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

    Lemma find_gsss'_irrelevant:
      forall x a xvs m1 m2,
        InMembers x xvs ->
        find x (adds' xvs m1) = Some a ->
        find x (adds' xvs m2) = Some a.

    Corollary find_gsss'_empty:
      forall x a xvs m,
        find x (adds' xvs (Env.empty _)) = Some a ->
        find x (adds' xvs m) = Some a.

    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 xs vs x (a: A) m,
        adds (x :: xs) (a :: vs) m = adds xs vs (add x a m).

    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 NoDup_snd_elements : forall env x1 x2 (y : A),
        NoDup (List.map snd (elements env)) ->
        find x1 env = Some y ->
        find x2 env = Some y ->
        x1 = x2.

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

    Corollary elements_from_list: forall xs,
        NoDupMembers xs ->
        Permutation.Permutation (elements (from_list xs)) 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).

    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.


  Global 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'.

    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.

    Lemma refines_elements : forall env1 env2,
        refines env1 env2 ->
        incl (List.map fst (elements env1)) (List.map fst (elements env2)).

  End EnvRefines.

  Global Existing Instance env_refines_preorder.
  Global Existing Instance Equivalence_Equiv.

  Global Hint Immediate refines_empty : env.
  Global Hint Extern 4 (refines _ (add ?x _ _) (add ?x _ _)) => apply refines_add : env.
  Global Hint Resolve refines_refl refines_trans refines_add refines_add_both refines_add_right
         refines_remove refines_remove_both refines_add_remove refines_orel_find
         refines_find_add_left refines_find_add_right refines_add_left refines_elements : env.

  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}.
    Variable (R : V -> V -> Prop).

    Hypothesis R_refl : Reflexive R.
    Hypothesis R_trans : Transitive R.

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

    Lemma refines_adds' : forall (xs : list (ident * V)) H,
        Forall (fun id => ~In id H) (List.map fst xs) ->
        refines R H (adds' xs H).

    Corollary refines_adds : forall ids (vs : list V) H,
        Forall (fun id => ~In id H) ids ->
        refines R 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.

  Global Hint Resolve refines_adds' refines_adds refines_adds_opt : env.

  Lemma refines_map : forall {V1 V2} {eq1 : V1 -> V1 -> Prop} {eq2 : V2 -> V2 -> Prop} (f : V1 -> V2) H1 H2,
      (forall x y, eq1 x y -> eq2 (f x) (f y)) ->
      Env.refines eq1 H1 H2 ->
      Env.refines eq2 (map f H1) (map f H2).

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

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

  Lemma adds_opt_mono {A: Type}:
    forall x (env: t A) ys rvos,
      In x env ->
      In x (adds_opt ys rvos env).

  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.

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

  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} : (@adds' A)
      with signature (eq ==> Equiv eq ==> Equiv eq)
        as adds'_Equiv.

  Import Permutation.

  Lemma adds'_Perm {A} : forall (xs ys : list (ident * A)) m,
      NoDupMembers xs ->
      Permutation xs ys ->
      Env.Equiv eq (adds' xs m) (adds' ys m).

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

  Lemma dom_map : forall {V1 V2} (f : V1 -> V2) xs H,
      dom (Env.map f H) xs <-> dom H 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_incl: forall H xs ys,
        incl xs ys ->
        dom_ub H xs ->
        dom_ub H ys.

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

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

    Global Opaque dom_ub.
  End EnvDomUpperBound.

  Lemma dom_ub_map : forall {V1 V2} (f : V1 -> V2) xs H,
      dom_ub (Env.map f H) xs <-> dom_ub H xs.

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

  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_incl: forall H xs ys,
        incl xs ys ->
        dom_lb H ys ->
        dom_lb H xs.

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

    Lemma dom_lb_refines:
      forall R H H' xs,
        Env.refines R H H' ->
        dom_lb H xs ->
        dom_lb H' xs.

    Lemma dom_lb_map:
      forall f H xs,
        dom_lb H xs <->
        dom_lb (map f H) xs.

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

    Corollary dom_lb_concat: forall H xss,
        Forall (dom_lb H) xss ->
        dom_lb H (concat xss).

    Global Opaque dom_lb.
  End EnvDomLowerBound.

  Global Hint Resolve dom_lb_nil : env.

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

  Lemma adds'_dom_ub : forall {A} (H : t A) d xs,
      dom_ub H d ->
      dom_ub (Env.adds' xs H) (d ++ List.map fst xs).

  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.

    Variable R : A -> A -> Prop.
    Hypothesis Hequiv: Equivalence R.

    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_find1' : forall m1 m2 x y1 y2,
        find x m1 = Some y1 ->
        find x m2 = Some y2 ->
        find x (union m1 m2) = Some y2.

    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.

    Corollary union_find3' : forall m1 m2 x y,
        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_find4' : forall m1 m2 x y,
        find x (union m1 m2) = Some y ->
        (find x m1 = Some y /\ find x m2 = None) \/ find x m2 = Some y.

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

    Lemma union_refines2 : forall m m1 m2,
        refines R m m1 ->
        refines R m m2 ->
        refines R 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 R m m1 ->
        refines R m m2 ->
        refines R 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 R m m1 ->
        refines R m m2 ->
        refines R m2 (union m1 m2).

    Lemma union_refines4' : forall m1 m2,
        refines R m2 (union m1 m2).

    Lemma union_In : forall x e1 e2,
        In x (union e1 e2) <-> In x e1 \/ In x e2.

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

    Lemma union_dom_lb : forall m1 m2 xs ys,
        dom_lb m1 xs ->
        dom_lb m2 ys ->
        dom_lb (union m1 m2) (xs ++ ys).

    Lemma union_dom_lb2 : forall m1 m2 xs,
        dom_lb m2 xs ->
        dom_lb (union m1 m2) xs.

    Lemma union_dom_ub : forall m1 m2 xs,
        dom_ub m1 xs ->
        dom_ub m2 xs ->
        dom_ub (union m1 m2) xs.

    Lemma union_dom_ub_app : forall m1 m2 xs ys,
        dom_ub m1 xs ->
        dom_ub m2 ys ->
        dom_ub (union m1 m2) (xs ++ ys).

    Corollary union_mem : forall x e1 e2,
        mem x (union e1 e2) = mem x e1 || mem x e2.

    Lemma elements_union : forall e1 e2,
        (forall x, Env.In x e1 -> ~Env.In x e2) ->
        Permutation.Permutation (elements (union e1 e2)) (elements e1 ++ elements e2).

    Definition unions (envs : list (Env.t A)) :=
      List.fold_left union envs (Env.empty _).
  End union.

  Add Parametric Morphism {A} (R : A -> A -> Prop) : union
      with signature Env.Equiv R ==> Env.Equiv R ==> Env.Equiv R
        as union_Equiv.

  Section union_fuse.
    Context {A : Type}.

    Variable fuse : A -> A -> A.

    Definition union_fuse (m1 m2 : t A) :=
      Env.fold (fun x a1 m2 => add x (or_default_with a1 (fuse a1) (Env.find x m2)) m2) m1 m2.

    Lemma union_fuse_spec : forall m1 m2 x,
        find x (union_fuse m1 m2) =
        match (find x m1), (find x m2) with
        | Some y1, Some y2 => Some (fuse y1 y2)
        | Some y1, None => Some y1
        | None, Some y2 => Some y2
        | None, None => None
        end.

    Corollary union_fuse_In : forall m1 m2 x,
        In x (union_fuse m1 m2) <-> In x m1 \/ In x m2.

  End union_fuse.

  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.


  Declare Scope env_scope.

  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.