Require Import Transp.
Require Import EquivarianceFacts.
Require Import Infrastructure.
Require Import Env.
Require Import SubstEnv.
Require Import Rel.
Require Import RelGood.
Require Import RelStable.

Lemma RelBot_supported_rel S:
  supported_rel S RelBot.
Proof.
  intros x y Hx Hy. apply RelBot_rel_equivariant.
Qed.

Hint Resolve RelBot_supported_rel: supported_rel.

Lemma RelBot_supported_vrel S:
  supported_vrel S RelBot.
Proof.
  intros x y Hx Hy. apply RelBot_vrel_equivariant.
Qed.

Hint Resolve RelBot_supported_vrel: supported_rel.

Lemma RelTopEnvVal_supported_rel S:
  supported_rel S RelTopEnvVal.
Proof.
  intros x y Hx Hy. apply RelTopEnvVal_rel_equivariant.
Qed.

Hint Resolve RelTopEnvVal_supported_rel: supported_rel.

Lemma RelTopVal_supported_vrel S:
  supported_vrel S RelTopVal.
Proof.
  intros x y Hx Hy. apply RelTopVal_vrel_equivariant.
Qed.

Hint Resolve RelTopVal_supported_vrel: supported_rel.

Lemma RelEqVal_supported_vrel S:
  supported_vrel S RelEqVal.
Proof.
  intros x y Hx Hy. apply RelEqVal_vrel_equivariant.
Qed.

Hint Resolve RelEqVal_supported_vrel: supported_rel.

Lemma RelInter_supported_rel S R1 R2:
  supported_rel S R1 →
  supported_rel S R2 →
  supported_rel S (RelInter R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelInter_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelInter_supported_rel: supported_rel.

Lemma RelInter_supported_vrel S R1 R2:
  supported_vrel S R1 →
  supported_vrel S R2 →
  supported_vrel S (RelInter R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelInter_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelInter_supported_vrel: supported_rel.

Lemma RelUnion_supported_rel S R1 R2:
  supported_rel S R1 →
  supported_rel S R2 →
  supported_rel S (RelUnion R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelUnion_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelUnion_supported_rel: supported_rel.

Lemma RelUnion_supported_vrel S R1 R2:
  supported_vrel S R1 →
  supported_vrel S R2 →
  supported_vrel S (RelUnion R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelUnion_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelUnion_supported_vrel: supported_rel.

Lemma RelCompose_supported_rel S R1 R2:
  supported_rel S R1 →
  supported_vrel S R2 →
  supported_rel S (RelCompose R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelCompose_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelCompose_supported_rel: supported_rel.

Lemma RelCompose_RelInv_supported_rel S R1 R2:
  supported_rel S R1 →
  supported_rel S R2 →
  supported_vrel S (RelCompose (RelInv R1) R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelCompose_RelInv_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelCompose_RelInv_supported_rel: supported_rel.

Lemma RelCompose_supported_vrel S R1 R2:
  supported_vrel S R1 →
  supported_vrel S R2 →
  supported_vrel S (RelCompose R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelCompose_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelCompose_supported_vrel: supported_rel.

Lemma RelUnitR_supported_rel S:
  supported_rel S RelUnitR.
Proof.
  intros x y Hx Hy. apply RelUnitR_rel_equivariant.
Qed.

Hint Resolve RelUnitR_supported_rel: supported_rel.

Lemma RelPairR_supported_rel S R1 R2:
  supported_rel S R1 →
  supported_rel S R2 →
  supported_rel S (RelPairR R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelPairR_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelPairR_supported_rel: supported_rel.

Lemma RelPairR_supported_vrel S R1 R2:
  supported_vrel S R1 →
  supported_vrel S R2 →
  supported_vrel S (RelPairR R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelPairR_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelPairR_supported_vrel: supported_rel.

Lemma RelPairL_supported_vrel S R1 R2:
  supported_vrel S R1 →
  supported_vrel S R2 →
  supported_vrel S (RelPairL R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelPairL_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelPairL_supported_vrel: supported_rel.

Lemma RelSumR_supported_rel S R1 R2:
  supported_rel S R1 →
  supported_rel S R2 →
  supported_rel S (RelSumR R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelSumR_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelSumR_supported_rel: supported_rel.

Lemma RelSumR_supported_vrel S R1 R2:
  supported_vrel S R1 →
  supported_vrel S R2 →
  supported_vrel S (RelSumR R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelSumR_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelSumR_supported_vrel: supported_rel.

Lemma RelSumL_supported_vrel S R1 R2:
  supported_vrel S R1 →
  supported_vrel S R2 →
  supported_vrel S (RelSumL R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelSumL_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelSumL_supported_vrel: supported_rel.

Lemma RelGather_supported_rel S E:
  supported_env_rel S E →
  supported_rel S (RelGather E).
Proof.
  intros HE x y Hx Hy.
  rewrite RelGather_rel_equivariant.
  rewrite (HE _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelGather_supported_rel: supported_rel.

Lemma RelSelf_supported_rel t:
  supported_rel (fv t) (RelSelf t).
Proof.
  intros x y Hx Hy.
  rewrite RelSelf_rel_equivariant.
  rewrite transp_term_fresh_eq; auto.
  reflexivity.
Qed.

Hint Resolve RelSelf_supported_rel: supported_rel.

Lemma FUN_supported_rel S R1 R2:
  supported_rel S R1 →
  supported_rel S R2 →
  supported_rel S (FUN S R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite FUN_rel_equivariant.
  rewrite transp_atoms_fresh_eq; auto.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve FUN_supported_rel: supported_rel.

Lemma APP_supported_rel S R1 R2:
  supported_rel S R1 →
  supported_rel S R2 →
  supported_rel S (APP R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite APP_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve APP_supported_rel: supported_rel.

Lemma depFUN_supported_rel S R1 R2:
  supported_rel S R1 →
  (∀ x y, x `notin` S → y `notin` S →
          pointwise RelEquiv
                    (fun v ⇒ transp_rel x y (R2 (transp_term x y v)))
                    R2) →
  supported_rel S (depFUN S R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite depFUN_rel_equivariant.
  rewrite transp_atoms_fresh_eq; auto.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.
Hint Resolve depFUN_supported_rel: supported_rel.

Lemma RelCompose_RelPush_supported_rel_strong S1 S2 S R1 x v R2:
  supported_rel S1 R1 →
  supported_rel S2 R2 →
  fv v [<=] S →
  supported_rel (add x (S1 `union` S2 `union` S)) (RelCompose (RelPush R1 x v) R2).
Proof.
  intros Hsupp1 Hsupp2 Hfv.
  intros x1 x2 Hx1 Hx2. intros e t; split; intros [e' [[Heq H1] H2]]; subst.
  - rewrite <- (Hsupp1 x1 x2) in H1; auto.
    simpl in H1. rewrite transp_env_term_involution in H1.
    rewrite transp_term_fresh_eq in H1; [ | fsetdec | fsetdec ].
    rewrite <- (Hsupp2 x1 x2) in H2; auto.
    simpl in H2. rewrite transp_term_involution in H2.
    simpl_env in H2. rewrite transp_env_term_app in H2.
    rewrite transp_env_term_one in H2.
    rewrite transp_atom_other in H2; auto.
    rewrite transp_env_term_involution in H2.
    rewrite transp_term_fresh_eq in H2; [ | fsetdec | fsetdec ].
    ∃ (x ¬ v ++ e). split; [ split; [ reflexivity | assumption ] | assumption ].
  - rewrite <- (Hsupp1 x1 x2) in H1; auto.
    simpl in H1.
    rewrite transp_term_fresh_eq in H1; [ | fsetdec | fsetdec ].
    rewrite <- (Hsupp2 x1 x2) in H2; auto.
    simpl in H2.
    simpl_env in H2. rewrite transp_env_term_app in H2.
    rewrite transp_env_term_one in H2.
    rewrite transp_atom_other in H2; auto.
    rewrite (transp_term_fresh_eq x1 x2 v) in H2; [ | fsetdec | fsetdec ].
    simpl.
    ∃ (x ¬ v ++ transp_env_term x1 x2 e). split; [ split; [ reflexivity | assumption ] | assumption ].
Qed.

Lemma RelCompose_RelPush_supported_rel S R1 x v R2:
  supported_rel S R1 →
  supported_rel (add x S) R2 →
  fv v [<=] empty →
  supported_rel (add x S) (RelCompose (RelPush R1 x v) R2).
Proof.
  intros Hsupp1 Hsupp2 Hfv.
  apply (supported_rel_subset (add x (S `union` (add x S) `union` empty))).
  - fsetdec.
  - apply RelCompose_RelPush_supported_rel_strong; assumption.
Qed.
Hint Resolve RelCompose_RelPush_supported_rel: supported_rel.

Lemma RelLet_strong_supported_rel S R1 R2:
  supported_family_rel S R1 →
  supported_rel S R2 →
  supported_rel S (RelLet_strong S R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelLet_strong_rel_equivariant.
  rewrite transp_atoms_fresh_eq; auto.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelLet_strong_supported_rel: supported_rel.

Fixpoint well_supported_env (E: env (rel (env term) term)) : Prop :=
  match E with
  | nil ⇒ True
  | (x, R) :: E ⇒ supported_rel (dom E) R ∧ well_supported_env E
  end.

Add Parametric Morphism: well_supported_env
    with signature env_rel_equiv ==> iff
      as well_supported_env_morphism_equiv.
Proof.
  intros E1 E2 HE. revert E2 HE.
  env induction E1; intros [| [y Ry] E2] HE; simpl in *; try tauto.
  destruct HE as [Heq [H HE]]. subst.
  rewrite H.
  rewrite HE at 1.
  rewrite IHE1; eauto.
  reflexivity.
Qed.

Lemma well_supported_env_equivariant x y E :
  well_supported_env (transp_env_rel x y E) ↔ well_supported_env E.
Proof.
  env induction E; simpl.
  - reflexivity.
  - rewrite IHE.
    rewrite <- (supported_rel_equivariant x y (dom xs) a).
    rewrite dom_equivariant_rel.
    reflexivity.
Qed.

Lemma well_supported_env_get E x R:
  well_supported_env E →
  get x E = Some R →
  supported_rel (dom E) R.
Proof.
  intros Hwf Hget. revert x R Hget.
  env induction E; intros; simpl in *; try discriminate.
  destruct Hwf as [Hsupp Hwf].
  apply (supported_rel_subset (dom xs)); [fsetdec|].
  destruct (x0 == x); subst; eauto.
  inversion Hget; subst. assumption.
Qed.

Lemma well_supported_env_weaken E:
  well_supported_env E →
  supported_env_rel (dom E) E.
Proof.
  intro H. env induction E; simpl in ×.
  - intros x R Hx HR. simpl. trivial.
  - destruct H as [Hsupp H].
    apply supported_env_rel_cons. split; [| split]; auto.
    + apply (supported_rel_subset (dom xs)); [fsetdec|]. assumption.
    + apply (supported_env_rel_subset (dom xs)); [fsetdec|]. auto.
Qed.
Hint Resolve well_supported_env_weaken : core.