Module FunctionalEnvironment

From Velus Require Import Common.CommonTactics.
From Velus Require Import Common.
From Velus Require Import Operators.

From Coq Require Import Setoid Morphisms.
Import Relation_Definitions.

Module FEnv.

  Definition t A := ident -> option A.

  Definition empty A : t A := fun _ => None.

  Section In.
    Context {A : Type}.

    Definition In x (env : t A) :=
      exists v, env x = Some v.

    Lemma not_find_In : forall env x,
        ~In x env <-> env x = None.
  End In.

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

    Definition Equiv (env1 env2 : t A) : Prop :=
      forall x, (orel R) (env1 x) (env2 x).

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

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

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

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

    Global Add Parametric Morphism : In
           with signature (eq --> Equiv --> iff)
             as Equiv_In.
  End Equiv.

  Global Existing Instance Equivalence_Equiv.

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

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

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

    Lemma In_refines : forall env1 env2,
        refines env1 env2 ->
        forall x, In x env1 -> In x env2.

    Lemma refines_None : forall m1 m2 x,
        refines m1 m2 ->
        m2 x = None ->
        m1 x = None.

    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.

  End refines.
  Global Hint Resolve refines_refl : fenv.


  Section dom.
    Context {A : Type}.

    Definition dom (env : t A) (xs : list ident) :=
      forall x, In x env <-> List.In x xs.
  End dom.

  Section dom_ub.
    Context {A : Type}.

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

    Lemma dom_ub_incl : forall env xs1 xs2,
        List.incl xs1 xs2 ->
        dom_ub env xs1 ->
        dom_ub env xs2.

    Lemma dom_ub_refines {R} : forall env1 env2 xs,
        refines R env2 env1 ->
        dom_ub env1 xs ->
        dom_ub env2 xs.

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

  Section dom_lb.
    Context {A : Type}.

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

    Lemma dom_lb_incl : forall env xs1 xs2,
        List.incl xs2 xs1 ->
        dom_lb env xs1 ->
        dom_lb env xs2.

    Lemma dom_lb_refines {R} : forall env1 env2 xs,
        refines R env1 env2 ->
        dom_lb env1 xs ->
        dom_lb env2 xs.

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

  Section restrict.
    Context {A : Type}.

    Definition restrict (env : t A) (xs : list ident) : t A :=
      fun x => if mem_ident x xs then env x else None.

    Lemma restrict_find : forall env xs x v,
        List.In x xs ->
        env x = Some v ->
        (restrict env xs) x = Some v.

    Lemma restrict_find_inv : forall env xs x v,
        (restrict env xs) x = Some v ->
        List.In x xs /\ env x = Some v.

    Corollary restrict_find_None1 : forall env xs x,
        ~List.In x xs ->
        (restrict env xs) x = None.

    Corollary restrict_find_None2 : forall env xs x,
        env x = None ->
        (restrict env xs) x = None.

    Lemma restrict_find_None_inv : forall env xs x,
        (restrict env xs) x = None ->
        env x = None \/ ~List.In x xs.

    Lemma restrict_refines : forall R xs (env : t A),
        Reflexive R ->
        refines R (restrict env xs) env.

    Lemma restrict_refines' : forall R xs env1 env2,
        refines R env1 env2 ->
        refines R (restrict env1 xs) (restrict env2 xs).

    Lemma incl_restrict_refines R `{Reflexive _ R} : forall xs ys (env : t A),
        List.incl xs ys ->
        refines R (restrict env xs) (restrict env ys).

    Lemma restrict_In : forall xs env x,
        In x (restrict env xs) <-> In x env /\ List.In x xs.

    Corollary restrict_dom_ub : forall env xs,
        dom_ub (restrict env xs) xs.

    Corollary restrict_dom_ub' : forall xs ys (env : t A),
        dom_ub env ys ->
        dom_ub (restrict env xs) ys.

    Corollary dom_lb_restrict_dom : forall xs (env : FEnv.t A),
        dom_lb env xs ->
        dom (restrict env xs) xs.

    Lemma restrict_Equiv : forall R xs env1 env2,
        Equiv R env1 env2 ->
        Equiv R (restrict env1 xs) (restrict env2 xs).
  End restrict.

  Section add.
    Context {A : Type}.

    Definition add x v (env : t A) :=
      fun y => if y ==b x then Some v else env y.

    Lemma gss : forall x v env,
        (add x v env) x = Some v.

    Lemma gso : forall x v env y,
        y <> x ->
        (add x v env) y = env y.

    Lemma add_In : forall env x v y,
        In y (add x v env) <-> x = y \/ In y env.

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

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

    Lemma add_dom_ub : forall env x v xs,
        dom_ub env xs ->
        dom_ub (add x v env) (x::xs).

    Lemma add_dom_lb : forall env x v xs,
        dom_lb env xs ->
        dom_lb (add x v env) (x::xs).

  End add.

  Section union.
    Context {A : Type}.

    Definition union (env1 env2 : t A) :=
      fun x => match env2 x with
            | Some v => Some v
            | None => env1 x
            end.

    Lemma union1 : forall env1 env2 x v,
        env1 x = Some v ->
        env2 x = Some v ->
        (union env1 env2) x = Some v.

    Lemma union2 : forall env1 env2 x v,
        env1 x = Some v ->
        env2 x = None ->
        (union env1 env2) x = Some v.

    Lemma union3 : forall env1 env2 x v,
        env1 x = None ->
        env2 x = Some v ->
        (union env1 env2) x = Some v.

    Fact union3' : forall env1 env2 x v,
        env2 x = Some v ->
        (union env1 env2) x = Some v.

    Lemma union4 : forall env1 env2 x v,
        (union env1 env2) x = Some v ->
        env1 x = Some v \/ env2 x = Some v.

    Corollary union_None : forall env1 env2 x,
        (union env1 env2) x = None <-> env1 x = None /\ env2 x = None.

    Fact union4' : forall env1 env2 x v,
        (union env1 env2) x = Some v ->
        env2 x = Some v \/ (env1 x = Some v /\ env2 x = None).

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

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

    Lemma union_dom_ub : forall env1 env2 xs,
        dom_ub env1 xs ->
        dom_ub env2 xs ->
        dom_ub (union env1 env2) xs.

    Lemma union_dom_lb : forall env1 env2 xs1 xs2,
        dom_lb env1 xs1 ->
        dom_lb env2 xs2 ->
        dom_lb (union env1 env2) (xs1 ++ xs2).

    Lemma union_dom_lb1 : forall env1 env2 xs,
        dom_lb env1 xs ->
        dom_lb (union env1 env2) xs.

    Lemma union_dom_lb2 : forall env1 env2 xs,
        dom_lb env2 xs ->
        dom_lb (union env1 env2) xs.

    Lemma union_refines1 R `{Reflexive _ R} : forall m1 m1' m2,
        refines R m1 m1' ->
        refines R (union m1 m2) (union m1' m2).

    Lemma union_refines4' R `{Reflexive _ R} : forall m1 m2,
        refines R m2 (union m1 m2).

    Lemma union_refines_inv R `{Reflexive _ R} : forall m1 m2 m',
        refines R (union m1 m2) m' ->
        (forall x, In x m1 -> ~In x m2) ->
        exists m2', Equiv R (union m1 m2') m'
               /\ refines R m2 m2'
               /\ (forall x, In x m2' <-> In x m' /\ ~In x m1).

    Lemma union_assoc R `{Reflexive _ R} : forall m1 m2 m3,
        Equiv R (union m1 (union m2 m3)) (union (union m1 m2) m3).
  End union.

  Section map.
    Context {A B : Type}.

    Definition map (f : A -> B) (env : t A) :=
      fun x => option_map f (env x).

    Lemma map_in_iff f : forall x env,
        In x (map f env) <-> In x env.

    Lemma dom_map f : forall env xs,
        dom (map f env) xs <-> dom env xs.

    Lemma dom_ub_map f : forall env xs,
        dom_ub (map f env) xs <-> dom_ub env xs.

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

    Lemma map_Equiv (R1 : relation A) (R2 : relation B) f : forall env1 env2,
        (forall x y, R1 x y -> R2 (f x) (f y)) ->
        Equiv R1 env1 env2 ->
        Equiv R2 (map f env1) (map f env2).

    Lemma refines_map (R1 : relation A) (R2 : relation B) f : forall env1 env2,
        (forall x y, R1 x y -> R2 (f x) (f y)) ->
        refines R1 env1 env2 ->
        refines R2 (map f env1) (map f env2).

    Lemma restrict_map R `{Reflexive _ R} f : forall env xs,
        Equiv R (restrict (map f env) xs) (map f (restrict env xs)).

    Lemma union_map R `{Reflexive _ R} f : forall env1 env2,
        Equiv R (map f (union env1 env2)) (union (map f env1) (map f env2)).
  End map.

  Lemma map_map {A B C} R `{Reflexive _ R} : forall env (f1 : A -> B) (f2 : B -> C),
      Equiv R (map f2 (map f1 env)) (map (fun x => f2 (f1 x)) env).

  Section mapi.
    Context {A B : Type}.

    Definition mapi (f : ident -> A -> B) (env : t A) :=
      fun x => option_map (f x) (env x).

    Lemma mapi_in_iff f : forall x env,
        In x (mapi f env) <-> In x env.
  End mapi.

  Section of_list.
    Context {A : Type}.

    Definition of_list (l : list (ident * A)) : t A :=
      fun x => assoc_ident x l.

    Lemma of_list_find_In : forall l x a,
        (of_list l) x = Some a ->
        List.In (x, a) l.

    Lemma of_list_In_find : forall l x a,
         NoDupMembers l ->
         List.In (x, a) l ->
         (of_list l) x = Some a.

    Lemma of_list_In : forall l x,
        In x (of_list l) <-> InMembers x l.

    Lemma of_list_None : forall l x,
        (of_list l) x = None <-> ~InMembers x l.

  End of_list.

End FEnv.


Global Hint Unfold FEnv.map FEnv.mapi : fenv.


Ltac simpl_fenv :=
  autounfold with fenv in *;
  inv_equalities.


Declare Scope fenv_scope.
Infix "+" := FEnv.union (left associativity, at level 50) : fenv_scope.
Delimit Scope fenv_scope with fenv.