Require Import Definitions.
Require Import Metatheory.
Require Import Env.
Require Import Rel.
Require Import SubstEnv.
Require Import EvalFacts.

Definition closed_relL {A: Type} (R: rel (env term) A): Prop :=
  ∀ e a,
    in_rel R e a →
    all_env (fun t ⇒ fv t [<=] empty) e.

Add Parametric Morphism A: (@closed_relL A)
    with signature (@RelEquiv (env term) A) --> iff
      as closed_relL_morphism_equiv.
Proof.
  intros R1 R2 H12; split;
    intros H e v Hev; apply (H e v); auto; apply (H12 e v); auto.
Qed.

Definition closed_relR {A: Type} (R: rel A term): Prop :=
  ∀ e a,
    in_rel R e a →
    fv a [<=] empty.

Add Parametric Morphism A: (@closed_relR A)
    with signature (@RelEquiv A term) --> iff
      as closed_relR_morphism_equiv.
Proof.
  intros R1 R2 H12; split;
    intros H e v Hev; apply (H e v); auto; apply (H12 e v); auto.
Qed.

Definition closed_rel (R: rel (env term) term) : Prop :=
  closed_relL R ∧ closed_relR R.

Add Parametric Morphism: closed_rel
    with signature (@RelEquiv (env term) term) --> iff
      as closed_morphism_equiv.
Proof.
  intros R1 R2 H12; split; intros [H1 H2]; split;
    try solve [rewrite H12; assumption | rewrite <- H12; assumption].
Qed.

Definition closed_vrel (R: rel term term): Prop :=
  ∀ v1 v2,
    in_rel R v1 v2 →
    fv v1 [<=] empty ∧ fv v2 [<=] empty.

Add Parametric Morphism: closed_vrel
    with signature (@RelEquiv term term) --> iff
      as closed_vrel_morphism_equiv.
Proof.
  intros R1 R2 H12; split;
    intros H e v Hev; apply (H e v); auto; apply (H12 e v); auto.
Qed.

Lemma closed_rel_relL R:
  closed_rel R → closed_relL R.
Proof.
  unfold closed_rel. tauto.
Qed.
Hint Resolve closed_rel_relL : core.

Lemma closed_vrel_relR R:
  closed_vrel R → closed_relR R.
Proof.
  intros H v1 v2 Hv.
  specialize (H _ _ Hv). tauto.
Qed.
Hint Resolve closed_vrel_relR : core.

Lemma closed_relL_RelBot {A}: @closed_relL A RelBot.
Proof.
  intros env a H. destruct H.
Qed.

Lemma closed_relR_RelBot {A}: @closed_relR A RelBot.
Proof.
  intros env a H. destruct H.
Qed.

Lemma closed_rel_RelBot: closed_rel RelBot.
Proof.
  split; auto using closed_relL_RelBot, closed_relR_RelBot.
Qed.

Lemma closed_vrel_RelBot: closed_vrel RelBot.
Proof.
  intros v1 v2 H. destruct H.
Qed.

Lemma closed_relL_RelInter {A: Type} (R1 R2: rel (env term) A):
  (closed_relL R1 ∨ closed_relL R2) →
  closed_relL (RelInter R1 R2).
Proof.
  intros [H|H] env a [H1 H2]; eauto.
Qed.

Lemma closed_relR_RelInter {A: Type} (R1 R2: rel A term):
  (closed_relR R1 ∨ closed_relR R2) →
  closed_relR (RelInter R1 R2).
Proof.
  intros [H|H] env a [H1 H2]; eauto.
Qed.

Lemma closed_rel_RelInter (R1 R2: rel (env term) term):
  (closed_rel R1 ∨ closed_rel R2) →
  closed_rel (RelInter R1 R2).
Proof.
  unfold closed_rel.
  intro. split.
  - apply closed_relL_RelInter; tauto.
  - apply closed_relR_RelInter; tauto.
Qed.

Lemma closed_vrel_RelInter (R1 R2: rel term term):
  (closed_vrel R1 ∨ closed_vrel R2) →
  closed_vrel (RelInter R1 R2).
Proof.
  unfold closed_vrel.
  intros [H|H] v1 v2 [Hv1 Hv2]; auto.
Qed.

Lemma closed_relL_RelUnion {A: Type} (R1 R2: rel (env term) A):
  closed_relL R1 →
  closed_relL R2 →
  closed_relL (RelUnion R1 R2).
Proof.
  intros Hwf1 Hwf2 env a [H|H]; eauto.
Qed.

Lemma closed_relR_RelUnion {A: Type} (R1 R2: rel A term):
  closed_relR R1 →
  closed_relR R2 →
  closed_relR (RelUnion R1 R2).
Proof.
  intros Hwf1 Hwf2 env a [H|H]; eauto.
Qed.

Lemma closed_rel_RelUnion (R1 R2: rel (env term) term):
  closed_rel R1 →
  closed_rel R2 →
  closed_rel (RelUnion R1 R2).
Proof.
  unfold closed_rel. intro. split.
  - apply closed_relL_RelUnion; tauto.
  - apply closed_relR_RelUnion; tauto.
Qed.

Lemma closed_vrel_RelUnion (R1 R2: rel term term):
  closed_vrel R1 →
  closed_vrel R2 →
  closed_vrel (RelUnion R1 R2).
Proof.
  unfold closed_vrel.
  intros H1 H2 v1 v2 [H|H]; auto.
Qed.

Lemma closed_relL_RelSelf t:
  closed_relL (RelSelf t).
Proof.
  intros e a H. simpl in ×.
  apply (all_env_sub good_value); try tauto; auto.
Qed.

Lemma closed_relR_RelSelf t:
  closed_relR (RelSelf t).
Proof.
  intros e a H. simpl in ×. intuition.
Qed.

Lemma closed_rel_RelSelf t:
  closed_rel (RelSelf t).
Proof.
  unfold closed_rel. split.
  - apply closed_relL_RelSelf.
  - apply closed_relR_RelSelf.
Qed.

Lemma closed_relL_RelLet0_strong (R1: atom → rel (env term) term) (R2: rel (env term) term) x:
  closed_relL R2 →
  closed_relL (RelLet0_strong R1 R2 x).
Proof.
  intros HR2 e a H.
  simpl in ×. destruct H as [v [H2 H1]]. eauto.
Qed.

Lemma closed_relR_RelLet0_strong (R1: atom → rel (env term) term) (R2: rel (env term) term) x:
  closed_relR (R1 x) →
  closed_relR (RelLet0_strong R1 R2 x).
Proof.
  intros HR1 e a H.
  simpl in ×. destruct H as [v [H2 H1]]. apply HR1 in H1. assumption.
Qed.

Lemma closed_rel_RelLet0_strong (R1: atom → rel (env term) term) (R2: rel (env term) term) x:
  closed_rel (R1 x) →
  closed_rel R2 →
  closed_rel (RelLet0_strong R1 R2 x).
Proof.
  unfold closed_rel. intros. split.
  - apply closed_relL_RelLet0_strong; tauto.
  - apply closed_relR_RelLet0_strong; firstorder.
Qed.

Lemma closed_relL_RelClose {A} S (R: atom → rel (env term) A):
  (∀ x, x `notin` S → closed_relL (R x)) →
  closed_relL (RelClose S R).
Proof.
  intros H e a [x [Hx HR]]. eapply H; eauto.
Qed.

Lemma closed_relR_RelClose {A} S (R: atom → rel (env A) term):
  (∀ x, x `notin` S → closed_relR (R x)) →
  closed_relR (RelClose S R).
Proof.
  intros H e a [x [Hx HR]]. eapply H; eauto.
Qed.

Lemma closed_rel_RelClose S (R: atom → rel (env term) term):
  (∀ x, x `notin` S → closed_rel (R x)) →
  closed_rel (RelClose S R).
Proof.
  unfold closed_rel. intros. split.
  - apply closed_relL_RelClose; firstorder.
  - apply closed_relR_RelClose; firstorder.
Qed.

Lemma closed_rel_RelLet_strong S (R1: atom → rel (env term) term) (R2: rel (env term) term):
  (∀ x, x `notin` S → closed_rel (R1 x)) →
  closed_rel R2 →
  closed_rel (RelLet_strong S R1 R2).
Proof.
  intros H1 H2.
  eapply closed_rel_RelClose; eauto.
  intros x Hx. eapply closed_rel_RelLet0_strong; eauto.
Qed.

Lemma closed_relL_FUN S (R1 R2: rel (env term) term):
  closed_relL (FUN S R1 R2).
Proof.
  intros e v [Hedom [HGE [HGV H]]].
  unfold good_value in HGE.
  repeat rewrite all_env_split in HGE.
  tauto.
Qed.

Lemma closed_relR_FUN S (R1 R2: rel (env term) term):
  closed_relR (FUN S R1 R2).
Proof.
  intros e v [Hedom [HGE [HGV H]]].
  unfold good_value in HGV. tauto.
Qed.

Lemma closed_rel_FUN S (R1 R2: rel (env term) term):
  closed_rel (FUN S R1 R2).
Proof.
  split; auto using closed_relL_FUN, closed_relR_FUN.
Qed.

Lemma closed_relL_APP (R1 R2: rel (env term) term):
  closed_relL R2 →
  closed_relL (APP R1 R2).
Proof.
  intros H2 e v H.
  destruct H as [e'' [v1 [v2 [H'' [Hv1 [Hv2 Heval]]]]]].
  eauto.
Qed.

Lemma closed_relR_APP (R1 R2: rel (env term) term):
  closed_relR R1 →
  closed_relR R2 →
  closed_relR (APP R1 R2).
Proof.
  intros H1 H2 e v H.
  destruct H as [e'' [v1 [v2 [H'' [Hv1 [Hv2 Heval]]]]]].
  rewrite (eval_fv _ _ Heval). simpl.
  apply H1 in Hv1. apply H2 in Hv2.
  fsetdec.
Qed.

Lemma closed_rel_APP (R1 R2: rel (env term) term):
  closed_rel R1 →
  closed_rel R2 →
  closed_rel (APP R1 R2).
Proof.
  unfold closed_rel. intros. split.
  - apply closed_relL_APP; tauto.
  - apply closed_relR_APP; tauto.
Qed.

Lemma closed_relL_RelUnitR:
  closed_relL RelUnitR.
Proof.
  intros e v H. destruct v; simpl in H; try contradiction.
  eapply all_env_sub; eauto.
Qed.

Lemma closed_relR_RelUnitR:
  closed_relR RelUnitR.
Proof.
  intros e v H. destruct v; simpl in H; try contradiction. simpl. reflexivity.
Qed.

Lemma closed_rel_RelUnitR:
  closed_rel RelUnitR.
Proof.
  split; auto using closed_relL_RelUnitR, closed_relR_RelUnitR.
Qed.

Lemma closed_relL_RelPairR (R1 R2: rel (env term) term):
  (closed_relL R1 ∨ closed_relL R2) →
  closed_relL (RelPairR R1 R2).
Proof.
  intros Hclosed e v H.
  simpl in H.
  destruct v; try contradiction.
  destruct H.
  destruct Hclosed; eauto.
Qed.

Lemma closed_relR_RelPairR {A} (R1 R2: rel A term):
  closed_relR R1 →
  closed_relR R2 →
  closed_relR (RelPairR R1 R2).
Proof.
  intros H1 H2 e v H.
  simpl in H.
  destruct v; try contradiction.
  destruct H as [HR1 HR2].
  apply H1 in HR1. apply H2 in HR2.
  simpl. fsetdec.
Qed.

Lemma closed_rel_RelPairR (R1 R2: rel (env term) term):
  closed_rel R1 →
  closed_rel R2 →
  closed_rel (RelPairR R1 R2).
Proof.
  unfold closed_rel. intros. split.
  - apply closed_relL_RelPairR; tauto.
  - apply closed_relR_RelPairR; tauto.
Qed.

Lemma closed_vrel_RelPairR (R1 R2: rel term term):
  closed_vrel R1 →
  closed_vrel R2 →
  closed_vrel (RelPairR R1 R2).
Proof.
  unfold closed_vrel.
  intros H1 H2 v1 v2 H.
  destruct v2; simpl in H; try contradiction.
  destruct H as [Hv1 Hv2].
  specialize (H1 _ _ Hv1).
  specialize (H2 _ _ Hv2).
  simpl. intuition auto. fsetdec.
Qed.

Lemma closed_vrel_RelPairL (R1 R2: rel term term):
  closed_vrel R1 →
  closed_vrel R2 →
  closed_vrel (RelPairL R1 R2).
Proof.
  unfold closed_vrel.
  intros H1 H2 v1 v2 H.
  destruct v1; simpl in H; try contradiction.
  destruct H as [Hv1 Hv2].
  specialize (H1 _ _ Hv1).
  specialize (H2 _ _ Hv2).
  simpl. intuition auto. fsetdec.
Qed.

Lemma closed_relL_RelSumR (R1 R2: rel (env term) term):
  closed_relL R1 →
  closed_relL R2 →
  closed_relL (RelSumR R1 R2).
Proof.
  intros H1 H2 e v H.
  simpl in H.
  destruct v; try contradiction; eauto.
Qed.

Lemma closed_relR_RelSumR {A} (R1 R2: rel A term):
  closed_relR R1 →
  closed_relR R2 →
  closed_relR (RelSumR R1 R2).
Proof.
  intros H1 H2 e v H.
  simpl in H.
  destruct v; try contradiction.
  - apply H1 in H. assumption.
  - apply H2 in H. assumption.
Qed.

Lemma closed_rel_RelSumR (R1 R2: rel (env term) term):
  closed_rel R1 →
  closed_rel R2 →
  closed_rel (RelSumR R1 R2).
Proof.
  unfold closed_rel. intros. split.
  - apply closed_relL_RelSumR; tauto.
  - apply closed_relR_RelSumR; tauto.
Qed.

Lemma closed_vrel_RelSumR (R1 R2: rel term term):
  closed_vrel R1 →
  closed_vrel R2 →
  closed_vrel (RelSumR R1 R2).
Proof.
  unfold closed_vrel.
  intros H1 H2 v1 v2 H.
  destruct v2; simpl in H; try contradiction; simpl; auto.
Qed.

Lemma closed_vrel_RelSumL (R1 R2: rel term term):
  closed_vrel R1 →
  closed_vrel R2 →
  closed_vrel (RelSumL R1 R2).
Proof.
  unfold closed_vrel.
  intros H1 H2 v1 v2 H.
  destruct v1; simpl in H; try contradiction; simpl; auto.
Qed.

Lemma closed_relL_RelCompose (R1: rel (env term) term) (R2: rel term term):
  closed_relL R1 →
  closed_relL (RelCompose R1 R2).
Proof.
  intros H1 e v H.
  destruct H as [v0 [He Hv]].
  eauto.
Qed.

Lemma closed_relR_RelCompose (R1: rel (env term) term) (R2: rel term term):
  closed_relR R2 →
  closed_relR (RelCompose R1 R2).
Proof.
  intros H2 e v H.
  destruct H as [v0 [He Hv]].
  apply H2 in Hv. assumption.
Qed.

Lemma closed_rel_RelCompose (R1: rel (env term) term) (R2: rel term term):
  closed_relL R1 →
  closed_relR R2 →
  closed_rel (RelCompose R1 R2).
Proof.
  unfold closed_rel. intros. split.
  - apply closed_relL_RelCompose; auto.
  - apply closed_relR_RelCompose; auto.
Qed.

Lemma closed_vrel_RelCompose (R1 R2: rel term term):
  closed_vrel R1 →
  closed_vrel R2 →
  closed_vrel (RelCompose R1 R2).
Proof.
  unfold closed_vrel.
  intros H1 H2 v1 v2 [v0 [Hv1 Hv2]].
  specialize (H1 _ _ Hv1).
  specialize (H2 _ _ Hv2).
  intuition auto.
Qed.

Lemma closed_vrel_RelComposeInv (R1: rel (env term) term) (R2: rel (env term) term):
  closed_rel R1 →
  closed_rel R2 →
  closed_vrel (RelCompose (RelInv R1) R2).
Proof.
  unfold closed_vrel.
  intros [H1 H1'] [H2 H2'] v1 v2 [v0 [Hv1 Hv2]].
  specialize (H1' _ _ Hv1).
  specialize (H2' _ _ Hv2).
  intuition auto.
Qed.

Lemma closed_vrel_RelInv (R: rel term term):
  closed_vrel R →
  closed_vrel (RelInv R).
Proof.
  intros H v1 v2 Hv. specialize (H _ _ Hv). tauto.
Qed.

Lemma good_env_closed e: all_env good_value e → all_env (fun t ⇒ fv t [<=] empty) e.
Proof.
  unfold good_value. repeat rewrite all_env_split. tauto.
Qed.
Hint Resolve good_env_closed : core.