Coral.Rel: binary relations

Author: Benoît Montagu

Synopsis: Binary relations.

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

Binary relations

A binary relation over A and B is a function of type A → B → Prop. Note: we wrapped the function in an inductive to work around a limitation of the universe consistency checker, that could not allow to work in a polymorphic manner with lists of relations.

Inductive rel (A B: Type): Type :=
| Rel: (A → B → Prop) → rel A B.

Application of a binary relation to elements.

Definition in_rel {A B} (R: rel A B) (a: A) (b: B) : Prop :=
match R with Rel _ _ r ⇒ r a b end.

Good relations

A relation satisfies good_rel if it relates environments of good values to good values.

Definition good_rel (R: rel (env term) term) : Prop :=
∀ e v, in_rel R e v →
all_env good_value e ∧ good_value v.

If R is a good relation and if it relates e to v, then e is an environment of good values.

Lemma good_rel_in_rel_L R e v:
  good_rel R →
  in_rel R e v →
  all_env good_value e.
Proof.
  intros H HR. apply H in HR. tauto.
Qed.
Hint Resolve good_rel_in_rel_L : core.

If R is a good relation and if it relates e to v, then v is a good value.

Lemma good_rel_in_rel_R R e v:
  good_rel R →
  in_rel R e v →
  good_value v.
Proof.
  intros H HR. apply H in HR. tauto.
Qed.
Hint Resolve good_rel_in_rel_R : core.

A relation satisfies good_vrel if it relates good values to good values.

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

If R is a good relation and if it relates v1 to v2, then v1 is a good value.

Lemma good_vrel_in_rel_L R v1 v2:
  good_vrel R →
  in_rel R v1 v2 →
  good_value v1.
Proof.
  intros H HR. apply H in HR. tauto.
Qed.
Hint Resolve good_vrel_in_rel_L : core.

If R is a good relation and if it relates v1 to v2, then v2 is a good value.

Lemma good_vrel_in_rel_R R v1 v2:
  good_vrel R →
  in_rel R v1 v2 →
  good_value v2.
Proof.
  intros H HR. apply H in HR. tauto.
Qed.
Hint Resolve good_vrel_in_rel_R : core.

Domain-bounded relations

A relation R satisfies dom_rel S if its left-hand side always contains environments whose domains are larger than the set S.

Definition dom_rel {A B: Type} S (R: rel (env A) B): Prop :=
∀ e v, in_rel R e v → S [<=] dom e.

Inclusion of relations

Definition RelIncl {A B: Type} (R1 R2: rel A B) : Prop :=
  ∀ x y, in_rel R1 x y → in_rel R2 x y.

Lemma RelIncl_refl {A B: Type} (R: rel A B) : RelIncl R R.
Proof.
  intros ? ? ?. assumption.
Qed.

Lemma RelIncl_trans {A B: Type} (R1 R2 R3: rel A B):
  RelIncl R1 R2 →
  RelIncl R2 R3 →
  RelIncl R1 R3.
Proof.
  intros H12 H23 ? ? ?. apply H23. apply H12. assumption.
Qed.

Add Parametric Relation (A B: Type): (rel A B) (@RelIncl A B)
    reflexivity proved by RelIncl_refl
    transitivity proved by RelIncl_trans
      as RelIncl_rel.

Add Parametric Morphism A B: (@in_rel A B)
    with signature RelIncl ++> eq ==> eq ==> impl
      as in_rel_morphism_incl.
Proof.
  intros R1 R2 H a b. intro Hab; apply H; assumption.
Qed.

Equivalence of relations

Definition RelEquiv {A B: Type} (R1 R2: rel A B) : Prop :=
  ∀ x y, in_rel R1 x y ↔ in_rel R2 x y.

Add Parametric Morphism A B: (@in_rel A B)
    with signature RelEquiv ==> eq ==> eq ==> iff
      as in_rel_morphism_equiv.
Proof.
  intros R1 R2 H a b. split; intro Hab; apply H; assumption.
Qed.

Lemma RelEquiv_refl {A B: Type} (R: rel A B) : RelEquiv R R.
Proof.
  intros ? ?. reflexivity.
Qed.

Lemma RelEquiv_sym {A B: Type} (R1 R2: rel A B):
  RelEquiv R1 R2 →
  RelEquiv R2 R1.
Proof.
  intros H12 ? ?. symmetry. apply H12.
Qed.

Lemma RelEquiv_trans {A B: Type} (R1 R2 R3: rel A B):
  RelEquiv R1 R2 →
  RelEquiv R2 R3 →
  RelEquiv R1 R3.
Proof.
  intros H12 H23 ? ?. rewrite <- (H23 x y). apply H12.
Qed.

Add Parametric Relation (A B: Type): (rel A B) (@RelEquiv A B)
    reflexivity proved by RelEquiv_refl
    symmetry proved by RelEquiv_sym
    transitivity proved by RelEquiv_trans
      as RelEquiv_rel.

Interplay between inclusion and equivalence

Lemma RelIncl_antisym {A B} (R1 R2: rel A B):
  RelIncl R1 R2 →
  RelIncl R2 R1 →
  RelEquiv R1 R2.
Proof.
  intros H12 H21 x y. split; auto.
Qed.

Lemma RelEquiv_RelIncl1 {A B} (R1 R2: rel A B):
  RelEquiv R1 R2 →
  RelIncl R1 R2.
Proof.
  intros H x y Hxy. apply H. assumption.
Qed.
Hint Resolve RelEquiv_RelIncl1 : core.

Lemma RelEquiv_RelIncl2 {A B} (R1 R2: rel A B):
  RelEquiv R1 R2 →
  RelIncl R2 R1.
Proof.
  intro H. symmetry in H. auto.
Qed.
Hint Resolve RelEquiv_RelIncl2 : core.

Require Import Setoid.

Add Parametric Morphism A B: (@RelIncl A B)
    with signature RelEquiv ==> RelEquiv ==> iff
      as RelIncl_morphism_equiv.
Proof.
  intros R1 R2 H12 R3 R4 H34. split; intro H.
  - transitivity R1; auto. transitivity R3; auto.
  - transitivity R2; auto. transitivity R4; auto.
Qed.

Add Parametric Morphism A B: (@dom_rel A B)
    with signature AtomSetImpl.Subset --> RelIncl --> impl
      as dom_rel_morphism_incl.
Proof.
  intros S1 S2 HS R1 R2 HR H e v Hev.
  apply HR in Hev. rewrite HS. eapply H; eauto.
Qed.

Add Parametric Morphism A B: (@dom_rel A B)
    with signature AtomSetImpl.Equal ==> RelEquiv ==> iff
      as dom_rel_morphism_equiv.
Proof.
  intros S1 S2 HS R1 R2 HR. split; intro H.
  - eapply dom_rel_morphism_incl; unfold flip; eauto. fsetdec.
  - eapply dom_rel_morphism_incl; unfold flip; eauto. fsetdec.
Qed.

Union of relations

This is Definition "Union" of Figure 2 of the ICFP'20 paper.

Definition RelUnion {A B: Type} (R1 R2: rel A B) : rel A B :=
  Rel A B
      (fun x y ⇒ in_rel R1 x y ∨ in_rel R2 x y).

Lemma RelUnion_incl {A B: Type} (R1 R2 S1 S2: rel A B):
  RelIncl R1 S1 →
  RelIncl R2 S2 →
  RelIncl (RelUnion R1 R2) (RelUnion S1 S2).
Proof.
  intros H1 H2 x y [? | ?]; [left|right]; auto.
Qed.

Add Parametric Morphism A B: (@RelUnion A B)
    with signature RelIncl ++> RelIncl ++> RelIncl
      as RelUnion_morphism_incl.
Proof.
  intros. apply RelUnion_incl; assumption.
Qed.

Lemma RelUnion_equiv {A B: Type} (R1 R2 S1 S2: rel A B):
  RelEquiv R1 S1 →
  RelEquiv R2 S2 →
  RelEquiv (RelUnion R1 R2) (RelUnion S1 S2).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelUnion_incl; auto.
Qed.

Add Parametric Morphism A B: (@RelUnion A B)
    with signature RelEquiv ==> RelEquiv ==> RelEquiv
      as RelUnion_morphism_equiv.
Proof.
  intros. apply RelUnion_equiv; assumption.
Qed.

Lemma RelUnion_comm {A B: Type} (R1 R2: rel A B):
  RelIncl (RelUnion R1 R2) (RelUnion R2 R1).
Proof.
  intros x y [H|H]; [right|left]; assumption.
Qed.

Lemma RelUnion_assoc1 {A B: Type} (R1 R2 R3: rel A B):
  RelIncl (RelUnion R1 (RelUnion R2 R3)) (RelUnion (RelUnion R1 R2) R3).
Proof.
  intros x y [H1|[H2|H3]].
  - left. left. assumption.
  - left. right. assumption.
  - right. assumption.
Qed.

Lemma RelUnion_assoc2 {A B: Type} (R1 R2 R3: rel A B):
  RelIncl (RelUnion (RelUnion R1 R2) R3) (RelUnion R1 (RelUnion R2 R3)).
Proof.
  intros x y [[H1|H2]|H3].
  - left. assumption.
  - right. left. assumption.
  - right. right. assumption.
Qed.

Lemma RelUnion_ub1 {A B: Type} (R1 R2: rel A B):
  RelIncl R1 (RelUnion R1 R2).
Proof.
  intros x y H. left. assumption.
Qed.

Lemma RelUnion_ub2 {A B: Type} (R1 R2: rel A B):
  RelIncl R2 (RelUnion R1 R2).
Proof.
  intros x y H. right. assumption.
Qed.

Lemma RelUnion_lub {A B: Type} (R1 R2 R: rel A B):
  RelIncl R1 R →
  RelIncl R2 R →
  RelIncl (RelUnion R1 R2) R.
Proof.
  intros H1 H2 x y [H|H].
  - apply H1. assumption.
  - apply H2. assumption.
Qed.

Lemma RelUnion_self {A B: Type} (R: rel A B):
  RelIncl (RelUnion R R) R.
Proof.
  apply RelUnion_lub; reflexivity.
Qed.

Intersection of relations

This is Definition "Intersectoin" of Figure 2 of the ICFP'20 paper.

Definition RelInter {A B: Type} (R1 R2: rel A B) : rel A B :=
  Rel A B
      (fun x y ⇒ in_rel R1 x y ∧ in_rel R2 x y).

Lemma RelInter_incl {A B: Type} (R1 R2 S1 S2: rel A B):
  RelIncl R1 S1 →
  RelIncl R2 S2 →
  RelIncl (RelInter R1 R2) (RelInter S1 S2).
Proof.
  intros H1 H2 x y [? ?]; split; auto.
Qed.

Add Parametric Morphism A B: (@RelInter A B)
    with signature RelIncl ++> RelIncl ++> RelIncl
      as RelInter_morphism_incl.
Proof.
  intros. apply RelInter_incl; assumption.
Qed.

Lemma RelInter_equiv {A B: Type} (R1 R2 S1 S2: rel A B):
  RelEquiv R1 S1 →
  RelEquiv R2 S2 →
  RelEquiv (RelInter R1 R2) (RelInter S1 S2).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelInter_incl; auto.
Qed.

Add Parametric Morphism A B: (@RelInter A B)
    with signature RelEquiv ==> RelEquiv ==> RelEquiv
      as RelInter_morphism_equiv.
Proof.
  intros. apply RelInter_equiv; assumption.
Qed.

Lemma RelInter_comm {A B: Type} (R1 R2: rel A B):
  RelIncl (RelInter R1 R2) (RelInter R2 R1).
Proof.
  intros x y [H1 H2]; split; assumption.
Qed.

Lemma RelInter_assoc1 {A B: Type} (R1 R2 R3: rel A B):
  RelIncl (RelInter R1 (RelInter R2 R3)) (RelInter (RelInter R1 R2) R3).
Proof.
  intros x y [H1 [H2 H3]]. split; [split|]; assumption.
Qed.

Lemma RelInter_assoc2 {A B: Type} (R1 R2 R3: rel A B):
  RelIncl (RelInter (RelInter R1 R2) R3) (RelInter R1 (RelInter R2 R3)).
Proof.
  intros x y [[H1 H2] H3]. split; [|split]; assumption.
Qed.

Lemma RelInter_lb1 {A B: Type} (R1 R2: rel A B):
  RelIncl (RelInter R1 R2) R1.
Proof.
  intros x y [H1 H2]. assumption.
Qed.

Lemma RelInter_lb2 {A B: Type} (R1 R2: rel A B):
  RelIncl (RelInter R1 R2) R2.
Proof.
  intros x y [H1 H2]. assumption.
Qed.

Lemma RelInter_glb {A B: Type} (R1 R2 R: rel A B):
  RelIncl R R1 →
  RelIncl R R2 →
  RelIncl R (RelInter R1 R2).
Proof.
  intros H1 H2 x y H. split.
  - apply H1. assumption.
  - apply H2. assumption.
Qed.

Lemma RelInter_self {A B: Type} (R: rel A B):
  RelIncl R (RelInter R R).
Proof.
  apply RelInter_glb; reflexivity.
Qed.

Lemma RelInter_dom_rel {A B: Type} S (R1 R2: rel (env A) B) :
  (dom_rel S R1 ∨ dom_rel S R2 ) →
  dom_rel S (RelInter R1 R2).
Proof.
  intros [H|H] e v [Hev1 Hev2]; eauto.
Qed.
Hint Resolve RelInter_dom_rel: dom_rel.

Interplay between union and intesection

Lemma RelInter_RelUnion_distrib_left {A B: Type} (R1 R2 R3: rel A B):
  RelEquiv (RelInter R1 (RelUnion R2 R3))
           (RelUnion (RelInter R1 R2) (RelInter R1 R3)).
Proof.
  intros x y; split; intro; simpl in *; tauto.
Qed.

Lemma RelInter_RelUnion_distrib_right {A B: Type} (R1 R2 R3: rel A B):
  RelEquiv (RelInter (RelUnion R1 R2) R3)
           (RelUnion (RelInter R1 R3) (RelInter R2 R3)).
Proof.
  intros x y; split; intro; simpl in *; tauto.
Qed.

Lemma RelInter_RelInter_distrib_left {A B: Type} (R1 R2 R3: rel A B):
  RelEquiv (RelInter R1 (RelInter R2 R3))
           (RelInter (RelInter R1 R2) (RelInter R1 R3)).
Proof.
  intros x y; split; intro; simpl in *; tauto.
Qed.

Lemma RelInter_RelInter_distrib_right {A B: Type} (R1 R2 R3: rel A B):
  RelEquiv (RelInter (RelInter R1 R2) R3)
           (RelInter (RelInter R1 R3) (RelInter R2 R3)).
Proof.
  intros x y; split; intro; simpl in *; tauto.
Qed.

Pointwise extension of relations

Definition pointwise {A B C: Type} (R : B → C → Prop) : ((A → B ) → (A → C ) → Prop) :=
  fun f1 f2 ⇒ ∀ x, R (f1 x) (f2 x).

Lemma pointwise_RelIncl_refl {A B C}: Reflexive (@pointwise A _ _ (@RelIncl B C)).
Proof.
  intros R a. reflexivity.
Qed.

Lemma pointwise_RelIncl_trans {A B C}: Transitive (@pointwise A _ _ (@RelIncl B C)).
Proof.
  intros R1 R2 R3 H12 H23 a. etransitivity; eauto.
Qed.

Add Parametric Relation (A B C: Type): (A → rel B C) (pointwise RelIncl)
    reflexivity proved by pointwise_RelIncl_refl
    transitivity proved by pointwise_RelIncl_trans
      as pointwise_RelIncl_rel.

Lemma pointwise_RelIncl_antisym {A B C} (R1 R2: A → rel B C) :
  pointwise RelIncl R1 R2 →
  pointwise RelIncl R2 R1 →
  pointwise RelEquiv R1 R2.
Proof.
  intros H12 H21 a. apply RelIncl_antisym; auto.
Qed.

Lemma pointwise_RelEquiv_RelIncl1 {A B C} (R1 R2: A → rel B C):
  pointwise RelEquiv R1 R2 →
  pointwise RelIncl R1 R2.
Proof.
  intros H x. apply RelEquiv_RelIncl1. auto.
Qed.
Hint Resolve pointwise_RelEquiv_RelIncl1 : core.

Lemma pointwise_RelEquiv_RelIncl2 {A B C} (R1 R2: A → rel B C):
  pointwise RelEquiv R1 R2 →
  pointwise RelIncl R2 R1.
Proof.
  intros H x. apply RelEquiv_RelIncl2. auto.
Qed.
Hint Resolve pointwise_RelEquiv_RelIncl2 : core.

Lemma pointwise_RelEquiv_refl {A B C}: Reflexive (@pointwise A _ _ (@RelEquiv B C)).
Proof.
  intros R a. reflexivity.
Qed.

Lemma pointwise_RelEquiv_sym {A B C}: Symmetric (@pointwise A _ _ (@RelEquiv B C)).
Proof.
  intros R1 R2 H12 a. symmetry. apply H12.
Qed.

Lemma pointwise_RelEquiv_trans {A B C}: Transitive (@pointwise A _ _ (@RelEquiv B C)).
Proof.
  intros R1 R2 R3 H12 H23 a. etransitivity; eauto.
Qed.

Add Parametric Relation (A B C: Type): (A → rel B C) (pointwise RelEquiv)
    reflexivity proved by pointwise_RelEquiv_refl
    symmetry proved by pointwise_RelEquiv_sym
    transitivity proved by pointwise_RelEquiv_trans
      as pointwise_RelEquiv_rel.

Add Parametric Morphism A B C: (@pointwise A _ _ (@RelIncl B C))
    with signature pointwise RelEquiv ==> pointwise RelEquiv ==> iff
      as pointwise_RelIncl_morphism_equiv.
Proof.
  intros R1 R2 H12 R3 R4 H34. split; intro H.
  - transitivity R1; auto. transitivity R3; auto.
  - transitivity R2; auto. transitivity R4; auto.
Qed.

FUN combinator

Definition FUN S (R1 R2: rel (env term) term):
  rel (env term) term :=
  Rel (env term) term
    (fun e v ⇒
       S [<=] dom e ∧
       all_env good_value e ∧
       good_value v ∧
       ∀ e',
         leq_env e e' →
         ∀ v1,
           in_rel R1 e' v1 →
           ∀ v2,
             eval (App v v1) v2 →
             in_rel R2 e' v2
    )
.

Lemma FUN_good_rel S R1 R2:
  good_rel (FUN S R1 R2).
Proof.
  intros e v [Hdom [HGE [HGV H]]]. auto.
Qed.

Lemma FUN_dom_rel S R1 R2:
  dom_rel S (FUN S R1 R2).
Proof.
  intros e v [Hedom ?]. assumption.
Qed.
Hint Resolve FUN_dom_rel: dom_rel.

Lemma FUN_incl S1 S2 R1 R2 R3 R4:
  S2 [<=] S1 →
  RelIncl R3 R1 →
  RelIncl R2 R4 →
  RelIncl (FUN S1 R1 R2) (FUN S2 R3 R4).
Proof.
  intros HS21 HR31 HR24 e v [Hdom [HGE [HGV H]]].
  split; [|split; [| split]]; auto.
  - fsetdec.
  - intros v1 Hv1 HNone v2 Hv2 Heval.
    destruct v; simpl in *; try contradiction; eauto.
Qed.

Add Parametric Morphism : FUN
    with signature AtomSetImpl.Subset --> RelIncl --> RelIncl ++> RelIncl
      as FUN_morphism_incl.
Proof.
  intros. apply FUN_incl; assumption.
Qed.

Lemma FUN_equiv S1 S2 R1 R2 R3 R4:
  S1 [=] S2 →
  RelEquiv R1 R3 →
  RelEquiv R2 R4 →
  RelEquiv (FUN S1 R1 R2) (FUN S2 R3 R4).
Proof.
  intros HS12 HR13 HR24. apply RelIncl_antisym; apply FUN_incl; auto; fsetdec.
Qed.

Add Parametric Morphism : FUN
    with signature AtomSetImpl.Equal ==> RelEquiv ==> RelEquiv ==> RelEquiv
      as FUN_morphism_equiv.
Proof.
  intros. apply FUN_equiv; assumption.
Qed.

APP combinator

This is an alternative definition for the "Application" of Figure 2 of the ICFP'20 paper. In Coral.RelExtra.APP_simplify, it is proved equivalent to the definition of the paper for stable relations. We use this relation in the development for historical reasons.

Definition APP (R1 R2: rel (env term) term): rel (env term) term :=
  Rel (env term) term
      (fun e v ⇒
         ∃ e' v1 v2 ,
           leq_env e' e ∧
           in_rel R1 e' v1 ∧
           in_rel R2 e v2 ∧
           eval (App v1 v2) v
      )
.

Lemma APP_incl R1 R2 S1 S2:
  RelIncl R1 S1 →
  RelIncl R2 S2 →
  RelIncl (APP R1 R2) (APP S1 S2).
Proof.
  intros H1 H2 a v H. unfold APP in ×.
  destruct H as [e' [v1 [v2 [He' [HS1 [HS2 Heval]]]]]].
  ∃ e', v1, v2. auto.
Qed.

Add Parametric Morphism: APP
    with signature RelIncl ++> RelIncl ++> RelIncl
      as APP_morphism_incl.
Proof.
  intros. apply APP_incl; assumption.
Qed.

Lemma APP_equiv R1 R2 S1 S2:
  RelEquiv R1 S1 →
  RelEquiv R2 S2 →
  RelEquiv (APP R1 R2) (APP S1 S2).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply APP_incl; auto.
Qed.

Add Parametric Morphism: APP
    with signature RelEquiv ==> RelEquiv ==> RelEquiv
      as APP_morphism_equiv.
Proof.
  intros. apply APP_equiv; assumption.
Qed.

Lemma APP_dom_rel S R1 R2:
  (dom_rel S R1 ∨ dom_rel S R2 ) →
  dom_rel S (APP R1 R2).
Proof.
  intros [H1|H2] e v [e' [v1 [v2 [Hleq [Hv1 [Hv2 Heval]]]]]].
  - apply leq_env_dom in Hleq. rewrite <- Hleq. eauto.
  - eauto.
Qed.
Hint Resolve APP_dom_rel: dom_rel.

Interplay between APP and FUN

Lemma APP_FUN_adjunction S R R1 R2:
  good_rel R1 →
  dom_rel S R1 →
  RelIncl (APP R1 R) R2 ↔ RelIncl R1 (FUN S R R2).
Proof.
  intros Hgood Hdom.
  split; intros Hincl e v H.
  - split; [| split; [| split]].
    + eapply Hdom; eauto.
    + eapply Hgood; eauto.
    + eapply Hgood; eauto.
    + intros e' H' v1 H1 v2 Heval.
      apply Hincl. ∃ e, v, v1. auto.
  - destruct H as [e' [v1 [v2 [H' [H1 [H2 Heval]]]]]].
    apply Hincl in H1. destruct H1 as [Hedom [HGE [HGV H1]]].
    specialize (H1 _ H' _ H2 _ Heval). assumption.
Qed.

Lemma APP_FUN_elim_strong S R1 R2 R3:
  RelIncl R3 R1 →
  RelIncl (APP (FUN S R1 R2) R3) R2.
Proof.
  intros H. rewrite (APP_FUN_adjunction S); auto using FUN_good_rel, FUN_dom_rel.
  apply FUN_incl; [reflexivity|assumption|reflexivity].
Qed.

Lemma APP_FUN_elim S R1 R2:
  RelIncl (APP (FUN S R1 R2) R1) R2.
Proof.
  apply APP_FUN_elim_strong; auto. reflexivity.
Qed.

depFUN combinator

This is Definition "Function" of Figure 2 of the ICFP'20 paper.

Definition depFUN S (R1: rel (env term) term) (R2: term → rel (env term) term):
  rel (env term) term :=
  Rel (env term) term
    (fun e v ⇒
       S [<=] dom e ∧
       all_env good_value e ∧
       good_value v ∧
       ∀ e',
         leq_env e e' →
         ∀ v1,
           in_rel R1 e' v1 →
           ∀ v2,
             eval (App v v1) v2 →
             in_rel (R2 v1) e' v2
    )
.

Lemma depFUN_good_rel S R1 R2:
  good_rel (depFUN S R1 R2).
Proof.
  intros e v [Hedom [HGE [HGV H]]]. auto.
Qed.
Hint Resolve depFUN_good_rel: good_rel.

Lemma depFUN_dom_rel S R1 R2:
  dom_rel S (depFUN S R1 R2).
Proof.
  intros e v [Hedom [HGE [HGV H]]]. assumption.
Qed.
Hint Resolve depFUN_dom_rel: dom_rel.

Lemma depFUN_incl S1 S2 R1 R2 R3 R4:
  S2 [<=] S1 →
  RelIncl R3 R1 →
  (∀ v, RelIncl (R2 v) (R4 v)) →
  RelIncl (depFUN S1 R1 R2) (depFUN S2 R3 R4).
Proof.
  intros HS21 HR31 HR24 e v [Hedom [HGE [HGV H]]].
  split; [|split; [| split]]; auto.
  - fsetdec.
  - intros e' Hleq v1 Hv1 v2 Hv2. specialize (HR24 v1).
    destruct v; simpl in *; try contradiction; eauto.
Qed.

Add Parametric Morphism : depFUN
    with signature AtomSetImpl.Subset --> RelIncl --> (pointwise RelIncl ) ++> RelIncl
      as depFUN_morphism_incl.
Proof.
  intros. apply depFUN_incl; assumption.
Qed.

Lemma depFUN_equiv S1 S2 R1 R2 R3 R4:
  S1 [=] S2 →
  RelEquiv R1 R3 →
  (∀ v, RelEquiv (R2 v) (R4 v)) →
  RelEquiv (depFUN S1 R1 R2) (depFUN S2 R3 R4).
Proof.
  intros HS12 HR13 HR24. apply RelIncl_antisym; apply depFUN_incl; auto; fsetdec.
Qed.

Add Parametric Morphism : depFUN
    with signature AtomSetImpl.Equal ==> RelEquiv ==> pointwise RelEquiv ==> RelEquiv
      as depFUN_morphism_equiv.
Proof.
  intros. apply depFUN_equiv; assumption.
Qed.

depAPP combinator

Definition depAPP (R1 R2: rel (env term) term) (t: term): rel (env term) term :=
  Rel (env term) term
      (fun e v ⇒
         ∃ e' v1 ,
           leq_env e' e ∧
           in_rel R1 e' v1 ∧
           in_rel R2 e t ∧
           eval (App v1 t) v
      )
.

Lemma depAPP_incl R1 R2 S1 S2:
  RelIncl R1 S1 →
  RelIncl R2 S2 →
  pointwise RelIncl (depAPP R1 R2) (depAPP S1 S2).
Proof.
  intros H1 H2 v0 a v H. unfold depAPP in ×.
  destruct H as [e' [v1 [He' [HS1 [HS2 Heval]]]]].
  ∃ e', v1. auto.
Qed.

Add Parametric Morphism: depAPP
    with signature RelIncl ++> RelIncl ++> pointwise RelIncl
      as depAPP_morphism_incl.
Proof.
  intros R1 R2 H12 R3 R4 H34 v. apply depAPP_incl; assumption.
Qed.

Lemma depAPP_equiv R1 R2 S1 S2:
  RelEquiv R1 S1 →
  RelEquiv R2 S2 →
  pointwise RelEquiv (depAPP R1 R2) (depAPP S1 S2).
Proof.
  intros H1 H2 v. apply RelIncl_antisym; apply depAPP_incl; auto.
Qed.

Add Parametric Morphism: depAPP
    with signature RelEquiv ==> RelEquiv ==> pointwise RelEquiv
      as depAPP_morphism_equiv.
Proof.
  intros R1 R2 H12 R3 R4 H34 v. apply depAPP_equiv; assumption.
Qed.

Interplay between depFUN and depApp

Lemma depAPP_depFUN_adjunction S R R1 R2:
  dom_rel S R1 →
  good_rel R1 →
  pointwise RelIncl (depAPP R1 R) R2 ↔ RelIncl R1 (depFUN S R R2).
Proof.
  intros Hdom Hgood. split.
  - intros Hincl e v H. split; [| split; [| split]].
    + eapply Hdom; eauto.
    + eapply Hgood; eauto.
    + eapply Hgood; eauto.
    + intros e' H' v1 H1 v2 Heval.
      apply Hincl. ∃ e, v. auto.
  - intros Hincl v0 e v H. destruct H as [e' [v1 [H' [H1 [H2 Heval]]]]].
    apply Hincl in H1. destruct H1 as [Hedom [HGE [HGV H1]]].
    specialize (H1 _ H' _ H2 _ Heval). assumption.
Qed.

Lemma depAPP_depFUN_elim_strong S R1 R2 R3:
  RelIncl R3 R1 →
  pointwise RelIncl (depAPP (depFUN S R1 R2) R3) R2.
Proof.
  intros H v. apply (depAPP_depFUN_adjunction S); auto using depFUN_good_rel, depFUN_dom_rel.
  apply depFUN_incl; [reflexivity|assumption|reflexivity].
Qed.

Lemma depAPP_depFUN_elim S R1 R2:
  pointwise RelIncl (depAPP (depFUN S R1 R2) R1) R2.
Proof.
  apply depAPP_depFUN_elim_strong; auto. reflexivity.
Qed.

Unit combinator

This is Definition "Right-unit" of Figure 2 of the ICFP'20 paper.

Definition RelUnitR: rel (env term) term :=
  Rel _ _
      (fun e v ⇒
         match v with
         | Unit ⇒ all_env good_value e
         | _ ⇒ False
         end
      )
.

Right-sided pair combinator

This is Definition "Right-pairing" of Figure 2 of the ICFP'20 paper.

Definition RelPairR {A: Type} (R1 R2: rel A term): rel A term :=
  Rel A term
      (fun a v ⇒
         match v with
         | Pair v1 v2 ⇒ in_rel R1 a v1 ∧ in_rel R2 a v2
         | _ ⇒ False
         end
      )
.

Lemma RelPairR_incl {A: Type} (R1 R2 S1 S2: rel A term):
  RelIncl R1 S1 →
  RelIncl R2 S2 →
  RelIncl (RelPairR R1 R2) (RelPairR S1 S2).
Proof.
  intros H1 H2 a v H. destruct v; simpl in *; try contradiction. destruct H; auto.
Qed.

Add Parametric Morphism A: (@RelPairR A)
    with signature RelIncl ++> RelIncl ++> RelIncl
      as RelPairR_morphism_incl.
Proof.
  intros. apply RelPairR_incl; assumption.
Qed.

Lemma RelPairR_equiv {A: Type} (R1 R2 S1 S2: rel A term):
  RelEquiv R1 S1 →
  RelEquiv R2 S2 →
  RelEquiv (RelPairR R1 R2) (RelPairR S1 S2).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelPairR_incl; auto.
Qed.

Add Parametric Morphism A: (@RelPairR A)
    with signature RelEquiv ==> RelEquiv ==> RelEquiv
      as RelPairR_morphism_equiv.
Proof.
  intros. apply RelPairR_equiv; assumption.
Qed.

Lemma RelPairR_dom_rel {A: Type} S (R1 R2: rel (env A) term):
  (dom_rel S R1 ∨ dom_rel S R2 ) →
  dom_rel S (RelPairR R1 R2).
Proof.
  intros [H|H] e v Hev; simpl in Hev; destruct v; try contradiction; destruct Hev; eauto.
Qed.
Hint Resolve RelPairR_dom_rel: dom_rel.

Left-sided pair combinator

This is Definition "Left-pairing" of Figure 2 of the ICFP'20 paper.

Definition RelPairL {A: Type} (R1 R2: rel term A): rel term A :=
  Rel term A
      (fun v a ⇒
         match v with
         | Pair v1 v2 ⇒ in_rel R1 v1 a ∧ in_rel R2 v2 a
         | _ ⇒ False
         end
      )
.

Lemma RelPairL_incl {A: Type} (R1 R2 S1 S2: rel term A):
  RelIncl R1 S1 →
  RelIncl R2 S2 →
  RelIncl (RelPairL R1 R2) (RelPairL S1 S2).
Proof.
  intros H1 H2 v a H. destruct v; simpl in *; try contradiction. destruct H; auto.
Qed.

Add Parametric Morphism A: (@RelPairL A)
    with signature RelIncl ++> RelIncl ++> RelIncl
      as RelPairL_morphism_incl.
Proof.
  intros. apply RelPairL_incl; assumption.
Qed.

Lemma RelPairL_equiv {A: Type} (R1 R2 S1 S2: rel term A):
  RelEquiv R1 S1 →
  RelEquiv R2 S2 →
  RelEquiv (RelPairL R1 R2) (RelPairL S1 S2).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelPairL_incl; auto.
Qed.

Add Parametric Morphism A: (@RelPairL A)
    with signature RelEquiv ==> RelEquiv ==> RelEquiv
      as RelPairL_morphism_equiv.
Proof.
  intros. apply RelPairL_equiv; assumption.
Qed.

Right-sided sum combinator

This is Definition "Right-suming" of Figure 2 of the ICFP'20 paper.

Definition RelSumR {A: Type} (R1 R2: rel A term): rel A term :=
  Rel A term
      (fun a v ⇒
         match v with
         | InjL v1 ⇒ in_rel R1 a v1
         | InjR v2 ⇒ in_rel R2 a v2
         | _ ⇒ False
         end
      )
.

Lemma RelSumR_incl {A: Type} (R1 R2 S1 S2: rel A term):
  RelIncl R1 S1 →
  RelIncl R2 S2 →
  RelIncl (RelSumR R1 R2) (RelSumR S1 S2).
Proof.
  intros H1 H2 a v H. destruct v; simpl in *; try contradiction; auto.
Qed.

Add Parametric Morphism A: (@RelSumR A)
    with signature RelIncl ++> RelIncl ++> RelIncl
      as RelSumR_morphism_incl.
Proof.
  intros. apply RelSumR_incl; assumption.
Qed.

Lemma RelSumR_equiv {A: Type} (R1 R2 S1 S2: rel A term):
  RelEquiv R1 S1 →
  RelEquiv R2 S2 →
  RelEquiv (RelSumR R1 R2) (RelSumR S1 S2).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelSumR_incl; auto.
Qed.

Add Parametric Morphism A: (@RelSumR A)
    with signature RelEquiv ==> RelEquiv ==> RelEquiv
      as RelSumR_morphism_equiv.
Proof.
  intros. apply RelSumR_equiv; assumption.
Qed.

Lemma RelSumR_dom_rel {A: Type} S (R1 R2: rel (env A) term):
  dom_rel S R1 →
  dom_rel S R2 →
  dom_rel S (RelSumR R1 R2).
Proof.
  intros H1 H2 e v Hev; simpl in Hev; destruct v; try contradiction; eauto.
Qed.
Hint Resolve RelSumR_dom_rel: dom_rel.

Left-sided sum combinator

This is Definition "Left-suming" of Figure 2 of the ICFP'20 paper.

Definition RelSumL {A: Type} (R1 R2: rel term A): rel term A :=
  Rel term A
      (fun v a ⇒
         match v with
         | InjL v1 ⇒ in_rel R1 v1 a
         | InjR v2 ⇒ in_rel R2 v2 a
         | _ ⇒ False
         end
      )
.

Lemma RelSumL_incl {A: Type} (R1 R2 S1 S2: rel term A):
  RelIncl R1 S1 →
  RelIncl R2 S2 →
  RelIncl (RelSumL R1 R2) (RelSumL S1 S2).
Proof.
  intros H1 H2 v a H. destruct v; simpl in *; try contradiction; auto.
Qed.

Add Parametric Morphism A: (@RelSumL A)
    with signature RelIncl ++> RelIncl ++> RelIncl
      as RelSumL_morphism_incl.
Proof.
  intros. apply RelSumL_incl; assumption.
Qed.

Lemma RelSumL_equiv {A: Type} (R1 R2 S1 S2: rel term A):
  RelEquiv R1 S1 →
  RelEquiv R2 S2 →
  RelEquiv (RelSumL R1 R2) (RelSumL S1 S2).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelSumL_incl; auto.
Qed.

Add Parametric Morphism A: (@RelSumL A)
    with signature RelEquiv ==> RelEquiv ==> RelEquiv
      as RelSumL_morphism_equiv.
Proof.
  intros. apply RelSumL_equiv; assumption.
Qed.

Composition of relations

This is Definition "Composition" of Figure 2 of the ICFP'20 paper.

Definition RelCompose {A B C: Type} (R1: rel A B) (R2: rel B C) : rel A C :=
  Rel A C
      (fun x z ⇒ ∃ y , in_rel R1 x y ∧ in_rel R2 y z).

Lemma RelCompose_incl {A B C: Type} (R1: rel A B) (R2: rel B C) (S1: rel A B) (S2: rel B C):
  RelIncl R1 S1 →
  RelIncl R2 S2 →
  RelIncl (RelCompose R1 R2) (RelCompose S1 S2).
Proof.
  intros H1 H2 x z [y [Hxy Hyz]]. ∃ y. auto.
Qed.

Add Parametric Morphism A B C: (@RelCompose A B C)
    with signature RelIncl ++> RelIncl ++> RelIncl
      as RelCompose_morphism_incl.
Proof.
  intros. apply RelCompose_incl; assumption.
Qed.

Lemma RelCompose_equiv {A B C: Type} (R1: rel A B) (R2: rel B C) (S1: rel A B) (S2: rel B C):
  RelEquiv R1 S1 →
  RelEquiv R2 S2 →
  RelEquiv (RelCompose R1 R2) (RelCompose S1 S2).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelCompose_incl; auto.
Qed.

Add Parametric Morphism A B C: (@RelCompose A B C)
    with signature RelEquiv ==> RelEquiv ==> RelEquiv
      as RelCompose_morphism_equiv.
Proof.
  intros. apply RelCompose_equiv; assumption.
Qed.

Lemma RelCompose_assoc1 {A B C D} (R1: rel A B) (R2: rel B C) (R3: rel C D):
  RelIncl (RelCompose R1 (RelCompose R2 R3)) (RelCompose (RelCompose R1 R2) R3).
Proof.
  intros xA xD [xB [H1 [xC [H2 H3]]]].
  ∃ xC. split; [| assumption].
  ∃ xB. split; assumption.
Qed.

Lemma RelCompose_assoc2 {A B C D} (R1: rel A B) (R2: rel B C) (R3: rel C D):
  RelIncl (RelCompose (RelCompose R1 R2) R3) (RelCompose R1 (RelCompose R2 R3)).
Proof.
  intros xA xD [xC [[xB [H1 H2]] H3]].
  ∃ xB. split; [assumption|].
  ∃ xC. split; assumption.
Qed.

Lemma RelCompose_dom_rel {A B C: Type} S (R1: rel (env A) B) (R2: rel B C):
  dom_rel S R1 →
  dom_rel S (RelCompose R1 R2).
Proof.
  intros H e v [v0 [Hev0 Hv0v]]. eauto.
Qed.
Hint Resolve RelCompose_dom_rel: dom_rel.

Identity relation

Definition RelEq {A: Type} : rel A A := Rel A A (fun x y ⇒ x = y).

Lemma RelEq_neutral_compose_left1 {A B: Type} (R: rel A B):
  RelIncl (RelCompose RelEq R) R.
Proof.
  intros x y [z [Heq H]]. unfold RelEq in Heq. congruence.
Qed.

Lemma RelEq_neutral_compose_left2 {A B: Type} (R: rel A B):
  RelIncl R (RelCompose RelEq R).
Proof.
  intros x y H. ∃ x. split; [reflexivity|assumption].
Qed.

Lemma RelEq_neutral_compose_left {A B: Type} (R: rel A B):
  RelEquiv (RelCompose RelEq R) R.
Proof.
  apply RelIncl_antisym; auto using RelEq_neutral_compose_left1, RelEq_neutral_compose_left2.
Qed.

Lemma RelEq_neutral_compose_right1 {A B: Type} (R: rel A B):
  RelIncl (RelCompose R RelEq) R.
Proof.
  intros x y [z [H Heq]]. unfold RelEq in Heq. congruence.
Qed.

Lemma RelEq_neutral_compose_right2 {A B: Type} (R: rel A B):
  RelIncl R (RelCompose R RelEq).
Proof.
  intros x y H. ∃ y. split; [assumption|reflexivity].
Qed.

Lemma RelEq_neutral_compose_right {A B: Type} (R: rel A B):
  RelEquiv (RelCompose R RelEq) R.
Proof.
  apply RelIncl_antisym; auto using RelEq_neutral_compose_right1, RelEq_neutral_compose_right2.
Qed.

Indentity relation on values

This is Definition "Equality" of Figure 2 of the ICFP'20 paper.

Definition RelEqVal : rel term term :=
Rel _ _ (fun v1 v2 ⇒ v1 = v2 ∧ good_value v1).

The full relation

Definition RelTop {A B: Type} : rel A B := Rel A B (fun x y ⇒ True).

Lemma RelTop_top {A B: Type} (R: rel A B): RelIncl R RelTop.
Proof.
  intros ? ? ?. constructor.
Qed.

Lemma RelTop_neutral_inter_left {A B: Type} (R: rel A B):
  RelIncl R (RelInter RelTop R).
Proof.
  apply RelInter_glb; [apply RelTop_top|reflexivity].
Qed.

Lemma RelTop_neutral_inter_right {A B: Type} (R: rel A B):
  RelIncl R (RelInter R RelTop).
Proof.
  apply RelInter_glb; [reflexivity|apply RelTop_top].
Qed.

Lemma RelTop_absorbant_union_left {A B: Type} (R: rel A B):
  RelIncl RelTop (RelUnion RelTop R).
Proof.
  intros x y H. left. assumption.
Qed.

Lemma RelTop_absorbant_union_right {A B: Type} (R: rel A B):
  RelIncl RelTop (RelUnion R RelTop).
Proof.
  intros x y H. right. assumption.
Qed.

Lemma RelTop_intro {A B: Type}: ∀ (a: A) (b: B), in_rel RelTop a b.
Proof.
  intros. constructor.
Qed.

The full relation on values

This is Definition "Top for values" of Figure 2 of the ICFP'20 paper.

Definition RelTopVal : rel term term :=
Rel _ _
(fun v1 v2 ⇒ good_value v1 ∧ good_value v2).

The full relation between environments of values and values

This is Definition "Top" of Figure 2 of the ICFP'20 paper.

Definition RelTopEnvVal : rel (env term) term :=
Rel _ _
(fun e v ⇒ all_env good_value e ∧ good_value v).

The empty relation

This is Definition "Bottom" of Figure 2 of the ICFP'20 paper.

Definition RelBot {A B: Type} : rel A B := Rel A B (fun x y ⇒ False).

Lemma RelBot_bot {A B: Type} (R: rel A B): RelIncl RelBot R.
Proof.
  intros ? ? ?. contradiction.
Qed.

Lemma RelBot_neutral_union_left {A B: Type} (R: rel A B):
  RelIncl (RelUnion RelBot R) R.
Proof.
  apply RelUnion_lub; [apply RelBot_bot|reflexivity].
Qed.

Lemma RelBot_neutral_union_right {A B: Type} (R: rel A B):
  RelIncl (RelUnion R RelBot) R.
Proof.
  apply RelUnion_lub; [reflexivity|apply RelBot_bot].
Qed.

Lemma RelBot_neutral_union_left_equiv {A B: Type} (R: rel A B):
  RelEquiv (RelUnion RelBot R) R.
Proof.
  apply RelIncl_antisym; auto using RelBot_neutral_union_left, RelUnion_ub2.
Qed.

Lemma RelBot_neutral_union_right_equiv {A B: Type} (R: rel A B):
  RelEquiv (RelUnion R RelBot) R.
Proof.
  apply RelIncl_antisym; auto using RelBot_neutral_union_right, RelUnion_ub1.
Qed.

Lemma RelBot_absorbant_inter_left {A B: Type} (R: rel A B):
  RelIncl (RelInter RelBot R) RelBot.
Proof.
  intros x y [H _]. assumption.
Qed.

Lemma RelBot_absorbant_inter_right {A B: Type} (R: rel A B):
  RelIncl (RelInter R RelBot) RelBot.
Proof.
  intros x y [_ H]. assumption.
Qed.

Lemma RelBot_absorbant_inter_left_equiv {A B: Type} (R: rel A B):
  RelEquiv (RelInter RelBot R) RelBot.
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_inter_left, RelBot_bot.
Qed.

Lemma RelBot_absorbant_inter_right_equiv {A B: Type} (R: rel A B):
  RelEquiv (RelInter R RelBot) RelBot.
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_inter_right, RelBot_bot.
Qed.

Lemma RelBot_absorbant_compose_left {A B C: Type} (R: rel B C):
  RelIncl (RelCompose (@RelBot A B) R) RelBot.
Proof.
  intros xA xC [xB [H _]]. contradiction.
Qed.

Lemma RelBot_absorbant_compose_right {A B C: Type} (R: rel A B):
  RelIncl (RelCompose R (@RelBot B C)) RelBot.
Proof.
  intros xA yC [xB [_ H]]. contradiction.
Qed.

Lemma RelBot_absorbant_compose_left_equiv {A B C: Type} (R: rel B C):
  RelEquiv (RelCompose (@RelBot A B) R) RelBot.
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_compose_left, RelBot_bot.
Qed.

Lemma RelBot_absorbant_compose_right_equiv {A B C: Type} (R: rel A B):
  RelEquiv (RelCompose R (@RelBot B C)) RelBot.
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_compose_right, RelBot_bot.
Qed.

Lemma RelBot_elim {A B: Type} (a: A) (b: B) (P: Prop): in_rel RelBot a b → P.
Proof.
  intro H. destruct H.
Qed.

Lemma RelBot_absorbant_pairR_left {A: Type} (R: rel A term):
  RelIncl (RelPairR RelBot R) RelBot.
Proof.
  intros x v H. simpl in H. destruct v; try contradiction. tauto.
Qed.

Lemma RelBot_absorbant_pairR_right {A: Type} (R: rel A term):
  RelIncl (RelPairR R RelBot) RelBot.
Proof.
  intros x v H. simpl in H. destruct v; try contradiction. tauto.
Qed.

Lemma RelBot_absorbant_pairR_left_equiv {A: Type} (R: rel A term):
  RelEquiv (RelPairR RelBot R) RelBot.
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_pairR_left, RelBot_bot.
Qed.

Lemma RelBot_absorbant_pairR_right_equiv {A: Type} (R: rel A term):
  RelEquiv (RelPairR R RelBot) RelBot.
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_pairR_right, RelBot_bot.
Qed.

Lemma RelBot_absorbant_pairL_left {A: Type} (R: rel term A):
  RelIncl (RelPairL RelBot R) RelBot.
Proof.
  intros v x H. simpl in H. destruct v; try contradiction. tauto.
Qed.

Lemma RelBot_absorbant_pairL_right {A: Type} (R: rel term A):
  RelIncl (RelPairL R RelBot) RelBot.
Proof.
  intros v x H. simpl in H. destruct v; try contradiction. tauto.
Qed.

Lemma RelBot_absorbant_pairL_left_equiv {A: Type} (R: rel term A):
  RelEquiv (RelPairL RelBot R) RelBot.
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_pairL_left, RelBot_bot.
Qed.

Lemma RelBot_absorbant_pairL_right_equiv {A: Type} (R: rel term A):
  RelEquiv (RelPairL R RelBot) RelBot.
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_pairL_right, RelBot_bot.
Qed.

Lemma RelBot_absorbant_sumL_left_right {A: Type}:
  RelIncl (RelSumL RelBot RelBot) (@RelBot term A).
Proof.
  intros v x H. simpl in H. destruct v; contradiction.
Qed.

Lemma RelBot_absorbant_sumL_left_right_equiv {A: Type}:
  RelEquiv (RelSumL RelBot RelBot) (@RelBot term A).
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_sumL_left_right, RelBot_bot.
Qed.

Lemma RelBot_absorbant_sumR_left_right {A: Type}:
  RelIncl (RelSumR RelBot RelBot) (@RelBot A term).
Proof.
  intros x v H. simpl in H. destruct v; contradiction.
Qed.

Lemma RelBot_absorbant_sumR_left_right_equiv {A: Type}:
  RelEquiv (RelSumR RelBot RelBot) (@RelBot A term).
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_sumR_left_right, RelBot_bot.
Qed.

Lemma RelBot_absorbant_app_left R:
  RelIncl (APP RelBot R) RelBot.
Proof.
  intros e v [e' [v1 [v2 [Hleq [H1 [H2 Heval]]]]]]. assumption.
Qed.

Lemma RelBot_absorbant_app_right R:
  RelIncl (APP R RelBot) RelBot.
Proof.
  intros e v [e' [v1 [v2 [Hleq [H1 [H2 Heval]]]]]]. assumption.
Qed.

Lemma RelBot_absorbant_app_left_equiv R:
  RelEquiv (APP RelBot R) RelBot.
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_app_left, RelBot_bot.
Qed.

Lemma RelBot_absorbant_app_right_equiv R:
  RelEquiv (APP R RelBot) RelBot.
Proof.
  apply RelIncl_antisym; auto using RelBot_absorbant_app_right, RelBot_bot.
Qed.

The converse combinator

Definition RelInv {A B: Type} (R: rel A B) : rel B A :=
  Rel B A (fun y x ⇒ in_rel R x y).

Lemma RelInv_incl {A B: Type} (R S: rel A B) :
  RelIncl R S →
  RelIncl (RelInv R) (RelInv S).
Proof.
  intros H x y Hxy. simpl in ×. auto.
Qed.

Add Parametric Morphism A B: (@RelInv A B)
    with signature RelIncl ++> RelIncl
      as RelInv_morphism_incl.
Proof.
  intros. apply RelInv_incl; assumption.
Qed.

Lemma RelInv_equiv {A B: Type} (R S: rel A B) :
  RelEquiv R S →
  RelEquiv (RelInv R) (RelInv S).
Proof.
  intros H. apply RelIncl_antisym; apply RelInv_incl; auto.
Qed.

Add Parametric Morphism A B: (@RelInv A B)
    with signature RelEquiv ==> RelEquiv
      as RelInv_morphism_equiv.
Proof.
  intros. apply RelInv_equiv; assumption.
Qed.

Lemma RelInv_involution {A B: Type} (R: rel A B):
  RelEquiv (RelInv (RelInv R)) R.
Proof.
  intros x y. simpl. reflexivity.
Qed.

Lemma RelInv_incl_reversed {A B: Type} (R S: rel A B) :
  RelIncl (RelInv R) (RelInv S) →
  RelIncl R S.
Proof.
  intro H.
  rewrite <- (RelInv_involution R).
  rewrite <- (RelInv_involution S).
  apply RelInv_incl.
  assumption.
Qed.

Lemma RelInv_equiv_reversed {A B: Type} (R S: rel A B) :
  RelEquiv (RelInv R) (RelInv S) →
  RelEquiv R S.
Proof.
  intros H. apply RelIncl_antisym; apply RelInv_incl_reversed; auto.
Qed.

Lemma RelInv_RelBot {A B}:
  RelEquiv (RelInv RelBot) (@RelBot A B).
Proof.
  intros x y. simpl. reflexivity.
Qed.

Lemma RelInv_RelTop {A B}:
  RelEquiv (RelInv RelTop) (@RelTop A B).
Proof.
  intros x y. simpl. reflexivity.
Qed.

Lemma RelInv_RelTopVal:
  RelEquiv (RelInv RelTopVal) RelTopVal.
Proof.
  intros x y. simpl. tauto.
Qed.

Lemma RelInv_RelEq {A}:
  RelEquiv (RelInv RelEq) (@RelEq A).
Proof.
  intros x y. simpl. split; intro; congruence.
Qed.

Lemma RelInv_RelEqVal:
  RelEquiv (RelInv RelEqVal) RelEqVal.
Proof.
  intros x y. simpl. split; intros [? ?]; split; congruence.
Qed.

Lemma RelInv_RelPairR {A} (R1 R2: rel A term):
  RelEquiv (RelInv (RelPairR R1 R2))
           (RelPairL (RelInv R1) (RelInv R2)).
Proof.
  intros v1 v2. simpl. destruct v1; tauto.
Qed.

Lemma RelInv_RelPairL {A} (R1 R2: rel term A):
  RelEquiv (RelInv (RelPairL R1 R2))
           (RelPairR (RelInv R1) (RelInv R2)).
Proof.
  rewrite <- (RelInv_involution R1) at 1.
  rewrite <- (RelInv_involution R2) at 1.
  rewrite <- RelInv_RelPairR.
  apply RelInv_involution.
Qed.

Lemma RelInv_RelSumR {A} (R1 R2: rel A term):
  RelEquiv (RelInv (RelSumR R1 R2))
           (RelSumL (RelInv R1) (RelInv R2)).
Proof.
  intros v1 v2. simpl. destruct v1; tauto.
Qed.

Lemma RelInv_RelSumL {A} (R1 R2: rel term A):
  RelEquiv (RelInv (RelSumL R1 R2))
           (RelSumR (RelInv R1) (RelInv R2)).
Proof.
  rewrite <- (RelInv_involution R1) at 1.
  rewrite <- (RelInv_involution R2) at 1.
  rewrite <- RelInv_RelSumR.
  apply RelInv_involution.
Qed.

Lemma RelInv_RelInter {A B} (R1 R2: rel A B):
  RelEquiv (RelInv (RelInter R1 R2))
           (RelInter (RelInv R1) (RelInv R2)).
Proof.
  intros x y. simpl. tauto.
Qed.

Lemma RelInv_RelUnion {A B} (R1 R2: rel A B):
  RelEquiv (RelInv (RelUnion R1 R2))
           (RelUnion (RelInv R1) (RelInv R2)).
Proof.
  intros x y. simpl. tauto.
Qed.

Lemma RelInv_RelCompose {A B C} (R1: rel A B) (R2: rel B C):
  RelEquiv (RelInv (RelCompose R1 R2))
           (RelCompose (RelInv R2) (RelInv R1)).
Proof.
  intros x y. simpl. firstorder.
Qed.

Lemma RelInv_RelIncl {A B} (R1 R2: rel A B):
  RelIncl R1 R2 ↔ RelIncl (RelInv R1) (RelInv R2).
Proof.
  split; intros H x y Hxy; simpl in *; auto.
  apply (H y x). assumption.
Qed.

Lemma RelInv_RelEquiv {A B} (R1 R2: rel A B):
  RelEquiv R1 R2 ↔ RelEquiv (RelInv R1) (RelInv R2).
Proof.
  split; intro H; apply RelIncl_antisym.
  - rewrite <- RelInv_RelIncl. auto.
  - rewrite <- RelInv_RelIncl. auto.
  - rewrite RelInv_RelIncl. auto.
  - rewrite RelInv_RelIncl. auto.
Qed.

Lemma RelInv_good_vrel R:
  good_vrel R ↔ good_vrel (RelInv R).
Proof.
  split; intros H v1 v2 Hv1v2; simpl in *; apply H in Hv1v2; tauto.
Qed.

Interplay between composition and the other combinators

Lemma RelCompose_RelInter_left {A B C} (R1 R2: rel A B) (R: rel B C):
  RelIncl
    (RelCompose (RelInter R1 R2) R)
    (RelInter (RelCompose R1 R) (RelCompose R2 R)).
Proof.
  intros x y [z [[H1 H2] H]]. split; ∃ z; auto.
Qed.

Lemma RelCompose_RelInter_right {A B C} (R: rel A B) (R1 R2: rel B C):
  RelIncl
    (RelCompose R (RelInter R1 R2))
    (RelInter (RelCompose R R1) (RelCompose R R2)).
Proof.
  intros x y [z [H [H1 H2]]]. split; ∃ z; auto.
Qed.

Lemma RelCompose_RelUnion_left {A B C} (R1 R2: rel A B) (R: rel B C):
  RelEquiv
    (RelCompose (RelUnion R1 R2) R)
    (RelUnion (RelCompose R1 R) (RelCompose R2 R)).
Proof.
  intros x y; split; intro H.
  - destruct H as [z [[H1|H2] H]]; [left|right]; ∃ z; auto.
  - destruct H as [[z [H1 H]] | [z [H2 H]]];
      ∃ z; split; [ left | | right | ]; assumption.
Qed.

Lemma RelCompose_RelUnion_right {A B C} (R: rel A B) (R1 R2: rel B C):
  RelEquiv
    (RelCompose R (RelUnion R1 R2))
    (RelUnion (RelCompose R R1) (RelCompose R R2)).
Proof.
  intros x y; split; intro H.
  - destruct H as [z [H [H1|H2]]]; [left|right]; ∃ z; auto.
  - destruct H as [[z [H H1]] | [z [H H2]]];
      ∃ z; split; [ | left | | right ]; assumption.
Qed.

Families of relations, indexed over a cofinite set of atoms

Definition FamilyRelEquiv {A B} (S: atoms) (R1 R2: atom → rel A B) : Prop :=
  ∀ x, x `notin ` S → RelEquiv (R1 x) (R2 x).

Lemma FamilyRelEquiv_subset {A B} (S1 S2: atoms) (R1 R2: atom → rel A B):
  S1 [<=] S2 →
  FamilyRelEquiv S1 R1 R2 →
  FamilyRelEquiv S2 R1 R2.
Proof.
  intros HS H x Hx. apply (H x); auto.
Qed.

Add Parametric Morphism A B: (@FamilyRelEquiv A B)
    with signature AtomSetImpl.Equal ==> pointwise RelEquiv ==> pointwise RelEquiv ==> iff
      as FamilyRelEquiv_morphism_equiv.
Proof.
  intros S1 S2 HS R1 R2 H12 R3 R4 H34.
  split; intros H x Hx.
  - rewrite <- (H12 x). rewrite <- (H34 x). apply H. fsetdec.
  - rewrite (H12 x). rewrite (H34 x). apply H. fsetdec.
Qed.

Lemma FamilyRelEquiv_refl {A B} S (R: atom → rel A B) :
  FamilyRelEquiv S R R.
Proof.
  intros x Hx. reflexivity.
Qed.

Lemma FamilyRelEquiv_sym {A B} S (R1 R2: atom → rel A B) :
  FamilyRelEquiv S R1 R2 →
  FamilyRelEquiv S R2 R1.
Proof.
  intros H x Hx. symmetry. auto.
Qed.

Lemma FamilyRelEquiv_trans {A B} S (R1 R2 R3: atom → rel A B) :
  FamilyRelEquiv S R1 R2 →
  FamilyRelEquiv S R2 R3 →
  FamilyRelEquiv S R1 R3.
Proof.
  intros H1 H2 x Hx. transitivity (R2 x); auto.
Qed.

Add Parametric Relation (A B: Type) (S: atoms): (atom → rel A B) (@FamilyRelEquiv A B S)
    reflexivity proved by (FamilyRelEquiv_refl S)
    symmetry proved by (FamilyRelEquiv_sym S)
    transitivity proved by (FamilyRelEquiv_trans S)
      as FamilyRelEquiv_rel.

An auxiliary combinator for the strong Let combinator

Definition RelLet0_strong {A: Type} (R: atom → rel (env A) A) (R1: rel (env A) A) x:
  rel (env A) A :=
  Rel _ _ (fun e a ⇒ ∃ v , in_rel R1 e v ∧ in_rel (R x) (x ¬ v ++ e) a).

Lemma RelLet0_strong_sound {A: Type} (R: atom → rel (env A) A) (R1: rel (env A) A) (e: env A) x v v':
  in_rel (R x) (x ¬ v' ++ e) v →
  in_rel R1 e v' →
  in_rel (RelLet0_strong R R1 x) e v.
Proof.
  intro H. ∃ v'. split; auto.
Qed.

Lemma RelLet0_strong_incl {A: Type} (R1 S1: atom → rel (env A) A) (R2 S2: rel (env A) A) x:
  RelIncl (R1 x) (S1 x) →
  RelIncl R2 S2 →
  RelIncl (RelLet0_strong R1 R2 x) (RelLet0_strong S1 S2 x).
Proof.
  intros H1 H2 x1 x2 [v [HR1 HR2]]. simpl in ×.
  ∃ v. split.
  - apply H2; auto.
  - apply H1; auto.
Qed.

Lemma RelLet0_strong_equiv {A: Type} (R1 S1: atom → rel (env A) A) (R2 S2: rel (env A) A) x:
  RelEquiv (R1 x) (S1 x) →
  RelEquiv R2 S2 →
  RelEquiv (RelLet0_strong R1 R2 x) (RelLet0_strong S1 S2 x).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelLet0_strong_incl; auto.
Qed.

Cofinite existential closure of an atom-indexed family of relations

Definition RelClose {A B: Type} (S: atoms) (R: atom → rel (env A) B) : rel (env A) B :=
  Rel _ _ (fun a b ⇒
             ∃ x ,
               x `notin ` S ∧ (* necessary to avoid some names *)
               in_rel (R x) a b).

Lemma RelClose_sound {A B: Type} (S: atoms) (R: atom → rel (env A) B) a b x :
  x `notin ` S →
  x `notin ` dom a →
  in_rel (R x) a b →
  in_rel (RelClose S R) a b.
Proof.
  intros Hx H. ∃ x. tauto.
Qed.

Lemma RelClose_incl {A B: Type} S (R1 R2: atom → rel (env A) B):
  (∀ x, x `notin ` S → RelIncl (R1 x) (R2 x)) →
  RelIncl (RelClose S R1) (RelClose S R2).
Proof.
  intros H x1 x2 [x [HS Hx]]. simpl.
  ∃ x. split; auto. apply (H x); auto.
Qed.

Lemma RelClose_equiv {A B: Type} S (R1 R2: atom → rel (env A) B):
  FamilyRelEquiv S R1 R2 →
  RelEquiv (RelClose S R1) (RelClose S R2).
Proof.
  intro H. apply RelIncl_antisym; apply RelClose_incl; auto.
Qed.

Lemma RelClose_subset {A B: Type} S1 S2 (R: atom → rel (env A) B):
  S2 [<=] S1 →
  RelIncl (RelClose S1 R) (RelClose S2 R).
Proof.
  intros H x1 x2 [x [HS Hx]]. simpl. ∃ x. split; auto.
Qed.

Lemma RelClose_same_set {A B: Type} S1 S2 (R1 R2: atom → rel (env A) B):
  S1 [=] S2 →
  pointwise RelEquiv R1 R2 →
  RelEquiv (RelClose S1 R1) (RelClose S2 R2).
Proof.
  intros HS HR. intros e v. split; intros [x [Hx H]].
  - ∃ x. split; [ fsetdec |]. apply HR. assumption.
  - ∃ x. split; [ fsetdec |]. apply HR. assumption.
Qed.

Add Parametric Morphism A B S: (@RelClose A B S)
    with signature (FamilyRelEquiv S ) ==> RelEquiv
      as RelClose_morphism_equiv.
Proof.
  intros R1 R2 HR.
  apply RelClose_equiv; auto.
Qed.

Add Parametric Morphism A B: (@RelClose A B)
    with signature AtomSetImpl.Equal ==> pointwise RelEquiv ==> RelEquiv
      as RelClose_morphism_equiv_atoms.
Proof.
  intros S1 S2 HS R1 R2 HR.
  apply (RelClose_same_set S1 S2 R1 R2); auto.
Qed.

Add Parametric Morphism A B: (@RelClose A B)
    with signature AtomSetImpl.Subset --> eq ==> RelIncl
      as RelClose_morphism_incl.
Proof.
  intros S1 S2 HS R.
  apply (RelClose_subset S1 S2); auto.
Qed.

The strong Let combinator

Definition RelLet_strong {A: Type} (S: atoms) (R: atom → rel (env A) A) (R1: rel (env A) A):
  rel (env A) A :=
  RelClose S (RelLet0_strong R R1).

Lemma RelLet_strong_sound {A: Type} (S: atoms) (R: atom → rel (env A) A) (R1: rel (env A) A) (e: env A) x v v':
  x `notin ` S →
  x `notin ` dom e →
  in_rel (R x) (x ¬ v' ++ e) v →
  in_rel R1 e v' →
  in_rel (RelLet_strong S R R1) e v.
Proof.
  intros Hx Hdom H1 H2. eapply RelClose_sound; eauto.
  eapply RelLet0_strong_sound; eauto.
Qed.

Lemma RelLet_strong_incl {A: Type} S (R1 R3: atom → rel (env A) A) (R2 R4: rel (env A) A):
  (∀ x, x `notin ` S → RelIncl (R1 x) (R3 x)) →
  RelIncl R2 R4 →
  RelIncl (RelLet_strong S R1 R2) (RelLet_strong S R3 R4).
Proof.
  intros H1 H2. apply RelClose_incl.
  intros x Hx. apply RelLet0_strong_incl; auto.
Qed.

Lemma RelLet_strong_equiv {A: Type} S (R1 R3: atom → rel (env A) A) (R2 R4: rel (env A) A):
  FamilyRelEquiv S R1 R3 →
  RelEquiv R2 R4 →
  RelEquiv (RelLet_strong S R1 R2) (RelLet_strong S R3 R4).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelLet_strong_incl; auto.
Qed.

Lemma RelLet_strong_subset {A: Type} S1 S2 (R1: atom → rel (env A) A) (R2: rel (env A) A):
  S2 [<=] S1 →
  RelIncl (RelLet_strong S1 R1 R2) (RelLet_strong S2 R1 R2).
Proof.
  intros H1 H2. apply RelClose_subset; auto.
Qed.

Lemma RelLet_strong_same_set {A: Type} S1 S2 (R1: atom → rel (env A) A) (R2: rel (env A) A):
  S1 [=] S2 →
  RelEquiv (RelLet_strong S1 R1 R2) (RelLet_strong S2 R1 R2).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelLet_strong_subset; fsetdec.
Qed.

Add Parametric Morphism A S: (@RelLet_strong A S)
    with signature FamilyRelEquiv S ==> RelEquiv ==> RelEquiv
      as RelLet_strong_morphism_equiv.
Proof.
  intros R1 R3 H13 R2 R4 H24.
  apply RelLet_strong_equiv; auto.
Qed.

Add Parametric Morphism A: (@RelLet_strong A)
    with signature AtomSetImpl.Equal ==> eq ==> RelEquiv ==> RelEquiv
      as RelLet_strong_morphism_equiv_set.
Proof.
  intros S1 S2 HS R R2 R4 H24.
  rewrite (RelLet_strong_same_set S1 S2 R R2); auto.
  apply RelLet_strong_equiv; auto. reflexivity.
Qed.

The Self combinator

This is Definition "Selfification" of Figure 2 of the ICFP'20 paper.

Definition RelSelf t : rel (env term) term :=
  Rel _ _
      (fun e v ⇒ subst_env e t = v ∧ fv t [<=] dom e ∧ all_env good_value e ∧ good_value v).

Lemma RelSelf_deterministic t e v1 v2:
  in_rel (RelSelf t) e v1 →
  in_rel (RelSelf t) e v2 →
  v1 = v2.
Proof.
  intros [Heval1 _] [Heval2 _]. congruence.
Qed.

Lemma RelSelf_sound_Var x e v:
  all_env good_value e →
  get x e = Some v →
  in_rel (RelSelf (Var x)) e v.
Proof.
  intros Hgood Hx.
  assert (good_value v) by (eapply all_env_get; eauto).
  simpl.
  split; [| split; [| split]]; auto.
  - rewrite (subst_env_Var_Some e x v); auto.
  - apply get_in_dom in Hx. simpl. fsetdec.
Qed.

Lemma RelSelf_sound_Lam t e' e:
  leq_env e e' →
  all_env good_value e →
  all_env good_value e' →
  fv t [<=] dom e →
  lc (Lam t) →
  in_rel (RelSelf (Lam t)) e' (subst_env e (Lam t)).
Proof.
  intros Hleq Hgood Hgood' Hfv Hlc.
  simpl.
  split; [| split; [| split]]; auto.
  - symmetry. apply subst_env_leq_env; auto.
    + eapply all_env_sub; eauto.
    + eapply all_env_sub; eauto.
  - apply leq_env_dom in Hleq. fsetdec.
  - split; [| split].
    + apply subst_env_lc; auto.
      eapply (all_env_sub good_value); eauto.
    + rewrite subst_env_Lam. simpl. trivial.
    + rewrite subst_env_fv_closed; auto.
      × simpl. fsetdec.
      × eapply all_env_sub; eauto.
Qed.

The Gather combinator

This is Definition "Gathering" of Figure 2 of the ICFP'20 paper.

Definition RelGather (E: env (rel (env term) term)): rel (env term) term :=
  Rel _ _
      (fun e v ⇒
         all_env good_value e
         ∧ good_value v
         ∧ ∀ x R, get x E = Some R → ∃ v', get x e = Some v' ∧ in_rel R e v').

Lemma RelGather_dom_rel (E: env (rel (env term) term)):
  dom_rel (dom E) (RelGather E).
Proof.
  intros e v [Hegood [Hvgood Hev]].
  intros x Hx.
  case_eq (get x E); intros.
  - apply Hev in H. destruct H as [v' [Hget Hev']].
    apply get_in_dom in Hget. assumption.
  - exfalso. apply get_notin_dom in H. contradiction.
Qed.
Hint Resolve RelGather_dom_rel: dom_rel.

Lemma RelGather_leq_env E E':
  leq_env E E' →
  RelIncl (RelGather E') (RelGather E).
Proof.
  intros H e v [HEGood [HvGood Hev]].
  split; [| split]; auto.
Qed.

The next two lemmas constitute Lemma 2.6 of the ICFP'20 paper.

Lemma RelGather_nil :
  RelEquiv (RelGather nil) RelTopEnvVal.
Proof.
  intros e v; split; intro H; simpl in *; try tauto.
  split; [| split]; try tauto.
  intros x R Heq. congruence.
Qed.

Lemma RelGather_cons E x R :
  x `notin ` dom E →
  good_rel R →
  RelEquiv
    (RelGather (x ¬ R ++ E))
    (RelInter (RelGather E) (RelCompose (RelInter (RelSelf (Var x)) R) RelTopVal)).
Proof.
  intros Hx Hgood.
  intros e v; split; intro H.
  - destruct H as [Hegood [Hvgood H]]. split.
    + split; [| split]; auto.
      intros y Ry Hy. destruct (y == x); subst.
      × exfalso. apply get_in_dom in Hy. contradiction.
      × apply H. simpl. destruct (y == x); try contradiction; auto.
    + destruct (H x R) as [v' [Hv' HR]].
      × simpl. destruct (x == x); try contradiction; auto.
      × ∃ v'. split; [ split | split; [| split]]; eauto.
        { simpl. split; [| split; [| split]]; eauto.
          - eapply subst_env_Var_Some; eauto.
          - apply get_in_dom in Hv'. fsetdec.
        }
  - destruct H as [[Hegood [Hvgood H]] [v' [[[Heq [Hin _]] HR] [Hv'good _]]]].
    split; [| split]; auto.
    intros y Ry Hy. simpl in Hy. destruct (y == x); try subst y; auto.
    inversion Hy; subst Ry. clear Hy.
    case_eq (get x e); intros.
    + rewrite (subst_env_Var_Some e x t) in Heq; auto.
      × subst. eauto.
      × eapply all_env_get in H0; eauto.
    + exfalso. apply get_notin_dom in H0. simpl in Hin. fsetdec.
Qed.

Lemma RelGather_iff E:
  uniq E →
  all_env good_rel E →
  RelEquiv (RelGather E)
           (RelInter
              RelTopEnvVal
              (Rel _ _
                   (fun e v ⇒ ∀ x R,
                        get x E = Some R →
                        in_rel (RelCompose (RelInter (RelSelf (Var x)) R) RelTopVal) e v))).
Proof.
  intros Huniq Hgood. env induction E.
  - rewrite RelGather_nil.
    intros e v; split; intro H.
    + split; [assumption |].
      intros x R Hx. simpl in Hx. discriminate.
    + destruct H. assumption.
  - simpl in Hgood. destruct Hgood as [Hgooda Hgood].
    rewrite RelGather_cons; auto.
    + rewrite IHE; auto.
      × { intros e v; split; intro H.
          - destruct H as [[Htop H] Hcompose].
            split; [ assumption |].
            intros y Ry Hy. simpl in Hy. destruct (y == x); subst; auto.
            inversion Hy; subst. clear Hy. auto.
          - destruct H as [Htop H].
            split; [ split |]; auto.
            intros y Ry Hy. apply H. simpl. destruct (y == x); subst; auto.
            exfalso. apply get_in_dom in Hy. solve_uniq.
        }
      × solve_uniq.
    + solve_uniq.
Qed.

Lemma compose_self_included x R:
  RelIncl
    (RelInter (RelSelf (Var x))
              (RelCompose (RelInter (RelSelf (Var x)) R) RelTopVal))
    R.
Proof.
  intros e v [Hself [v' [[Hself' HR] Htop]]].
  assert (v = v') by eauto using RelSelf_deterministic.
  congruence.
Qed.

This is Lemma 2.7 of the ICFP'20 paper.

Lemma RelSelf_RelGather_RelIncl E x R:
  uniq E →
  all_env good_rel E →
  get x E = Some R →
  RelIncl (RelInter (RelSelf (Var x)) (RelGather E)) R.
Proof.
  intros Huniq Hgood Hx.
  rewrite <- (compose_self_included x R).
  rewrite RelGather_iff; auto.
  apply RelInter_incl.
  - reflexivity.
  - intros e v [Htop H]. auto.
Qed.

Existential closure of a family of relations

Definition RelCloseV {A B C} (R: A → rel B C) : rel B C :=
  Rel _ _ (fun e v ⇒ ∃ t , in_rel (R t) e v).

Add Parametric Morphism A B C: (@RelCloseV A B C)
    with signature pointwise RelIncl ++> RelIncl
      as RelCloseV_morphism_incl.
Proof.
  intros R1 R2 H12 e v [t H].
  ∃ t. apply H12. assumption.
Qed.

Add Parametric Morphism A B C: (@RelCloseV A B C)
    with signature pointwise RelEquiv ==> RelEquiv
      as RelCloseV_morphism_equiv.
Proof.
  intros R1 R2 H12.
  apply RelIncl_antisym; apply RelCloseV_morphism_incl; auto.
Qed.

Lemma RelCloseV_dom_rel {A B} S (R: A → rel (env A) B):
  (∀ v, dom_rel S (R v)) →
  dom_rel S (RelCloseV R).
Proof.
  intros H e v [v' Hv'].
  apply H in Hv'. assumption.
Qed.
Hint Resolve RelCloseV_dom_rel: dom_rel.

APP is the existential closure of depAPP.

Lemma APP_rewrite R1 R2 :
RelEquiv (APP R1 R2) (RelCloseV (depAPP R1 R2)).
Proof.
intros e v; split; intro H; simpl in *; firstorder.
Qed.

The Remove combinator

Definition RelRemove {A} (R1 R2: rel (env A) A) x : rel (env A) A :=
  Rel _ _
      (fun e v ⇒ ∃ v', in_rel R2 e v' ∧ in_rel R1 (x ¬ v' ++ e) v).

Lemma RelRemove_incl {A} (R1 R2 S1 S2: rel (env A) A) x:
  RelIncl R1 S1 →
  RelIncl R2 S2 →
  RelIncl (RelRemove R1 R2 x) (RelRemove S1 S2 x).
Proof.
  intros H1 H2 a v H. simpl in ×.
  destruct H as [v' [H2' H1']].
  ∃ v'. auto.
Qed.

Add Parametric Morphism A: (@RelRemove A)
    with signature RelIncl ++> RelIncl ==> eq ++> RelIncl
      as RelRemove_morphism_incl.
Proof.
  intros. apply RelRemove_incl; assumption.
Qed.

Lemma RelRemove_equiv {A} (R1 R2 S1 S2: rel (env A) A) x :
  RelEquiv R1 S1 →
  RelEquiv R2 S2 →
  RelEquiv (RelRemove R1 R2 x) (RelRemove S1 S2 x).
Proof.
  intros H1 H2. apply RelIncl_antisym; apply RelRemove_incl; auto.
Qed.

Add Parametric Morphism A: (@RelRemove A)
    with signature RelEquiv ==> RelEquiv ==> eq ==> RelEquiv
      as RelRemove_morphism_equiv.
Proof.
  intros. apply RelRemove_equiv; assumption.
Qed.

The Push combinator

This is Definition "Push" of Figure 2 of the ICFP'20 paper.

Definition RelPush {A} (R: rel (env A) A) x (v: A) : rel (env A) (env A) :=
  Rel _ _ (fun e e' ⇒ e' = x ¬ v ++ e ∧ in_rel R e v).

Add Parametric Morphism A: (@RelPush A)
    with signature RelIncl ++> eq ==> eq ==> RelIncl
      as RelPush_morphism_incl.
Proof.
  intros R1 R2 H12 x v e v' [Heq H]. split; auto.
Qed.

Add Parametric Morphism A: (@RelPush A)
    with signature RelEquiv ==> eq ==> eq ==> RelEquiv
      as RelPush_morphism_equiv.
Proof.
  intros R1 R2 H12 x v.
  apply RelIncl_antisym; apply RelPush_morphism_incl; auto.
Qed.

Add Parametric Morphism A: (@RelPush A)
    with signature RelIncl ++> eq ==> pointwise RelIncl
      as RelPush_morphism_pointwise_incl.
Proof.
  intros R1 R2 H12 x v. apply RelPush_morphism_incl; auto.
Qed.

Add Parametric Morphism A: (@RelPush A)
    with signature RelEquiv ==> eq ==> pointwise RelEquiv
      as RelPush_morphism_pointwise_equiv.
Proof.
  intros R1 R2 H12 x v. apply RelPush_morphism_equiv; auto.
Qed.

Lemma RelCompose_RelPush_dom_rel {A B} S x (R1: rel (env A) A) (R2: rel (env A) B) v:
  dom_rel S R1 →
  dom_rel S (RelCompose (RelPush R1 x v) R2).
Proof.
  intros Hdom1 e v' [e' [[Heq H1] H2]].
  apply Hdom1 in H1. assumption.
Qed.
Hint Resolve RelCompose_RelPush_dom_rel: dom_rel.

Lemma push_compose_rewrite {A B} R1 x (v: A) (R2: rel (env A) B):
  RelEquiv (RelCompose (RelPush R1 x v) R2)
           (Rel _ _ (fun e v2 ⇒ in_rel R1 e v ∧ in_rel R2 (x ¬ v ++ e) v2)).
Proof.
  intros e v'; split; intro H; simpl in ×.
  - destruct H as [p [[Heq H1] H2]]. subst. auto.
  - destruct H as [H1 H2]. eauto.
Qed.

Lemma push_compose_pointwise_rewrite {A B} R1 x (R2: rel (env A) B) :
  pointwise RelEquiv
            (fun v ⇒ RelCompose (RelPush R1 x v) R2)
            (fun v ⇒ Rel _ _ (fun e v2 ⇒ in_rel R1 e v ∧ in_rel R2 (x ¬ v ++ e) v2)).
Proof.
  intro v. apply push_compose_rewrite.
Qed.

RelRemove R1 R2 x is the existential closure of the composition of RelPush R2 x with R1.

Lemma RelRemove_rewrite {A} R1 (R2: rel (env A) A) x :
  RelEquiv (RelRemove R1 R2 x)
           (RelCloseV (fun v ⇒ RelCompose (RelPush R2 x v) R1)).
Proof.
  rewrite push_compose_pointwise_rewrite.
  reflexivity.
Qed.