Require Import Definitions.
Require Import Metatheory.
Require Import Env.
Require Import SubstEnv.
Require Import Rel.
Require Import Transp.
Require Import RelGood.

Definition stable_rel (R: rel (env term) term): Prop :=
  ∀ e a,
    in_rel R e a →
    ∀ e',
      all_env good_value e' →
      leq_env e e' →
      in_rel R e' a.

Add Parametric Morphism: stable_rel
    with signature (@RelEquiv (env term) term) ==> iff
      as stable_morphism_equiv.
Proof.
  intros R1 R2 H12; split; intro H; intros e v Hea e' Hgood' Hleq.
  - apply H12 in Hea. apply H12. eapply H; eauto.
  - apply H12 in Hea. apply H12. eapply H; eauto.
Qed.

Lemma stable_RelBot: stable_rel RelBot.
Proof.
  intros env a H env' H'. destruct H.
Qed.
Hint Resolve stable_RelBot: stable_rel.

Lemma stable_RelTop: stable_rel RelTop.
Proof.
  intros env a H env' H'. trivial.
Qed.
Hint Resolve stable_RelTop: stable_rel.

Lemma stable_RelTopEnvVal: stable_rel RelTopEnvVal.
Proof.
  intros env a H env' Hgood H'. destruct H. split; auto.
Qed.
Hint Resolve stable_RelTopEnvVal: stable_rel.

Lemma stable_RelInter (R1 R2: rel (env term) term):
  stable_rel R1 →
  stable_rel R2 →
  stable_rel (RelInter R1 R2).
Proof.
  intros Hwf1 Hwf2 env a [H1 H2] env' H'. split; eauto.
Qed.
Hint Resolve stable_RelInter: stable_rel.

Lemma stable_RelUnion (R1 R2: rel (env term) term):
  stable_rel R1 →
  stable_rel R2 →
  stable_rel (RelUnion R1 R2).
Proof.
  intros Hwf1 Hwf2 env a [H|H] env' H'; [left|right]; eauto.
Qed.
Hint Resolve stable_RelUnion: stable_rel.

Lemma stable_RelSelf t:
  stable_rel (RelSelf t).
Proof.
  intros e v Hev e' Hgood Hleq.
  simpl in Hev. destruct Hev as [Heq [Hfv [Hegood Hvgood]]]. simpl.
  split; [| split; [| split]]; auto.
  - rewrite <- subst_env_leq_env with (e := e); auto.
  - apply leq_env_dom in Hleq. fsetdec.
Qed.
Hint Resolve stable_RelSelf: stable_rel.

Lemma stable_RelLet0_strong (R1: atom → rel (env term) term) (R2: rel (env term) term) x:
  good_rel (R1 x) →
  stable_rel (R1 x) →
  stable_rel R2 →
  stable_rel (RelLet0_strong R1 R2 x).
Proof.
  intros Hgood1 HR1 HR2 e a H e' Hgood H'.
  simpl in ×. destruct H as [v [H2 H1]].
  ∃ v. split.
  - eapply HR2; eauto.
  - eapply HR1; eauto.
    + simpl. split; auto. eapply (Hgood1 _ _ H1); eauto.
    + simpl_env. auto using leq_env_update_stable.
Qed.

Lemma parametric_family_rel_RelLet0_strong S R1 R2:
  parametric_family_rel S R1 →
  supported_rel S R2 →
  parametric_family_rel S (RelLet0_strong R1 R2).
Proof.
  intros Hparam Hsupp x y Hx Hy e v. simpl.
  split; intros [v' [H2 H1]].
  - ∃ (transp_term x y v'). split.
    + apply (in_rel_equivariant x y) in H2.
      rewrite transp_env_term_involution in H2.
      rewrite (Hsupp x y) in H2; auto.
    + apply (in_rel_equivariant x y) in H1.
      rewrite (Hparam x y) in H1; auto.
      simpl_env in H1.
      rewrite transp_env_term_app in H1.
      rewrite transp_env_term_one in H1.
      rewrite transp_atom_thisL in H1.
      rewrite transp_env_term_involution in H1.
      rewrite transp_term_involution in H1.
      assumption.
  - ∃ (transp_term x y v'). split.
    + apply (in_rel_equivariant x y).
      rewrite transp_env_term_involution.
      rewrite transp_term_involution.
      rewrite (Hsupp x y); auto.
    + apply (in_rel_equivariant x y).
      rewrite (Hparam x y); auto.
      simpl_env.
      rewrite transp_env_term_app.
      rewrite transp_env_term_one.
      rewrite transp_atom_thisL.
      rewrite transp_env_term_involution.
      repeat rewrite transp_term_involution.
      assumption.
Qed.

Lemma stable_RelClose S (R: atom → rel (env term) term):
  (∀ x, x `notin` S → stable_rel (R x)) →
  stable_rel (RelClose S R).
Proof.
  intros Hstable e a [x [Hx HR]] e' Hgood' H'.
  simpl.
  ∃ x. split; auto.
  eapply Hstable; eauto.
Qed.

Lemma stable_RelLet_strong S (R1: atom → rel (env term) term) (R2: rel (env term) term):
  (∀ x, x `notin` S → good_rel (R1 x)) →
  (∀ x, x `notin` S → stable_rel (R1 x)) →
  stable_rel R2 →
  stable_rel (RelLet_strong S R1 R2).
Proof.
  intros Hgood1 Hstable1 Hstable2.
  eapply stable_RelClose; eauto.
  intros x Hx. eapply stable_RelLet0_strong; eauto.
Qed.
Hint Resolve stable_RelLet_strong: stable_rel.

Lemma stable_FUN S (R1 R2: rel (env term) term):
  stable_rel (FUN S R1 R2).
Proof.
  intros e v [Hedom [HGE [HGV H]]] e' Hgood H'.
  split; [| split; [| split]]; auto.
  - apply leq_env_dom in H'. fsetdec.
  - intros e'' H'' v1 Hv1 v2 Heval.
    eapply (H e''); eauto using leq_env_trans.
Qed.
Hint Resolve stable_FUN: stable_rel.

Lemma stable_APP (R1 R2: rel (env term) term):
  stable_rel R2 →
  stable_rel (APP R1 R2).
Proof.
  intros H2 e v H e' H'.
  destruct H as [e'' [v1 [v2 [H'' [Hv1 [Hv2 Heval]]]]]].
  ∃ e'', v1, v2.
  split; eauto using leq_env_trans.
Qed.
Hint Resolve stable_APP: stable_rel.

Lemma stable_depFUN S (R1: rel (env term) term) (R2: term → rel (env term) term):
  stable_rel (depFUN S R1 R2).
Proof.
  intros e v [Hedom [HGE [HGV H]]] e' Hgood H'.
  split; [| split; [| split]]; auto.
  - apply leq_env_dom in H'. fsetdec.
  - intros e'' H'' v1 Hv1 v2 Heval.
    eapply (H e''); eauto using leq_env_trans.
Qed.
Hint Resolve stable_depFUN: stable_rel.

Lemma stable_RelCompose_RelPush R1 x v R2 :
  good_rel R1 →
  stable_rel R1 →
  stable_rel R2 →
  stable_rel (RelCompose (RelPush R1 x v) R2).
Proof.
  intros Hgood1 Hstable1 Hstable2.
  intros e t [e'' [[Heq H1] H2]] e' Hgood' Hleq. subst.
  ∃ (x ¬ v ++ e'). split; [ split; [ reflexivity | ] | ].
  - eapply Hstable1; eauto.
  - eapply Hstable2; eauto.
    + simpl; split; eauto.
    + apply leq_env_update_stable. assumption.
Qed.

Lemma stable_RelUnitR:
  stable_rel RelUnitR.
Proof.
  intros e v H e' H' Hleq.
  simpl in H. simpl.
  destruct v; try contradiction.
  assumption.
Qed.
Hint Resolve stable_RelUnitR: stable_rel.

Lemma stable_RelPairR (R1 R2: rel (env term) term):
  stable_rel R1 →
  stable_rel R2 →
  stable_rel (RelPairR R1 R2).
Proof.
  intros H1 H2 e v H e' H'.
  simpl in H. simpl.
  destruct v; try contradiction.
  destruct H. split; eauto.
Qed.
Hint Resolve stable_RelPairR: stable_rel.

Lemma stable_RelSumR (R1 R2: rel (env term) term):
  stable_rel R1 →
  stable_rel R2 →
  stable_rel (RelSumR R1 R2).
Proof.
  intros H1 H2 e v H e' H'.
  simpl in H. simpl.
  destruct v; try contradiction; eauto.
Qed.
Hint Resolve stable_RelSumR: stable_rel.

Lemma stable_RelCompose (R1: rel (env term) term) (R2: rel term term):
  stable_rel R1 →
  stable_rel (RelCompose R1 R2).
Proof.
  intros H1 e v H e' H'.
  destruct H as [v0 [He Hv]].
  ∃ v0. eauto.
Qed.
Hint Resolve stable_RelCompose: stable_rel.

Lemma stable_RelGather E:
  all_env stable_rel E →
  stable_rel (RelGather E).
Proof.
  intros HE e v [HEGood [HvGood H]] e' Hgood Hleq.
  split; [| split]; auto.
  intros x R HR.
  assert (stable_rel R) as Hstable by (eapply all_env_get; eauto).
  apply H in HR. destruct HR as [v' [Hget HR]].
  ∃ v'. split; eauto.
Qed.
Hint Resolve stable_RelGather: stable_rel.