Coral.RelLc: relations that relate locally-closed terms

Author: Benoît Montagu

Synopsis: Relations that relate locally-closed terms.

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

Definitions

A relation R satisfies lc_relL if it has on its LHS only environments of locally-closed terms.

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

Add Parametric Morphism A: (@lc_relL A)
    with signature (@RelEquiv (env term) A ) --> iff
      as lc_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.

A relation R satisfies lc_relR if it has on its RHS only locally-closed terms.

Definition lc_relR {A: Type} (R: rel A term): Prop :=
  ∀ e a,
    in_rel R e a →
    lc a.

Add Parametric Morphism A: (@lc_relR A)
    with signature (@RelEquiv A term ) --> iff
      as lc_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.

A relation R satisfies lc_rel if it has on its LHS only environments of locally-closed terms and has on its RHS only locally-closed terms.

Definition lc_rel (R: rel (env term) term) : Prop :=
  lc_relL R ∧ lc_relR R.

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

A relation R satisfies lc_vrel if it has on its LHS and on its RHS only locally-closed terms.

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

Add Parametric Morphism: lc_vrel
    with signature (@RelEquiv term term ) --> iff
      as lc_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 lc_rel_relL R:
  lc_rel R → lc_relL R.
Proof.
  unfold lc_rel. tauto.
Qed.
Hint Resolve lc_rel_relL : core.

Lemma lc_vrel_relR R:
  lc_vrel R → lc_relR R.
Proof.
  intros H v1 v2 Hv.
  specialize (H _ _ Hv). tauto.
Qed.
Hint Resolve lc_vrel_relR : core.

Properties of RelBot

Lemma lc_relL_RelBot {A}: @lc_relL A RelBot.
Proof.
  intros env a H. destruct H.
Qed.

Lemma lc_relR_RelBot {A}: @lc_relR A RelBot.
Proof.
  intros env a H. destruct H.
Qed.

Lemma lc_rel_RelBot: lc_rel RelBot.
Proof.
  split; auto using lc_relL_RelBot, lc_relR_RelBot.
Qed.

Lemma lc_vrel_RelBot: lc_vrel RelBot.
Proof.
  intros v1 v2 H. destruct H.
Qed.

Properties of RelInter

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

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

Lemma lc_rel_RelInter (R1 R2: rel (env term) term):
  (lc_rel R1 ∨ lc_rel R2 ) →
  lc_rel (RelInter R1 R2).
Proof.
  unfold lc_rel.
  intro. split.
  - apply lc_relL_RelInter; tauto.
  - apply lc_relR_RelInter; tauto.
Qed.

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

Properties of RelUnion

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

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

Lemma lc_rel_RelUnion (R1 R2: rel (env term) term):
  lc_rel R1 →
  lc_rel R2 →
  lc_rel (RelUnion R1 R2).
Proof.
  unfold lc_rel. intro. split.
  - apply lc_relL_RelUnion; tauto.
  - apply lc_relR_RelUnion; tauto.
Qed.

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

Properties of RelSelf

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

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

Lemma lc_rel_RelSelf t:
  lc_rel (RelSelf t).
Proof.
  unfold lc_rel. split.
  - apply lc_relL_RelSelf.
  - apply lc_relR_RelSelf.
Qed.

Properties of RelLet0_strong

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

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

Lemma lc_rel_RelLet0_strong (R1: atom → rel (env term) term) (R2: rel (env term) term) x:
  lc_rel (R1 x) →
  lc_rel R2 →
  lc_rel (RelLet0_strong R1 R2 x).
Proof.
  unfold lc_rel. intros. split.
  - apply lc_relL_RelLet0_strong; tauto.
  - apply lc_relR_RelLet0_strong. firstorder.
Qed.

Properties of RelClose

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

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

Lemma lc_rel_RelClose S (R: atom → rel (env term) term):
  (∀ x, x `notin ` S → lc_rel (R x)) →
  lc_rel (RelClose S R).
Proof.
  unfold lc_rel. intros. split.
  - apply lc_relL_RelClose; firstorder.
  - apply lc_relR_RelClose; firstorder.
Qed.

Properties of RelLet_strong

Lemma lc_rel_RelLet_strong S (R1: atom → rel (env term) term) (R2: rel (env term) term):
  (∀ x, x `notin ` S → lc_rel (R1 x)) →
  lc_rel R2 →
  lc_rel (RelLet_strong S R1 R2).
Proof.
  intros H1 H2.
  eapply lc_rel_RelClose; eauto.
  intros x Hx. eapply lc_rel_RelLet0_strong; eauto.
Qed.

Properties of FUN

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

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

Lemma lc_rel_FUN S (R1 R2: rel (env term) term):
  lc_rel (FUN S R1 R2).
Proof.
  split; auto using lc_relL_FUN, lc_relR_FUN.
Qed.

Properties of APP

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

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

Lemma lc_rel_APP (R1 R2: rel (env term) term):
  lc_rel R1 →
  lc_rel R2 →
  lc_rel (APP R1 R2).
Proof.
  unfold lc_rel. intros. split.
  - apply lc_relL_APP; tauto.
  - apply lc_relR_APP; tauto.
Qed.

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

Properties of RelUnitR

Lemma lc_relR_RelUnitR:
  lc_relR RelUnitR.
Proof.
  intros e v H. destruct v; simpl in H; try contradiction. auto.
Qed.

Lemma lc_rel_RelUnitR:
  lc_rel RelUnitR.
Proof.
  split; auto using lc_relL_RelUnitR, lc_relR_RelUnitR.
Qed.

Properties of RelPairR

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

Lemma lc_relR_RelPairR {A} (R1 R2: rel A term):
  lc_relR R1 →
  lc_relR R2 →
  lc_relR (RelPairR R1 R2).
Proof.
  intros H1 H2 e v H.
  simpl in H.
  destruct v; try contradiction.
  destruct H. eauto.
Qed.

Lemma lc_rel_RelPairR (R1 R2: rel (env term) term):
  lc_rel R1 →
  lc_rel R2 →
  lc_rel (RelPairR R1 R2).
Proof.
  unfold lc_rel. intros. split.
  - apply lc_relL_RelPairR; tauto.
  - apply lc_relR_RelPairR; tauto.
Qed.

Lemma lc_vrel_RelPairR (R1 R2: rel term term):
  lc_vrel R1 →
  lc_vrel R2 →
  lc_vrel (RelPairR R1 R2).
Proof.
  unfold lc_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).
  intuition auto.
Qed.

Properties of RelPairL

Lemma lc_vrel_RelPairL (R1 R2: rel term term):
  lc_vrel R1 →
  lc_vrel R2 →
  lc_vrel (RelPairL R1 R2).
Proof.
  unfold lc_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).
  intuition auto.
Qed.

Properties of RelSumR

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

Lemma lc_relR_RelSumR {A} (R1 R2: rel A term):
  lc_relR R1 →
  lc_relR R2 →
  lc_relR (RelSumR R1 R2).
Proof.
  intros H1 H2 e v H.
  simpl in H.
  destruct v; try contradiction; eauto.
Qed.

Lemma lc_rel_RelSumR (R1 R2: rel (env term) term):
  lc_rel R1 →
  lc_rel R2 →
  lc_rel (RelSumR R1 R2).
Proof.
  unfold lc_rel. intros. split.
  - apply lc_relL_RelSumR; tauto.
  - apply lc_relR_RelSumR; tauto.
Qed.

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

Properties of RelSumL

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

Properties of RelCompose

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

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

Lemma lc_rel_RelCompose (R1: rel (env term) term) (R2: rel term term):
  lc_relL R1 →
  lc_relR R2 →
  lc_rel (RelCompose R1 R2).
Proof.
  unfold lc_rel. intros. split.
  - apply lc_relL_RelCompose; auto.
  - apply lc_relR_RelCompose; auto.
Qed.

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

Properties of RelInv

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

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

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