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

Definition value_relL {A: Type} (R: rel (env term) A): Prop :=
  ∀ e a,
    in_rel R e a →
    all_env is_value e.

Add Parametric Morphism A: (@value_relL A)
    with signature (@RelEquiv (env term) A) --> iff
      as value_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 value_relR {A: Type} (R: rel A term): Prop :=
  ∀ e a,
    in_rel R e a →
    is_value a.

Add Parametric Morphism A: (@value_relR A)
    with signature (@RelEquiv A term) --> iff
      as value_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 value_rel (R: rel (env term) term) : Prop :=
  value_relL R ∧ value_relR R.

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

Definition value_vrel (R: rel term term): Prop :=
  ∀ v1 v2,
    in_rel R v1 v2 →
    is_value v1 ∧ is_value v2.

Add Parametric Morphism: value_vrel
    with signature (@RelEquiv term term) --> iff
      as value_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 value_rel_relL R:
  value_rel R → value_relL R.
Proof.
  unfold value_rel. tauto.
Qed.
Hint Resolve value_rel_relL : core.

Lemma value_vrel_relR R:
  value_vrel R → value_relR R.
Proof.
  intros H v1 v2 Hv.
  specialize (H _ _ Hv). tauto.
Qed.
Hint Resolve value_vrel_relR : core.

Lemma value_relL_RelBot {A}: @value_relL A RelBot.
Proof.
  intros env a H. destruct H.
Qed.

Lemma value_relR_RelBot {A}: @value_relR A RelBot.
Proof.
  intros env a H. destruct H.
Qed.

Lemma value_rel_RelBot: value_rel RelBot.
Proof.
  split; auto using value_relL_RelBot, value_relR_RelBot.
Qed.

Lemma value_vrel_RelBot: value_vrel RelBot.
Proof.
  intros v1 v2 H. destruct H.
Qed.

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

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

Lemma value_rel_RelInter (R1 R2: rel (env term) term):
  (value_rel R1 ∨ value_rel R2) →
  value_rel (RelInter R1 R2).
Proof.
  unfold value_rel.
  intro. split.
  - apply value_relL_RelInter; tauto.
  - apply value_relR_RelInter; tauto.
Qed.

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

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

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

Lemma value_rel_RelUnion (R1 R2: rel (env term) term):
  value_rel R1 →
  value_rel R2 →
  value_rel (RelUnion R1 R2).
Proof.
  unfold value_rel. intro. split.
  - apply value_relL_RelUnion; tauto.
  - apply value_relR_RelUnion; tauto.
Qed.

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

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

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

Lemma value_rel_RelSelf t:
  value_rel (RelSelf t).
Proof.
  unfold value_rel. split.
  - apply value_relL_RelSelf.
  - apply value_relR_RelSelf.
Qed.

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

Lemma value_relR_RelLet0_strong (R1: atom → rel (env term) term) (R2: rel (env term) term) x:
  value_relR (R1 x) →
  value_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 value_rel_RelLet0_strong (R1: atom → rel (env term) term) (R2: rel (env term) term) x:
  value_rel (R1 x) →
  value_rel R2 →
  value_rel (RelLet0_strong R1 R2 x).
Proof.
  unfold value_rel. intros. split.
  - apply value_relL_RelLet0_strong; tauto.
  - apply value_relR_RelLet0_strong; firstorder.
Qed.

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

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

Lemma value_rel_RelClose S (R: atom → rel (env term) term):
  (∀ x, x `notin` S → value_rel (R x)) →
  value_rel (RelClose S R).
Proof.
  unfold value_rel. intros. split.
  - apply value_relL_RelClose; firstorder.
  - apply value_relR_RelClose; firstorder.
Qed.

Lemma value_rel_RelLet_strong S (R1: atom → rel (env term) term) (R2: rel (env term) term):
  (∀ x, x `notin` S → value_rel (R1 x)) →
  value_rel R2 →
  value_rel (RelLet_strong S R1 R2).
Proof.
  intros H1 H2.
  eapply value_rel_RelClose; eauto.
  intros x Hx. eapply value_rel_RelLet0_strong; eauto.
Qed.

Lemma value_relL_FUN S (R1 R2: rel (env term) term):
  value_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 value_relR_FUN S (R1 R2: rel (env term) term):
  value_relR (FUN S R1 R2).
Proof.
  intros e v [Hedom [HGE [HGV H]]].
  unfold good_value in HGV. tauto.
Qed.

Lemma value_rel_FUN S (R1 R2: rel (env term) term):
  value_rel (FUN S R1 R2).
Proof.
  split; auto using value_relL_FUN, value_relR_FUN.
Qed.

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

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

Lemma value_rel_APP (R1 R2: rel (env term) term):
  value_rel R1 →
  value_rel R2 →
  value_rel (APP R1 R2).
Proof.
  unfold value_rel. intros. split.
  - apply value_relL_APP; tauto.
  - apply value_relR_APP; tauto.
Qed.

Lemma value_relL_RelUnitR:
  value_relL RelUnitR.
Proof.
  intros e v H. destruct v; simpl in H; try contradiction.
  apply (all_env_sub good_value); auto.
Qed.

Lemma value_relR_RelUnitR:
  value_relR RelUnitR.
Proof.
  intros e v H. destruct v; simpl in H; try contradiction. simpl. trivial.
Qed.

Lemma value_rel_RelUnitR:
  value_rel RelUnitR.
Proof.
  split; auto using value_relL_RelUnitR, value_relR_RelUnitR.
Qed.

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

Lemma value_relR_RelPairR {A} (R1 R2: rel A term):
  value_relR R1 →
  value_relR R2 →
  value_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. eauto.
Qed.

Lemma value_rel_RelPairR (R1 R2: rel (env term) term):
  value_rel R1 →
  value_rel R2 →
  value_rel (RelPairR R1 R2).
Proof.
  unfold value_rel. intros. split.
  - apply value_relL_RelPairR; tauto.
  - apply value_relR_RelPairR; tauto.
Qed.

Lemma value_vrel_RelPairR (R1 R2: rel term term):
  value_vrel R1 →
  value_vrel R2 →
  value_vrel (RelPairR R1 R2).
Proof.
  unfold value_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.
Qed.

Lemma value_vrel_RelPairL (R1 R2: rel term term):
  value_vrel R1 →
  value_vrel R2 →
  value_vrel (RelPairL R1 R2).
Proof.
  unfold value_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.
Qed.

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

Lemma value_relR_RelSumR {A} (R1 R2: rel A term):
  value_relR R1 →
  value_relR R2 →
  value_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 value_rel_RelSumR (R1 R2: rel (env term) term):
  value_rel R1 →
  value_rel R2 →
  value_rel (RelSumR R1 R2).
Proof.
  unfold value_rel. intros. split.
  - apply value_relL_RelSumR; tauto.
  - apply value_relR_RelSumR; tauto.
Qed.

Lemma value_vrel_RelSumR (R1 R2: rel term term):
  value_vrel R1 →
  value_vrel R2 →
  value_vrel (RelSumR R1 R2).
Proof.
  unfold value_vrel.
  intros H1 H2 v1 v2 H.
  destruct v2; simpl in H; try contradiction.
  - specialize (H1 _ _ H). simpl. intuition auto.
  - specialize (H2 _ _ H). simpl. intuition auto.
Qed.

Lemma value_vrel_RelSumL (R1 R2: rel term term):
  value_vrel R1 →
  value_vrel R2 →
  value_vrel (RelSumL R1 R2).
Proof.
  unfold value_vrel.
  intros H1 H2 v1 v2 H.
  destruct v1; simpl in H; try contradiction.
  - specialize (H1 _ _ H). simpl. intuition auto.
  - specialize (H2 _ _ H). simpl. intuition auto.
Qed.

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

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

Lemma value_rel_RelCompose (R1: rel (env term) term) (R2: rel term term):
  value_relL R1 →
  value_relR R2 →
  value_rel (RelCompose R1 R2).
Proof.
  unfold value_rel. intros. split.
  - apply value_relL_RelCompose; auto.
  - apply value_relR_RelCompose; auto.
Qed.

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

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

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

Lemma good_env_value e: all_env good_value e → all_env is_value e.
Proof.
  unfold good_value. repeat rewrite all_env_split. tauto.
Qed.
Hint Resolve good_env_value : core.