Coral.PointwiseRel: abstraction of relations into pointwise relations

Author: Benoît Montagu
Copyright © Inria 2020 CeCILL-B License
Synopsis: Abstraction of relations into pointwise relations by means the independent attribute abstraction, and proof of abstraction of the various combinators on relations.

Require Import Infrastructure.
Require Import Env.
Require Import Rel.
Require Import RelStable.
Require Import Transp.
Require Import SupportFacts.
Require Import EquivarianceFacts.
Require Import RelExtra.
Require Import RelGood.
Require Import SubstEnv.

Pointwise relations. This is the definition in Section 5.1 of the ICFP'20 paper.
Inductive prel {A B: Type} : Type :=
| Bottom
Bottom element
| PRel: env (rel A B) → rel A B → prel.
Pair of an environment of relations and of a relation

Comparison

prel_leq pr1 pr2 holds when pr1 is smaller than pr2 (in terms of inclusion. Related pointwise relations are required to have identical domains. This is Figure 5 of the ICFP'20 paper.
Inductive prel_leq {A B: Type} : @prel A B → @prel A B → Prop :=
| PRelLeqBot: ∀ prel,
    prel_leq Bottom prel
| PRelLeqPointwise: ∀ g1 g2 this1 this2,
    dom g2 [=] dom g1 →
    (∀ x gx1 gx2,
        get x g1 = Some gx1 →
        get x g2 = Some gx2 →
        RelIncl gx1 gx2
    ) →
    RelIncl this1 this2 →
    prel_leq (PRel g1 this1) (PRel g2 this2).

prel_leq is a reflexive relation. This is the first half of Lemma 5.1 of the ICFP'20 paper.
Lemma prel_leq_refl {A B} (pR: @prel A B):
  prel_leq pR pR.
Proof.
  destruct pR as [| g this].
  - apply PRelLeqBot.
  - apply PRelLeqPointwise.
    + reflexivity.
    + intros x gx1 gx2 H1 H2. assert (gx1 = gx2) by congruence.
      subst. reflexivity.
    + reflexivity.
Qed.

prel_leq is a transitive relation. This is the second half of Lemma 5.1 of the ICFP'20 paper.
Lemma prel_leq_trans {A B} (pR1: @prel A B) (pR2: @prel A B) (pR3: @prel A B):
  prel_leq pR1 pR2 →
  prel_leq pR2 pR3 →
  prel_leq pR1 pR3.
Proof.
  intros H12 H23.
  destruct pR1 as [| g1 this1]; [ solve [apply PRelLeqBot] |].
  destruct pR2 as [| g2 this2]; [ solve [inversion H12] |].
  destruct pR3 as [| g3 this3]; [ solve [inversion H23] |].
  inversion H12; subst.
  inversion H23; subst.
  apply PRelLeqPointwise.
  - transitivity (dom g2); assumption.
  - intros x gx1 gx3 Hx1 Hx3.
    case_eq (get x g2); intros.
    + rename r into gx2. transitivity gx2; eauto.
    + exfalso. apply get_notin_dom in H. apply get_in_dom in Hx3. fsetdec.
  - transitivity this2; assumption.
Qed.

Add Parametric Relation (A B: Type): (@prel A B) (@prel_leq A B)
    reflexivity proved by prel_leq_refl
    transitivity proved by prel_leq_trans
      as prel_leq_Rel.

Equivalence of pointwise relations

prel_equiv pr1 pr2 holds when pr1 is equivalent than pr2 (in terms of inclusion. Related pointwise relations are required to have identical domains.
Inductive prel_equiv {A B: Type} : @prel A B → @prel A B → Prop :=
| PRelEquivBot:
    prel_equiv Bottom Bottom
| PRelEquivPointwise: ∀ g1 g2 this1 this2,
    dom g2 [=] dom g1 →
    (∀ x gx1 gx2,
        get x g1 = Some gx1 →
        get x g2 = Some gx2 →
        RelEquiv gx1 gx2
    ) →
    RelEquiv this1 this2 →
    prel_equiv (PRel g1 this1) (PRel g2 this2).

prel_equiv is a symmetric relation.
Lemma prel_equiv_sym {A B} (pR1 pR2: @prel A B):
  prel_equiv pR1 pR2 →
  prel_equiv pR2 pR1.
Proof.
  intro H. destruct H.
  - apply PRelEquivBot.
  - apply PRelEquivPointwise.
    + symmetry. assumption.
    + intros. symmetry. eauto.
    + symmetry. assumption.
Qed.

prel_equiv implies prel_leq
Lemma prel_equiv_leq1 {A B} (pR1 pR2: @prel A B):
  prel_equiv pR1 pR2 →
  prel_leq pR1 pR2.
Proof.
  intros H. destruct H.
  - apply PRelLeqBot.
  - apply PRelLeqPointwise; eauto.
Qed.
Hint Resolve prel_equiv_leq1: core.

prel_equiv implies the reverse of prel_leq
Lemma prel_equiv_leq2 {A B} (pR1 pR2: @prel A B):
  prel_equiv pR1 pR2 →
  prel_leq pR2 pR1.
Proof.
  intro H. apply prel_equiv_sym in H.
  apply prel_equiv_leq1; assumption.
Qed.
Hint Resolve prel_equiv_leq2: core.

Antisymmetry for prel_leq.
Lemma prel_leq_antisym {A B} (pR1 pR2: @prel A B):
  prel_leq pR1 pR2 →
  prel_leq pR2 pR1 →
  prel_equiv pR1 pR2.
Proof.
  intros H12 H21. destruct H12; inversion H21; subst.
  - apply PRelEquivBot.
  - apply PRelEquivPointwise.
    + fsetdec.
    + intros. apply RelIncl_antisym; eauto.
    + apply RelIncl_antisym; assumption.
Qed.

prel_equiv is a reflexive relation.
Lemma prel_equiv_refl {A B} (prel: @prel A B):
  prel_equiv prel prel.
Proof.
  apply prel_leq_antisym; reflexivity.
Qed.

prel_equiv is a transitive relation.
Lemma prel_equiv_trans {A B} (pR1: @prel A B) (pR2: @prel A B) (pR3: @prel A B):
  prel_equiv pR1 pR2 →
  prel_equiv pR2 pR3 →
  prel_equiv pR1 pR3.
Proof.
  intros H12 H23.
  apply prel_leq_antisym; transitivity pR2; auto.
Qed.

Add Parametric Relation (A B: Type): (@prel A B) (@prel_equiv A B)
    reflexivity proved by prel_equiv_refl
    symmetry proved by prel_equiv_sym
    transitivity proved by prel_equiv_trans
      as prel_equiv_Rel.

Require Import Setoid.

Add Parametric Morphism A B: (@prel_leq A B)
    with signature prel_equiv ==> prel_equiv ==> iff
      as prel_leq_morphism_equiv.
Proof.
  intros pR1 pR2 H12 pR3 pR4 H34. split; intro H.
  - transitivity pR1; auto. transitivity pR3; auto.
  - transitivity pR2; auto. transitivity pR4; auto.
Qed.

Add Parametric Morphism A B: (@PRel A B)
    with signature env_rel_incl ++> RelIncl ++> prel_leq
      as PRel_morphism_incl.
Proof.
  intros pR1 pR2 H12 pR3 pR4 H34. apply PRelLeqPointwise.
  - apply env_rel_incl_dom in H12. fsetdec.
  - intros x gx1 gx2 Hx1 Hx2. eapply env_rel_incl_get; eauto.
  - assumption.
Qed.

Add Parametric Morphism A B: (@PRel A B)
    with signature env_rel_equiv ==> RelEquiv ++> prel_equiv
      as PRel_morphism_equiv.
Proof.
  intros pR1 pR2 H12 pR3 pR4 H34.
  apply prel_leq_antisym.
  - apply PRel_morphism_incl; auto using env_rel_incl_refl_equiv.
  - symmetry in H12. symmetry in H34.
    apply PRel_morphism_incl; auto using env_rel_incl_refl_equiv.
Qed.

Concretization

The concretization of a pointwise relation pR for a domain S is a relation between substitutions whose domains are larger than S and values. This is the first half of Figure 6 of the ICFP'20 paper.
Definition concretize (S: atoms) (pR: prel) : rel (env term) term :=
  match pR with
  | Bottom ⇒ RelBot
  | PRel g this ⇒
    Rel _ _
        (fun e v ⇒
           all_env good_value e
           ∧ good_value v
           ∧ S [<=] dom e
           ∧ S [=] dom g
           ∧ (∀ x vx gx,
                 x `in` S →
                 get x e = Some vx →
                 get x g = Some gx →
                 in_rel gx vx v)
           ∧ (∀ v', good_value v' → in_rel this v' v)
        )
  end.

Emptiness test

The range of an environment of binary relations and of a binary relation is the intersection of the RHS of the relations. The range can be used to test for the vacuity of a pointwise relation.
Definition range {A} (g: env (rel term A)) (this: rel term A) : rel term A :=
  RelInter
    (Rel _ _ (fun v1 v2 ⇒ ∀ x gx, get x g = Some gx → ∃ v0, good_value v0 ∧ in_rel gx v0 v2))
    (Rel _ _ (fun v1 v2 ⇒ ∀ v, good_value v → in_rel this v v2)).

A sufficient condition for the ranges to be included.
Lemma range_incl {A} (g1 g2: env (rel term A)) (this1 this2: rel term A) :
  dom g2 [<=] dom g1 →
  (∀ (x : atom) (gx1 gx2 : rel term A),
      get x g1 = Some gx1 → get x g2 = Some gx2 → RelIncl gx1 gx2) →
  RelIncl this1 this2 →
  RelIncl (range g1 this1) (range g2 this2).
Proof.
  intros Hdom Hg Hthis.
  intros u v [Hgv Hthisv]. split.
  - intros x gx Hx.
    case_eq (get x g1); intros.
    + assert (RelIncl r gx) by eauto.
      apply Hgv in H. destruct H as [v0 [Hgood H]].
      ∃ v0. split; [assumption|]. apply H0. assumption.
    + exfalso. apply get_in_dom in Hx. apply get_notin_dom in H. fsetdec.
  - intros v0 Hgood. apply Hthis. apply (Hthisv v0). assumption.
Qed.

A sufficient condition for the ranges to be equivalent.
Lemma range_equiv {A} (g1 g2: env (rel term A)) (this1 this2: rel term A) :
  dom g1 [=] dom g2 →
  (∀ (x : atom) (gx1 gx2 : rel term A),
      get x g1 = Some gx1 → get x g2 = Some gx2 → RelEquiv gx1 gx2) →
  RelEquiv this1 this2 →
  RelEquiv (range g1 this1) (range g2 this2).
Proof.
  intros Hdom Hg Hthis. apply RelIncl_antisym.
  - apply range_incl; eauto. fsetdec.
  - apply range_incl; eauto. fsetdec.
Qed.

For a pointiwse relation to be semantically empty, it suffices that its range is empty.
Lemma concretize_pointwise_empty_condition_range S g this :
  RelIncl (range g this) RelBot →
  RelIncl (concretize S (PRel g this)) RelBot.
Proof.
  intro Hrange.
  intros e v [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]]. simpl.
  apply (Hrange Unit v). simpl. split.
  - intros x gx Hx.
    case_eq (get x e); intros.
    + ∃ t. split.
      × eapply all_env_get; eauto.
      × eapply Hg; eauto. apply get_in_dom in Hx. fsetdec.
    + exfalso. apply get_in_dom in Hx. apply get_notin_dom in H. fsetdec.
  - assumption.
Qed.

A sufficient condition for a pointwise relation to be semantically empty: one of its constituent relations is empty.
Lemma concretize_pointwise_empty_condition S g this :
  ((∃ x gx, x `in` S ∧ get x g = Some gx ∧ RelIncl gx RelBot)
   ∨ RelIncl this RelBot) →
  RelIncl (concretize S (PRel g this)) RelBot.
Proof.
  intro H.
  apply concretize_pointwise_empty_condition_range.
  destruct H as [[x [gx [HxS [Hget Hincl]]]] | Hincl ].
  - intros u v [Hg Hthis].
    apply Hg in Hget. destruct Hget as [v0 [Hgood Hv0]].
    apply (Hincl v0 v). assumption.
  - intros u v [Hg Hthis]. simpl.
    apply (Hincl Unit v).
    apply Hthis. auto with good_rel.
Qed.

Auxiliary lemma that builds an environment from the condition that asserts that for a given RHS value v, there exists for every gx in g a LHS value v0 such that gx relates v0 to v.
Lemma build_env_from_good_rels g v :
  uniq g →
  all_env good_vrel g →
  (∀ (x : atom) (gx : rel term term),
      get x g = Some gx → ∃ v0 : term, good_value v0 ∧ in_rel gx v0 v) →
  ∃ e : env term,
    all_env good_value e ∧
    dom g [=] dom e ∧
    (∀ (x : atom) (vx : term) (gx : rel term term),
     get x e = Some vx → get x g = Some gx → in_rel gx vx v).
Proof.
  intros Huniq Hggood Hg.
  env induction g.
  - ∃ nil. split; [| split]; auto.
    + reflexivity.
    + intros. exfalso. simpl in ×. congruence.
  - simpl in Hggood. destruct Hggood as [Hgooda Hggood].
    destruct IHg as [e [Hegood [Hedom H]]]; auto.
    + solve_uniq.
    + intros y gy Hy.
      destruct (x == y); subst.
      × exfalso. apply get_in_dom in Hy. solve_uniq.
      × apply (Hg y gy). simpl. destruct (y == x); congruence.
    + destruct (Hg x a) as [vx [Hgoodx Hx]].
      { simpl. destruct (x == x); congruence. }
      ∃ ((x, vx) :: e). split; [| split].
      × split; auto.
      × simpl. fsetdec.
      × { intros y vy gy Hgete Hgetg.
          simpl in Hgete. simpl in Hgetg.
          destruct (y == x); subst.
          - congruence.
          - eauto.
        }
Qed.

A sufficient condition to build an environment that is on the LHS of a pointwise relation, given a fixed RHS value v.
Lemma build_env_in_concretize S g this v :
  S [=] dom g →
  uniq g →
  all_env good_vrel g →
  good_vrel this →
  (∀ (x : atom) (gx : rel term term),
      get x g = Some gx → ∃ v0 : term, good_value v0 ∧ in_rel gx v0 v) →
  (∀ v' : term, good_value v' → in_rel this v' v) →
  ∃ e : env term, in_rel (concretize S (PRel g this)) e v.
Proof.
  intros Hgdom Huniq Hggood Hthisgood Hg Hthis.
  destruct (build_env_from_good_rels g v) as [e [Hegood [Hedom Heg]]]; auto.
  ∃ e. split; [| split; [| split; [| split; [| split]]]]; auto.
  - assert (in_rel this Unit v) by eauto with good_rel. eauto.
  - fsetdec.
  - intros. eauto.
Qed.

If the concretizations of two pointwise relations are included, then their ranges are also included.
Lemma concretize_incl_range_incl S g1 this1 g2 this2:
  S [=] dom g1 →
  uniq g1 →
  all_env good_vrel g1 →
  good_vrel this1 →
  RelIncl (concretize S (PRel g1 this1)) (concretize S (PRel g2 this2)) →
  RelIncl (range g1 this1) (range g2 this2).
Proof.
  intros Hdom1 Huniq1 Hgoodg1 Hgoodthis1 Hincl.
  intros u v [Hg1 Hthis1]. simpl in Hg1, Hthis1.
  destruct (build_env_in_concretize S g1 this1 v) as [e Hev]; auto.
  apply Hincl in Hev. clear Hincl.
  destruct Hev as [Hegood [Hvgood [Hedom [Hg2dom [Hg2 Hthis2]]]]].
  split; simpl; auto.
  intros x gx Hx2.
  assert (∃ vx, get x e = Some vx) as [vx Hxe].
  { case_eq (get x e); intros; eauto.
    exfalso. apply get_in_dom in Hx2. apply get_notin_dom in H. fsetdec.
  }
  ∃ vx. split.
  + eapply all_env_get; eauto.
  + eapply Hg2; eauto. apply get_in_dom in Hx2. fsetdec.
Qed.

If a relation is semantically empty, then its range is also empty. This is the reversed implication of previous lemma concretize_pointwise_empty_condition_range.
Lemma concretize_incl_range_incl_bottom S g this :
  S [=] dom g →
  uniq g →
  all_env good_vrel g →
  good_vrel this →
  RelIncl (concretize S (PRel g this)) RelBot →
  RelIncl (range g this) RelBot.
Proof.
  intros Hgdom Huniq Hggood Hthisgood H.
  rewrite (concretize_incl_range_incl S g this nil RelBot); auto.
  - intros v1 v2 [Hnil Hbot]. simpl in ×.
    apply (Hbot Unit); auto with good_rel.
  - rewrite H. apply RelBot_bot.
Qed.

Properties of concretize

A sufficient condition to add a binding to the LHS substitution of a pointwise relation.
Lemma concretize_update S g this e x gx vx v:
  all_env good_vrel g →
  get x g = Some gx →
  in_rel gx vx v →
  in_rel (concretize S (PRel g this)) e v →
  in_rel (concretize S (PRel g this)) ((x, vx) :: e) v.
Proof.
  intros Hggood Hxget Hrx Hev.
  destruct Hev as [Hegood [Hvgood [Hdome [Hdomg [Hg Hthis]]]]].
  split; [ split | split; [| split; [| split; [| split]]]]; simpl; auto.
  - assert (good_vrel gx) by (eapply all_env_get; eauto). eauto.
  - fsetdec.
  - intros y vy gy HyS Hygete Hygetg.
    destruct (y == x); subst; eauto. congruence.
Qed.

Soundness of prel_leq. This is Lemma 5.3 of the ICFP'20 paper.
Lemma concretize_monotonic S pR1 pR2:
  prel_leq pR1 pR2 →
  RelIncl (concretize S pR1) (concretize S pR2).
Proof.
  intros Hleq e v Hev.
  destruct Hleq.
  - destruct Hev.
  - destruct Hev as [Hegood [Hvgood [Hdome [Hdomg [Hg Hthis]]]]].
    split; [| split; [| split; [| split; [| split ] ] ] ].
    + assumption.
    + assumption.
    + assumption.
    + fsetdec.
    + intros x vx gx2 Hx Hget Hget2.
      case_eq (get x g1); intros.
      × eapply H0; eauto.
      × exfalso. apply get_in_dom in Hget2. apply get_notin_dom in H2. fsetdec.
    + intros v' Hvgood'. apply H1; auto.
Qed.


Add Parametric Morphism: concretize
    with signature AtomSetImpl.Equal ==> prel_equiv ==> RelEquiv
      as concretize_morphism_equiv.
Proof.
  intros S1 S2 HS pR1 pR2 HPr.
  inversion HPr; subst; simpl.
  - reflexivity.
  - intros e v. simpl.
    apply iff_split; [ reflexivity |].
    apply iff_split; [ reflexivity |].
    apply iff_split; [ rewrite HS; reflexivity |].
    apply iff_split; [ rewrite HS; rewrite H; reflexivity |].
    apply iff_split.
    + split; intros Hg x vx gx HxS Hxe Hxg.
      × { case_eq (get x g1); intros.
          - rewrite <- (H0 x r gx); auto.
            apply (Hg x); auto.
            fsetdec.
          - exfalso. apply get_in_dom in Hxg. apply get_notin_dom in H2. fsetdec.
        }
      × { case_eq (get x g2); intros.
          - rewrite (H0 x gx r); auto.
            apply (Hg x); auto.
            fsetdec.
          - exfalso. apply get_in_dom in Hxg. apply get_notin_dom in H2. fsetdec.
        }
    + split; intros Hthis v' Hgoodv'.
      × rewrite <- H1. eauto.
      × rewrite H1. eauto.
Qed.

concretize is always a stable relation.
Lemma concretize_stable S pR: stable_rel (concretize S pR).
Proof.
  intros e v Hev. destruct pR as [| g this]; [ solve [destruct Hev] |].
  destruct Hev as [Hegood [Hvgood [Hdome [Hdomg [Hg Hthis]]]]].
  intros e' Hgood Hleq. split; [| split; [| split; [| split; [| split ] ] ] ].
  - assumption.
  - assumption.
  - rewrite Hdome. apply leq_env_dom. assumption.
  - fsetdec.
  - intros x vx gx Hx Hgete' Hgetg.
    case_eq (get x e); intros.
    + assert (vx = t).
      { apply Hleq in H. congruence. }
      subst t. eauto.
    + exfalso. apply get_notin_dom in H. fsetdec.
  - intros v' Hvgood'. apply Hthis. assumption.
Qed.
Hint Resolve concretize_stable: stable_rel.

concretize is always a good relation.
Lemma concretize_good S pR :
  good_rel (concretize S pR).
Proof.
  destruct pR as [| g this ]; auto with good_rel.
  intros e v [Hegood [Hvgood H]].
  split; assumption.
Qed.
Hint Resolve concretize_good: good_rel.

concretize S pR is always a relation that satisfies dom_rel S.
Lemma concretize_dom_rel S pR :
  dom_rel S (concretize S pR).
Proof.
  intros e v Hev.
  destruct pR as [| g this]; simpl in Hev; tauto.
Qed.
Hint Resolve concretize_dom_rel: dom_rel.

Concretization of an environment of pointwise relations

concretize_env maps each pointwise relation to its concretization for the domain that is the domain of the preceding environment.
Definition concretize_env (E: env (@prel term term)) : env (rel (env term) term) :=
  map_env_dom (fun _ pR S ⇒ concretize S pR) E.

Specification of the concretization of an environment.
Lemma concretize_env_spec E1 x pR E2 R:
  x `notin` dom E2 →
  get x (concretize_env (E2 ++ [(x, pR)] ++ E1)) = Some R →
  RelEquiv R (concretize (dom E1) pR).
Proof.
  intros Hx Hget.
  apply map_env_dom_spec with (equal := RelEquiv) in Hget; auto.
  intros y a S1 S2 HS. rewrite HS. reflexivity.
Qed.

concretize_env E has the same domain as E.
Lemma concretize_env_dom E:
  dom (concretize_env E) [=] dom E.
Proof.
  apply map_env_dom_dom.
Qed.

concretize_env E has no duplicate binding.
Lemma concretize_env_uniq E:
  uniq E ↔ uniq (concretize_env E).
Proof.
  apply map_env_dom_uniq.
Qed.

Transposition of pointwise relations

transp_prel x y pR is the transposition of the name x for the name y in the pointwise relation pR.
Definition transp_prel x y pR :=
  match pR with
  | Bottom ⇒ Bottom
  | PRel g this ⇒
    PRel
      (transp_env_vrel x y g)
      (transp_vrel x y this)
  end.

Lemma transp_prel_refl x pR:
  prel_equiv (transp_prel x x pR) pR.
Proof.
  destruct pR as [| g this]; simpl.
  - reflexivity.
  - rewrite transp_env_vrel_refl. rewrite transp_vrel_refl. reflexivity.
Qed.

Lemma transp_prel_sym x y pR:
  prel_equiv (transp_prel x y pR) (transp_prel y x pR).
Proof.
  destruct pR as [| g this]; simpl.
  - reflexivity.
  - rewrite transp_env_vrel_swap. rewrite transp_vrel_swap. reflexivity.
Qed.

Lemma transp_prel_involution x y pR:
  prel_equiv (transp_prel x y (transp_prel x y pR)) pR.
Proof.
  destruct pR as [| g this]; simpl.
  - reflexivity.
  - rewrite transp_env_vrel_involution. rewrite transp_vrel_involution. reflexivity.
Qed.

supported_prel S pR means that pR is finitely supported by S.
Definition supported_prel S pR : Prop :=
  match pR with
  | Bottom ⇒ True
  | PRel g this ⇒
    supported_env_vrel S g
    ∧ supported_vrel S this
  end.

supported_prel is covariant in the set of atoms.
Lemma supported_prel_subset S1 S2 pR :
  S1 [<=] S2 →
  supported_prel S1 pR →
  supported_prel S2 pR.
Proof.
  intros Hincl H. destruct pR as [| g this ]; simpl in ×.
  - trivial.
  - destruct H as [Hg Hthis].
    split.
    + eauto using supported_env_vrel_subset.
    + eauto using supported_vrel_subset.
Qed.

Fundamental property of supporting sets.
Lemma transp_prel_fresh_eq S x y pR :
  supported_prel S pR →
  x `notin` S →
  y `notin` S →
  prel_equiv (transp_prel x y pR) pR.
Proof.
  intros Hsupp Hx Hy. destruct pR as [| g this]; simpl in ×.
  - reflexivity.
  - destruct Hsupp as [Hsupp1 Hsupp2].
    rewrite (transp_env_vrel_fresh_eq S x y); auto.
    rewrite (transp_vrel_fresh_eq S x y); auto.
    reflexivity.
Qed.

Lemma transp_prel_trans S x y z pR :
  supported_prel S pR →
  x `notin` S →
  y `notin` S →
  prel_equiv (transp_prel x y (transp_prel y z pR)) (transp_prel x z pR).
Proof.
  intros Hsupp Hx Hy. destruct pR as [| g this]; simpl in ×.
  - reflexivity.
  - destruct Hsupp as [Hsupp1 Hsupp2].
    rewrite (transp_env_vrel_trans S x y z); auto.
    rewrite (transp_vrel_trans S x y z); auto.
    reflexivity.
Qed.

If pR is supported by S, then its concretization for the domain S is supported by S.
Lemma concretize_supported S pR:
  supported_prel S pR →
  supported_rel S (concretize S pR).
Proof.
  intro H. destruct pR as [| g this ]; simpl in *; auto with supported_rel.
  destruct H as [Hg Hthis].
  intros x y Hx Hy e v. simpl.
  apply iff_split; [| apply iff_split; [| apply iff_split; [| apply iff_split; [| apply iff_split ] ] ] ].
  - rewrite all_env_term_equivariant; auto using good_value_equivariant.
    reflexivity.
  - apply good_value_equivariant.
  - rewrite (atoms_incl_equivariant x y).
    rewrite (transp_atoms_fresh_eq x y S); auto.
    rewrite dom_equivariant_term.
    rewrite transp_env_term_involution.
    reflexivity.
  - reflexivity.
  - split; intros H z vz gz HzS Hzeget Hzgget.
    + apply (in_vrel_equivariant x y).
      assert (supported_vrel S gz) as Hsupp by (eapply supported_env_vrel_get; eauto).
      rewrite (Hsupp x y); auto.
      apply (H (transp_atom x y z)); auto.
      × apply (in_equivariant x y).
        rewrite transp_atom_involution.
        rewrite transp_atoms_fresh_eq; auto.
      × rewrite <- get_transp_env_term_equivariant.
        rewrite Hzeget. reflexivity.
      × rewrite transp_atom_other; [ auto | fsetdec | fsetdec ].
    + apply (in_vrel_equivariant x y).
      assert (supported_vrel S gz) as Hsupp by (eapply supported_env_vrel_get; eauto).
      rewrite (Hsupp x y); auto.
      rewrite transp_term_involution.
      apply (H z); auto.
      apply (get_transp_env_term_Some_equivariant x y).
      rewrite (transp_atom_other x y z); [ | fsetdec | fsetdec ].
      rewrite transp_term_involution.
      assumption.
  - split; intros H v' Hgood.
    + apply (in_vrel_equivariant x y).
      rewrite (Hthis x y); auto.
      assert (fv v' [<=] empty) as Hfv by auto.
      rewrite (transp_term_fresh_eq x y v'); [| fsetdec | fsetdec ].
      apply H; assumption.
    + apply (in_vrel_equivariant x y).
      rewrite (Hthis x y); auto.
      assert (fv v' [<=] empty) as Hfv by auto.
      rewrite (transp_term_fresh_eq x y v'); [| fsetdec | fsetdec ].
      rewrite transp_term_involution.
      apply H; assumption.
Qed.

Good pointwise relation

A good pointwise relation for the domain S is either empty, or contains only good relations, and its map has domain S and has no duplicate bindings.
Definition good_prel S pR : Prop :=
  match pR with
  | Bottom ⇒ True
  | PRel g this ⇒
    S [=] dom g ∧
    uniq g ∧
    all_env good_vrel g ∧
    good_vrel this
  end.

Add Parametric Morphism: good_prel
    with signature AtomSetImpl.Equal ==> eq ==> iff
      as good_prel_morphism_equiv.
Proof.
  intros S1 S2 HS pR. destruct pR; simpl in ×.
  - tauto.
  - rewrite HS. tauto.
Qed.

A weaker version of good_prel, that does not impose the constraint on the domains.
Definition good_prel0 pR : Prop :=
  match pR with
  | Bottom ⇒ True
  | PRel g this ⇒
    uniq g ∧
    all_env good_vrel g ∧
    good_vrel this
  end.

Wellformed environment of pointwise relations

An environment E of pointwise relations is wellformed if each of its constituent is wellformed for the domain that is the domain of the preceding environment.
Definition wf_prel_env (E: env (@prel term term)) : Prop :=
  forall_env_dom (fun _ pR S ⇒ good_prel S pR) E.

Specification lemma for wf_prel_env.
Lemma wf_prel_env_spec E1 x pR E2:
  x `notin` dom E2 →
  wf_prel_env (E2 ++ [(x, pR)] ++ E1) →
  good_prel (dom E1) pR.
Proof.
  intros Hx Hwf.
  apply forall_env_dom_spec in Hwf; auto.
  intros y a S1 S2 HS HS1. rewrite <- HS. assumption.
Qed.

Necessary and sufficient condition to add a binding to a wellformed environment.
Lemma wf_prel_env_cons x pR E:
  wf_prel_env ((x, pR) :: E) ↔
  (good_prel (dom E) pR ∧ wf_prel_env E).
Proof.
  unfold wf_prel_env.
  rewrite forall_env_dom_cons.
  - reflexivity.
  - intros y a S1 S2 HS HS1. rewrite <- HS. assumption.
Qed.

Every pointwise relation of a wellformed environment satisfies good_prel0.
Lemma wf_prel_env_good0 E:
  uniq E →
  wf_prel_env E →
  all_env good_prel0 E.
Proof.
  intros Huniq Hwf.
  env induction E.
  - trivial.
  - simpl in ×. rewrite wf_prel_env_cons in Hwf. destruct Hwf as [Hgood Hwf].
    split.
    + destruct a; simpl in *; tauto.
    + apply IHE; auto. solve_uniq.
Qed.
Hint Resolve wf_prel_env_good0: core.

Abstraction

Abstraction of a relation as a pointwise relation, given a domain S. The definition takes the form of a relation (as opposed to a function) because is it not computable. This is the second half of Figure 6 of the ICFP'20 paper.
Inductive abstract (S: atoms) (R: rel (env term) term): (@prel term term) → Prop :=
| AbstractEmpty:
    RelIncl R RelBot →
    abstract S R Bottom
| AbstractOther g this:
    ¬ RelIncl R RelBot →
    dom g [=] S →
    (∀ x Rx,
        get x g = Some Rx →
        RelEquiv Rx (Rel _ _ (fun v1 v2 ⇒ ∃ e, S [<=] dom e ∧
                                             get x e = Some v1 ∧
                                             in_rel R e v2))
    ) →
    RelEquiv this (Rel _ _ (fun v1 v2 ⇒ good_value v1 ∧
                                      ∃ e, S [<=] dom e ∧
                                           in_rel R e v2)) →
    abstract S R (PRel g this).

Add Parametric Morphism: abstract
    with signature AtomSetImpl.Equal ==> RelEquiv ==> prel_equiv ==> iff
      as abstract_morphism_equiv.
Proof.
  intros S1 S2 HS R1 R2 HR pR1 pR2 HpR.
  split; intro H; destruct H; inversion HpR; subst.
  - apply AbstractEmpty. rewrite <- HR. assumption.
  - constructor.
    + rewrite <- HR. assumption.
    + fsetdec.
    + intros x Rx Hx.
      case_eq (get x g); intros.
      × transitivity r; [ solve [symmetry; eapply H6; eauto] |].
        rewrite (H1 x r); auto.
        { intros v1 v2. split; intros [e [Hedom [Hget H12]]]; simpl in ×.
          - ∃ e. split; [ fsetdec | split; [ assumption |]]. rewrite <- HR. assumption.
          - ∃ e. split; [ fsetdec | split; [ assumption |]]. rewrite HR. assumption.
        }
      × exfalso. apply get_in_dom in Hx. apply get_notin_dom in H3. fsetdec.
    + rewrite <- H8. rewrite H2.
      intros v1 v2; split; intros [Hgood [e [Hedom H12]]]; simpl in ×.
      × split; [assumption |]. ∃ e. split; [fsetdec|]. rewrite <- HR. assumption.
      × split; [assumption |]. ∃ e. split; [fsetdec|]. rewrite HR. assumption.
  - apply AbstractEmpty. rewrite HR. assumption.
  - constructor.
    + rewrite HR. assumption.
    + fsetdec.
    + intros x Rx Hx.
      case_eq (get x g); intros.
      × transitivity r; [ solve [eapply H7; eauto] |].
        rewrite (H1 x r); auto.
        { intros v1 v2. split; intros [e [Hedom [Hget H12]]]; simpl in ×.
          - ∃ e. split; [ fsetdec | split; [ assumption |] ]. rewrite HR. assumption.
          - ∃ e. split; [ fsetdec | split; [ assumption |] ]. rewrite <- HR. assumption.
        }
      × exfalso. apply get_in_dom in Hx. apply get_notin_dom in H3. fsetdec.
    + rewrite H8. rewrite H2.
      intros v1 v2; split; intros [Hgood [e [Hegood H12]]]; simpl in ×.
      × split; [ assumption |]. ∃ e. split; [fsetdec|]. rewrite HR. assumption.
      × split; [ assumption |]. ∃ e. split; [fsetdec|]. rewrite <- HR. assumption.
Qed.

abstract S is monotonic
Lemma abstract_monotonic S R1 R2 pR1 pR2:
  abstract S R1 pR1 →
  abstract S R2 pR2 →
  RelIncl R1 R2 →
  prel_leq pR1 pR2.
Proof.
  intros Habs1 Habs2 Hincl.
  destruct pR1 as [| g1 this1]; inversion Habs1; subst;
    [| destruct pR2 as [| g2 this2]; inversion Habs2; subst ].
  - constructor.
  - exfalso. apply H1. clear H1. transitivity R2; assumption.
  - constructor.
    + fsetdec.
    + intros x gx1 gx2 Hget1 Hget2.
      rewrite (H3 x gx1); auto. erewrite (H7 x gx2); eauto.
      intros v1 v2 [e [Hedom [Hget HR1]]]. ∃ e. split; [fsetdec | split; [ assumption|]].
      apply Hincl. assumption.
    + rewrite H4. rewrite H8.
      intros v1 v2 [Hgood [e [Hedom HR1]]]. split; [ assumption|].
      ∃ e. split; [fsetdec|]. apply Hincl. assumption.
Qed.

abstract S is a functional relation: given some relation R, there is at most one pointwise relation in the output, up to equivalence.
Lemma abstract_functional S R pR1 pR2:
  abstract S R pR1 →
  abstract S R pR2 →
  prel_equiv pR1 pR2.
Proof.
  intros H1 H2.
  destruct H1; destruct H2; try contradiction.
  - constructor.
  - constructor.
    + fsetdec.
    + intros x gx1 gx2 Hget1 Hget2.
      erewrite H1; eauto. erewrite <- H5; eauto. reflexivity.
    + rewrite H3. rewrite <- H6. reflexivity.
Qed.

Require Import Classical.

For every domain S and relation R, there is a pointwise relation that is the abstraction of R for the domain S.
Lemma abstract_inhabited S R:
  ∃ pR, abstract S R pR.
Proof.
  destruct (classic (RelIncl R RelBot)) as [Hincl | Hnotincl].
  - ∃ Bottom. constructor. assumption.
  - ∃ (PRel
         (env_of_atoms
            (fun x ⇒ Rel _ _ (fun v1 v2 ⇒ ∃ e, S [<=] dom e ∧
                                           get x e = Some v1 ∧
                                           in_rel R e v2))
            S
         )
         (Rel _ _ (fun v1 v2 ⇒ good_value v1 ∧ ∃ e, S [<=] dom e ∧ in_rel R e v2))
      ).
    constructor; auto.
    + apply env_of_atoms_dom.
    + intros x Rx Hget.
      apply env_of_atoms_get_inv in Hget. subst. reflexivity.
    + reflexivity.
Qed.

Adjunction property between abstract S and concretize S. The adjunction holds for good relations that also satisfy dom_rel S. This is Lemma 5.2 of the ICFP'20 paper.
Lemma adjunction S R pR absR:
  abstract S R absR →
  (good_rel R ∧ dom_rel S R ∧ prel_leq absR pR)
  ↔ RelIncl R (concretize S pR).
Proof.
  intros Habs. split.
  - intros [HRgood [HRdom Hleq]].
    destruct pR as [| g this]; simpl; inversion Hleq; subst; inversion Habs; subst.
    + assumption.
    + rewrite H. apply RelBot_bot.
    + intros e v Hev. simpl. split; [| split; [| split; [| split; [| split ]]]].
      × eauto.
      × eauto.
      × eauto.
      × fsetdec.
      × { intros x vx gx HxS Hxe Hxg.
          case_eq (get x g1); intros.
          - apply (H3 x r gx); auto. rewrite (H6 x r); auto. simpl.
            ∃ e. split; [| split]; eauto.
          - exfalso. apply get_in_dom in Hxg. apply get_notin_dom in H. fsetdec.
        }
      × intros v' Hgood. apply H4. rewrite H7. simpl.
        split; [assumption|].
        ∃ e; split; eauto.
  - intro Hincl. split; [| split ].
    + rewrite Hincl. apply concretize_good.
    + rewrite Hincl. apply concretize_dom_rel.
    + destruct pR as [| g this]; simpl in *; inversion Habs; subst.
      × constructor.
      × contradiction.
      × constructor.
      × { constructor.
          - assert (∃ e v, in_rel R e v) as [e [v Hev]].
            { destruct (classic (∃ e v, in_rel R e v)) as [? | Hnot]; [ assumption |].
              exfalso. apply H. intros e v Hev. simpl. apply Hnot. eauto. }
            apply Hincl in Hev. simpl in Hev.
            destruct Hev as [Hegood [Hvgood [Hdome [Hdomg [Hg Hthig]]]]].
            fsetdec.
          - intros x gx0 gx Hx0 Hx. rewrite (H1 x gx0); auto.
            intros v1 v2 [e [Hedom [Hget Hev]]].
            apply Hincl in Hev. simpl in Hev.
            destruct Hev as [Hegood [Hvgood [HSe [HSg [Hg Hthis]]]]].
            apply (Hg x v1 gx); auto. apply get_in_dom in Hx0. fsetdec.
          - rewrite H2. intros v1 v2 [Hgood [e [Hegood Hev]]].
            apply Hincl in Hev.
            destruct Hev as [Hegood' [Hvgood [HSe [HSg [Hg Hthis]]]]].
            apply Hthis; assumption.
        }
Qed.

smash of pointwise relations

The smash of a pointwise relation pR is a canonical form of pR that is smaller than pR, but has an equivalent concretization. The definition takes the form of a relation (as opposed to a function), because it is not computable.
Inductive smash {A}: @prel term A → @prel term A → Prop :=
| SmashBottom: smash Bottom Bottom
| SmashPRelEmpty: ∀ g this,
    RelIncl (range g this) RelBot →
    smash (PRel g this) Bottom
| SmashPRelOther: ∀ g this pR,
    ¬ RelIncl (range g this) RelBot →
    prel_equiv pR
               (PRel (map (RelInter (range g this)) g)
                     (RelInter (range g this) this)) →
    smash (PRel g this) pR
.

smash is functional: given some input, it has at most one output, up to equivalence.
Lemma smash_functional {A} (pR pR1 pR2: @prel term A) :
  smash pR pR1 →
  smash pR pR2 →
  prel_equiv pR1 pR2.
Proof.
  intros H1 H2.
  destruct H1; inversion H2; subst; try solve [firstorder | reflexivity].
  rewrite H0. rewrite H6. reflexivity.
Qed.

For every pR, its smash exists.
Lemma smash_inhabited {A} (pR: @prel term A):
  ∃ pR', smash pR pR'.
Proof.
  destruct pR as [| g this ].
  - ∃ Bottom. constructor.
  - destruct (classic (RelIncl (range g this) RelBot)).
    + ∃ Bottom. eapply SmashPRelEmpty; eauto.
    + ∃ (PRel (map (RelInter (range g this)) g) (RelInter (range g this) this)).
      apply SmashPRelOther; auto. reflexivity.
Qed.

smash is monotonic.
Lemma smash_monotonic {A} (pR1 pR2 pR3 pR4: @prel term A):
  smash pR1 pR2 →
  smash pR3 pR4 →
  prel_leq pR1 pR3 →
  prel_leq pR2 pR4.
Proof.
  intros H12 H34 Hleq.
  destruct Hleq.
  - inversion H12; subst. constructor.
  - inversion H12; subst.
    + constructor.
    + inversion H34; subst.
      × exfalso.
        apply H4. rewrite <- H7.
        apply range_incl; auto. fsetdec.
      × { rewrite H6. rewrite H8. constructor; auto.
          - repeat rewrite dom_map. fsetdec.
          - intros x gx1 gx2 Hx1 Hx2.
            rewrite get_map in Hx1.
            case_eq (get x g1); intros; rewrite H2 in Hx1; inversion Hx1; subst; clear Hx1.
            rewrite get_map in Hx2.
            case_eq (get x g2); intros; rewrite H3 in Hx2; inversion Hx2; subst; clear Hx2.
            rewrite (H0 x r r0); auto.
            rewrite (range_incl g1 g2 this1 this2); auto.
            + reflexivity.
            + fsetdec.
          - rewrite (range_incl g1 g2 this1 this2); auto.
            + rewrite H1. reflexivity.
            + fsetdec.
        }
Qed.

Add Parametric Morphism A: (@smash A)
    with signature prel_equiv ==> prel_equiv ==> iff
      as smash_morphism_equiv.
Proof.
  assert (∀ (pR1 pR2 pR3 pR4: @prel term A),
             prel_equiv pR1 pR2 →
             prel_equiv pR3 pR4 →
             smash pR1 pR3 →
             smash pR2 pR4).
  { intros pR1 pR2 pR3 pR4 H12 H34 H.
    destruct H12; destruct H34; auto.
    - inversion H.
    - inversion H; subst.
      + constructor. rewrite <- H4.
        apply range_incl; eauto. fsetdec.
      + inversion H7.
    - inversion H; subst.
      constructor.
      + intro Hincl. apply H8. clear H8. rewrite <- Hincl. clear Hincl.
        apply range_incl; eauto. fsetdec.
      + inversion H10; subst. constructor.
        × repeat rewrite dom_map in ×. fsetdec.
        × repeat rewrite dom_map in ×.
          intros x gx3 gx2 Hx3 Hx2.
          assert (∃ gx0, get x g0 = Some gx0) as [gx0 Hx0].
          { case_eq (get x g0); intros; eauto.
            exfalso. apply get_in_dom in Hx3. apply get_notin_dom in H6. fsetdec.
          }
          assert (∃ gx1, get x g1 = Some gx1) as [gx1 Hx1].
          { case_eq (get x g1); intros; eauto.
            exfalso. apply get_in_dom in Hx0. apply get_notin_dom in H6. fsetdec.
          }
          assert (get x (map (RelInter (range g1 this1)) g1) = Some (RelInter (range g1 this1) gx1)) as Hgx1'.
          { rewrite get_map. rewrite Hx1. reflexivity. }
          assert (∃ gx20, get x g2 = Some gx20) as [gx20 Hx20].
          { case_eq (get x g2); intros; eauto.
            exfalso. rewrite get_map in Hx2. rewrite H6 in Hx2. discriminate.
          }
          assert (gx2 = RelInter (range g2 this2) gx20); subst.
          { rewrite get_map in Hx2. rewrite Hx20 in Hx2. congruence. }
          rewrite <- (H4 x gx0 gx3); auto. clear H4.
          rewrite (H13 x gx0 (RelInter (range g1 this1) gx1)); auto. clear H13.
          rewrite (H1 x gx1 gx20); auto.
          rewrite (range_equiv g1 g2 this1 this2); auto; try fsetdec.
          reflexivity.
        × rewrite <- H5. rewrite H14.
          rewrite (range_equiv g1 g2 this1 this2); auto; try fsetdec.
          rewrite H2. reflexivity.
  }
  intros pR1 pR2 H12 pR3 pR4 H34.
  split; intro H'.
  - eauto.
  - symmetry in H12. symmetry in H34. eauto.
Qed.

smash pR is always smaller than pR.
Lemma smash_leq {A} (pR1 pR2: @prel term A) :
  smash pR1 pR2 →
  prel_leq pR2 pR1.
Proof.
  intro H; destruct H.
  - reflexivity.
  - constructor.
  - rewrite H0. constructor.
    + rewrite dom_map. reflexivity.
    + intros x gx1 gx2 Hx1 Hx2.
      rewrite get_map in Hx1.
      rewrite Hx2 in Hx1. inversion Hx1; subst. clear Hx1.
      apply RelInter_lb2.
    + apply RelInter_lb2.
Qed.

The smash of the smash of pR is greater than the smash of pR.
Lemma smash_smash_leq {A} (pR1 pR2 pR3: @prel term A) :
  smash pR1 pR2 →
  smash pR2 pR3 →
  prel_leq pR2 pR3.
Proof.
  intros H12 H23.
  destruct pR1 as [| g1 this1 ]; inversion H12; subst.
  - constructor.
  - constructor.
  - rewrite H3 in H23. rewrite H3. clear H12 H3.
    inversion H23; subst.
    + exfalso. apply H1. clear H1. intros v1 v2 [Hg Hthis]. simpl in Hg, Hthis. simpl.
      apply (H3 v1 v2). clear H3. split; simpl.
      × intros x gx Hx. rewrite get_map in Hx.
        case_eq (get x g1); intros; rewrite H in Hx; inversion Hx; subst; clear Hx.
        destruct (Hg x r H) as [v [Hgoodv Hr]].
        ∃ v. split; [ assumption | split; [| assumption ] ].
        split; simpl; assumption.
      × intros v Hgoodv. split; auto.
    + rewrite H4. clear H4 H23. constructor.
      × repeat rewrite dom_map. reflexivity.
      × intros x gx1 gx2 Hgx1 Hgx2.
        rewrite get_map in Hgx1.
        case_eq (get x g1); intros; rewrite H in Hgx1; inversion Hgx1; subst; clear Hgx1.
        repeat rewrite get_map in Hgx2.
        rewrite H in Hgx2. inversion Hgx2; subst; clear Hgx2.
        intros v1 v2 [[Hg Hthis] Hr]. simpl in Hg, Hthis, Hr.
        split; split; [ | | split | ]; simpl; auto.
        intros y gy Hy. rewrite get_map in Hy.
        case_eq (get y g1); intros; rewrite H0 in Hy; inversion Hy; subst; clear Hy.
        destruct (Hg y r0 H0) as [v [Hgoodv Hr0]].
        ∃ v. split; [| split; [ split |]]; auto.
      × intros v1 v2 [[Hg Hthis] Hthis']. simpl in Hg, Hthis, Hthis'.
        split; [ split | split; [ split |] ]; simpl; auto.
        intros x gx Hx.
        rewrite get_map in Hx.
        case_eq (get x g1); intros; rewrite H in Hx; inversion Hx; subst; clear Hx.
        destruct (Hg x r H) as [v [Hgoodv Hr]].
        ∃ v. split; [| split; [ split |]]; simpl; auto.
Qed.

The smash of the smash of pR is equivalent to the smash of pR.
Lemma smash_smash_equiv {A} (pR1 pR2 pR3: @prel term A) :
  smash pR1 pR2 →
  smash pR2 pR3 →
  prel_equiv pR2 pR3.
Proof.
  intros H12 H23.
  apply prel_leq_antisym.
  - eapply smash_smash_leq; eauto.
  - apply smash_leq; assumption.
Qed.

smash is sound: the concretization of the smash pR is greater than the concretization of pR.
Lemma smash_soundness S pR1 pR2 :
  smash pR1 pR2 →
  RelIncl (concretize S pR1) (concretize S pR2).
Proof.
  intros Hsmash. destruct Hsmash.
  - reflexivity.
  - apply concretize_pointwise_empty_condition_range. assumption.
  - rewrite H0. clear H0.
    intros e v [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]].
    split; [| split; [| split; [| split; [| split ]]]]; auto.
    + rewrite dom_map. assumption.
    + intros x vx gx HxS Hxgete Hxgetg.
      rewrite get_map in Hxgetg.
      case_eq (get x g); intros; rewrite H0 in Hxgetg; inversion Hxgetg; subst.
      split; [ split; simpl; [| assumption ] | solve [eauto] ].
      intros y gy Hgety.
      case_eq (get y e); intros.
      × { ∃ t. split.
          - eapply all_env_get; eauto.
          - eapply (Hg y); eauto. apply get_in_dom in Hgety. fsetdec.
        }
      × exfalso. apply get_in_dom in Hgety. apply get_notin_dom in H1. fsetdec.
    + intros v' Hgoodv'. split; [| solve [auto] ].
      split; simpl; [| assumption ].
      intros y gy Hgety.
      case_eq (get y e); intros.
      × { ∃ t. split.
          - eapply all_env_get; eauto.
          - eapply (Hg y); eauto. apply get_in_dom in Hgety. fsetdec.
        }
      × exfalso. apply get_in_dom in Hgety. apply get_notin_dom in H0. fsetdec.
Qed.

The concretization of the smash pR is equivalent to the concretization of pR.
Lemma concretize_smash S pR1 pR2 :
  smash pR1 pR2 →
  RelEquiv (concretize S pR1) (concretize S pR2).
Proof.
  intros Hsmash.
  apply RelIncl_antisym; auto using smash_soundness, concretize_monotonic, smash_leq.
Qed.

Assume that pR1 is a good pointwise relation. If the concretization of pR1 is smaller than the concretization of pR2, then the smash of pR1 is smaller than pR2.
Lemma concretize_monotonic_inv_smash S pR1 pR2 pR3:
  good_prel S pR1 →
  RelIncl (concretize S pR1) (concretize S pR2) →
  smash pR1 pR3 →
  prel_leq pR3 pR2.
Proof.
  intros HpRgood Hincl Hsmash.
  destruct pR1 as [| g1 this1].
  - inversion Hsmash; subst. constructor.
  - inversion Hsmash; subst.
    + constructor.
    + destruct HpRgood as [Hdomg1 [Huniqg1 [Hgoodg1 Hgoodthis1]]].
      rewrite H3. clear Hsmash H3. destruct pR2 as [| g2 this2].
      × exfalso. apply H1. clear H1. apply (concretize_incl_range_incl_bottom S); auto.
      × { constructor.
          - rewrite dom_map.
            assert (∃ e v, in_rel (concretize S (PRel g1 this1)) e v) as [e [v Hev]].
            { destruct (classic (∃ e v, in_rel (concretize S (PRel g1 this1)) e v)); auto.
              exfalso. apply H1. clear H1. apply (concretize_incl_range_incl_bottom S); auto.
              intros e v Hev. simpl. apply H. clear H. eauto.
            }
            assert (in_rel (concretize S (PRel g2 this2)) e v) as Hev2 by auto.
            simpl in Hev, Hev2.
            transitivity S; [symmetry|]; tauto.
          - intros x gx1' gx2 Hx1' Hx2.
            rewrite get_map in Hx1'.
            case_eq (get x g1); intros; rewrite H in Hx1'; inversion Hx1'; subst; clear Hx1'.
            intros v1 v2 [[Hg1 Hthis1] Hv12r].
            destruct (build_env_in_concretize S g1 this1 v2) as [e Hev]; auto.
            apply (concretize_update S g1 this1 e x r v1 v2) in Hev; auto.
            apply Hincl in Hev.
            destruct Hev as [Hegood [Hv2good [Hdome [Hdomg1' [Hg1' Hthis1']]]]].
            apply (Hg1' x); auto.
            + apply get_in_dom in Hx2. fsetdec.
            + simpl. destruct (x == x); congruence.
          - intros v1 v2 [[Hg1 Hthis1] Hv12this1].
            destruct (build_env_in_concretize S g1 this1 v2) as [e Hev]; auto.
            apply Hincl in Hev.
            destruct Hev as [Hegood [Hv2good [Hdome [Hdomg1' [Hg1' Hthis1']]]]].
            apply Hthis1'. eauto.
        }
Qed.

Assume that pR1 is a good pointwise relation. Then, smash pR1 is smaller than pR2 iff concretize S pR1 is smaller than concretize S pR2.
Lemma concretize_prel_leq_iff S pR1 pR2 pR3:
  good_prel S pR1 →
  smash pR1 pR3 →
  prel_leq pR3 pR2 ↔ RelIncl (concretize S pR1) (concretize S pR2).
Proof.
  intros Hgood Hsmash. split; intro H.
  - transitivity (concretize S pR3).
    + rewrite concretize_smash.
      × reflexivity.
      × assumption.
    + apply concretize_monotonic. assumption.
  - eapply concretize_monotonic_inv_smash; eassumption.
Qed.

Assume that pR1 and pR2 good pointwise relations. Then, smash pR1 is equivalent to smash pR2 iff concretize S pR1 is equivalent to concretize S pR2.
Lemma concretize_prel_equiv_iff S pR1 pR2 pR3 pR4:
  good_prel S pR1 →
  good_prel S pR2 →
  smash pR1 pR3 →
  smash pR2 pR4 →
  prel_equiv pR3 pR4 ↔ RelEquiv (concretize S pR1) (concretize S pR2).
Proof.
  intros Hgood1 Hgood2 Hsmash1 Hsmash2. split; intro H.
  - apply RelIncl_antisym.
    + eapply concretize_prel_leq_iff; eauto.
      transitivity pR4; auto using smash_leq.
    + eapply concretize_prel_leq_iff; eauto.
      transitivity pR3; auto using smash_leq.
  - apply prel_leq_antisym.
    + apply (concretize_smash S) in Hsmash2.
      rewrite Hsmash2 in H. clear Hsmash2.
      apply (concretize_prel_leq_iff S pR1 pR4 pR3); auto.
    + apply (concretize_smash S) in Hsmash1.
      rewrite Hsmash1 in H. clear Hsmash1.
      apply (concretize_prel_leq_iff S pR2 pR3 pR4); auto.
Qed.

Intersection of pointwise relations

Intersection (auxiliary definition). This is on Figure 7 of the ICFP'20 paper.
Definition pRelInter0 {A B} (pR1 pR2: @prel A B) : option (@prel A B) :=
  match pR1, pR2 with
  | Bottom, _ | _, Bottom ⇒ Some Bottom
  | PRel g1 this1, PRel g2 this2 ⇒
    match map2 RelInter g1 g2 with
    | Some g ⇒ Some (PRel g (RelInter this1 this2))
    | None ⇒ None
    end
  end.

Intersection
Definition pRelInter {A B} (pR1 pR2 pR3: @prel A B) : Prop :=
  pRelInter0 pR1 pR2 = Some pR3.

Intersection is a morphism for prel_equiv.
Lemma pRelInter_prel_equiv {A B} (pR1 pR2 pR3 pR1' pR2': @prel A B):
  prel_equiv pR1 pR1' →
  prel_equiv pR2 pR2' →
  pRelInter pR1 pR2 pR3 →
  ∃ pR3', prel_equiv pR3 pR3' ∧ pRelInter pR1' pR2' pR3'.
Proof.
  intros Hequiv1 Hequiv2 H.
  unfold pRelInter in H.
  destruct Hequiv1; [| destruct Hequiv2 ].
  - inversion H; subst.
    ∃ Bottom. split; constructor.
  - inversion H; subst.
    ∃ Bottom. split; constructor.
  - simpl in H.
    case_eq (map2 RelInter g1 g0); intros; rewrite H6 in H; inversion H; subst; clear H.
    case_eq (map2 RelInter g2 g3); intros.
    + ∃ (PRel e0 (RelInter this2 this3)). split.
      × { constructor.
          - apply map2_dom1 in H6. apply map2_dom1 in H. fsetdec.
          - intros x ex e0x Hx Hx0.
            assert (∃ g1x, get x g1 = Some g1x) as [g1x Hg1x].
            { case_eq (get x g1); intros; eauto.
              exfalso. apply map2_dom1 in H6. apply get_in_dom in Hx.
              apply get_notin_dom in H7. fsetdec.
            }
            assert (∃ g0x, get x g0 = Some g0x) as [g0x Hg0x].
            { case_eq (get x g0); intros; eauto.
              exfalso. apply map2_dom2 in H6. apply get_in_dom in Hx.
              apply get_notin_dom in H7. fsetdec.
            }
            assert (ex = RelInter g1x g0x) by eauto using map2_get. subst.
            assert (∃ g2x, get x g2 = Some g2x) as [g2x Hg2x].
            { case_eq (get x g2); intros; eauto.
              exfalso. apply map2_dom1 in H. apply get_in_dom in Hx0.
              apply get_notin_dom in H7. fsetdec.
            }
            assert (∃ g3x, get x g3 = Some g3x) as [g3x Hg3x].
            { case_eq (get x g3); intros; eauto.
              exfalso. apply map2_dom2 in H. apply get_in_dom in Hx0.
              apply get_notin_dom in H7. fsetdec.
            }
            assert (e0x = RelInter g2x g3x) by eauto using map2_get. subst.
            rewrite (H1 x g1x g2x); auto.
            rewrite (H4 x g0x g3x); auto.
            reflexivity.
          - rewrite H2. rewrite H5. reflexivity.
        }
      × unfold pRelInter. simpl. rewrite H. reflexivity.
    + exfalso. revert H. apply map2_not_None_iff.
      assert (dom g1 [=] dom g0).
      { transitivity (dom e); [| symmetry ]; eauto using map2_dom1, map2_dom2. }
      fsetdec.
Qed.

If pR1 and pR2 are wellformed with the same domain, then pRelInter pR1 pR2 is well defined.
Lemma pRelInter_inhabited S pR1 pR2 :
  good_prel S pR1 →
  good_prel S pR2 →
  ∃ pR3, pRelInter pR1 pR2 pR3.
Proof.
  intros Hgood1 Hgood2.
  destruct pR1 as [| g1 this1]; [| destruct pR2 as [| g2 this2 ] ].
  - ∃ Bottom. constructor.
  - ∃ Bottom. constructor.
  - destruct Hgood1 as [Hdom1 [Huniq1 [Hggood1 Hthisgood1]]].
    destruct Hgood2 as [Hdom2 [Huniq2 [Hggood2 Hthisgood2]]].
    case_eq (map2 RelInter g1 g2); intros.
    + ∃ (PRel e (RelInter this1 this2)). unfold pRelInter. simpl. rewrite H.
      reflexivity.
    + exfalso. revert H. apply map2_not_None_iff. fsetdec.
Qed.

Intersection preserves wellformedness.
Lemma pRelInter_good S pR1 pR2 pR3:
  pRelInter pR1 pR2 pR3 →
  good_prel S pR1 →
  good_prel S pR2 →
  good_prel S pR3.
Proof.
  intros H Hgood1 Hgood2.
  unfold pRelInter in H.
  destruct pR1 as [| g1 this1]; [| destruct pR2 as [| g2 this2] ].
  - inversion H; subst. simpl. trivial.
  - inversion H; subst. simpl. trivial.
  - destruct Hgood1 as [Hdom1 [Huniq1 [Hggood1 Hthisgood1]]].
    destruct Hgood2 as [Hdom2 [Huniq2 [Hggood2 Hthisgood2]]].
    simpl in H.
    case_eq (map2 RelInter g1 g2); intros; rewrite H0 in H; inversion H; subst.
    split; [| split; [| split]].
    + apply map2_dom1 in H0. fsetdec.
    + eauto using map2_uniq.
    + eapply map2_all_env; eauto.
      intros x v1 v2 Hx1 Hx2.
      eapply all_env_get in Hx1; eauto.
      eapply all_env_get in Hx2; eauto.
      eauto with good_rel.
    + eauto with good_rel.
Qed.

Intersection is a lower bound of the first operand. (auxiliary lemma)
Lemma pRelInter0_leq1 {A B} (pR1 pR2 pR: @prel A B):
  pRelInter0 pR1 pR2 = Some pR →
  prel_leq pR pR1.
Proof.
  revert pR2 pR.
  induction pR1; intros [| g2 this2] pR Heq; simpl in Heq.
  - inversion Heq; subst. reflexivity.
  - inversion Heq; subst. reflexivity.
  - inversion Heq; subst. constructor.
  - case_eq (map2 RelInter e g2); intros; rewrite H in Heq; inversion Heq; subst.
    clear Heq. constructor.
    + apply map2_dom1 in H. assumption.
    + intros x gxe0 gxe Hx0 Hx.
      assert (∃ gx2, get x g2 = Some gx2) as [gx2 Hx2].
      { case_eq (get x g2); intros; eauto.
        exfalso. apply get_in_dom in Hx0. apply get_notin_dom in H0.
        apply map2_dom2 in H. fsetdec.
      }
      assert (gxe0 = RelInter gxe gx2) by eauto using map2_get. subst.
      apply RelInter_lb1.
    + apply RelInter_lb1.
Qed.

Intersection is a lower bound of the first operand.
Lemma pRelInter_leq1 {A B} (pR1 pR2 pR: @prel A B):
  pRelInter pR1 pR2 pR →
  prel_leq pR pR1.
Proof.
  intro H. unfold pRelInter in H.
  eauto using pRelInter0_leq1.
Qed.

Intersection is a lower bound of the second operand. (auxiliary lemma)
Lemma pRelInter0_leq2 {A B} (pR1 pR2 pR: @prel A B):
  pRelInter0 pR1 pR2 = Some pR →
  prel_leq pR pR2.
Proof.
  revert pR2 pR.
  induction pR1; intros [| g2 this2] pR Heq; simpl in Heq.
  - inversion Heq; subst. reflexivity.
  - inversion Heq; subst. constructor.
  - inversion Heq; subst. reflexivity.
  - case_eq (map2 RelInter e g2); intros; rewrite H in Heq; inversion Heq; subst.
    clear Heq. constructor.
    + apply map2_dom2 in H. assumption.
    + intros x gxe0 gxe Hx0 Hx.
      assert (∃ ex, get x e = Some ex) as [ex Hex].
      { case_eq (get x e); intros; eauto.
        exfalso. apply get_in_dom in Hx0. apply get_notin_dom in H0.
        apply map2_dom1 in H. fsetdec.
      }
      assert (gxe0 = RelInter ex gxe) by eauto using map2_get. subst.
      apply RelInter_lb2.
    + apply RelInter_lb2.
Qed.

Intersection is a lower bound of the second operand.
Lemma pRelInter_leq2 {A B} (pR1 pR2 pR: @prel A B):
  pRelInter pR1 pR2 pR →
  prel_leq pR pR2.
Proof.
  intro H. unfold pRelInter in H.
  eauto using pRelInter0_leq2.
Qed.

Soundness for intersection (auxiliary lemma)
Lemma pRelInter_soundness0 S pR1 pR2 pR pR':
  abstract S (RelInter (concretize S pR1) (concretize S pR2)) pR →
  pRelInter pR1 pR2 pR' →
  prel_leq pR pR'.
Proof.
  intros Habs Hinter.
  destruct pR1 as [| g1 this1]; [| destruct pR2 as [| g2 this2] ].
  - rewrite RelBot_absorbant_inter_left_equiv in Habs.
    inversion Habs; subst.
    + unfold pRelInter in Hinter. simpl in Hinter.
      inversion Hinter; subst. reflexivity.
    + exfalso. apply H. reflexivity.
  - rewrite RelBot_absorbant_inter_right_equiv in Habs.
    inversion Habs; subst.
    + unfold pRelInter in Hinter. simpl in Hinter.
      inversion Hinter; subst. reflexivity.
    + exfalso. apply H. reflexivity.
  - unfold pRelInter in Hinter. simpl in Hinter.
    case_eq (map2 RelInter g1 g2); intros; rewrite H in Hinter; try discriminate.
    inversion Habs; subst.
    + constructor.
    + inversion Hinter; subst. clear Hinter.
      { constructor.
        - assert (S [=] dom g1).
          { destruct (classic (S [=] dom g1)); auto.
            exfalso. apply H0. clear H0.
            intros env v [H0 _]. simpl in H0. simpl. tauto.
          }
          apply map2_dom1 in H. fsetdec.
        - intros x gx ex Hgx Hex.
          assert (∃ gx1, get x g1 = Some gx1) as [gx1 Hx1].
          { case_eq (get x g1); intros; eauto.
            exfalso. apply get_in_dom in Hex. apply get_notin_dom in H4.
            apply map2_dom1 in H. fsetdec.
          }
          assert (∃ gx2, get x g2 = Some gx2) as [gx2 Hx2].
          { case_eq (get x g2); intros; eauto.
            exfalso. apply get_in_dom in Hex. apply get_notin_dom in H4.
            apply map2_dom2 in H. fsetdec.
          }
          rewrite (H2 x gx); auto.
          assert (ex = RelInter gx1 gx2) by eauto using map2_get. subst.
          intros v1 v2 [env [Henvdom [Hx [[Hegood [Hvgood [Hedom [Hdom1 [Hg1 Hthis1]]]]]
[Hegood' [Hvgood' [Hedom' [Hdom2 [Hg2 Hthis2]]]]]]]]].
          split.
          + eapply Hg1; eauto. apply get_in_dom in Hgx. fsetdec.
          + eapply Hg2; eauto. apply get_in_dom in Hgx. fsetdec.
        - rewrite H3.
          intros v1 v2 [Hgood [env [Henvdom [[Hegood [Hvgood [Hedom [Hdom1 [Hg1 Hthis1]]]]]
[Hegood' [Hvgood' [Hedom' [Hdom2 [Hg2 Hthis2]]]]]]]]].
          split; auto.
      }
Qed.

Soundness for intersection. This is bullet 2 of Lemma 5.4 of the ICFP'20 paper.
Lemma pRelInter_soundness S pR1 pR2 pR :
  pRelInter pR1 pR2 pR →
  RelIncl (RelInter (concretize S pR1) (concretize S pR2)) (concretize S pR).
Proof.
  destruct (abstract_inhabited S (RelInter (concretize S pR1) (concretize S pR2)))
    as [pR' H'].
  intro H.
  rewrite <- adjunction; eauto.
  split; auto with good_rel.
  split; auto with dom_rel.
  eapply pRelInter_soundness0; eauto.
Qed.

Completeness for intersection
Lemma pRelInter_completeness S pR1 pR2 pR :
  pRelInter pR1 pR2 pR →
  RelIncl (concretize S pR) (RelInter (concretize S pR1) (concretize S pR2)).
Proof.
  intro H.
  apply RelInter_glb; apply concretize_monotonic;
    eauto using pRelInter_leq1, pRelInter_leq2.
Qed.

Adequacy for intersection
Lemma pRelInter_adequacy S pR1 pR2 pR :
  pRelInter pR1 pR2 pR →
  RelEquiv (concretize S pR) (RelInter (concretize S pR1) (concretize S pR2)).
Proof.
  intro H.
  apply RelIncl_antisym; eauto using pRelInter_soundness, pRelInter_completeness.
Qed.

Union of pointwise relations

Union (auxiliary definition). This is on Figure 7 of the ICFP'20 paper.
Definition pRelUnion0 {A B} (pR1 pR2: @prel A B) : option (@prel A B) :=
  match pR1, pR2 with
  | Bottom, pR | pR, Bottom ⇒ Some pR
  | PRel g1 this1, PRel g2 this2 ⇒
    match map2 RelUnion g1 g2 with
    | Some g ⇒ Some (PRel g (RelUnion this1 this2))
    | None ⇒ None
    end
  end.

Union
Definition pRelUnion {A B} (pR1 pR2 pR: @prel A B) : Prop :=
  pRelUnion0 pR1 pR2 = Some pR.

Union is a morphism for prel_equiv.
Lemma pRelUnion_prel_equiv {A B} (pR1 pR2 pR3 pR1' pR2': @prel A B):
  prel_equiv pR1 pR1' →
  prel_equiv pR2 pR2' →
  pRelUnion pR1 pR2 pR3 →
  ∃ pR3', prel_equiv pR3 pR3' ∧ pRelUnion pR1' pR2' pR3'.
Proof.
  intros Hequiv1 Hequiv2 H.
  unfold pRelUnion in H.
  destruct Hequiv1; [| destruct Hequiv2 ].
  - inversion H; subst.
    ∃ pR2'. split; [ assumption | constructor ].
  - inversion H; subst.
    ∃ (PRel g2 this2). split; constructor; assumption.
  - simpl in H.
    case_eq (map2 RelUnion g1 g0); intros; rewrite H6 in H; inversion H; subst; clear H.
    case_eq (map2 RelUnion g2 g3); intros.
    + ∃ (PRel e0 (RelUnion this2 this3)). split.
      × { constructor.
          - apply map2_dom1 in H6. apply map2_dom1 in H. fsetdec.
          - intros x ex e0x Hx Hx0.
            assert (∃ g1x, get x g1 = Some g1x) as [g1x Hg1x].
            { case_eq (get x g1); intros; eauto.
              exfalso. apply map2_dom1 in H6. apply get_in_dom in Hx.
              apply get_notin_dom in H7. fsetdec.
            }
            assert (∃ g0x, get x g0 = Some g0x) as [g0x Hg0x].
            { case_eq (get x g0); intros; eauto.
              exfalso. apply map2_dom2 in H6. apply get_in_dom in Hx.
              apply get_notin_dom in H7. fsetdec.
            }
            assert (ex = RelUnion g1x g0x) by eauto using map2_get. subst.
            assert (∃ g2x, get x g2 = Some g2x) as [g2x Hg2x].
            { case_eq (get x g2); intros; eauto.
              exfalso. apply map2_dom1 in H. apply get_in_dom in Hx0.
              apply get_notin_dom in H7. fsetdec.
            }
            assert (∃ g3x, get x g3 = Some g3x) as [g3x Hg3x].
            { case_eq (get x g3); intros; eauto.
              exfalso. apply map2_dom2 in H. apply get_in_dom in Hx0.
              apply get_notin_dom in H7. fsetdec.
            }
            assert (e0x = RelUnion g2x g3x) by eauto using map2_get. subst.
            rewrite (H1 x g1x g2x); auto.
            rewrite (H4 x g0x g3x); auto.
            reflexivity.
          - rewrite H2. rewrite H5. reflexivity.
        }
      × unfold pRelUnion. simpl. rewrite H. reflexivity.
    + exfalso. revert H. apply map2_not_None_iff.
      assert (dom g1 [=] dom g0).
      { transitivity (dom e); [| symmetry ]; eauto using map2_dom1, map2_dom2. }
      fsetdec.
Qed.

If pR1 and pR2 are wellformed with the same domain, then pRelUnion pR1 pR2 is well defined.
Lemma pRelUnion_inhabited S pR1 pR2 :
  good_prel S pR1 →
  good_prel S pR2 →
  ∃ pR3, pRelUnion pR1 pR2 pR3.
Proof.
  intros Hgood1 Hgood2.
  destruct pR1 as [| g1 this1]; [| destruct pR2 as [| g2 this2 ] ].
  - ∃ pR2. constructor.
  - ∃ (PRel g1 this1). constructor.
  - destruct Hgood1 as [Hdom1 [Huniq1 [Hggood1 Hthisgood1]]].
    destruct Hgood2 as [Hdom2 [Huniq2 [Hggood2 Hthisgood2]]].
    case_eq (map2 RelUnion g1 g2); intros.
    + ∃ (PRel e (RelUnion this1 this2)). unfold pRelUnion. simpl. rewrite H.
      reflexivity.
    + exfalso. revert H. apply map2_not_None_iff. fsetdec.
Qed.

Union preserves wellformedness.
Lemma pRelUnion_good S pR1 pR2 pR3:
  pRelUnion pR1 pR2 pR3 →
  good_prel S pR1 →
  good_prel S pR2 →
  good_prel S pR3.
Proof.
  intros H Hgood1 Hgood2.
  unfold pRelUnion in H.
  destruct pR1 as [| g1 this1]; [| destruct pR2 as [| g2 this2] ].
  - inversion H; subst. assumption.
  - inversion H; subst. assumption.
  - destruct Hgood1 as [Hdom1 [Huniq1 [Hggood1 Hthisgood1]]].
    destruct Hgood2 as [Hdom2 [Huniq2 [Hggood2 Hthisgood2]]].
    simpl in H.
    case_eq (map2 RelUnion g1 g2); intros; rewrite H0 in H; inversion H; subst.
    split; [| split; [| split]].
    + apply map2_dom1 in H0. fsetdec.
    + eauto using map2_uniq.
    + eapply map2_all_env; eauto.
      intros x v1 v2 Hx1 Hx2.
      eapply all_env_get in Hx1; eauto.
      eapply all_env_get in Hx2; eauto.
      eauto with good_rel.
    + eauto with good_rel.
Qed.

Union is an upper bound for the first operand. (auxiliary lemma)
Lemma pRelUnion0_leq1 {A B} (pR1 pR2 pR: @prel A B) :
  pRelUnion0 pR1 pR2 = Some pR →
  prel_leq pR1 pR.
Proof.
  intro H.
  destruct pR1 as [| g1 this1]; [| destruct pR2 as [| g2 this2 ] ]; simpl in ×.
  - constructor.
  - inversion H; subst. reflexivity.
  - case_eq (map2 RelUnion g1 g2); intros; rewrite H0 in H; inversion H; subst. clear H.
    constructor.
    + apply map2_dom1 in H0. fsetdec.
    + intros x gx1 ex Hx1 Hx.
      assert (∃ gx2, get x g2 = Some gx2) as [gx2 Hx2].
      { case_eq (get x g2); intros; eauto.
        exfalso. apply get_in_dom in Hx. apply get_notin_dom in H.
        apply map2_dom2 in H0. fsetdec.
      }
      assert (ex = RelUnion gx1 gx2) by eauto using map2_get. subst.
      apply RelUnion_ub1.
    + apply RelUnion_ub1.
Qed.

Union is an upper bound for the first operand.
Lemma pRelUnion_leq1 {A B} (pR1 pR2 pR: @prel A B) :
  pRelUnion pR1 pR2 pR →
  prel_leq pR1 pR.
Proof.
  exact (pRelUnion0_leq1 pR1 pR2 pR).
Qed.

Union is an upper bound for the second operand. (auxiliary lemma)
Lemma pRelUnion0_leq2 {A B} (pR1 pR2 pR: @prel A B) :
  pRelUnion0 pR1 pR2 = Some pR →
  prel_leq pR2 pR.
Proof.
  intro H.
  destruct pR1 as [| g1 this1]; [| destruct pR2 as [| g2 this2 ] ]; simpl in ×.
  - inversion H; subst. reflexivity.
  - constructor.
  - case_eq (map2 RelUnion g1 g2); intros; rewrite H0 in H; inversion H; subst. clear H.
    constructor.
    + apply map2_dom2 in H0. fsetdec.
    + intros x gx2 ex Hx2 Hx.
      assert (∃ gx1, get x g1 = Some gx1) as [gx1 Hx1].
      { case_eq (get x g1); intros; eauto.
        exfalso. apply get_in_dom in Hx. apply get_notin_dom in H.
        apply map2_dom1 in H0. fsetdec.
      }
      assert (ex = RelUnion gx1 gx2) by eauto using map2_get. subst.
      apply RelUnion_ub2.
    + apply RelUnion_ub2.
Qed.

Union is an upper bound for the second operand.
Lemma pRelUnion_leq2 {A B} (pR1 pR2 pR: @prel A B) :
  pRelUnion pR1 pR2 pR →
  prel_leq pR2 pR.
Proof.
  exact (pRelUnion0_leq2 pR1 pR2 pR).
Qed.

Soundness of union. This is bullet 1 of Lemma 5.4 of the ICFP'20 paper.
Lemma pRelUnion_soundness S pR1 pR2 pR:
  pRelUnion pR1 pR2 pR →
  RelIncl (RelUnion (concretize S pR1) (concretize S pR2)) (concretize S pR).
Proof.
  intro H.
  apply RelUnion_lub; apply concretize_monotonic;
    eauto using pRelUnion0_leq1, pRelUnion0_leq2.
Qed.

Composition of pointwise relations

Composition. This is on Figure 7 of the ICFP'20 paper.
Definition pRelCompose {A B C} (pR: @prel A B) (R: rel B C) : @prel A C :=
  match pR with
  | Bottom ⇒ Bottom
  | PRel g this ⇒
    PRel (map (fun r ⇒ RelCompose r R) g) (RelCompose this R)
  end.

Soundness of composition (auxiliary lemma).
Lemma pRelCompose_soundness0 S pR R pR' :
  abstract S (RelCompose (concretize S pR) R) pR' →
  prel_leq pR' (pRelCompose pR R).
Proof.
  intro H.
  destruct pR as [| g this].
  - simpl in ×. rewrite RelBot_absorbant_compose_left_equiv in H. inversion H; subst.
    + constructor.
    + exfalso. apply H0. reflexivity.
  - inversion H; subst.
    + constructor.
    + constructor.
      × rewrite dom_map.
        assert (S [=] dom g).
        { assert (∃ e v, in_rel (RelCompose (concretize S (PRel g this)) R) e v)
            as [e [v [v' [Hev' Hv'v]]]].
          { destruct (classic (∃ e v, in_rel (RelCompose (concretize S (PRel g this)) R) e v)); auto.
            exfalso. apply H0. clear H0. intros e v Hev. apply H4. clear H4. eauto.
          }
          simpl in Hev'. tauto.
        }
        fsetdec.
      × { intros x gx1 gx2 Hx1 Hx2.
          rewrite (H2 x gx1); auto. clear H2.
          case_eq (get x g); intros.
          - rewrite get_map in Hx2. rewrite H2 in Hx2. inversion Hx2; subst. clear Hx2.
            intros v1 v2 [e [Hedom' [Hxe [v [[Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]] Hvv2]]]]].
            ∃ v. split; [| assumption].
            apply (Hg x); auto.
            apply get_in_dom in H2. fsetdec.
          - exfalso. rewrite get_map in Hx2. rewrite H2 in Hx2. discriminate.
        }
      × rewrite H3. clear H3.
        intros v1 v2 [Hv1good [e [Hedom' [v [[Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]] Hvv2]]]]].
        ∃ v. split; [| assumption].
        apply Hthis; auto.
Qed.

Soundness of composition. This is bullet 3 of Lemma 5.4 of the ICFP'20 paper.
Lemma pRelCompose_soundness S pR R :
  good_vrel R →
  RelIncl (RelCompose (concretize S pR) R) (concretize S (pRelCompose pR R)).
Proof.
  destruct (abstract_inhabited S (RelCompose (concretize S pR) R)) as [pR' H'].
  intro H.
  rewrite <- adjunction; eauto.
  split; auto with good_rel.
  split; auto with dom_rel.
  eapply pRelCompose_soundness0; eauto.
Qed.

Right-sided pair of pointwise relations

Right-sided pair (auxiliary definition). This is on Figure 7 of the ICFP'20 paper.
Definition pRelPairR0 {A} (pR1 pR2: @prel A term) : option (@prel A term) :=
  match pR1, pR2 with
  | Bottom, _ | _, Bottom ⇒ Some Bottom
  | PRel g1 this1, PRel g2 this2 ⇒
    match map2 RelPairR g1 g2 with
    | Some g ⇒ Some (PRel g (RelPairR this1 this2))
    | None ⇒ None
    end
  end.

Right-sided pair
Definition pRelPairR {A} (pR1 pR2 pR: @prel A term) : Prop :=
  pRelPairR0 pR1 pR2 = Some pR.

Soundness of right-sided pair (auxiliary lemma).
Lemma pRelPairR_soundness0 S pR1 pR2 pR' pR12 :
  abstract S (RelPairR (concretize S pR1) (concretize S pR2)) pR' →
  pRelPairR pR1 pR2 pR12 →
  prel_leq pR' pR12.
Proof.
  intros Habs Hpair. unfold pRelPairR in Hpair.
  destruct pR1 as [| g1 this1]; [| destruct pR2 as [| g2 this2 ]].
  - simpl in ×. rewrite RelBot_absorbant_pairR_left_equiv in Habs. inversion Habs; subst.
    + constructor.
    + exfalso. apply H. reflexivity.
  - simpl in ×. rewrite RelBot_absorbant_pairR_right_equiv in Habs. inversion Habs; subst.
    + constructor.
    + exfalso. apply H. reflexivity.
  - inversion Habs; subst.
    + constructor.
    + simpl in Hpair.
      case_eq (map2 RelPairR g1 g2); intros; rewrite H3 in Hpair;
        inversion Hpair; subst; clear Hpair.
      constructor.
      × assert (S [=] dom g1).
        { assert (∃ e v, in_rel (RelPairR (concretize S (PRel g1 this1)) (concretize S (PRel g2 this2))) e v)
            as [e' [v Hev]].
          { destruct (classic (∃ e v, in_rel (RelPairR (concretize S (PRel g1 this1)) (concretize S (PRel g2 this2))) e v)); auto.
            exfalso. apply H. clear H. intros e' v Hev. apply H4. clear H4. eauto.
          }
          simpl in Hev. destruct v; tauto.
        }
        apply map2_dom1 in H3.
        fsetdec.
      × { intros x gx1 gx2 Hx1 Hx2.
          rewrite (H1 x gx1); auto. clear H1.
          assert (∃ g1x, get x g1 = Some g1x) as [g1x Hg1x].
          { case_eq (get x g1); intros; eauto.
            exfalso. apply get_in_dom in Hx2. apply get_notin_dom in H1.
            apply map2_dom1 in H3. fsetdec.
          }
          assert (∃ g2x, get x g2 = Some g2x) as [g2x Hg2x].
          { case_eq (get x g2); intros; eauto.
            exfalso. apply get_in_dom in Hx2. apply get_notin_dom in H1.
            apply map2_dom2 in H3. fsetdec.
          }
          assert (gx2 = RelPairR g1x g2x) by eauto using map2_get. subst.
          intros v1 v2 [e' [He'dom [Hxe' Hv]]].
          destruct v2; try tauto.
          destruct Hv as [[Hegood1 [Hvgood1 [Hedom1 [Hgdom1 [Hg1 Hthis1]]]]]
[Hegood2 [Hvgood2 [Hedom2 [Hgdom2 [Hg2 Hthis2]]]]]].
          simpl. split.
          - apply (Hg1 x); auto. apply get_in_dom in Hg1x. fsetdec.
          - apply (Hg2 x); auto. apply get_in_dom in Hg1x. fsetdec.
        }
      × { rewrite H2. clear H2.
          intros v1 v2 [Hv1good [e' [He'dom Hv]]].
          simpl in Hv. destruct v2; try tauto.
          destruct Hv as [[Hegood1 [Hvgood1 [Hedom1 [Hgdom1 [Hg1 Hthis1]]]]]
[Hegood2 [Hvgood2 [Hedom2 [Hgdom2 [Hg2 Hthis2]]]]]].
          split.
          - apply Hthis1; auto.
          - apply Hthis2; auto.
        }
Qed.

Soundness of right-sided pair. This is bullet 4 of Lemma 5.4 of the ICFP'20 paper.
Lemma pRelPairR_soundness S pR1 pR2 pR12:
  pRelPairR pR1 pR2 pR12 →
  RelIncl (RelPairR (concretize S pR1) (concretize S pR2)) (concretize S pR12).
Proof.
  destruct (abstract_inhabited S (RelPairR (concretize S pR1) (concretize S pR2))) as [pR' H'].
  intro H.
  rewrite <- adjunction; eauto.
  split; auto with good_rel.
  split; auto with dom_rel.
  eapply pRelPairR_soundness0; eauto.
Qed.

Right-sided sum of pointwise relations

Right-sided sum (auxiliary definition). This is on Figure 7 of the ICFP'20 paper.
Definition pRelSumR0 {A} (pR1 pR2: @prel A term) : option (@prel A term) :=
  match pR1, pR2 with
  | Bottom, Bottom ⇒ Some Bottom
  | Bottom, PRel g2 this2 ⇒
    Some (PRel (map (RelSumR RelBot) g2) (RelSumR RelBot this2))
  | PRel g1 this1, Bottom ⇒
    Some (PRel (map (fun r ⇒ RelSumR r RelBot) g1) (RelSumR this1 RelBot))
  | PRel g1 this1, PRel g2 this2 ⇒
    match map2 RelSumR g1 g2 with
    | Some g ⇒ Some (PRel g (RelSumR this1 this2))
    | None ⇒ None
    end
  end.

Right-sided sum.
Definition pRelSumR {A} (pR1 pR2 pR: @prel A term) : Prop :=
  pRelSumR0 pR1 pR2 = Some pR.

Soundness of right-sided sum (auxiliary lemma).
Lemma pRelSumR_soundness0 S pR1 pR2 pR' pR12 :
  abstract S (RelSumR (concretize S pR1) (concretize S pR2)) pR' →
  pRelSumR pR1 pR2 pR12 →
  prel_leq pR' pR12.
Proof.
  intros Habs Hsum. unfold pRelSumR in Hsum.
  destruct pR1 as [| g1 this1]; destruct pR2 as [| g2 this2 ].
  - simpl in ×. rewrite RelBot_absorbant_sumR_left_right_equiv in Habs. inversion Habs; subst.
    + constructor.
    + exfalso. apply H. reflexivity.
  - inversion Habs; subst.
    + constructor.
    + simpl in Hsum. inversion Hsum; subst. clear Hsum. constructor.
      × rewrite dom_map.
        assert (S [=] dom g2).
        { assert (∃ e v, in_rel (RelSumR (concretize S Bottom) (concretize S (PRel g2 this2))) e v)
            as [e' [v Hev]].
          { destruct (classic (∃ e v, in_rel (RelSumR (concretize S Bottom) (concretize S (PRel g2 this2))) e v)); auto.
            exfalso. apply H. clear H. intros e' v Hev. apply H3. clear H3. eauto.
          }
          simpl in Hev. destruct v; tauto.
        }
        fsetdec.
      × intros x gx1 gx2 Hx1 Hx2.
        rewrite (H1 x gx1); auto. clear H1.
        rewrite get_map in Hx2.
        case_eq (get x g2); intros; rewrite H1 in Hx2; inversion Hx2; subst; clear Hx2.
        intros v1 v2 [e [Hedom' [Hxe Hv1v2]]].
        simpl in Hv1v2. destruct v2; try tauto.
        destruct Hv1v2 as [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]].
        simpl.
        apply (Hg x); auto. apply get_in_dom in H1. fsetdec.
      × rewrite H2. clear H2.
        intros v1 v2 [e [Hedom' [Hxe Hv1v2]]].
        simpl in Hv1v2. destruct v2; try tauto.
        destruct Hv1v2 as [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]].
        simpl.
        apply Hthis; auto.
  - inversion Habs; subst.
    + constructor.
    + simpl in Hsum. inversion Hsum; subst. clear Hsum. constructor.
      × rewrite dom_map.
        assert (S [=] dom g1).
        { assert (∃ e v, in_rel (RelSumR (concretize S (PRel g1 this1)) (concretize S Bottom)) e v)
            as [e' [v Hev]].
          { destruct (classic (∃ e v, in_rel (RelSumR (concretize S (PRel g1 this1)) (concretize S Bottom)) e v)); auto.
            exfalso. apply H. clear H. intros e' v Hev. apply H3. clear H3. eauto.
          }
          simpl in Hev. destruct v; tauto.
        }
        fsetdec.
      × intros x gx1 gx2 Hx1 Hx2.
        rewrite (H1 x gx1); auto. clear H1.
        rewrite get_map in Hx2.
        case_eq (get x g1); intros; rewrite H1 in Hx2; inversion Hx2; subst; clear Hx2.
        intros v1 v2 [e [Hedom' [Hxe Hv1v2]]].
        simpl in Hv1v2. destruct v2; try tauto.
        destruct Hv1v2 as [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]].
        simpl.
        apply (Hg x); auto. apply get_in_dom in H1. fsetdec.
      × rewrite H2. clear H2.
        intros v1 v2 [e [Hedom' [Hxe Hv1v2]]].
        simpl in Hv1v2. destruct v2; try tauto.
        destruct Hv1v2 as [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]].
        simpl.
        apply Hthis; auto.
  - inversion Habs; subst.
    + constructor.
    + simpl in Hsum.
      case_eq (map2 RelSumR g1 g2); intros; rewrite H3 in Hsum;
        inversion Hsum; subst; clear Hsum.
      constructor.
      × { assert (S [=] dom g1 ∨ S [=] dom g2) as [HS|HS].
          { assert (∃ e v, in_rel (RelSumR (concretize S (PRel g1 this1)) (concretize S (PRel g2 this2))) e v)
              as [e' [v Hev]].
            { destruct (classic (∃ e v, in_rel (RelSumR (concretize S (PRel g1 this1)) (concretize S (PRel g2 this2))) e v)); auto.
              exfalso. apply H. clear H. intros e' v Hev. apply H4. clear H4. eauto.
            }
            simpl in Hev. destruct v; tauto.
          }
          - apply map2_dom1 in H3.
            fsetdec.
          - apply map2_dom2 in H3.
            fsetdec.
        }
      × { intros x gx1 gx2 Hx1 Hx2.
          rewrite (H1 x gx1); auto. clear H1.
          assert (∃ g1x, get x g1 = Some g1x) as [g1x Hg1x].
          { case_eq (get x g1); intros; eauto.
            exfalso. apply get_in_dom in Hx2. apply get_notin_dom in H1.
            apply map2_dom1 in H3. fsetdec.
          }
          assert (∃ g2x, get x g2 = Some g2x) as [g2x Hg2x].
          { case_eq (get x g2); intros; eauto.
            exfalso. apply get_in_dom in Hx2. apply get_notin_dom in H1.
            apply map2_dom2 in H3. fsetdec.
          }
          assert (gx2 = RelSumR g1x g2x) by eauto using map2_get. subst.
          intros v1 v2 [e' [Hedom' [Hxe' Hv]]].
          simpl in Hv. destruct v2; try tauto.
          - destruct Hv as [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]].
            simpl.
            apply (Hg x); auto. apply get_in_dom in Hg1x. fsetdec.
          - destruct Hv as [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]].
            simpl.
            apply (Hg x); auto. apply get_in_dom in Hg2x. fsetdec.
        }
      × { rewrite H2. clear H2.
          intros v1 v2 [Hv1good [e' [He'dom Hv]]].
          simpl in Hv. destruct v2; try tauto.
          - destruct Hv as [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]].
            simpl.
            apply Hthis; auto.
          - destruct Hv as [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]].
            simpl.
            apply Hthis; auto.
        }
Qed.

Soundness of right-sided sum. This is bullet 5 of Lemma 5.4 of the ICFP'20 paper.
Lemma pRelSumR_soundness S pR1 pR2 pR12:
  pRelSumR pR1 pR2 pR12 →
  RelIncl (RelSumR (concretize S pR1) (concretize S pR2)) (concretize S pR12).
Proof.
  destruct (abstract_inhabited S (RelSumR (concretize S pR1) (concretize S pR2))) as [pR' H'].
  intro H.
  rewrite <- adjunction; eauto.
  split; auto with good_rel.
  split; auto with dom_rel.
  eapply pRelSumR_soundness0; eauto.
Qed.

Closure of name abstraction for pointwise relations

The closure of name abstraction is soundly abstracted by the identity. (auxiliary lemma)
Lemma RelClose_lambda_rel_soundness0 S x pR pR':
  x `notin` S →
  abstract S (RelClose S (lambda_rel x (concretize S pR))) pR' →
  prel_leq pR' pR.
Proof.
  intros Hx Habs.
  destruct pR as [| g this ].
  - simpl in Habs. inversion Habs; subst.
    + constructor.
    + exfalso. apply H. clear H.
      intros e v [y [Hy H]]. assumption.
  - inversion Habs; subst; constructor.
    + assert (S [=] dom g).
      { assert (∃ e v, in_rel (RelClose S (lambda_rel x (concretize S (PRel g this)))) e v)
          as [e' [v Hev]].
        { destruct (classic (∃ e v, in_rel (RelClose S (lambda_rel x (concretize S (PRel g this)))) e v)); auto.
          exfalso. apply H. clear H. intros e' v Hev. apply H3. clear H3. eauto.
        }
        simpl in Hev. destruct Hev as [y Hev]. tauto.
      }
      fsetdec.
    + intros y gy1 gy2 Hy1 Hy2.
      rewrite (H1 y gy1); auto. clear H1.
      intros v1 v2 [e [Hedom' [Hxe Hv1v2]]].
      simpl in Hv1v2.
      destruct Hv1v2 as [z [Hz [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]]]].
      assert (y `in` S ∧ y ≠ x ∧ y ≠ z) as [HyS [Hyx Hyz]].
      { apply get_in_dom in Hy2. split; [| split]; fsetdec. }
      assert (fv v1 [<=] empty) as Hfv_v1.
      { assert (good_value v1).
        { apply (all_env_get _ e y); auto.
          apply all_env_term_equivariant in Hegood; auto using good_value_equivariant.
        }
        eauto.
      }
      assert (fv v2 [<=] empty) as Hfv_v2.
      { apply good_value_equivariant in Hvgood. auto. }
      rewrite <- (transp_term_fresh_eq z x v1);
        [| rewrite Hfv_v1; fsetdec | rewrite Hfv_v1; fsetdec ].
      rewrite <- (transp_term_fresh_eq z x v2);
        [| rewrite Hfv_v2; fsetdec | rewrite Hfv_v2; fsetdec ].
      apply (Hg y); auto.
      apply (get_transp_env_term_Some_equivariant z x) in Hxe.
      rewrite <- (transp_atom_other z x y); auto.
    + rewrite H2. clear H2.
      intros v1 v2 [Hgoodv1 [e [Hedom' [y [Hy Hv1v2]]]]].
      destruct Hv1v2 as [Hegood [Hvgood [Hedom [Hgdom [Hg Hthis]]]]].
      assert (fv v2 [<=] empty) as Hfv_v2.
      { apply good_value_equivariant in Hvgood. auto. }
      rewrite <- (transp_term_fresh_eq y x v2);
        [| rewrite Hfv_v2; fsetdec | rewrite Hfv_v2; fsetdec ].
      apply Hthis; auto.
Qed.

The closure of name abstraction is soundly abstracted by the identity.
Lemma RelClose_lambda_rel_soundness S x pR:
  x `notin` S →
  RelIncl (RelClose S (lambda_rel x (concretize S pR))) (concretize S pR).
Proof.
  destruct (abstract_inhabited S (RelClose S (lambda_rel x (concretize S pR)))) as [pR' H'].
  intro H.
  rewrite <- adjunction; eauto.
  split; auto with good_rel.
  split; auto with dom_rel.
  eapply RelClose_lambda_rel_soundness0; eauto.
Qed.

The closure of name abstraction is completely abstracted by the identity.
Lemma RelClose_lambda_rel_completeness S x pR:
  x `notin` S →
  RelIncl (concretize S pR) (RelClose S (lambda_rel x (concretize S pR))).
Proof.
  intros Hx e v Hev.
  ∃ x. split; [ assumption |].
  simpl.
  rewrite transp_env_term_refl.
  rewrite transp_term_refl.
  assumption.
Qed.

The identity adequately abstract the closure of name abstraction.
Lemma RelClose_lambda_rel_adequacy S x pR:
  x `notin` S →
  RelEquiv (RelClose S (lambda_rel x (concretize S pR))) (concretize S pR).
Proof.
  intro Hx; apply RelIncl_antisym;
    auto using RelClose_lambda_rel_soundness, RelClose_lambda_rel_completeness.
Qed.

Let-binding

Let-binding of pointwise relations (auxiliary definition). This is on Figure 7 of the ICFP'20 paper.
Definition pRelLet0 x (pR1 pR2: @prel term term) : option (@prel term term) :=
  match pR1, pR2 with
  | Bottom, _ | _, Bottom ⇒ Some Bottom
  | PRel g1 this1, PRel g2 this2 ⇒
    match get x g2 with
    | Some g2x ⇒
      match map2 (fun r1 r2 ⇒ RelInter (RelCompose r1 g2x) r2) g1 (remove_all x g2) with
      | Some g ⇒ Some (PRel g (RelInter (RelCompose this1 g2x) this2))
      | None ⇒ None
      end
    | None ⇒ None
    end
  end.

Let-binding of pointwise relations
Definition pRelLet x (pR1 pR2 pR: @prel term term) : Prop :=
  pRelLet0 x pR1 pR2 = Some pR.

Soundness of the abstraction for an intermediate form of let-binding (auxiliary lemma).
Lemma RelCloseV_RelCompose_RelPush_soundness0 S x pR1 pR2 pR12 pR:
  pRelLet x pR1 pR2 pR12 →
  abstract S (RelCloseV (fun v ⇒ RelCompose (RelPush (concretize S pR1) x v) (concretize (add x S) pR2))) pR →
  prel_leq pR pR12.
Proof.
  intros HLet Habs. unfold pRelLet in HLet.
  destruct pR1 as [| g1 this1 ]; [| destruct pR2 as [| g2 this2 ]]; simpl in HLet.
  - simpl in Habs. inversion Habs; subst.
    + constructor.
    + exfalso. apply H. clear H.
      intros e v [v' [e' [[Heq H] Hev]]]. assumption.
  - inversion Habs; subst.
    + constructor.
    + exfalso. apply H. clear H. intros e v [v' Hev].
      simpl concretize in Hev. rewrite RelBot_absorbant_compose_right_equiv in Hev.
      assumption.
  - case_eq (get x g2); intros; rewrite H in HLet; try discriminate.
    case_eq (map2 (fun r1 r2 : rel term term ⇒ RelInter (RelCompose r1 r) r2) g1 (remove_all x g2)); intros; rewrite H0 in HLet; inversion HLet; subst; clear HLet.
    inversion Habs; subst; constructor.
    + assert (S [=] dom g1).
      { assert (∃ e v, in_rel
                         (RelCloseV
                            (fun v : term ⇒
                               RelCompose (RelPush (concretize S (PRel g1 this1)) x v)
                                          (concretize (add x S) (PRel g2 this2)))) e v)
          as [e' [v Hev]].
        { destruct (classic (∃ e v, in_rel
                                      (RelCloseV
                                         (fun v : term ⇒
                                            RelCompose (RelPush (concretize S (PRel g1 this1)) x v)
                                                       (concretize (add x S) (PRel g2 this2)))) e v)); auto.
          exfalso. apply H1. clear H1. intros e' v Hev. apply H5. clear H5. eauto.
        }
        simpl in Hev. destruct Hev as [t [y Hev]]. tauto.
      }
      apply map2_dom1 in H0. fsetdec.
    + intros y gy ey Hgy Hey.
      rewrite (H3 y gy); auto. clear H3.
      assert (∃ gy1, get y g1 = Some gy1) as [gy1 Hgy1].
      { case_eq (get y g1); intros; eauto.
        exfalso. apply get_in_dom in Hey. apply get_notin_dom in H3.
        apply map2_dom1 in H0. fsetdec.
      }
      assert (∃ gy2, get y (remove_all x g2) = Some gy2) as [gy2 Hgy2].
      { case_eq (get y (remove_all x g2)); intros; eauto.
        exfalso. apply get_in_dom in Hey. apply get_notin_dom in H3.
        apply map2_dom2 in H0. fsetdec.
      }
      assert (ey = RelInter (RelCompose gy1 r) gy2) by (eapply map2_get in H0; eauto).
      subst.
      intros v1 v2 [e' [He'dom [Hye' Hv1v2]]].
      simpl in Hv1v2.
      destruct Hv1v2 as [t [e'' [[Heq [Hegood1 [Hvgood1 [Hedom1 [Hgdom1 [Hg1 Hthis1]]]]]] [Hegood2 [Hvgood2 [Hedom2 [Hgdom2 [Hg2 Hthis2]]]]]]]].
      subst.
      split.
      × { ∃ t. split.
          - eapply Hg1; eauto. apply get_in_dom in Hgy1. fsetdec.
          - eapply Hg2; eauto. simpl. destruct (x == x); congruence.
        }
      × { eapply (Hg2 y); eauto.
          - apply get_in_dom in Hgy2. rewrite dom_remove_all in Hgy2. fsetdec.
          - simpl. destruct (y == x); subst; auto.
            exfalso. rewrite get_remove_all_this in Hgy2. discriminate.
          - rewrite get_remove_all_other in Hgy2; [ assumption |].
            intro Heq. subst. rewrite get_remove_all_this in Hgy2. discriminate.
        }
    + rewrite H4. clear H4.
      intros v1 v2 [e' [He'dom [Hye' Hv1v2]]].
      simpl in Hv1v2.
      destruct Hv1v2 as [t [e'' [[Heq [Hegood1 [Hvgood1 [Hedom1 [Hgdom1 [Hg1 Hthis1]]]]]] [Hegood2 [Hvgood2 [Hedom2 [Hgdom2 [Hg2 Hthis2]]]]]]]].
      subst. split.
      × { ∃ t. split.
          - apply Hthis1; auto.
          - apply (Hg2 x); auto. simpl. destruct (x == x); congruence.
        }
      × apply Hthis2; auto.
Qed.

Soundness of the abstraction for an intermediate form of let-binding.
Lemma RelCloseV_RelCompose_RelPush_soundness S x pR1 pR2 pR12:
  pRelLet x pR1 pR2 pR12 →
  RelIncl (RelCloseV (fun v ⇒ RelCompose (RelPush (concretize S pR1) x v) (concretize (add x S) pR2))) (concretize S pR12).
Proof.
  destruct (abstract_inhabited S (RelCloseV (fun v ⇒ RelCompose (RelPush (concretize S pR1) x v) (concretize (add x S) pR2)))) as [pR' H'].
  intro H.
  rewrite <- adjunction; eauto.
  split; auto with good_rel.
  split; auto with dom_rel.
  eapply RelCloseV_RelCompose_RelPush_soundness0; eauto.
Qed.

Soundness of the abstraction for let-binding. This is bullet 6 of Lemma 5.4 of the ICFP'20 paper.
Lemma pRelLet_soundness S x pR1 pR2 pR12:
  x `notin` S →
  pRelLet x pR1 pR2 pR12 →
  RelIncl (RelLet S x (concretize S pR1) (concretize (add x S) pR2)) (concretize S pR12).
Proof.
  intros Hx H.
  unfold RelLet.
  rewrite <- (RelClose_lambda_rel_soundness S x pR12 Hx).
  apply RelClose_incl. intros y Hy.
  apply lambda_rel_morphism_incl; auto.
  apply RelCloseV_RelCompose_RelPush_soundness; auto.
Qed.

Application of pointwise relations

Application combinator for binary relations on values. This is on Figure 8 of the ICFP'20 paper.
Definition APPv {A} (R1 R2: rel A term) : rel A term :=
  Rel _ _
      (fun v v' ⇒
         ∃ v1 v2,
           in_rel R1 v v1 ∧
           in_rel R2 v v2 ∧
           eval (App v1 v2) v'
      ).

Add Parametric Morphism A: (@APPv A)
    with signature RelIncl ++> RelIncl ++> RelIncl
      as APPv_morphism_incl.
Proof.
  intros R1 R2 H12 R3 R4 H34.
  intros v1 v2 [v3 [v4 [H [H' Happ]]]]. ∃ v3, v4. auto.
Qed.

Add Parametric Morphism A: (@APPv A)
    with signature RelEquiv ==> RelEquiv ==> RelEquiv
      as APPv_morphism_equiv.
Proof.
  intros R1 R2 H12 R3 R4 H34.
  apply RelIncl_antisym; apply APPv_morphism_incl; auto.
Qed.

Application of pointwise relations (auxiliary definition) This is on Figure 7 of the ICFP'20 paper.
Definition pRelApp0 {A} (pR1 pR2: @prel A term) : option (@prel A term) :=
  match pR1, pR2 with
  | Bottom, _ | _, Bottom ⇒ Some Bottom
  | PRel g1 this1, PRel g2 this2 ⇒
    match map2 APPv g1 g2 with
    | Some g ⇒ Some (PRel g (APPv this1 this2))
    | None ⇒ None
    end
  end.

Application of pointwise relations
Definition pRelApp {A} (pR1 pR2 pR: @prel A term) : Prop :=
  pRelApp0 pR1 pR2 = Some pR.

Soundness of the abstraction of application (auxiliary lemma)
Lemma pRelApp_soundness0 S pR1 pR2 pR' pR12 :
  abstract S (APP (concretize S pR1) (concretize S pR2)) pR' →
  pRelApp pR1 pR2 pR12 →
  prel_leq pR' pR12.
Proof.
  intros Habs Happ. unfold pRelApp in Happ.
  destruct pR1 as [| g1 this1]; [| destruct pR2 as [| g2 this2 ] ].
  - simpl in ×. rewrite RelBot_absorbant_app_left_equiv in Habs. inversion Habs; subst.
    + constructor.
    + exfalso. apply H. reflexivity.
  - simpl in ×. rewrite RelBot_absorbant_app_right_equiv in Habs. inversion Habs; subst.
    + constructor.
    + exfalso. apply H. reflexivity.
  - inversion Habs; subst.
    + constructor.
    + simpl in Happ.
      case_eq (map2 APPv g1 g2); intros; rewrite H3 in Happ;
        inversion Happ; subst; clear Happ.
      constructor.
      × { assert (S [=] dom g1) as HS.
          { assert (∃ e v, in_rel (APP (concretize S (PRel g1 this1)) (concretize S (PRel g2 this2))) e v)
              as [e' [v Hev]].
            { destruct (classic (∃ e v, in_rel (APP (concretize S (PRel g1 this1)) (concretize S (PRel g2 this2))) e v)); auto.
              exfalso. apply H. clear H. intros e' v Hev. apply H4. clear H4. eauto.
            }
            simpl in Hev. destruct Hev as [? [? [? ?]]]. tauto.
          }
          apply map2_dom1 in H3.
          fsetdec.
        }
      × { intros x gx1 gx2 Hx1 Hx2.
          rewrite (H1 x gx1); auto. clear H1.
          assert (∃ g1x, get x g1 = Some g1x) as [g1x Hg1x].
          { case_eq (get x g1); intros; eauto.
            exfalso. apply get_in_dom in Hx2. apply get_notin_dom in H1.
            apply map2_dom1 in H3. fsetdec.
          }
          assert (∃ g2x, get x g2 = Some g2x) as [g2x Hg2x].
          { case_eq (get x g2); intros; eauto.
            exfalso. apply get_in_dom in Hx2. apply get_notin_dom in H1.
            apply map2_dom2 in H3. fsetdec.
          }
          assert (gx2 = APPv g1x g2x) by eauto using map2_get. subst.
          intros v1 v2 [e' [He'dom [Hxe' Hv]]].
          simpl in Hv. destruct Hv as [e'' [v1' [v2' [Hleq [[Hgoode'' [Hgoodv1' [Hdome'' [Hdomg1 [Hg1 Hthis1]]]]] [[Hgoode''2 [Hgoodv2' [Hdome''2 [Hdomg2 [Hg2 Hthis2]]]]] Heval]]]]]].
          ∃ v1', v2'. split; [| split]; auto.
          - apply (Hg1 x); auto.
            + apply get_in_dom in Hg1x. fsetdec.
            + case_eq (get x e''); intros.
              × apply Hleq in H1. congruence.
              × exfalso. apply get_in_dom in Hg1x. apply get_notin_dom in H1. fsetdec.
          - apply (Hg2 x); auto.
            apply get_in_dom in Hg2x. fsetdec.
        }
      × { rewrite H2. clear H2.
          intros v1 v2 [Hv1good [e' [He'dom Hv]]].
          simpl in Hv. destruct Hv as [e'' [v1' [v2' [Hleq [[Hgoode'' [Hgoodv1' [Hdome'' [Hdomg1 [Hg1 Hthis1]]]]] [[Hgoode''2 [Hgoodv2' [Hdome''2 [Hdomg2 [Hg2 Hthis2]]]]] Heval]]]]]].
          ∃ v1', v2'. split; [| split].
          - apply Hthis1; auto.
          - apply Hthis2; auto.
          - assumption.
        }
Qed.

Soundness of the abstraction of application
Lemma pRelApp_soundness S pR1 pR2 pR12:
  pRelApp pR1 pR2 pR12 →
  RelIncl (APP (concretize S pR1) (concretize S pR2)) (concretize S pR12).
Proof.
  destruct (abstract_inhabited S (APP (concretize S pR1) (concretize S pR2))) as [pR' H'].
  intro H.
  rewrite <- adjunction; eauto.
  split; auto with good_rel.
  split; auto with dom_rel.
  eapply pRelApp_soundness0; eauto.
Qed.

Functions of pointwise relations

Right-sided function combinator for binary relations on values. This is on Figure 8 of the ICFP'20 paper.
Definition FUNvR (R1 R2 R3: rel term term) : rel term term :=
  Rel _ _
      (fun v f ⇒
         good_value v ∧
         good_value f ∧
         ∀ v1 v2, eval (App f v1) v2 →
                  in_rel R1 v v1 →
                  (in_rel R2 v1 v2 ∧ in_rel R3 v v2)
      ).

Add Parametric Morphism: FUNvR
    with signature RelIncl --> RelIncl ++> RelIncl ++> RelIncl
      as FUNvR_morphism_incl.
Proof.
  intros Arg1 Arg2 HArg Inner1 Inner2 HInner Outer1 Outer2 HOuter.
  intros f v [Hf [Hv H]]. split; [| split]; auto.
  intros v1 v2 Happ HArg2.
  rewrite <- HInner. rewrite <- HOuter.
  apply H; auto.
Qed.

Add Parametric Morphism: FUNvR
    with signature RelEquiv ==> RelEquiv ==> RelEquiv ==> RelEquiv
      as FUNvR_morphism_equiv.
Proof.
  intros Arg1 Arg2 HArg Inner1 Inner2 HInner Outer1 Outer2 HOuter.
  apply RelIncl_antisym; apply FUNvR_morphism_incl; unfold flip; auto.
Qed.

Lemma FUNvR_good R1 R2 R3:
  good_vrel (FUNvR R1 R2 R3).
Proof.
  intros v1 v2. simpl. tauto.
Qed.
Hint Resolve FUNvR_good: good_rel.

Left-sided function combinator for binary relations on values. This is on Figure 8 of the ICFP'20 paper.
Definition FUNvL (R1 R2 R3: rel term term) : rel term term :=
  Rel _ _
      (fun f v ⇒
         good_value f ∧
         good_value v ∧
         ∀ v1 v2, eval (App f v1) v2 →
                  in_rel R1 v1 v →
                  (in_rel R2 v1 v2 ∧ in_rel R3 v2 v)
      ).

Add Parametric Morphism: FUNvL
    with signature RelIncl --> RelIncl ++> RelIncl ++> RelIncl
      as FUNvL_morphism_incl.
Proof.
  intros Arg1 Arg2 HArg Inner1 Inner2 HInner Outer1 Outer2 HOuter.
  intros f v [Hf [Hv H]]. split; [| split]; auto.
  intros v1 v2 Happ HArg2.
  rewrite <- HInner. rewrite <- HOuter.
  apply H; auto.
Qed.

Add Parametric Morphism: FUNvL
    with signature RelEquiv ==> RelEquiv ==> RelEquiv ==> RelEquiv
      as FUNvL_morphism_equiv.
Proof.
  intros Arg1 Arg2 HArg Inner1 Inner2 HInner Outer1 Outer2 HOuter.
  apply RelIncl_antisym; apply FUNvL_morphism_incl; unfold flip; auto.
Qed.

Lemma FUNvL_good R1 R2 R3:
  good_vrel (FUNvL R1 R2 R3).
Proof.
  intros v1 v2. simpl. tauto.
Qed.
Hint Resolve FUNvL_good: good_rel.

Commutation lemma between converse and the right-sided function combinator.
Lemma RelInv_FUNvR R1 R2 R3:
  RelEquiv (RelInv (FUNvR R1 R2 R3))
           (FUNvL (RelInv R1) R2 (RelInv R3)).
Proof.
  intros f v. simpl. tauto.
Qed.

Commutation lemma between converse and the left-sided function combinator.
Lemma RelInv_FUNvL R1 R2 R3:
  RelEquiv (RelInv (FUNvL R1 R2 R3))
           (FUNvR (RelInv R1) R2 (RelInv R3)).
Proof.
  rewrite <- (RelInv_involution R1) at 1.
  rewrite <- (RelInv_involution R3) at 1.
  rewrite <- RelInv_FUNvR.
  apply RelInv_involution.
Qed.

Function that takes the intersection on the LHS of a pointwise relation.
Definition intersectL {A} S (g: env (rel term A)) (this: rel term A) (R: rel term A)
  : rel term A :=
  RelInter
    (Rel _ _ (fun v1 v2 ⇒ in_rel R v1 v2 → ∀ z, z `in` S → ∀ rz, get z g = Some rz → ∀ v, good_value v → in_rel rz v v2))
    (Rel _ _ (fun v1 v2 ⇒ in_rel R v1 v2 → ∀ v, good_value v → in_rel this v v2)).

Function combinator on pointwise relations (auxiliary definition). This is on Figure 7 of the ICFP'20 paper.
Definition pRelFun0 S x (pR1 pR2: @prel term term) : option prel :=
  match pR1, pR2 with
  | Bottom, _ ⇒
    Some (PRel (env_of_atoms (fun _ ⇒ FUNvR RelBot RelBot RelBot) S)
               (FUNvR RelBot RelBot RelBot)
         )
  | PRel g this, Bottom ⇒
    Some (PRel (mapi (fun y ry ⇒ FUNvR (RelInter (intersectL (remove y S) g this ry) ry) RelBot RelBot) g)
               (FUNvR (RelInter (intersectL S g this this) this) RelBot RelBot))
  | PRel g1 this1, PRel g2 this2 ⇒
    match get x g2 with
    | Some g2x ⇒
      match mapi2 (fun y ry1 ry2 ⇒
                     FUNvR (RelInter (intersectL (remove y S) g1 this1 ry1) ry1)
                             g2x
                             (RelInter (RelCompose ry1 g2x) ry2)
                  )
                  g1
                  (remove_all x g2)
      with
      | Some g ⇒
        Some (PRel g
                   (FUNvR (RelInter (intersectL S g1 this1 this1) this1)
                            g2x
                            (RelInter (RelCompose this1 g2x) this2)
                   )
             )
      | None ⇒ None
      end
    | None ⇒ None
    end
  end.

Function combinator on pointwise relations.
Definition pRelFun S x (pR1 pR2 pR: @prel term term) : Prop :=
  pRelFun0 S x pR1 pR2 = Some pR.

Soundness of the abstraction of the function combinator on relations. (auxiliary lemma)
Lemma pRelFun_soundness0 S x pR1 pR2 pR' pR12 :
  x `notin` S →
  good_prel S pR1 →
  abstract S (RelLam S x (concretize S pR1) (concretize (add x S) pR2)) pR' →
  pRelFun S x pR1 pR2 pR12 →
  prel_leq pR' pR12.
Proof.
  intros HxS HgoodpR1 Habs Hfun. unfold pRelFun in Hfun.
  destruct pR1 as [| g1 this1]; [| destruct pR2 as [| g2 this2 ] ].
  - simpl in ×. inversion Hfun; subst. clear Hfun.
    inversion Habs; subst.
    + constructor.
    + constructor.
      × rewrite env_of_atoms_dom. fsetdec.
      × { intros y gy gy' Hgy Hgy'.
          rewrite (H1 y); auto. clear H1.
          apply env_of_atoms_get_inv in Hgy'. subst gy'.
          intros v1 v2 Hv1v2.
          destruct Hv1v2 as [Hedom [e [Hedom' [Hey [Hegood [Hv2good Hrel]]]]]].
          split; [| split ].
          - eapply all_env_get in Hegood; eauto.
          - assumption.
          - simpl. tauto.
        }
      × rewrite H2. clear H2.
        intros v1 v2 [Hv1good [e [Hegood [Hv2good ?]]]]. simpl. tauto.
  - simpl in Hfun. inversion Hfun; subst. clear Hfun.
    inversion Habs; subst; constructor.
    + rewrite dom_mapi. simpl in HgoodpR1. destruct HgoodpR1 as [Heq _]. fsetdec.
    + intros y gy gy' Hgy Hgy'.
      rewrite (H1 y); auto. clear H1 H2.
      rewrite get_mapi in Hgy'.
      case_eq (get y g1); intros; rewrite H1 in Hgy'; inversion Hgy'; subst; clear Hgy'.
      intros v1 v2 [e [Hedom [Hey [Hedom' [Hegood [Hv2good Hfun]]]]]].
      split; [| split].
      × eapply all_env_get in Hegood; eauto.
      × assumption.
      × intros v3 v4 Heval [[Hgother Hthis] Hr].
        specialize (Hgother Hr). specialize (Hthis Hr).
        assert (in_rel (concretize S (PRel g1 this1)) e v3) as HpR1.
        { simpl in HgoodpR1. simpl.
          split; [| split; [| split; [| split; [| split]]]]; try tauto.
          - assert (good_vrel r).
            { eapply all_env_get; eauto. tauto. }
            eauto.
          - intros z vz gz Hz Hgetez Hgetg1z.
            destruct (z == y); subst.
            + congruence.
            + apply (Hgother z); auto. eapply all_env_get; eauto.
        }
        eapply Hfun in HpR1; eauto using leq_env_refl. clear Hfun.
        destruct HpR1 as [z [Hz [e' [Hpush Hbot]]]].
        simpl in Hbot. contradiction.
    + rewrite H2. clear H2.
      intros v1 v2 [Hv1good [e [Hedom [Hedom' [Hegood [Hv2good Hfun]]]]]].
      split; [| split].
      × assumption.
      × assumption.
      × { intros v3 v4 Happ [[Hg Hthis_other] Hthis].
          specialize (Hg Hthis). specialize (Hthis_other Hthis).
          assert (in_rel (concretize S (PRel g1 this1)) e v3) as HpR1.
          { simpl in HgoodpR1. simpl.
            split; [| split; [| split; [| split; [| split]]]]; try tauto.
            - assert (good_vrel this1) by tauto. eauto.
            - intros z vz gz Hz Hgetez Hgetg1z.
              apply (Hg z); auto.
              eapply all_env_get; eauto.
          }
          eapply Hfun in HpR1; eauto using leq_env_refl. clear Hfun.
          destruct HpR1 as [z [Hz [e' [Hpush Hbot]]]].
          simpl in Hbot. contradiction.
        }
  - simpl in Hfun. case_eq (get x g2); intros; rewrite H in Hfun; try discriminate.
    case_eq (mapi2
               (fun (y : atom) (ry1 ry2 : rel term term) ⇒
                  FUNvR (RelInter (intersectL (remove y S) g1 this1 ry1) ry1)
                          r
                          (RelInter (RelCompose ry1 r) ry2)
               )
               g1
               (remove_all x g2)); intros;
      rewrite H0 in Hfun; inversion Hfun; subst; clear Hfun.
    inversion Habs; subst.
    + constructor.
    + constructor.
      × assert (S [=] dom g1) as HS.
        { simpl in HgoodpR1. tauto. }
        apply mapi2_dom1 in H0.
        fsetdec.
      × { intros y gy gey Hgy Hey.
          rewrite (H3 y gy); auto. clear H3.
          assert (∃ g1y, get y g1 = Some g1y) as [g1y Hg1y].
          { case_eq (get y g1); intros; eauto.
            exfalso. apply get_in_dom in Hey. apply get_notin_dom in H3.
            apply mapi2_dom1 in H0. fsetdec.
          }
          assert (∃ g2y, get y g2 = Some g2y) as [g2y Hg2y].
          { case_eq (get y g2); intros; eauto.
            exfalso. apply get_in_dom in Hey. apply get_notin_dom in H3.
            apply mapi2_dom2 in H0. rewrite dom_remove_all in H0.
            fsetdec.
          }
          assert (gey = FUNvR (RelInter (intersectL (remove y S) g1 this1 g1y) g1y) r (RelInter (RelCompose g1y r) g2y)).
          { eapply mapi2_get in H0; eauto.
            rewrite get_remove_all_other; auto.
            assert (S [=] dom g1) by (simpl in HgoodpR1; tauto).
            apply get_in_dom in Hg1y.
            fsetdec.
          }
          subst gey.
          intros v1 v2 [e' [He'dom [Hye' [He''dom [He'good [Hv2good Hfun]]]]]].
          simpl.
          split; [| split].
          - eapply all_env_get; eauto.
          - assumption.
          - intros v3 v4 Happ [[Hgother Hthis] Hrel].
            specialize (Hgother Hrel). specialize (Hthis Hrel).
            assert (in_rel (concretize S (PRel g1 this1)) e' v3) as HpR1.
            { simpl in HgoodpR1. simpl.
              split; [| split; [| split; [| split; [| split]]]]; try tauto.
              - assert (good_vrel g1y).
                { eapply all_env_get; eauto. simpl in HgoodpR1. tauto. }
                eauto.
              - intros z vz gz Hz He'z Hg1z.
                destruct (z == y); subst.
                + congruence.
                + apply (Hgother z); auto.
                  eapply all_env_get; eauto.
            }
            eapply Hfun in HpR1; eauto using leq_env_refl.
            destruct HpR1 as [z [Hz [e'' [[Heq HpR1] HpR2]]]]. subst e''.
            destruct HpR2 as [He'good2 [Hv4good [Hdome' [Hdomg2 [Hg2 Hthis2]]]]].
            assert (fv v4 [<=] empty) as Hfv_v4.
            { apply good_value_equivariant in Hv4good. auto. }
            split; [| split].
            + rewrite <- (transp_term_fresh_eq z x v4);
                [| rewrite Hfv_v4; fsetdec | rewrite Hfv_v4; fsetdec ].
              apply (Hg2 x); auto.
            + ∃ v3. split.
              × assumption.
              × rewrite <- (transp_term_fresh_eq z x v4);
                  [| rewrite Hfv_v4; fsetdec | rewrite Hfv_v4; fsetdec ].
                apply (Hg2 x); auto.
            + rewrite <- (transp_term_fresh_eq z x v4);
                [| rewrite Hfv_v4; fsetdec | rewrite Hfv_v4; fsetdec ].
              apply (Hg2 y); auto.
              × apply get_in_dom in Hgy. fsetdec.
              × { simpl. destruct (y == x); subst.
                  - exfalso. apply get_in_dom in Hgy. fsetdec.
                  - rewrite <- (transp_atom_other z x y).
                    + rewrite <- get_transp_env_term_equivariant.
                      rewrite Hye'. simpl.
                      assert (fv v1 [<=] empty) as Hfv_v1.
                      { assert (good_value v1) by (eapply (all_env_get _ e'); eauto).
                        auto.
                      }
                      rewrite transp_term_fresh_eq;
                        [ reflexivity
                        | rewrite Hfv_v1; fsetdec | rewrite Hfv_v1; fsetdec ].
                    + apply get_in_dom in Hgy. fsetdec.
                    + congruence.
                }
        }
      × { rewrite H4. clear H4.
          intros v1 v2 [Hv1good [e' [He'dom Hv]]].
          destruct Hv as [He''dom [He'good [Hv2good Hfun]]].
          split; [| split].
          - assumption.
          - assumption.
          - intros v3 v4 Happ [[Hg1 Hthis1] Hrel].
            specialize (Hg1 Hrel). specialize (Hthis1 Hrel).
            simpl in HgoodpR1.
            assert (in_rel (concretize S (PRel g1 this1)) e' v3) as HpR1.
            { simpl.
              split; [| split; [| split; [| split; [| split]]]]; try tauto.
              - assert (good_vrel this1) by tauto. eauto.
              - intros y vy gy HyS Hye' Hyg1.
                apply (Hg1 y); auto.
                eapply (all_env_get _ e'); eauto.
            }
            eapply Hfun in HpR1; eauto using leq_env_refl. clear Hfun.
            destruct HpR1 as [z [Hz [e'' [[Heq HpR1] HpR2]]]]. subst e''.
            destruct HpR2 as [He'good2 [Hv4good [Hdome' [Hdomg2 [Hg2 Hthis2]]]]].
            assert (fv v4 [<=] empty) as Hfv_v4.
            { apply good_value_equivariant in Hv4good. auto. }
            simpl. split; [| split].
            + rewrite <- (transp_term_fresh_eq z x v4);
                [| rewrite Hfv_v4; fsetdec | rewrite Hfv_v4; fsetdec ].
              apply (Hg2 x); auto.
            + ∃ v3. split.
              × assumption.
              × rewrite <- (transp_term_fresh_eq z x v4);
                  [| rewrite Hfv_v4; fsetdec | rewrite Hfv_v4; fsetdec ].
                apply (Hg2 x); auto.
            + rewrite <- (transp_term_fresh_eq z x v4);
                [| rewrite Hfv_v4; fsetdec | rewrite Hfv_v4; fsetdec ].
              apply Hthis2; auto.
        }
Qed.

Soundness of the abstraction of the function combinator on relations.
Lemma pRelFun_soundness S x pR1 pR2 pR12:
  x `notin` S →
  good_prel S pR1 →
  pRelFun S x pR1 pR2 pR12 →
  RelIncl (RelLam S x (concretize S pR1) (concretize (add x S) pR2)) (concretize S pR12).
Proof.
  destruct (abstract_inhabited S (RelLam S x (concretize S pR1) (concretize (add x S) pR2))) as [pR' H'].
  intros Hx Hgood H.
  rewrite <- adjunction; eauto.
  split; auto with good_rel.
  split; auto with dom_rel.
  eapply pRelFun_soundness0; eauto.
Qed.

Self pointwise relation

The pointwise relation self combinator of some variable, for a given domain. This is on Figure 7 of the ICFP'20 paper.
Definition pRelSelf S x : prel :=
  PRel (env_of_atoms (fun y ⇒ if y == x then RelEqVal else RelTopVal) S) RelTopVal.

Soundness of the abstraction of of the self of a variable.
Lemma pRelSelf_soundness0 S x pR :
  abstract S (RelSelf (Var x)) pR →
  prel_leq pR (pRelSelf S x).
Proof.
  intros Habs. unfold pRelSelf.
  inversion Habs; subst.
  - constructor.
  - constructor.
    + rewrite env_of_atoms_dom. fsetdec.
    + intros y gy gy' Hgetgy Hgetgy'.
      assert (y `in` S) as Hy by (apply get_in_dom in Hgetgy; fsetdec).
      rewrite env_of_atoms_get in Hgetgy'; [| assumption ].
      inversion Hgetgy'; subst; clear Hgetgy'.
      rewrite (H1 y); auto. clear H1.
      intros v1 v2 [e [Hedom [Hgetey [Hgetex [Hxe [Hegood Hv2good]]]]]].
      simpl in Hxe.
      case_eq (get x e); intros.
      × { assert (good_value t) by (eapply all_env_get; eauto).
          assert (fv t [<=] empty) as Hfv_t by eauto.
          rewrite subst_env_Var_Some with (t := t) in Hgetex; auto.
          subst t.
          assert (good_value v1) by (eapply all_env_get; eauto).
          destruct (y == x); subst; split; auto.
          congruence.
        }
      × exfalso. apply get_notin_dom in H1. fsetdec.
    + rewrite H2. clear H2.
      intros v1 v2 [Hgoodv1 [e [Hedom [Hgetex [Hxedom [Hegood Hv2good]]]]]].
      simpl in Hxedom.
      case_eq (get x e); intros.
      × { assert (good_value t) by (eapply all_env_get; eauto).
          assert (fv t [<=] empty) as Hfv_t by eauto.
          rewrite subst_env_Var_Some with (t := t) in Hgetex; auto.
          subst t.
          split; assumption.
        }
      × exfalso. apply get_notin_dom in H2. fsetdec.
Qed.

Gather of pointwise relations

Gather (auxiliary definition).
Definition def_gather0 {A} (g: env (rel term A)) (this: rel term A) :=
  fold_right
    (fun p racc ⇒
       match p with
       | (z, rz) ⇒ RelInter (RelCompose (RelInv rz) RelTopVal) racc
       end)
    (RelInv this)
    g.

Gather (other auxiliary definition).
Definition def_gather1 (E: env (@prel term term)) x : rel term term :=
  fold_right
    (fun p acc ⇒
       match p with
       | (y, Bottom) ⇒ RelBot
       | (y, PRel gy thisy) ⇒
         if x == y
         then RelInter (def_gather0 gy thisy) acc
         else
           match get x gy with
           | Some gyx ⇒ RelInter (RelCompose gyx RelTopVal) acc
           | None ⇒ acc
           end
       end)
    RelTopVal
    E.

Gather on pointwise relations. This is on Figure 7 of the ICFP'20 paper.
Definition pRelGather (E: env (@prel term term)) : @prel term term :=
  PRel (mapi (fun x _ ⇒ def_gather1 E x) E) RelTopVal.

Equivalent formulation of def_gather0.
Lemma def_gather0_rewrite g this :
  uniq g →
  all_env good_vrel g →
  good_vrel this →
  RelEquiv
    (def_gather0 g this)
    (Rel _ _
         (fun a v ⇒
            (∀ x rx, get x g = Some rx → ∃ v', in_rel rx v' a) ∧ in_rel this v a
         )
    ).
Proof.
  intros Huniq Hggood Hthisgood.
  unfold def_gather0. env induction g; simpl.
  - intros v1 v2. split; intro H; simpl in ×.
    + split; [| assumption].
      intros; discriminate.
    + tauto.
  - intros v1 v2. split; intro H; simpl in ×.
    + destruct H as [HTopVal Hfold].
      rewrite IHg in Hfold; try tauto. clear IHg. simpl in Hfold.
      destruct Hfold as [Hg Hthis].
      split; try tauto.
      intros y ry Hget. destruct (y == x); subst.
      × inversion Hget; subst; clear Hget. firstorder.
      × eauto.
      × solve_uniq.
    + destruct H as [Hg Hthis]. split.
      × { specialize (Hg x a). destruct (x == x); [| contradiction ].
          specialize (Hg eq_refl). destruct Hg as [v' Hv'].
          ∃ v'. split; [| split]; auto.
          - assert (good_vrel a) by tauto. eauto.
          - eauto.
        }
      × { rewrite IHg; [ split; [| tauto] | solve_uniq | tauto ].
          intros y ry Hget.
          specialize (Hg y ry). destruct (y == x); subst.
          - exfalso. apply get_in_dom in Hget. solve_uniq.
          - specialize (Hg Hget). assumption.
        }
Qed.

Equivalent formulation of def_gather1.
Lemma def_gather1_rewrite x E :
  all_env good_prel0 E →
  uniq E →
  RelEquiv
    (def_gather1 E x)
    (Rel _ _
         (fun v1 v2 ⇒
            good_value v1 ∧
            good_value v2 ∧
            (∀ y, get y E = Some Bottom → False) ∧
            (∀ y gy thisy, get y E = Some (PRel gy thisy) →
                           if x == y
                           then in_rel (def_gather0 gy thisy) v1 v2
                           else ∀ gyx, get x gy = Some gyx →
                                       ∃ v', in_rel gyx v1 v'
            )
    )).
Proof.
  intros Hgood Huniq.
  unfold def_gather1. env induction E.
  - intros v1 v2. split; intro H; simpl in ×.
    + split; [| split; [| split ] ]; try tauto; try congruence.
    + tauto.
  - intros v1 v2; split; intro H.
    + simpl. simpl in H. destruct a as [| g this ]; [ contradiction |].
      destruct (x == x0); subst.
      × { destruct H as [Hlhs Hfold].
          rewrite IHE in Hfold; [| simpl in Hgood; tauto | solve_uniq]. clear IHE.
          simpl in_rel in Hlhs.
          destruct Hfold as [Hgood1 [Hgood2 [Hbot H]]].
          split; [| split; [| split]]; auto.
          - intros y Hget. destruct (y == x0); subst.
            + exfalso. congruence.
            + apply Hbot in Hget. assumption.
          - intros y gy thisy Hget. destruct (y == x0); subst.
            + inversion Hget; subst; clear Hget.
              destruct (x0 == x0); [| contradiction ].
              assumption.
            + apply H in Hget.
              destruct (x0 == y); subst; [ contradiction |].
              assumption.
        }
      × { case_eq (get x g); intros; rewrite H0 in H.
          - destruct H as [Hr Hfold].
            rewrite IHE in Hfold; [| simpl in Hgood; tauto |solve_uniq]. clear IHE.
            destruct Hfold as [Hgood1 [Hgood2 [Hbot H]]].
            split; [| split; [| split]]; auto.
            + intros y Hget. destruct (y == x0); subst.
              × exfalso. congruence.
              × apply Hbot in Hget. assumption.
            + intros y gy thisy Hget. destruct (y == x0); subst.
              × inversion Hget; subst; clear Hget.
                destruct (x == x0); subst; [ contradiction |].
                intros gyx Hget. assert (gyx = r) by congruence. subst gyx.
                destruct Hr as [v' [Hr ?]]. ∃ v'. assumption.
              × apply H in Hget. assumption.
          - rewrite IHE in H; [| simpl in Hgood; tauto | solve_uniq ]. clear IHE.
            destruct H as [Hgood1 [Hgood2 [Hbot H]]].
            split; [| split; [| split ] ]; auto.
            + intros y Hget. destruct (y == x0); subst.
              × exfalso. congruence.
              × apply Hbot in Hget. assumption.
            + intros y gy thisy Hget.
              destruct (y == x0); subst.
              × inversion Hget; subst; clear Hget.
                destruct (x == x0); subst; [ contradiction |].
                intros gyx Hget. exfalso. congruence.
              × apply H in Hget. assumption.
        }
    + destruct H as [Hgood1 [Hgood2 [Hbot H]]].
      simpl. destruct a as [| g this ].
      × apply (Hbot x0). simpl. destruct (x0 == x0); congruence.
      × { destruct (x == x0); subst.
          - split.
            + specialize (H x0 g this).
              simpl in H. destruct (x0 == x0); subst; [| contradiction ].
              specialize (H eq_refl). assumption.
            + rewrite IHE; [| simpl in Hgood; tauto | solve_uniq ].
              split; [| split; [| split ] ]; auto.
              × { intros y Hget. apply (Hbot y).
                  simpl. destruct (y == x0); subst.
                  - exfalso. apply get_in_dom in Hget. solve_uniq.
                  - assumption.
                }
              × { intros y gy thisy Hget.
                  destruct (x0 == y); subst.
                  - exfalso. apply get_in_dom in Hget. solve_uniq.
                  - specialize (H y gy thisy). simpl in H.
                    destruct (y == x0); [ congruence |].
                    specialize (H Hget). destruct (x0 == y); [ congruence |].
                    assumption.
                }
          - case_eq (get x g); intros.
            + split.
              × specialize (H x0 g this). simpl in H.
                destruct (x0 == x0); [| contradiction].
                specialize (H eq_refl).
                destruct (x == x0); subst; [contradiction |].
                assert (good_vrel r) by (simpl in Hgood; eapply all_env_get; eauto; tauto).
                apply H in H0. destruct H0 as [v' Hr].
                ∃ v'. split; [| split]; auto. eauto.
              × { rewrite IHE; [| simpl in Hgood; tauto | solve_uniq ].
                  split; [| split; [| split]]; auto.
                  - intros y Hy. apply (Hbot y). simpl.
                    destruct (y == x0); subst; auto.
                    exfalso. apply get_in_dom in Hy. solve_uniq.
                  - intros y gy thisy Hy.
                    specialize (H y gy thisy).
                    simpl in H. destruct (y == x0); subst.
                    + exfalso. apply get_in_dom in Hy. solve_uniq.
                    + specialize (H Hy). assumption.
                }
            + rewrite IHE; [| simpl in Hgood; tauto | solve_uniq ].
              split; [| split; [| split]]; auto.
              × intros y Hy. apply (Hbot y). simpl.
                destruct (y == x0); subst; auto.
                exfalso. apply get_in_dom in Hy. solve_uniq.
              × { intros y gy thisy Hy.
                  specialize (H y gy thisy).
                  simpl in H. destruct (y == x0); subst.
                  - exfalso. apply get_in_dom in Hy. solve_uniq.
                  - specialize (H Hy). assumption.
                }
        }
Qed.

Soundness of the abstraction of gather (auxiliary lemma).
Lemma pRelGather_soundness0 E pR :
  uniq E →
  wf_prel_env E →
  abstract (dom E) (RelGather (concretize_env E)) pR →
  prel_leq pR (pRelGather E).
Proof.
  intros Huniq Hwf Habs. unfold pRelGather.
  inversion Habs; subst.
  - constructor.
  - constructor.
    + rewrite dom_mapi. fsetdec.
    + intros x gx gx' Hgetgx Hgetgx'.
      rewrite get_mapi in Hgetgx'.
      case_eq (get x E); intros; rewrite H3 in Hgetgx'; inversion Hgetgx'; subst; clear Hgetgx'.
      rewrite def_gather1_rewrite; auto.
      rewrite (H1 x); auto. clear H1 H2.
      intros v1 v2 [e [Hedom [Hgetex Hrel]]].
      destruct Hrel as [Hegood [Hv2good Hrel]].
      split; [| split; [| split ] ].
      × eapply all_env_get; eauto.
      × assumption.
      × intros y HgetEy. apply H. clear H. intros e' v' [He'good [Hv'good H']].
        simpl.
        assert (∃ Ry, get y (concretize_env E) = Some Ry) as [Ry Hget].
        { case_eq (get y (concretize_env E)); intros; eauto.
          exfalso. apply get_notin_dom in H. apply get_in_dom in HgetEy.
          rewrite concretize_env_dom in H.
          contradiction.
        }
        pose proof (get_decompose_env E y Bottom) as [H'' _].
        specialize (H'' HgetEy).
        destruct H'' as [E1 [E2 [Heq Hy]]]. subst.
        specialize (H' _ _ Hget).
        destruct H' as [v'' [Hget'' HR]].
        apply concretize_env_spec in Hget; auto.
        rewrite Hget in HR. simpl in HR. assumption.
      × { intros y gy thisy HgetEy.
          pose proof (get_decompose_env E y (PRel gy thisy)) as [H' _].
          specialize (H' HgetEy).
          destruct H' as [E1 [E2 [Heq Hy]]].
          assert (good_prel (dom E2) (PRel gy thisy)) as Hgood.
          { subst. eapply wf_prel_env_spec; eauto. }
          simpl in Hgood. destruct Hgood as [Hdomgy [Huniqgy [Hgoodgy Hgoodthisy]]].
          assert (∃ Ry, get y (concretize_env E) = Some Ry) as [Ry Hget].
          { case_eq (get y (concretize_env E)); intros; eauto.
            exfalso. apply get_notin_dom in H1. rewrite concretize_env_dom in H1.
            apply get_in_dom in HgetEy. contradiction.
          }
          assert (RelEquiv Ry (concretize (dom E2) (PRel gy thisy))) as Hequiv.
          { subst E. eapply concretize_env_spec; eauto. }
          specialize (Hrel _ _ Hget). destruct Hrel as [v' [Hgetex' HR]].
          rewrite Hequiv in HR. clear Hequiv. simpl in HR.
          destruct HR as [He'good [Hv1good [He'dom [Hgydom [Hgy Hthisy]]]]].
          destruct (x == y); [subst y|].
          - rewrite def_gather0_rewrite; auto.
            assert (v1 = v') by congruence. subst v'. clear Hgetex'.
            split.
            + intros z rz Hgetzgy.
              assert (∃ v', get z e = Some v') as [v' Hgetez].
              { case_eq (get z e); intros; eauto.
                exfalso. apply get_in_dom in Hgetzgy. apply get_notin_dom in H1. fsetdec.
              }
              ∃ v'. apply (Hgy z); auto.
              apply get_in_dom in Hgetzgy. fsetdec.
            + apply Hthisy; auto.
          - intros gyx Hgetgyx. ∃ v'. apply (Hgy x); auto.
            apply get_in_dom in Hgetgyx. fsetdec.
        }
    + rewrite H2. clear H1 H2.
      intros v1 v2 [Hv1good [e [Hedom Hrel]]].
      split; [assumption |].
      assert (good_rel (RelGather (concretize_env E))) by auto with good_rel.
      eauto.
Qed.

Soundness of the abstraction of gather.
Lemma pRelGather_soundness E:
  uniq E →
  wf_prel_env E →
  RelIncl (RelGather (concretize_env E)) (concretize (dom E) (pRelGather E)).
Proof.
  intros Huniq Hwf.
  destruct (abstract_inhabited (dom E) (RelGather (concretize_env E))) as [pR' H'].
  rewrite <- adjunction; eauto.
  split; auto with good_rel.
  split.
  - rewrite <- (concretize_env_dom E).
    apply RelGather_dom_rel.
  - eapply pRelGather_soundness0; eauto.
Qed.