Module FunctionalEnvironment

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

From Coq Require Import Setoid Morphisms.
From Coq Require Import Classes.RelationClasses.
Import Relation_Definitions.

Module FEnv.

  Class fenv_key (A : Type) :=
    { fenv_key_eqdec : EqDec A eq }.

  Global Instance ident_fenv_key : fenv_key ident :=
    {| fenv_key_eqdec := EqDec_instance_0 |}.

  Section FEnv.
    Context {K : Type} `{K_key : fenv_key K}.
    Local Instance: EqDec K eq := { equiv_dec := fenv_key_eqdec }.

    Definition t A := K -> 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 find_In : forall env x v,
          env x = Some v -> In x env.

      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.


    Section dom.
      Context {A : Type}.

      Definition dom (env : t A) (xs : list K) :=
        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 K) :=
        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 K) :=
        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 K) : t A :=
        fun x => if List.existsb (fun y => y ==b 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.

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

      Fact union_empty R `{Reflexive _ R} : forall m,
          Equiv R (union (empty _) m) m.
    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 : K -> 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 (K * A)) : t A :=
        fun x => option_map snd (List.find (fun y => x ==b fst y) l).

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

      Fact find_some' : forall {A} (xs : list (K * A)) x v ,
          NoDupMembers xs ->
          List.In (x, v) xs ->
          List.find (fun xtc => x ==b fst xtc) xs = Some (x, v).

      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.
End FEnv.


Global Hint Resolve FEnv.refines_refl : 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.