Require Import Definitions.
Require Import Metatheory.
Require Import Env.
Require Import Rel.
Require Import RelClosed.
Require Import RelValue.
Require Import RelLc.

Lemma good_value_Unit:
  good_value Unit.
Proof.
  split; [| split]; simpl; auto.
  reflexivity.
Qed.
Hint Resolve good_value_Unit: good_rel.

Lemma good_value_Pair v1 v2:
  good_value v1 →
  good_value v2 →
  good_value (Pair v1 v2).
Proof.
  unfold good_value. simpl. intuition auto. fsetdec.
Qed.
Hint Resolve good_value_Pair: good_rel.

Lemma good_value_Pair_inv_L v1 v2:
  good_value (Pair v1 v2) →
  good_value v1.
Proof.
  intros [Hlc [Hval Hfv]].
  split; [| split].
  - inversion Hlc; subst; auto.
  - simpl in Hval. tauto.
  - simpl in Hfv. fsetdec.
Qed.
Hint Resolve good_value_Pair_inv_L: good_rel.

Lemma good_value_Pair_inv_R v1 v2:
  good_value (Pair v1 v2) →
  good_value v2.
Proof.
  intros [Hlc [Hval Hfv]].
  split; [| split].
  - inversion Hlc; subst; auto.
  - simpl in Hval. tauto.
  - simpl in Hfv. fsetdec.
Qed.
Hint Resolve good_value_Pair_inv_R: good_rel.

Lemma good_value_InjL v:
  good_value v →
  good_value (InjL v).
Proof.
  unfold good_value. simpl. intuition auto.
Qed.
Hint Resolve good_value_InjL: good_rel.

Lemma good_value_InjL_inv v:
  good_value (InjL v) →
  good_value v.
Proof.
  intros [Hlc [Hval Hfv]].
  split; [| split].
  - inversion Hlc; subst; auto.
  - assumption.
  - assumption.
Qed.
Hint Resolve good_value_InjL_inv: good_rel.

Lemma good_value_InjR v:
  good_value v →
  good_value (InjR v).
Proof.
  unfold good_value. simpl. intuition auto.
Qed.
Hint Resolve good_value_InjR: good_rel.

Lemma good_value_InjR_inv v:
  good_value (InjR v) →
  good_value v.
Proof.
  intros [Hlc [Hval Hfv]].
  split; [| split].
  - inversion Hlc; subst; auto.
  - assumption.
  - assumption.
Qed.
Hint Resolve good_value_InjR_inv: good_rel.

Lemma good_rel_iff R:
  good_rel R ↔ (lc_rel R ∧ value_rel R ∧ closed_rel R).
Proof.
  split; intro H.
  - split; [| split]; split; intros e v Hev;
      specialize (H e v Hev);
      unfold good_value in H;
      repeat rewrite all_env_split in H;
      tauto.
  - destruct H as [[HElc Hlc] [[HEval Hval] [HEclosed Hclosed]]].
    intros e v Hev.
    specialize (HElc _ _ Hev).
    specialize (Hlc _ _ Hev).
    specialize (HEval _ _ Hev).
    specialize (Hval _ _ Hev).
    specialize (HEclosed _ _ Hev).
    specialize (Hclosed _ _ Hev).
    unfold good_value. repeat rewrite all_env_split.
    tauto.
Qed.

Add Parametric Morphism: good_rel
    with signature (@RelIncl (env term) term) --> impl
      as good_rel_morphism_incl.
Proof.
  intros R1 R2 H12. intros Hgood e v Hev.
  apply H12 in Hev. eauto.
Qed.

Add Parametric Morphism: good_rel
    with signature (@RelEquiv (env term) term) ==> iff
      as good_rel_morphism_equiv.
Proof.
  intros R1 R2 H12.
  split; intro H; eapply good_rel_morphism_incl; unfold flip; eauto.
Qed.

Lemma good_rel_lc R: good_rel R → lc_rel R.
Proof.
  intro H. apply good_rel_iff in H. tauto.
Qed.
Hint Resolve good_rel_lc: good_rel.

Lemma good_rel_value R: good_rel R → value_rel R.
Proof.
  intro H. apply good_rel_iff in H. tauto.
Qed.
Hint Resolve good_rel_value: good_rel.

Lemma good_rel_closed R: good_rel R → closed_rel R.
Proof.
  intro H. apply good_rel_iff in H. tauto.
Qed.
Hint Resolve good_rel_closed: good_rel.

Lemma good_vrel_iff R:
  good_vrel R ↔ (lc_vrel R ∧ value_vrel R ∧ closed_vrel R).
Proof.
  split; intro H.
  - split; [| split]; intros e v Hev;
      specialize (H e v Hev);
      unfold good_value in H;
      repeat rewrite all_env_split in H;
      tauto.
  - destruct H as [Hlc [Hval Hclosed]].
    intros e v Hev.
    specialize (Hlc _ _ Hev).
    specialize (Hval _ _ Hev).
    specialize (Hclosed _ _ Hev).
    unfold good_value.
    tauto.
Qed.

Add Parametric Morphism: good_vrel
    with signature (@RelEquiv term term) --> iff
      as good_vrel_morphism_equiv.
Proof.
  intros R1 R2 H12; split; intro H;
    apply good_vrel_iff in H; apply good_vrel_iff;
      [rewrite <- H12 in H | rewrite H12 in H]; assumption.
Qed.

Lemma good_vrel_lc R: good_vrel R → lc_vrel R.
Proof.
  intro H. apply good_vrel_iff in H. tauto.
Qed.
Hint Resolve good_vrel_lc: good_rel.

Lemma good_vrel_value R: good_vrel R → value_vrel R.
Proof.
  intro H. apply good_vrel_iff in H. tauto.
Qed.
Hint Resolve good_vrel_value: good_rel.

Lemma good_vrel_closed R: good_vrel R → closed_vrel R.
Proof.
  intro H. apply good_vrel_iff in H. tauto.
Qed.
Hint Resolve good_vrel_closed: good_rel.

Lemma all_env_good_rel_lc_rel E:
  all_env good_rel E →
  all_env lc_rel E.
Proof.
  intro H. apply all_env_sub with (P1 := good_rel); auto.
  intros x Hgood. auto with good_rel.
Qed.
Hint Resolve all_env_good_rel_lc_rel: good_rel.

Lemma all_env_good_rel_value_rel E:
  all_env good_rel E →
  all_env value_rel E.
Proof.
  intro H. apply all_env_sub with (P1 := good_rel); auto.
  intros x Hgood. auto with good_rel.
Qed.
Hint Resolve all_env_good_rel_value_rel: good_rel.

Lemma all_env_good_rel_closed_rel E:
  all_env good_rel E →
  all_env closed_rel E.
Proof.
  intro H. apply all_env_sub with (P1 := good_rel); auto.
  intros x Hgood. auto with good_rel.
Qed.
Hint Resolve all_env_good_rel_closed_rel: good_rel.

Lemma good_rel_RelBot: good_rel RelBot.
Proof.
  apply good_rel_iff.
  auto using lc_rel_RelBot, value_rel_RelBot, closed_rel_RelBot.
Qed.
Hint Resolve good_rel_RelBot: good_rel.

Lemma good_vrel_RelBot: good_vrel RelBot.
Proof.
  apply good_vrel_iff.
  auto using lc_vrel_RelBot, value_vrel_RelBot, closed_vrel_RelBot.
Qed.
Hint Resolve good_vrel_RelBot: good_rel.

Lemma good_vrel_RelEqVal: good_vrel RelEqVal.
Proof.
  intros v1 v2 H. destruct H; subst. auto.
Qed.
Hint Resolve good_vrel_RelEqVal: good_rel.

Lemma good_rel_RelTopEnvVal: good_rel RelTopEnvVal.
Proof.
  intros e v H. assumption.
Qed.
Hint Resolve good_rel_RelTopEnvVal: good_rel.

Lemma good_vrel_RelTopVal: good_vrel RelTopVal.
Proof.
  intros v1 v2 H. assumption.
Qed.
Hint Resolve good_vrel_RelTopVal: good_rel.

Lemma good_rel_RelInter (R1 R2: rel (env term) term):
  (good_rel R1 ∨ good_rel R2) →
  good_rel (RelInter R1 R2).
Proof.
  intro H.
  repeat rewrite good_rel_iff in H.
  apply good_rel_iff.
  intuition auto using lc_rel_RelInter, value_rel_RelInter, closed_rel_RelInter.
Qed.
Hint Resolve good_rel_RelInter: good_rel.

Lemma good_vrel_RelInter (R1 R2: rel term term):
  (good_vrel R1 ∨ good_vrel R2) →
  good_vrel (RelInter R1 R2).
Proof.
  intro H.
  repeat rewrite good_vrel_iff in H.
  apply good_vrel_iff.
  intuition auto using lc_vrel_RelInter, value_vrel_RelInter, closed_vrel_RelInter.
Qed.
Hint Resolve good_vrel_RelInter: good_rel.

Lemma good_rel_RelUnion (R1 R2: rel (env term) term):
  good_rel R1 →
  good_rel R2 →
  good_rel (RelUnion R1 R2).
Proof.
  intros H1 H2.
  rewrite good_rel_iff in H1.
  rewrite good_rel_iff in H2.
  apply good_rel_iff.
  intuition auto using lc_rel_RelUnion, value_rel_RelUnion, closed_rel_RelUnion.
Qed.
Hint Resolve good_rel_RelUnion: good_rel.

Lemma good_vrel_RelUnion (R1 R2: rel term term):
  good_vrel R1 →
  good_vrel R2 →
  good_vrel (RelUnion R1 R2).
Proof.
  intros H1 H2.
  rewrite good_vrel_iff in H1.
  rewrite good_vrel_iff in H2.
  apply good_vrel_iff.
  intuition auto using lc_vrel_RelUnion, value_vrel_RelUnion, closed_vrel_RelUnion.
Qed.
Hint Resolve good_vrel_RelUnion: good_rel.

Lemma good_rel_RelSelf t:
  good_rel (RelSelf t).
Proof.
  rewrite good_rel_iff.
  intuition auto using lc_rel_RelSelf, value_rel_RelSelf, closed_rel_RelSelf.
Qed.
Hint Resolve good_rel_RelSelf: good_rel.

Lemma good_rel_RelLet0_strong (R1: atom → rel (env term) term) (R2: rel (env term) term) x:
  good_rel (R1 x) →
  good_rel R2 →
  good_rel (RelLet0_strong R1 R2 x).
Proof.
  intros H1 H2.
  rewrite good_rel_iff in H1.
  rewrite good_rel_iff in H2.
  apply good_rel_iff.
  intuition auto using lc_rel_RelLet0_strong, value_rel_RelLet0_strong, closed_rel_RelLet0_strong.
Qed.
Hint Resolve good_rel_RelLet0_strong: good_rel.

Lemma good_rel_RelLet_strong S (R1: atom → rel (env term) term) (R2: rel (env term) term):
  (∀ x, x `notin` S → good_rel (R1 x)) →
  good_rel R2 →
  good_rel (RelLet_strong S R1 R2).
Proof.
  intros H1 H2.
  assert ((∀ x, x `notin` S → lc_rel (R1 x))
          ∧ (∀ x, x `notin` S → value_rel (R1 x))
          ∧ (∀ x, x `notin` S → closed_rel (R1 x)))
    as [? [? ?]].
  { split; [| split]; intros x Hx; specialize (H1 x Hx); apply good_rel_iff in H1; tauto. }
  rewrite good_rel_iff in H2.
  apply good_rel_iff.
  intuition auto using lc_rel_RelLet_strong, value_rel_RelLet_strong, closed_rel_RelLet_strong.
Qed.
Hint Resolve good_rel_RelLet_strong: good_rel.

Lemma good_rel_FUN S (R1 R2: rel (env term) term):
  good_rel (FUN S R1 R2).
Proof.
  apply good_rel_iff.
  intuition auto using lc_rel_FUN, value_rel_FUN, closed_rel_FUN.
Qed.
Hint Resolve good_rel_FUN: good_rel.

Lemma good_rel_APP (R1 R2: rel (env term) term):
  good_rel R1 →
  good_rel R2 →
  good_rel (APP R1 R2).
Proof.
  intros H1 H2.
  rewrite good_rel_iff in H1.
  rewrite good_rel_iff in H2.
  apply good_rel_iff.
  intuition auto using lc_rel_APP, value_rel_APP, closed_rel_APP.
Qed.
Hint Resolve good_rel_APP: good_rel.

Lemma good_rel_UnitR:
  good_rel RelUnitR.
Proof.
  apply good_rel_iff.
  split; [| split];
    auto using lc_rel_RelUnitR, value_rel_RelUnitR, closed_rel_RelUnitR.
Qed.
Hint Resolve good_rel_UnitR: good_rel.

Lemma good_rel_RelPairR (R1 R2: rel (env term) term):
  good_rel R1 →
  good_rel R2 →
  good_rel (RelPairR R1 R2).
Proof.
  intros H1 H2.
  rewrite good_rel_iff in H1.
  rewrite good_rel_iff in H2.
  apply good_rel_iff.
  intuition auto using lc_rel_RelPairR, value_rel_RelPairR, closed_rel_RelPairR.
Qed.
Hint Resolve good_rel_RelPairR: good_rel.

Lemma good_vrel_RelPairR (R1 R2: rel term term):
  good_vrel R1 →
  good_vrel R2 →
  good_vrel (RelPairR R1 R2).
Proof.
  intros H1 H2.
  rewrite good_vrel_iff in H1.
  rewrite good_vrel_iff in H2.
  apply good_vrel_iff.
  intuition auto using lc_vrel_RelPairR, value_vrel_RelPairR, closed_vrel_RelPairR.
Qed.
Hint Resolve good_vrel_RelPairR: good_rel.

Lemma good_vrel_RelPairL (R1 R2: rel term term):
  good_vrel R1 →
  good_vrel R2 →
  good_vrel (RelPairL R1 R2).
Proof.
  intros H1 H2.
  rewrite good_vrel_iff in H1.
  rewrite good_vrel_iff in H2.
  apply good_vrel_iff.
  intuition auto using lc_vrel_RelPairL, value_vrel_RelPairL, closed_vrel_RelPairL.
Qed.
Hint Resolve good_vrel_RelPairL: good_rel.

Lemma good_rel_RelSumR (R1 R2: rel (env term) term):
  good_rel R1 →
  good_rel R2 →
  good_rel (RelSumR R1 R2).
Proof.
  intros H1 H2.
  rewrite good_rel_iff in H1.
  rewrite good_rel_iff in H2.
  apply good_rel_iff.
  intuition auto using lc_rel_RelSumR, value_rel_RelSumR, closed_rel_RelSumR.
Qed.
Hint Resolve good_rel_RelSumR: good_rel.

Lemma good_vrel_RelSumR (R1 R2: rel term term):
  good_vrel R1 →
  good_vrel R2 →
  good_vrel (RelSumR R1 R2).
Proof.
  intros H1 H2.
  rewrite good_vrel_iff in H1.
  rewrite good_vrel_iff in H2.
  apply good_vrel_iff.
  intuition auto using lc_vrel_RelSumR, value_vrel_RelSumR, closed_vrel_RelSumR.
Qed.
Hint Resolve good_vrel_RelSumR: good_rel.

Lemma good_vrel_RelSumL (R1 R2: rel term term):
  good_vrel R1 →
  good_vrel R2 →
  good_vrel (RelSumL R1 R2).
Proof.
  intros H1 H2.
  rewrite good_vrel_iff in H1.
  rewrite good_vrel_iff in H2.
  apply good_vrel_iff.
  intuition auto using lc_vrel_RelSumL, value_vrel_RelSumL, closed_vrel_RelSumL.
Qed.
Hint Resolve good_vrel_RelSumL: good_rel.

Lemma good_rel_RelCompose (R1: rel (env term) term) (R2: rel term term):
  good_rel R1 →
  good_vrel R2 →
  good_rel (RelCompose R1 R2).
Proof.
  intros H1 H2.
  apply good_rel_iff in H1.
  apply good_vrel_iff in H2.
  apply good_rel_iff.
  intuition auto using lc_rel_RelCompose, value_rel_RelCompose, closed_rel_RelCompose.
Qed.
Hint Resolve good_rel_RelCompose: good_rel.

Lemma good_vrel_RelCompose (R1 R2: rel term term):
  good_vrel R1 →
  good_vrel R2 →
  good_vrel (RelCompose R1 R2).
Proof.
  intros H1 H2.
  apply good_vrel_iff in H1.
  apply good_vrel_iff in H2.
  apply good_vrel_iff.
  intuition auto using lc_vrel_RelCompose, value_vrel_RelCompose, closed_vrel_RelCompose.
Qed.
Hint Resolve good_vrel_RelCompose: good_rel.

Lemma good_vrel_RelComposeInv (R1: rel (env term) term) (R2: rel (env term) term):
  good_rel R1 →
  good_rel R2 →
  good_vrel (RelCompose (RelInv R1) R2).
Proof.
  intros H1 H2.
  apply good_rel_iff in H1.
  apply good_rel_iff in H2.
  apply good_vrel_iff.
  intuition auto using lc_vrel_RelComposeInv, value_vrel_RelComposeInv, closed_vrel_RelComposeInv.
Qed.
Hint Resolve good_vrel_RelComposeInv: good_rel.

Lemma good_vrel_RelInv (R: rel term term):
  good_vrel R →
  good_vrel (RelInv R).
Proof.
  intro H.
  apply good_vrel_iff in H.
  apply good_vrel_iff.
  intuition auto using lc_vrel_RelInv, value_vrel_RelInv, closed_vrel_RelInv.
Qed.
Hint Resolve good_vrel_RelInv: good_rel.

Lemma good_rel_RelGather E:
  good_rel (RelGather E).
Proof.
  intros e v [HEgood [HvGood H]]. tauto.
Qed.
Hint Resolve good_rel_RelGather: good_rel.

Lemma good_rel_RelCloseV {A} R:
  (∀ (v: A), good_rel (R v)) →
  good_rel (RelCloseV R).
Proof.
  intro H.
  intros e v [a Ha].
  apply H in Ha. assumption.
Qed.
Hint Resolve good_rel_RelCloseV: good_rel.

Lemma good_rel_RelCompose_RelPush x R1 R2 v:
  good_rel R1 →
  good_rel R2 →
  good_rel (RelCompose (RelPush R1 x v) R2).
Proof.
  intros Hgood1 Hgood2.
  intros e v' [e' [[Heq H1] H2]].
  apply Hgood1 in H1. apply Hgood2 in H2.
  tauto.
Qed.
Hint Resolve good_rel_RelCompose_RelPush: good_rel.