Require Import Var Val Env CSet Map.

Set Implicit Arguments.

Definition envOfType (E:onv val) (ET:onv ty) : Prop :=
  ∀ x t, ET x = Some t → ∃ v, E x = Some v ∧ valOfType v t.

Definition ompty X : onv X := fun _ ⇒ None.

Lemma envOfType_update E (ET:onv ty) (ETd:envOfType E ET) v t (vtd:valOfType v t) x
  : envOfType (E[x<-Some v]) (ET[x<-Some t]).

Lemma envOfType_empty E
  : envOfType E (ompty ty).

Definition subEnv Y (E E´:onv Y)
  := ∀ x y, E x = Some y → E´ x = Some y.

Lemma subEnv_refl Y (E:onv Y)
  : subEnv E E.

Lemma subEnv_empty Y (E:onv Y)
  : subEnv (ompty Y) E.

Lemma envOfType_weakening E ET ET´
  : subEnv ET ET´ → envOfType E ET´ → envOfType E ET.

Lemma subEnv_update Y (ET ET´:onv Y) x y
  : subEnv ET ET´ → subEnv (ET[x<-y]) (ET´[x<-y]).

Lemma subEnv_trans Y (ET ET´ ET´´:onv Y)
  : subEnv ET ET´ → subEnv ET´ ET´´ → subEnv ET ET´´.

Definition typed_eq {X Y:Type} (ET:onv Y) (E E´: env X) :=
  ∀ x t, ET x = Some t → E x = E´ x.

Lemma typed_eq_refl (X Y:Type) (ET:onv Y) : ∀ (E:env X), typed_eq ET E E.

Hint Resolve typed_eq_refl.

Global Instance typed_eq_Refl {X Y Z:Type} {ET:onv Y}
  : Reflexive (typed_eq ET) := @typed_eq_refl X Y ET.

Lemma typed_eq_sym X Y ET : ∀ E E´, @typed_eq X Y ET E E´ → typed_eq ET E´ E.

Global Instance typed_eq_Sym {X Y ET} `{Defaulted X} : Symmetric (typed_eq ET) :=
  @typed_eq_sym X Y ET.

Lemma typed_eq_trans X Y ET : ∀ E E´ E´´,
  @typed_eq X Y ET E E´ → typed_eq ET E´ E´´ → typed_eq ET E E´´.

Global Instance typed_eq_Trans {X Y ET} `{Defaulted X} : Transitive (typed_eq ET) :=
  @typed_eq_trans X Y ET.

Lemma typed_eq_update Y (ET:onv Y) (E E´:env val) (y:Y) (x:var) (z:val)
  : typed_eq ET E E´ → typed_eq (ET [x <- Some y]) (E [x <- z]) (E´ [x <- z]).

Lemma typed_eq_empty (Y:Type) (E E´:env val)
  : typed_eq (ompty Y) E E´.

Lemma typed_eq_envOfType ET E E´
  : typed_eq ET E E´ → envOfType E ET → envOfType E´ ET.

Lemma typed_eq_weakening Y (ET ET´: onv Y) (E E´:env val)
  : typed_eq ET E E´ → subEnv ET´ ET → typed_eq ET´ E E´.


Definition updD (D:env nat) (Z:list var) :=
  update_list D (fun x ⇒ S(D x)) Z.

Lemma updD_no_param D Z x
  : x ∉ of_list Z
  → (updD D Z) x === D x.

Lemma updD_param D Z x
  : x ∈ of_list Z
  → (updD D Z) x === S (D x).