Lvc.Isa.MoreExp

Require Import Util DecSolve Val CSet Map Get Env EnvTy Option.
Require Import Arith Exp OptionMap.

Set Implicit Arguments.

Lemma exp_eval_agree E E´ e v
: agree_on eq (Exp.freeVars e) E E´
  → exp_eval E e = v
  → exp_eval E´ e = v.

Lemma omap_exp_eval_agree E E´ Y v
: agree_on eq (list_union (List.map freeVars Y)) E E´
  → omap (exp_eval E) Y = v
  → omap (exp_eval E´) Y = v.

Lemma exp_eval_live_agree E E´ e lv v
: live_exp_sound e lv
  → agree_on eq lv E E´
  → exp_eval E e = v
  → exp_eval E´ e = v.

Lemma omap_exp_eval_live_agree E E´ lv Y v
: (∀ n y, get Y n y → live_exp_sound y lv)
  → agree_on eq lv E E´
  → omap (exp_eval E) Y = v
  → omap (exp_eval E´) Y = v.

Lemma omap_self_update E Z l
: omap (exp_eval E) (List.map Var Z) = ⎣l ⎦
   → E [Z <-- List.map Some l] ≡ E.