Require Import Infrastructure.
Require Import Env.
Require Import SubstEnv.
Require Import Rel.
Require Import RelExtra.
Require Import OkEnv.
Require Import EvalFacts.
Require Import RelGood.
Require Import RelStable.
Require Import Transp.
Require Import SupportFacts.
Require Import EquivarianceFacts.
Require Import OkEnv.
Require Import RelWf.

Definition ok_env_rel E (R: rel (env term) term) : Prop :=
  ∀ e v, in_rel R e v →
         all_env good_value e →
         ok_env E e.

Add Parametric Morphism: ok_env_rel
    with signature env_rel_equiv ==> RelEquiv ==> iff
      as ok_env_rel_morphism_equiv.
Proof.
  intros E1 E2 HE R1 R2 HR.
  split; intros H e v Hev Hgood.
  - rewrite <- HR in Hev. rewrite <- HE. eauto.
  - rewrite HR in Hev. rewrite HE. eauto.
Qed.

Lemma ok_env_rel_equivariant x y E R:
  ok_env_rel E R ↔ ok_env_rel (transp_env_rel x y E) (transp_rel x y R).
Proof.
  revert E R.
  assert (∀ E R, ok_env_rel E R → ok_env_rel (transp_env_rel x y E) (transp_rel x y R)).
  { intros E R H e v Hev Hgood.
    simpl in Hev.
    apply (ok_env_equivariant x y).
    rewrite transp_env_rel_involution.
    apply (H _ _ Hev).
    apply all_env_term_equivariant; auto using good_value_equivariant.
  }
  intros E R. split; intro; auto.
  apply H in H0.
  rewrite transp_rel_involution in H0.
  rewrite transp_env_rel_involution in H0.
  assumption.
Qed.

Lemma ok_env_rel_RelGather E:
  uniq E →
  ok_env_rel E (RelGather E).
Proof.
  intros Huniq. env induction E.
  - intros e v Hev Hgood.
    apply ok_envLeq with (e := nil).
    + constructor.
    + apply leq_env_nil_l.
    + simpl. trivial.
  - assert (ok_env_rel E (RelGather E)).
    { apply IHE. solve_uniq. }
    intros e v Hev Hgood.
    assert (in_rel (RelGather E) e v).
    { destruct Hev as [HEgood [Hgood' Hev]].
      split; [| split]; auto.
      intros y R HR.
      destruct (y == x); subst.
      - exfalso. apply get_in_dom in HR. solve_uniq.
      - destruct (Hev y R) as [v' [Hv' HR']].
        + rewrite get_update_other; auto.
        + ∃ v'. split; auto.
    }
    apply H in H0; auto.
    destruct Hev as [_ [_ Hev]].
    destruct (Hev x a) as [v' [Hv' HR']]; auto using get_update_this. clear Hev.
    case_eq (get x E); intros.
    + exfalso. apply get_in_dom in H1. solve_uniq.
    + apply ok_envLeq with (e := x ¬ v' ++ e).
      × constructor; auto.
      × apply leq_env_update3; auto.
      × simpl. split; auto. eapply all_env_get; eauto.
Qed.

Lemma ok_env_rel_RelBot E:
  ok_env_rel E RelBot.
Proof.
  intros ? ? [].
Qed.

Lemma ok_env_rel_RelInter E R1 R2:
  (ok_env_rel E R1 ∨ ok_env_rel E R2) →
  ok_env_rel E (RelInter R1 R2).
Proof.
  intros [H|H] e v [H1 H2] Hgood; eauto.
Qed.

Lemma ok_env_rel_RelUnion E R1 R2:
  ok_env_rel E R1 →
  ok_env_rel E R2 →
  ok_env_rel E (RelUnion R1 R2).
Proof.
  intros H1 H2 e v [H|H] Hgood; eauto.
Qed.

Lemma ok_env_rel_RelCompose E R1 R2:
  ok_env_rel E R1 →
  ok_env_rel E (RelCompose R1 R2).
Proof.
  intros H1 e v [v' [H1v H2v]] Hgood. eauto.
Qed.

Lemma ok_env_rel_RelPairR E R1 R2:
  (ok_env_rel E R1 ∨ ok_env_rel E R2) →
  ok_env_rel E (RelPairR R1 R2).
Proof.
  intros [H1|H2] e v H Hgood;
    destruct v; simpl in H; try contradiction; destruct H;
      eauto.
Qed.

Lemma ok_env_rel_RelSumR E R1 R2:
  ok_env_rel E R1 →
  ok_env_rel E R2 →
  ok_env_rel E (RelSumR R1 R2).
Proof.
  intros H1 H2 e v H Hgood.
  destruct v; simpl in H; try contradiction; eauto.
Qed.

Lemma ok_env_rel_RelRemove E R1 R2 x:
  ok_env_rel E R2 →
  ok_env_rel E (RelRemove R1 R2 x).
Proof.
  intros H2 e v [v' [H2' H1']] Hgood. eauto.
Qed.

Lemma ok_env_rel_RelClose E S R:
  (∀ x, x `notin` S → ok_env_rel E (R x)) →
  ok_env_rel E (RelClose S R).
Proof.
  intros H e v [x [Hx Hev]] Hgood.
  apply (H x Hx _ _ Hev); auto.
Qed.

Lemma ok_env_rel_lambda_rel E S x R:
  x `notin` S →
  dom E [<=] S →
  supported_env_rel S E →
  ok_env_rel E R →
  (∀ y, y `notin` S → ok_env_rel E ((lambda_rel x R) y)).
Proof.
  intros HxS HES HS HR y Hy e v Hev Hgood.
  apply (ok_env_rel_equivariant y x) in HR.
  apply HR in Hev.
  specialize (Hev Hgood).
  rewrite (transp_env_rel_fresh_eq S) in Hev; auto.
Qed.

Lemma ok_env_rel_RelLet E x R1 R2:
  x `notin` dom E →
  well_supported_env E →
  ok_env_rel E R1 →
  ok_env_rel E (RelLet (dom E) x R1 R2).
Proof.
  intros Hx HE HR1.
  apply ok_env_rel_RelClose.
  intros y Hy.
  apply (ok_env_rel_lambda_rel E (dom E)); auto.
  - reflexivity.
  - rewrite <- RelRemove_rewrite.
    apply ok_env_rel_RelRemove. assumption.
Qed.

Lemma ok_env_rel_APP E R1 R2:
  ok_env_rel E R2 →
  ok_env_rel E (APP R1 R2).
Proof.
  intros H2 e v [e' [v1 [v2 [Hleq [HR1 [HR2 Heval]]]]]] Hgood.
  eauto.
Qed.

Definition eval_rel t R: Prop :=
  ∀ e v, in_rel R e v →
         all_env good_value e →
         eval (subst_env e t) v.

Add Parametric Morphism: eval_rel
    with signature eq ==> RelEquiv ==> iff
      as eval_rel_morphism_equiv.
Proof.
  intros t R1 R2 HR.
  split; intros H e v Hev Hgood.
  - rewrite <- HR in Hev. auto.
  - rewrite HR in Hev. auto.
Qed.

Lemma eval_rel_equivariant x y t R:
  eval_rel t R ↔ eval_rel (transp_term x y t) (transp_rel x y R).
Proof.
  revert t R.
  assert (∀ t R, eval_rel t R → eval_rel (transp_term x y t) (transp_rel x y R)).
  { intros t R H; simpl in ×.
    unfold eval_rel in ×.
    intros e v Hev Hgood.
    apply (in_rel_equivariant x y) in Hev.
    rewrite transp_rel_involution in Hev.
    apply (all_env_term_equivariant good_value good_value_equivariant x y) in Hgood.
    apply <- (eval_equivariant x y).
    rewrite subst_env_equivariant.
    rewrite transp_term_involution.
    apply H; assumption.
  }
  intros t R; split; intro H'; auto.
  apply H in H'.
  rewrite transp_term_involution in H'.
  rewrite transp_rel_involution in H'.
  assumption.
Qed.

Lemma eval_rel_RelSelf t:
  eval_rel t (RelSelf t).
Proof.
  intros e v H Hgood. simpl in H. destruct H as [Heq [Hfv [Hdgood Hvgood]]].
  rewrite Heq. auto.
Qed.

Lemma eval_rel_RelInter t R1 R2:
  (eval_rel t R1 ∨ eval_rel t R2) →
  eval_rel t (RelInter R1 R2).
Proof.
  intros [H|H] e v [H1 H2]; eauto.
Qed.

Lemma eval_rel_Let x t1 t2 R1 R2 S:
  x `notin` S →
  good_rel R1 →
  supported_rel S R1 →
  fv t2 [<=] add x S →
  good_rel R2 →
  eval_rel t1 R1 →
  eval_rel t2 R2 →
  eval_rel (Let t1 (close x t2)) (RelLet S x R1 R2).
Proof.
  intros Hx Hgood1 Hsupp1 Hfv2 Hgood2 H1 H2 e v [y [Hy [v' [e' [[Heq H1'] H2']]]]] Hgood.
  subst.
  assert (fv v' [<=] empty) as Hfv' by eauto.
  rewrite eval_subst_env_iff; auto. ∃ v'. split.
  - apply (in_rel_equivariant y x) in H1'.
    rewrite (Hsupp1 y x) in H1'; auto.
    rewrite transp_env_term_involution in H1'.
    rewrite (transp_term_fresh_eq y x v') in H1';
      [| rewrite Hfv'; fsetdec | rewrite Hfv'; fsetdec ].
    auto.
  - rewrite <- (transp_term_fresh_eq y x (close x t2));
      [ | rewrite fv_close; fsetdec | rewrite fv_close; fsetdec ].
    rewrite close_equivariant.
    rewrite transp_atom_thisR.
    rewrite <- (subst_env_closed e v'); auto.
    rewrite <- subst_env_open; auto.
    rewrite (subst_intro y); [| rewrite fv_close; fsetdec].
    rewrite open_close.
    replace (subst_env e (subst v' y (transp_term y x t2))) with (subst_env (y ¬ v' ++ e) (transp_term y x t2))
      by reflexivity.
    apply (eval_equivariant y x).
    rewrite subst_env_equivariant.
    rewrite transp_env_term_app.
    rewrite transp_env_term_one.
    rewrite transp_atom_thisL.
    rewrite (transp_term_fresh_eq y x v'); [| fsetdec | fsetdec].
    rewrite transp_term_involution.
    apply H2 in H2'. apply H2'.
    simpl. split; eauto.
Qed.

Lemma eval_rel_App t1 t2 R1 R2:
  stable_rel R1 →
  good_rel R1 →
  good_rel R2 →
  eval_rel t1 R1 →
  eval_rel t2 R2 →
  eval_rel (App t1 t2) (APP R1 R2).
Proof.
  intros Hstable1 Hgood1 Hgood2 H1 H2 e v [e' [v1 [v2 [Hleq [H1' [H2' Heval]]]]]] Hgood.
  apply eval_iff in Heval.
  destruct Heval as [t1' [t2' [Heval1 [Heval2 Heval3]]]].
  apply eval_of_value in Heval1; eauto. subst v1.
  apply eval_of_value in Heval2; eauto. subst t2'.
  apply eval_subst_env_iff; auto.
  ∃ (subst_env e t1'), (subst_env e v2).
  split; [| split].
  - rewrite <- subst_env_Lam.
    apply H1; auto.
    rewrite subst_env_closed; [| eauto].
    eapply Hstable1; eauto.
  - apply H2; auto.
    rewrite subst_env_closed; [| eauto].
    assumption.
  - rewrite <- subst_env_open; [| eauto].
    rewrite subst_env_closed; auto.
    rewrite fv_open_upper.
    assert (fv (Lam t1') [<=] empty) as Hfv1 by eauto. simpl in Hfv1.
    assert (fv v2 [<=] empty) as Hfv2 by eauto.
    fsetdec.
Qed.

Lemma eval_rel_Unit:
  eval_rel Unit RelUnitR.
Proof.
  intros e v H Hgood.
  destruct v; simpl in *; try contradiction.
  apply eval_subst_env_iff; auto.
Qed.

Lemma eval_rel_Pair t1 t2 R1 R2:
  eval_rel t1 R1 →
  eval_rel t2 R2 →
  eval_rel (Pair t1 t2) (RelPairR R1 R2).
Proof.
  intros H1 H2 e v H Hgood.
  destruct v; simpl in *; try contradiction.
  destruct H as [H1' H2'].
  apply H1 in H1'. specialize (H1' Hgood).
  apply H2 in H2'. specialize (H2' Hgood).
  apply eval_subst_env_iff; auto.
  eauto.
Qed.

Lemma eval_rel_Fst t R:
  eval_rel t R →
  eval_rel (Fst t) (RelCompose R (RelPairL RelEqVal RelTopVal)).
Proof.
  intros H e v [v' [H1' H2']] Hgood.
  destruct v'; simpl in *; try contradiction.
  destruct H2' as [[Heq _] _].
  subst v.
  apply H in H1'. specialize (H1' Hgood).
  apply eval_subst_env_iff; auto.
  eauto.
Qed.

Lemma eval_rel_Snd t R:
  eval_rel t R →
  eval_rel (Snd t) (RelCompose R (RelPairL RelTopVal RelEqVal)).
Proof.
  intros H e v [v' [H1' H2']] Hgood.
  destruct v'; simpl in *; try contradiction.
  destruct H2' as [_ [Heq _]].
  subst v.
  apply H in H1'. specialize (H1' Hgood).
  apply eval_subst_env_iff; auto.
  eauto.
Qed.

Lemma eval_rel_InjL t R:
  eval_rel t R →
  eval_rel (InjL t) (RelSumR R RelBot).
Proof.
  intros H e v H' Hgood.
  destruct v; simpl in *; try contradiction.
  apply H in H'. specialize (H' Hgood).
  apply eval_subst_env_iff; auto.
  eauto.
Qed.

Lemma eval_rel_InjR t R:
  eval_rel t R →
  eval_rel (InjR t) (RelSumR RelBot R).
Proof.
  intros H e v H' Hgood.
  destruct v; simpl in *; try contradiction.
  apply H in H'. specialize (H' Hgood).
  apply eval_subst_env_iff; auto.
  eauto.
Qed.

Lemma eval_rel_Match t x1 t1 x2 t2 R R1 R2 S:
  x1 `notin` S →
  x2 `notin` S →
  good_rel R →
  supported_rel S R →
  fv t1 [<=] add x1 S →
  fv t2 [<=] add x2 S →
  good_rel R1 →
  good_rel R2 →
  eval_rel t R →
  eval_rel t1 R1 →
  eval_rel t2 R2 →
  eval_rel (Match t (close x1 t1) (close x2 t2))
           (RelUnion
              (RelLet S x1 (RelCompose R (RelSumL RelEqVal RelBot)) R1)
              (RelLet S x2 (RelCompose R (RelSumL RelBot RelEqVal)) R2)).
Proof.
  intros Hx1 Hx2 Hgood Hsupp Hfv1 Hfv2 Hgood1 Hgood2 H H1 H2 e v.
  intros [ [y [Hy [v1' [e' [[Heq [v' [H' H'']]] H1']]]]]
| [y [Hy [v2' [e' [[Heq [v' [H' H'']]] H2']]]]] ] Hgood'; subst.
  - assert (fv v' [<=] empty) as Hfv' by eauto.
    destruct v'; simpl in H''; try contradiction. destruct H'' as [Heq H'']. subst v1'.
    rewrite eval_subst_env_iff; auto. left. ∃ v'. split.
    + apply (in_rel_equivariant y x1) in H'.
      rewrite (Hsupp y x1) in H'; auto.
      rewrite transp_env_term_involution in H'.
      rewrite (transp_term_fresh_eq y x1) in H';
        [| rewrite Hfv'; fsetdec | rewrite Hfv'; fsetdec ].
      auto.
    + rewrite <- (transp_term_fresh_eq y x1 (close x1 t1));
        [ | rewrite fv_close; fsetdec | rewrite fv_close; fsetdec ].
      rewrite close_equivariant.
      rewrite transp_atom_thisR.
      rewrite <- (subst_env_closed e v'); auto.
      rewrite <- subst_env_open; auto.
      rewrite (subst_intro y); [| rewrite fv_close; fsetdec].
      rewrite open_close.
      replace (subst_env e (subst v' y (transp_term y x1 t1))) with (subst_env (y ¬ v' ++ e) (transp_term y x1 t1))
        by reflexivity.
      apply (eval_equivariant y x1).
      rewrite subst_env_equivariant.
      rewrite transp_env_term_app.
      rewrite transp_env_term_one.
      rewrite transp_atom_thisL.
      rewrite (transp_term_fresh_eq y x1 v'); [| fsetdec | fsetdec].
      rewrite transp_term_involution.
      apply H1 in H1'. apply H1'.
      simpl. split.
      × apply good_value_InjL_inv. eauto.
      × apply all_env_term_equivariant; auto using good_value_equivariant.
  - assert (fv v' [<=] empty) as Hfv' by eauto.
    destruct v'; simpl in H''; try contradiction. destruct H'' as [Heq H'']. subst v2'.
    rewrite eval_subst_env_iff; auto. right. ∃ v'. split.
    + apply (in_rel_equivariant y x2) in H'.
      rewrite (Hsupp y x2) in H'; auto.
      rewrite transp_env_term_involution in H'.
      rewrite (transp_term_fresh_eq y x2) in H';
        [| rewrite Hfv'; fsetdec | rewrite Hfv'; fsetdec ].
      auto.
    + rewrite <- (transp_term_fresh_eq y x2 (close x2 t2));
        [ | rewrite fv_close; fsetdec | rewrite fv_close; fsetdec ].
      rewrite close_equivariant.
      rewrite transp_atom_thisR.
      rewrite <- (subst_env_closed e v'); auto.
      rewrite <- subst_env_open; auto.
      rewrite (subst_intro y); [| rewrite fv_close; fsetdec].
      rewrite open_close.
      replace (subst_env e (subst v' y (transp_term y x2 t2))) with (subst_env (y ¬ v' ++ e) (transp_term y x2 t2))
        by reflexivity.
      apply (eval_equivariant y x2).
      rewrite subst_env_equivariant.
      rewrite transp_env_term_app.
      rewrite transp_env_term_one.
      rewrite transp_atom_thisL.
      rewrite (transp_term_fresh_eq y x2 v'); [| fsetdec | fsetdec].
      rewrite transp_term_involution.
      apply H2 in H2'. apply H2'.
      simpl. split.
      × apply good_value_InjR_inv. eauto.
      × apply all_env_term_equivariant; auto using good_value_equivariant.
Qed.

Definition CollectingSem (inputs: env term → Prop) (t: term) : rel (env term) term :=
  Rel _ _ (fun e v ⇒ eval (subst_env e t) v
                   ∧ inputs e
                   ∧ all_env good_value e).

Definition Rsem E t : rel (env term) term :=
  CollectingSem (ok_env E) t.

Add Parametric Morphism: Rsem
    with signature env_rel_equiv ==> eq ==> RelEquiv
      as Rsem_morphism_equiv.
Proof.
  intros E1 E2 HE t. intros e v.
  split; (intros [Heval [Hok Hgood]]; split; [| split]); auto.
  - rewrite <- HE. assumption.
  - rewrite HE. assumption.
Qed.

Add Parametric Morphism: Rsem
    with signature env_rel_incl ==> eq ==> RelIncl
      as Rsem_morphism_incl.
Proof.
  intros E1 E2 HE t. intros e v.
  intros [Heval [Hok Hgood]]; split; [| split]; auto.
  eauto using ok_env_env_rel_incl.
Qed.

Lemma Collecting_steps inputs t1 t2:
  steps t1 t2 →
  RelIncl (CollectingSem inputs t2) (CollectingSem inputs t1).
Proof.
  intros Hsteps.
  intros e v; intros [Heval [Hok Hgood]].
  split; [| split]; auto.
  destruct Heval as [Hsteps2 Hval]. split; auto.
  rewrite <- Hsteps2.
  apply steps_subst_env; auto.
Qed.

Lemma Rsem_steps E t1 t2:
  steps t1 t2 →
  RelIncl (Rsem E t2) (Rsem E t1).
Proof.
  apply Collecting_steps.
Qed.

Lemma Rsem_good E t:
  lc t →
  fv t [<=] dom E →
  good_rel (Rsem E t).
Proof.
  intros Hlc Hfv e v [Heval [Hok Hgood]].
  split; auto.
  apply eval_good_value in Heval; auto.
  - apply subst_env_lc; auto.
  - apply subst_env_closed_fv; auto.
    apply ok_env_dom in Hok. fsetdec.
Qed.

Lemma Rsem_stable E t:
  fv t [<=] dom E →
  stable_rel (Rsem E t).
Proof.
  intros Hfv e v [Heval [Hok Hgood]] e' Hgood' Hleq.
  split; [| split]; auto.
  - erewrite <- subst_env_leq_env; eauto.
    apply ok_env_dom in Hok. fsetdec.
  - eapply ok_envLeq; eauto.
Qed.

Lemma Rsem_equivariant x y E t:
  RelEquiv (transp_rel x y (Rsem E t)) (Rsem (transp_env_rel x y E) (transp_term x y t)).
Proof.
  intros e v; split; intros [HEval [Hstrong Hgood]]; (split; [| split]); auto.
  - apply (eval_equivariant x y) in HEval.
    rewrite subst_env_equivariant in HEval.
    rewrite transp_env_term_involution in HEval.
    rewrite transp_term_involution in HEval.
    assumption.
  - apply (ok_env_equivariant x y) in Hstrong.
    rewrite transp_env_term_involution in Hstrong.
    assumption.
  - apply (all_env_term_equivariant _ good_value_equivariant x y) in Hgood.
    rewrite transp_env_term_involution in Hgood.
    assumption.
  - apply (eval_equivariant x y) in HEval.
    rewrite subst_env_equivariant in HEval.
    rewrite transp_term_involution in HEval.
    assumption.
  - apply (ok_env_equivariant x y) in Hstrong.
    rewrite transp_env_rel_involution in Hstrong.
    assumption.
  - apply (all_env_term_equivariant _ good_value_equivariant x y) in Hgood.
    assumption.
Qed.

Lemma Rsem_supported_rel S E t:
  supported_env_rel S E →
  supported_rel (S `union` fv t) (Rsem E t).
Proof.
  intros HS x y Hx Hy.
  rewrite Rsem_equivariant.
  rewrite (HS x y); auto.
  rewrite transp_term_fresh_eq; auto.
  reflexivity.
Qed.

Lemma Rsem_wf_rel S E t:
  lc t →
  fv t [<=] dom E →
  supported_env_rel S E →
  wf_rel (S `union` fv t) (Rsem E t).
Proof.
  intros.
  split; [| split];
    auto using Rsem_good, Rsem_stable, Rsem_supported_rel.
Qed.

Lemma Rsem_ok_env_rel E t:
  ok_env_rel E (Rsem E t).
Proof.
  intros e v H Hgood. destruct H as [? [? ?]]. assumption.
Qed.

Lemma Rsem_dom E t e v:
  in_rel (Rsem E t) e v →
  dom E [<=] dom e.
Proof.
  intro H. apply ok_env_dom. simpl in H. tauto.
Qed.

Lemma Rsem_eval_rel E t:
  eval_rel t (Rsem E t).
Proof.
  intros e v H Hgood. destruct H as [? [? ?]]. assumption.
Qed.

Lemma RelIncl_Rsem_iff R E t:
  lc t →
  fv t [<=] dom E →
  (RelIncl R (Rsem E t)) ↔ (good_rel R ∧ ok_env_rel E R ∧ eval_rel t R).
Proof.
  intros Hlc Hfv.
  split; intro H; auto using Rsem_ok_env_rel, Rsem_eval_rel.
  - split; [| split]; intros e v Hev; apply H in Hev; destruct Hev as [Heval [Hok Hgood]]; auto.
    split; [assumption |].
    apply eval_good_value in Heval; auto.
    + apply subst_env_lc; auto.
    + apply subst_env_closed_fv; auto.
      apply ok_env_dom in Hok. fsetdec.
  - destruct H as [Hgood [Hstrong Heval]].
    intros e v Hev.
    split; [| split].
    + apply Heval; eauto.
    + eapply Hstrong; eauto.
    + eauto.
Qed.

Lemma RelIncl_Rsem_Self_Gather E t:
  lc t →
  fv t [<=] dom E →
  uniq E →
  RelIncl (RelInter (RelSelf t) (RelGather E)) (Rsem E t).
Proof.
  intros Hlc Hfv Huniq.
  apply RelIncl_Rsem_iff; auto.
  split; [ | split ].
  - auto with good_rel.
  - apply ok_env_rel_RelInter. right. apply ok_env_rel_RelGather; auto.
  - apply eval_rel_RelInter. left. apply eval_rel_RelSelf.
Qed.

Lemma Rsem_RelIncl_RelGather E t:
  lc t →
  fv t [<=] dom E →
  all_env stable_rel E →
  RelIncl (Rsem E t) (RelGather E).
Proof.
  intros Hlc Hfv Hstable.
  intros e v [Heval [Hok Hgood]].
  simpl. split; [| split]; auto.
  - apply (eval_good_value (subst_env e t)); auto.
    + apply subst_env_lc; auto.
    + apply subst_env_closed_fv; auto.
      apply ok_env_dom in Hok. fsetdec.
  - intros x R H. case_eq (get x e); intros.
    + ∃ t0. split; auto. eapply ok_env_get; eauto.
    + exfalso. eapply ok_env_get_None in H0; eauto. congruence.
Qed.

Lemma Rsem_RelIncl_RelSelf E t:
  lc t →
  is_extended_value t →
  fv t [<=] dom E →
  RelIncl (Rsem E t) (RelSelf t).
Proof.
  intros Hlc Hval Hfv.
  intros e v [Heval [Hok Hgood]].
  simpl. split; [| split; [| split]]; auto.
  - apply eval_of_value; auto.
    apply subst_env_is_value_iff; auto.
    apply ok_env_dom in Hok. fsetdec.
  - apply ok_env_dom in Hok. fsetdec.
  - apply eval_good_value in Heval; auto.
    + apply subst_env_lc; auto.
    + apply subst_env_closed_fv; auto.
      apply ok_env_dom in Hok. fsetdec.
Qed.

Lemma Rsem_RelIncl_Var_get E x R:
  wf_env_rel E →
  get x E = Some R →
  RelIncl (Rsem E (Var x)) R.
Proof.
  intros Hwf Hx.
  intros e v [Heval [Hok Hgood]].
  case_eq (get x e); intros.
  - assert (good_value t) as Hvgood.
    { eapply all_env_get; eauto. }
    rewrite (subst_env_Var_Some e x t) in Heval; auto.
    apply eval_of_value in Heval; subst; auto.
    eapply ok_env_get; eauto.
  - exfalso. eapply ok_env_get_None in H; eauto. congruence.
Qed.

Lemma Rsem_RelIncl_Var_self E x:
  x `in` dom E →
  RelIncl (Rsem E (Var x)) (RelSelf (Var x)).
Proof.
  intros Hx.
  apply Rsem_RelIncl_RelSelf; simpl; auto. fsetdec.
Qed.

Lemma Rsem_RelIncl_Var E x:
  wf_env_rel E →
  x `in` dom E →
  RelIncl (Rsem E (Var x))
          (RelInter (RelSelf (Var x)) (RelGather E)).
Proof.
  intros Hwf Hx.
  apply RelInter_glb.
  - apply Rsem_RelIncl_Var_self; eauto using get_in_dom.
  - apply Rsem_RelIncl_RelGather; auto.
    simpl. fsetdec.
Qed.

Lemma RelIncl_Rsem_Let E x t1 t2:
  lc t1 →
  lc t2 →
  fv t1 [<=] dom E →
  fv t2 [<=] add x (dom E) →
  x `notin` dom E →
  wf_env_rel E →
  RelIncl
    (RelLet (dom E) x (Rsem E t1) (Rsem (x ¬ Rsem E t1 ++ E) t2))
    (Rsem E (Let t1 (close x t2))).
Proof.
  intros Hlc1 Hlc2 Hfv1 Hfv2 Hx Hwf.
  apply RelIncl_Rsem_iff; [ | | split; [| split] ].
  - rewrite <- (open_close t2 x) in Hlc2.
    eapply lc_Let_exists; eauto.
  - simpl. rewrite fv_close. fsetdec.
  - apply RelLet_good; auto using Rsem_good.
    apply (supported_rel_subset (dom E `union` fv t1)); [ fsetdec |].
    apply Rsem_supported_rel; auto.
  - apply ok_env_rel_RelLet; auto using Rsem_ok_env_rel.
  - apply eval_rel_Let; auto using Rsem_good, Rsem_eval_rel.
    apply (supported_rel_subset (dom E `union` fv t1)); [ fsetdec |].
    apply Rsem_supported_rel; auto.
Qed.

Lemma dep_conj (P1 P2: Prop):
  P1 → (P1 → P2) → P1 ∧ P2.
Proof.
  tauto.
Qed.

Lemma notin_included_empty x S:
  S [<=] empty →
  x `notin` S.
Proof.
  intro. fsetdec.
Qed.
Hint Resolve notin_included_empty : core.

Lemma Rsem_RelIncl_Let E x t1 t2:
  lc t1 →
  lc t2 →
  fv t1 [<=] dom E →
  fv t2 [<=] add x (dom E) →
  x `notin` dom E →
  wf_env_rel E →
  RelIncl
    (Rsem E (Let t1 (close x t2)))
    (RelLet (dom E) x (Rsem E t1) (Rsem (x ¬ Rsem E t1 ++ E) t2)).
Proof.
  intros Hlc1 Hlc2 Hfv1 Hfv2 Hx Hwf.
  intros e v H.
  assert (good_value v) as Hgood2.
  { apply Rsem_good in H.
    - tauto.
    - auto with lngen.
    - simpl. rewrite fv_close. fsetdec.
  }
  assert (fv v [<=] empty) as Hfv_v by auto.
  pick fresh y for (singleton x `union` fv t1 `union` fv t2 `union` dom e `union` dom E).
  rewrite <- (transp_term_fresh_eq y x (close x t2)) in H;
    [ | rewrite fv_close; fsetdec | rewrite fv_close; fsetdec ].
  rewrite close_equivariant in H.
  rewrite transp_atom_thisR in H.
  destruct H as [Heval [Hok Hgood]].
  rewrite eval_subst_env_iff in Heval; auto.
  destruct Heval as [v1 [Heval1 Heval2]].
  assert (good_value v1) as Hgood1.
  { apply eval_good_value in Heval1; auto.
    - apply subst_env_lc; auto.
    - apply subst_env_closed_fv; auto.
      apply ok_env_dom in Hok. fsetdec.
  }
  assert (fv v1 [<=] empty) as Hfv_v1 by auto.
  rewrite <- (subst_env_closed e v1) in Heval2; auto.
  rewrite <- subst_env_open in Heval2; auto.
  rewrite <- subst_spec in Heval2.
  replace (subst_env e (subst v1 y (transp_term y x t2)))
    with (subst_env (y ¬ v1 ++ e) (transp_term y x t2)) in Heval2 by reflexivity.
  apply (in_rel_equivariant y x).
  rewrite RelLet_rel_equivariant.
  repeat rewrite Rsem_equivariant.
  rewrite transp_env_rel_app.
  rewrite transp_env_rel_one.
  rewrite transp_atom_thisR.
  rewrite transp_atoms_fresh_eq; auto.
  assert (env_rel_equiv
            ([(y, transp_rel y x (Rsem E t1))] ++ transp_env_rel y x E)
            ([(y, (Rsem E (transp_term y x t1)))] ++ E)) as Heq.
  { simpl; split; [| split]; auto.
    - rewrite Rsem_equivariant. rewrite transp_env_rel_fresh_eq; auto.
      reflexivity.
    - rewrite transp_env_rel_fresh_eq; auto. reflexivity.
  }
  rewrite Heq. clear Heq.
  rewrite transp_env_rel_fresh_eq; auto.
  rewrite (transp_term_fresh_eq y x t1); [ | eauto | eauto ].
  rewrite (transp_term_fresh_eq y x v); [ | eauto | eauto ].
  pick fresh z for (singleton x `union` singleton y `union` fv t1 `union` dom e `union` dom E).
  ∃ z. split; auto.
  unfold lambda_rel. unfold transp_rel. unfold in_rel at 1. rewrite <- RelRemove_rewrite.
  ∃ v1.
  rewrite transp_env_term_trans; auto.
  rewrite (transp_term_fresh_eq z y v); [ auto | eauto | eauto ].
  apply dep_conj; [| intro HRsem1 ].
  - split; [| split]; auto.
    + apply (eval_equivariant z x) in Heval1.
      rewrite subst_env_equivariant in Heval1.
      rewrite transp_term_fresh_eq in Heval1; auto.
      rewrite transp_term_fresh_eq in Heval1; [ auto | eauto | eauto ].
    + apply (ok_env_equivariant z x) in Hok.
      rewrite transp_env_rel_fresh_eq in Hok; auto.
    + apply all_env_term_equivariant; auto using good_value_equivariant.
  - split; [| split].
    + apply (eval_equivariant z x) in Heval2.
      rewrite subst_env_equivariant in Heval2.
      rewrite transp_env_term_app in Heval2.
      rewrite transp_env_term_one in Heval2.
      rewrite transp_atom_other in Heval2; auto.
      rewrite (transp_term_fresh_eq z x v1) in Heval2; [ | eauto | eauto ].
      rewrite (transp_term_fresh_eq z x v) in Heval2; [ | eauto | eauto ].
      rewrite (transp_term_freshL_is_subst y x t2) in Heval2; auto.
      rewrite (transp_term_freshL_is_subst y x t2); auto.
      rewrite (transp_term_fresh_eq z x (subst (Var y) x t2)) in Heval2; auto.
      × rewrite fv_subst_upper. simpl. clear Fr. fsetdec.
      × rewrite fv_subst_upper. simpl. clear Fr0. fsetdec.
    + apply ok_env_update; auto.
      × apply (ok_env_equivariant z x) in Hok.
        rewrite transp_env_rel_fresh_eq in Hok; auto.
      × rewrite <- (transp_atom_other z x y); auto.
        rewrite <- get_transp_env_term_equivariant.
        case_eq (get y e); intros; simpl; auto.
        exfalso. apply get_in_dom in H. clear Fr0. fsetdec.
    + simpl; split; auto.
      apply all_env_term_equivariant; auto using good_value_equivariant.
Qed.

Lemma Rsem_RelIncl_Lam_self E x t:
  lc t →
  fv t [<=] add x (dom E) →
  RelIncl (Rsem E (Lam (close x t))) (RelSelf (Lam (close x t))).
Proof.
  intros Hlc Hfv.
  apply Rsem_RelIncl_RelSelf; simpl; auto with lngen.
  rewrite fv_close. fsetdec.
Qed.

Lemma conj_recombine (A B C: Prop) :
  A ∧ B ∧ C ↔ (A ∧ B) ∧ C.
Proof.
  tauto.
Qed.

Lemma Rsem_RelIncl_Lam_RelLam R E x t:
  lc t →
  fv t [<=] add x (dom E) →
  x `notin` dom E →
  wf_rel (dom E) R →
  wf_env_rel E →
  RelIncl
    (Rsem E (Lam (close x t)))
    (RelLam (dom E) x R (Rsem (x ¬ R ++ E) t)).
Proof.
  intros Hlc Hfv Hx [HgoodR [HstableR HsuppR]] Hwf.
  intros e v H.
  assert (all_env good_value e ∧ good_value v) as [Hegood Hvgood].
  { apply Rsem_good in H; auto.
    - auto with lngen.
    - simpl. rewrite fv_close. fsetdec.
  }
  assert (fv v [<=] empty) as Hfv_v by auto.
  split; [| split; [| split]]; eauto using Rsem_dom.
  intros e' Hleq v1 HRv1 v2 Heval2.
  assert (all_env good_value e' ∧ good_value v1) as [He'good Hv1good] by auto.
  assert (fv v1 [<=] empty) as Hfv_v1 by auto.
  assert (good_value v2) as Hgood2.
  { apply eval_good_value in Heval2; auto.
    simpl. fsetdec.
  }
  pick fresh y for (singleton x `union` fv t `union` dom e' `union` dom E).
  rewrite <- (transp_term_fresh_eq y x (close x t)) in H;
    [ | rewrite fv_close; fsetdec | rewrite fv_close; fsetdec ].
  rewrite close_equivariant in H.
  rewrite transp_atom_thisR in H.
  rewrite transp_term_freshL_is_subst in H; auto.
  destruct H as [Heval [Hok Hgood]].
  rewrite eval_subst_env_iff in Heval; auto.
  apply (in_rel_equivariant y x).
  rewrite RelClose_rel_equivariant.
  rewrite transp_atoms_fresh_eq; auto.
  rewrite lambda_rel_equivariant.
  rewrite transp_atom_thisR.
  cut (in_rel
         (RelClose (dom E)
                   (lambda_rel y
                               (RelCompose (RelPush R y v1) (Rsem ([(y, R)] ++ E) (transp_term y x t)))))
         (transp_env_term y x e') (transp_term y x v2)).
  - intros [z [Hz [e'' [[Heq H1] H2]]]]. subst.
    ∃ z. split; auto.
    unfold lambda_rel.
    rewrite RelCompose_RelPush_equivariant.
    rewrite (HsuppR y x); auto.
    rewrite transp_atom_thisR.
    rewrite RelCompose_RelPush_transp_term; auto.
    rewrite Rsem_equivariant.
    assert (env_rel_equiv (transp_env_rel y x ([(x, R)] ++ E)) ([(y, R)] ++ E)) as Heq.
    { rewrite transp_env_rel_app. rewrite transp_env_rel_one.
      rewrite transp_atom_thisR.
      simpl; split; [| split] ; auto.
      rewrite transp_env_rel_fresh_eq; auto. reflexivity.
    }
    rewrite Heq. clear Heq.
    unfold transp_rel. unfold in_rel at 1.
    ∃ (y ¬ v1 ++ (transp_env_term z y (transp_env_term y x e'))).
    split; [ split |]; auto.
  - rewrite (transp_term_fresh_eq y x v2); [ | eauto | eauto ].
    rewrite transp_term_freshL_is_subst; auto.
    pick fresh z for (singleton x `union` singleton y `union` dom e' `union` dom E).
    ∃ z. split; auto.
    unfold lambda_rel. unfold transp_rel. unfold in_rel at 1.
    ∃ (y ¬ v1 ++ (transp_env_term z y (transp_env_term y x e'))).
    apply → conj_recombine. split; [ reflexivity |].
    rewrite transp_env_term_trans; auto.
    rewrite (transp_term_fresh_eq z y v2); [ auto | eauto | eauto ].
    apply dep_conj; [| intro HRsem1 ].
    + apply (in_rel_equivariant z x) in HRv1.
      rewrite (HsuppR z x) in HRv1; auto.
      rewrite transp_term_fresh_eq in HRv1; auto.
    + rewrite subst_env_Lam in Heval.
      erewrite subst_env_leq_env in Heval; eauto;
        [| apply ok_env_dom in Hok; rewrite fv_close; rewrite fv_subst_upper; simpl;
           rewrite Hfv; rewrite Hok; clear; fsetdec ].
      apply eval_iff in Heval2.
      destruct Heval2 as [t0 [v1' [Heval'0 [Heval'1 Heval2]]]].
      apply eval_of_value in Heval'0; auto. subst v.
      inversion Heval; subst. clear Heval.
      apply eval_of_value in Heval'1; auto. subst v1'.
      rewrite <- (subst_env_closed e' v1) in Heval2; auto.
      rewrite <- subst_env_open in Heval2; auto.
      rewrite <- subst_spec in Heval2.
      replace (subst_env e' (subst v1 y (subst (Var y) x t)))
        with (subst_env (y ¬ v1 ++ e') (subst (Var y) x t))
        in Heval2 by reflexivity.
      split; [| split].
      × apply (eval_equivariant z x) in Heval2.
        rewrite subst_env_equivariant in Heval2.
        rewrite transp_env_term_app in Heval2.
        rewrite transp_env_term_one in Heval2.
        rewrite transp_atom_other in Heval2; auto.
        rewrite (transp_term_fresh_eq z x v1) in Heval2; [ | eauto | eauto ].
        rewrite (transp_term_fresh_eq z x v2) in Heval2; [ | eauto | eauto ].
        { rewrite (transp_term_fresh_eq z x (subst (Var y) x t)) in Heval2; auto.
          - rewrite fv_subst_upper. simpl. clear Fr. fsetdec.
          - rewrite fv_subst_upper. simpl. clear Fr0. fsetdec.
        }
      × { apply ok_env_update; auto.
          - apply (ok_env_leq_env _ e e') in Hok; eauto.
            apply (ok_env_equivariant z x) in Hok.
            rewrite transp_env_rel_fresh_eq in Hok; auto.
          - rewrite <- (transp_atom_other z x y); auto.
            rewrite <- get_transp_env_term_equivariant.
            case_eq (get y e'); intros; simpl; auto.
            exfalso. apply get_in_dom in H. clear Fr0. fsetdec.
        }
      × simpl; split; auto.
        apply all_env_term_equivariant; auto using good_value_equivariant.
Qed.

Lemma Rsem_RelIncl_RelLam R E x t:
  lc t →
  fv t [<=] add x (dom E) →
  x `notin` dom E →
  wf_rel (dom E) R →
  wf_env_rel E →
  RelIncl
    (Rsem E (Lam (close x t)))
    (RelInter
       (RelLam (dom E) x R (Rsem (x ¬ R ++ E) t))
       (RelInter (RelSelf (Lam (close x t))) (RelGather E))
    ).
Proof.
  intros Hlc Hfv Hx HwfR Hwf.
  apply RelInter_glb; [| apply RelInter_glb].
  - apply Rsem_RelIncl_Lam_RelLam; auto.
  - apply Rsem_RelIncl_Lam_self; auto.
  - apply Rsem_RelIncl_RelGather; auto with lngen.
    simpl. rewrite fv_close. fsetdec.
Qed.

Lemma RelIncl_Rsem_App E t1 t2:
  lc t1 →
  lc t2 →
  fv t1 [<=] dom E →
  fv t2 [<=] dom E →
  RelIncl
    (APP (Rsem E t1) (Rsem E t2))
    (Rsem E (App t1 t2)).
Proof.
  intros Hlc1 Hlc2 Hfv1 Hfv2.
  apply RelIncl_Rsem_iff; [ | | split; [| split] ].
  - auto.
  - simpl. fsetdec.
  - apply good_rel_APP; auto using Rsem_good.
  - apply ok_env_rel_APP; auto using Rsem_ok_env_rel.
  - apply eval_rel_App; auto using Rsem_eval_rel, Rsem_good, Rsem_stable.
Qed.

Lemma Rsem_RelIncl_App E t1 t2:
  RelIncl
    (Rsem E (App t1 t2))
    (APP (Rsem E t1) (Rsem E t2)).
Proof.
  intros e v [Heval [Hok Hgood]].
  apply eval_subst_env_iff in Heval; auto.
  destruct Heval as [t0 [v2 [Heval1 [Heval2 Heval3]]]].
  ∃ e, (Lam t0), v2. split; [| split; [| split]].
  - reflexivity.
  - split; [| split]; auto.
  - split; [| split]; auto.
  - apply eval_iff.
    ∃ t0, v2. split; [| split]; auto.
    + apply eval_refl. simpl. trivial.
    + apply eval_refl. eapply eval_is_value; eauto.
Qed.

Lemma RelIncl_Rsem_Unit E:
  uniq E →
  RelIncl
    (RelInter RelUnitR (RelGather E))
    (Rsem E Unit).
Proof.
  intros Huniq.
  apply RelIncl_Rsem_iff; [ | | split; [| split] ].
  - auto.
  - simpl. fsetdec.
  - auto with good_rel.
  - apply ok_env_rel_RelInter. right. apply ok_env_rel_RelGather; auto.
  - apply eval_rel_RelInter. left. apply eval_rel_Unit.
Qed.

Lemma Rsem_RelIncl_Unit_UnitR E:
  RelIncl (Rsem E Unit) RelUnitR.
Proof.
  intros e v [Heval [Hok Hgood]].
  apply eval_subst_env_iff in Heval; auto. subst.
  simpl. assumption.
Qed.

Lemma Rsem_RelIncl_Unit E:
  all_env stable_rel E →
  RelIncl
    (Rsem E Unit)
    (RelInter RelUnitR (RelGather E)).
Proof.
  intro Hstable.
  apply RelInter_glb.
  - apply Rsem_RelIncl_Unit_UnitR.
  - apply Rsem_RelIncl_RelGather; auto.
    simpl. fsetdec.
Qed.

Lemma RelIncl_Rsem_Pair E t1 t2:
  lc t1 →
  lc t2 →
  fv t1 [<=] dom E →
  fv t2 [<=] dom E →
  RelIncl
    (RelPairR (Rsem E t1) (Rsem E t2))
    (Rsem E (Pair t1 t2)).
Proof.
  intros Hlc1 Hlc2 Hfv1 Hfv2.
  apply RelIncl_Rsem_iff; [ | | split; [| split] ].
  - auto.
  - simpl. fsetdec.
  - apply good_rel_RelPairR; auto using Rsem_good.
  - apply ok_env_rel_RelPairR; auto using Rsem_ok_env_rel.
  - apply eval_rel_Pair; auto using Rsem_eval_rel, Rsem_good, Rsem_stable.
Qed.