Coral.Corr: the correlation abstract domain

Author: Benoît Montagu
Copyright © Inria 2020 CeCILL-B License
Synopsis: Definition, specification and correctness proofs of the correlation abstract domain and its operations. Correlations are abstract binary relations over typed values of the lambda-calculus extended with pairs and sums. This version supports higher-order values.

Require Import Infrastructure.
Require Import Rel.
Require Import PointwiseRel.
Require Import RelGood.
Require Import Types.
Require Import Lia.
Require Import EvalFacts.

Sides

The side of a correlation: left-hand side, or right-hand side.
Inductive side : Type := L | R.

flip_side one side for the other.
Definition flip_side (s: side) : side :=
  match s with
  | L ⇒ R
  | R ⇒ L
  end.

Decidable equality for the type side.
Definition side_eq_dec (s1 s2: side): { s1 = s2 } + { s1 ≠ s2 }.
  decide equality.
Defined.

flip_side is an involution.
Lemma flip_side_involution s:
  flip_side (flip_side s) = s.
Proof.
  destruct s; reflexivity.
Qed.

As a consequence, flip_side is injective.
Lemma flip_side_injective s1 s2:
  flip_side s1 = flip_side s2 →
  s1 = s2.
Proof.
  intro H. rewrite <- (flip_side_involution s1).
  rewrite H. apply flip_side_involution.
Qed.

The abstract domain of correlations

Definition of the type of correlations. This the definition in Section 5.2 on page 18 of the ICFP'20 paper.
Inductive corr: Type :=
| CTop
Full relation
| CBot
Empty relation
| CEq
Identity relation
| CPair (s: side) (c1 c2: corr)
Side-indexed pair combinator
| CSum (s: side) (c1 c2: corr)
Side-indexed sum combinator
| CFun (s: side) (carg cinner couter: corr)
Side-indexed function combinator
.

wf_corr c ty1 ty2 holds when the correlation c is assigned type ty1 × ty2, i.e. when it relates values of type ty1 on the left-hand side with values of type ty2 on the right-hand side. This is the Figure 10 of the ICFP'20 paper.
Fixpoint wf_corr (c: corr) (ty1 ty2: ty) : Prop :=
  match c with
  | CTop | CBot ⇒ True
  | CEq ⇒ ty1 = ty2
  | CPair L c1 c2 ⇒
    match ty1 with
    | TPair ty1L ty1R ⇒
      wf_corr c1 ty1L ty2 ∧ wf_corr c2 ty1R ty2
    | _ ⇒ False
    end
  | CPair R c1 c2 ⇒
    match ty2 with
    | TPair ty2L ty2R ⇒
      wf_corr c1 ty1 ty2L ∧ wf_corr c2 ty1 ty2R
    | _ ⇒ False
    end
  | CSum L c1 c2 ⇒
    match ty1 with
    | TSum ty1L ty1R ⇒
      wf_corr c1 ty1L ty2 ∧ wf_corr c2 ty1R ty2
    | _ ⇒ False
    end
  | CSum R c1 c2 ⇒
    match ty2 with
    | TSum ty2L ty2R ⇒
      wf_corr c1 ty1 ty2L ∧ wf_corr c2 ty1 ty2R
    | _ ⇒ False
    end
  | CFun L carg cinner couter ⇒
    match ty1 with
    | TFun ty1L ty1R ⇒
      wf_corr carg ty1L ty2 ∧ wf_corr cinner ty1L ty1R ∧ wf_corr couter ty1R ty2
    | _ ⇒ False
    end
  | CFun R carg cinner couter ⇒
    match ty2 with
    | TFun ty2L ty2R ⇒
      wf_corr carg ty1 ty2L ∧ wf_corr cinner ty2L ty2R ∧ wf_corr couter ty1 ty2R
    | _ ⇒ False
    end
  end.

Concretization function for correlations: concretize_corr ty1 ty2 c is a binary relation over terms of type ty1 on the left-hand side and terms ty2 on the right-hand side. This is the Figure 9 of the ICFP'20 paper.
Fixpoint concretize_corr (ty1 ty2: ty) (c: corr) : rel term term :=
  match c with
  | CTop ⇒ RelInter RelTopVal (RelTyped ty1 ty2)
  | CBot ⇒ RelBot
  | CEq ⇒
    if ty_eq_dec ty1 ty2
    then RelInter RelEqVal (RelTyped ty1 ty2)
    else RelBot
  | CPair L c1 c2 ⇒
    match ty1 with
    | TPair ty1L ty1R ⇒
      RelPairL (concretize_corr ty1L ty2 c1) (concretize_corr ty1R ty2 c2)
    | _ ⇒
      RelBot
    end
  | CPair R c1 c2 ⇒
    match ty2 with
    | TPair ty2L ty2R ⇒
      RelPairR (concretize_corr ty1 ty2L c1) (concretize_corr ty1 ty2R c2)
    | _ ⇒
      RelBot
    end
  | CSum L c1 c2 ⇒
    match ty1 with
    | TSum ty1L ty1R ⇒
      RelSumL (concretize_corr ty1L ty2 c1) (concretize_corr ty1R ty2 c2)
    | _ ⇒
      RelBot
    end
  | CSum R c1 c2 ⇒
    match ty2 with
    | TSum ty2L ty2R ⇒
      RelSumR (concretize_corr ty1 ty2L c1) (concretize_corr ty1 ty2R c2)
    | _ ⇒
      RelBot
    end
  | CFun L carg cinner couter ⇒
    match ty1 with
    | TFun ty1L ty1R ⇒
      RelInter
        (FUNvL (concretize_corr ty1L ty2 carg)
               (concretize_corr ty1L ty1R cinner)
               (concretize_corr ty1R ty2 couter)
        )
        (RelTyped ty1 ty2)
    | _ ⇒
      RelBot
    end
  | CFun R carg cinner couter ⇒
    match ty2 with
    | TFun ty2L ty2R ⇒
      RelInter
        (FUNvR (concretize_corr ty1 ty2L carg)
               (concretize_corr ty2L ty2R cinner)
               (concretize_corr ty1 ty2R couter)
        )
        (RelTyped ty1 ty2)
    | _ ⇒
      RelBot
    end
  end.

concretize_corr always creates a good relation, i.e. a relation over closed values.
Lemma concretize_corr_good ty1 ty2 c:
  good_vrel (concretize_corr ty1 ty2 c).
Proof.
  revert ty1 ty2.
  induction c; intros; simpl;
    auto with good_rel;
    try solve [ destruct s; [ destruct ty1 | destruct ty2 ]; auto with good_rel ].
  destruct (ty_eq_dec ty1 ty2); auto with good_rel.
Qed.
Hint Resolve concretize_corr_good: good_rel.

concretize_corr is always below RelTopVal, the full relation over values.
Lemma concretize_corr_below_top ty1 ty2 c:
  RelIncl (concretize_corr ty1 ty2 c) RelTopVal.
Proof.
  intros v1 v2 H. apply concretize_corr_good in H. assumption.
Qed.

concretize_corr ty1 ty2 c is always below RelTyped ty1 ty2, the full relation over typed values with types ty1 on the LHS and ty2 on the RHS.
Lemma concretize_corr_typed ty1 ty2 c:
  RelIncl (concretize_corr ty1 ty2 c) (RelTyped ty1 ty2).
Proof.
  revert ty1 ty2. induction c; intros; simpl.
  - apply RelInter_lb2.
  - apply RelBot_bot.
  - destruct (ty_eq_dec ty1 ty2); [| apply RelBot_bot ].
    apply RelInter_lb2.
  - destruct s; [ destruct ty1 | destruct ty2 ]; try solve [ apply RelBot_bot ].
    + intros v1 v2 H. destruct v1; simpl in H; try contradiction.
      destruct H as [H1 H2].
      apply IHc1 in H1. destruct H1 as [H11 H12].
      apply IHc2 in H2. destruct H2 as [H21 H22].
      split; auto.
      constructor; auto.
    + intros v1 v2 H. destruct v2; simpl in H; try contradiction.
      destruct H as [H1 H2].
      apply IHc1 in H1. destruct H1 as [H11 H12].
      apply IHc2 in H2. destruct H2 as [H21 H22].
      split; auto.
      constructor; auto.
  - destruct s; [ destruct ty1 | destruct ty2 ]; try solve [ apply RelBot_bot ].
    + intros v1 v2 H. destruct v1; simpl in H; try contradiction.
      × apply IHc1 in H. destruct H as [H1 H2]. split; auto. constructor; auto.
      × apply IHc2 in H. destruct H as [H1 H2]. split; auto. constructor; auto.
    + intros v1 v2 H. destruct v2; simpl in H; try contradiction.
      × apply IHc1 in H. destruct H as [H1 H2]. split; auto. constructor; auto.
      × apply IHc2 in H. destruct H as [H1 H2]. split; auto. constructor; auto.
  - destruct s; [ destruct ty1 | destruct ty2 ]; try solve [ apply RelBot_bot ].
    + apply RelInter_lb2.
    + apply RelInter_lb2.
Qed.

Flip

flip_corr c returns the converse correlation, i.e. where all the sides were flipped. This is Figure 18 of the ICFP'20 paper.
Fixpoint flip_corr (c: corr) : corr :=
  match c with
  | CTop as c | CBot as c | CEq as c ⇒ c
  | CPair s c1 c2 ⇒ CPair (flip_side s) (flip_corr c1) (flip_corr c2)
  | CSum s c1 c2 ⇒ CSum (flip_side s) (flip_corr c1) (flip_corr c2)
  | CFun s carg cinner couter ⇒ CFun (flip_side s) (flip_corr carg) cinner (flip_corr couter)
  end.

flip_corr is an involution.
Lemma flip_corr_involution c:
  flip_corr (flip_corr c) = c.
Proof.
  induction c; simpl in *; auto.
  - rewrite flip_side_involution. congruence.
  - rewrite flip_side_involution. congruence.
  - rewrite flip_side_involution. congruence.
Qed.

As a consequence, flip_corr is injective.
Lemma flip_corr_injective c1 c2:
  flip_corr c1 = flip_corr c2 →
  c1 = c2.
Proof.
  intro H. rewrite <- (flip_corr_involution c1).
  rewrite H. apply flip_corr_involution.
Qed.

The concretization of corr_flip c is the converse of the concretization of c.
Lemma concretize_corr_flip ty1 ty2 c:
  RelEquiv (concretize_corr ty2 ty1 (flip_corr c)) (RelInv (concretize_corr ty1 ty2 c)).
Proof.
  revert ty1 ty2.
  induction c; intros; simpl.
  - rewrite RelInv_RelInter. rewrite RelInv_RelTopVal. rewrite RelInv_RelTyped.
    reflexivity.
  - rewrite RelInv_RelBot. reflexivity.
  - destruct (ty_eq_dec ty2 ty1); destruct (ty_eq_dec ty1 ty2); try congruence.
    + subst. rewrite RelInv_RelInter.
      rewrite RelInv_RelEqVal. rewrite RelInv_RelTyped. reflexivity.
    + rewrite RelInv_RelBot. reflexivity.
  - destruct s; simpl; [ destruct ty1 | destruct ty2 ]; try reflexivity.
    + rewrite IHc1. rewrite IHc2.
      rewrite RelInv_RelPairL. reflexivity.
    + rewrite IHc1. rewrite IHc2.
      rewrite RelInv_RelPairR. reflexivity.
  - destruct s; simpl; [ destruct ty1 | destruct ty2 ]; try reflexivity.
    + rewrite IHc1. rewrite IHc2.
      rewrite RelInv_RelSumL. reflexivity.
    + rewrite IHc1. rewrite IHc2.
      rewrite RelInv_RelSumR. reflexivity.
  - destruct s; simpl; [ destruct ty1 | destruct ty2 ]; try reflexivity.
    + rewrite RelInv_RelInter. rewrite RelInv_RelTyped.
      rewrite IHc1. rewrite IHc3. rewrite RelInv_FUNvL. reflexivity.
    + rewrite RelInv_RelInter. rewrite RelInv_RelTyped.
      rewrite IHc1. rewrite IHc3. rewrite RelInv_FUNvR. reflexivity.
Qed.

flip_corr flips the types of values.
Lemma flip_corr_wf ty1 ty2 c:
  wf_corr c ty1 ty2 →
  wf_corr (flip_corr c) ty2 ty1.
Proof.
  revert ty1 ty2.
  induction c; intros ty1 ty2 Hwf; simpl in *; auto;
    try solve [ destruct s; simpl; [destruct ty1 | destruct ty2]; intuition auto ].
Qed.

Convenience function that tests whether a correlation is equal to CTop.
Definition is_top (c: corr) : { c = CTop } + { c ≠ CTop }.
Proof.
  destruct c.
  - left. reflexivity.
  - right. discriminate.
  - right. discriminate.
  - right. discriminate.
  - right. discriminate.
  - right. discriminate.
Defined.

Projection

An index is either One or Two. Indices are used to refer to the first or second projection of a pair, or the first or second case of a binary tagged sum.
Inductive index: Type := One | Two.

Projection on pairs

proj_pair strong s i c projects the correlation c on the component index of a pair on its side s. The boolean strong controls whether one should try to be more precise, at the cost of a loss of monotonicity. This is the Figure 12 of the ICFP'20 paper.
Fixpoint proj_pair (strong:bool) (s: side) (i: index) (c: corr): corr :=
  match c with
  | CTop as c | CBot as c ⇒ c
  | CEq ⇒
    match i with
    | One ⇒ CPair (flip_side s) CEq CTop
    | Two ⇒ CPair (flip_side s) CTop CEq
    end
  | CSum s' c1 c2 ⇒
    if side_eq_dec s s'
    then
      if strong
      then CBot
      else CTop
    else CSum s' (proj_pair strong s i c1) (proj_pair strong s i c2)
  | CPair s' c1 c2 ⇒
    if side_eq_dec s s'
    then
      match i with
      | One ⇒ c1
      | Two ⇒ c2
      end
    else CPair s' (proj_pair strong s i c1) (proj_pair strong s i c2)
  | CFun s' carg cinner couter ⇒
    if side_eq_dec s s'
    then CTop
    else
      if strong
      then
        if is_top carg
        then CFun s' (proj_pair strong s i carg) cinner (proj_pair strong s i couter)
        else CTop
      else CTop
  end.

proj_pair commutes with flip_corr. This is useful to factorize proofs.
Lemma proj_pair_flip strong s i c :
  flip_corr (proj_pair strong s i c)
  = proj_pair strong (flip_side s) i (flip_corr c).
Proof.
  induction c.
  - reflexivity.
  - reflexivity.
  - simpl. destruct i; reflexivity.
  - simpl flip_corr. simpl proj_pair.
    destruct (side_eq_dec s s0).
    + subst. destruct (side_eq_dec (flip_side s0) (flip_side s0)); try contradiction.
      destruct i; reflexivity.
    + destruct (side_eq_dec (flip_side s) (flip_side s0)).
      × exfalso. auto using flip_side_injective.
      × rewrite <- IHc1. rewrite <- IHc2. reflexivity.
  - simpl flip_corr. simpl proj_pair.
    destruct (side_eq_dec s s0).
    + subst. destruct (side_eq_dec (flip_side s0) (flip_side s0)); try contradiction.
      destruct strong; reflexivity.
    + destruct (side_eq_dec (flip_side s) (flip_side s0)).
      × exfalso. auto using flip_side_injective.
      × rewrite <- IHc1. rewrite <- IHc2. reflexivity.
  - simpl flip_corr. simpl proj_pair.
    destruct (side_eq_dec s s0).
    + subst. destruct (side_eq_dec (flip_side s0) (flip_side s0)); try contradiction.
      reflexivity.
    + destruct (side_eq_dec (flip_side s) (flip_side s0)).
      × exfalso. auto using flip_side_injective.
      × { rewrite <- IHc1. rewrite <- IHc3.
          destruct strong; [| reflexivity].
          destruct (is_top c1).
          - subst. simpl. reflexivity.
          - destruct (is_top (flip_corr c1)).
            + exfalso. destruct c1; simpl in *; congruence.
            + reflexivity.
        }
Qed.

When strong = false, if we call proj_pair twice in a row with distinct sides, then the ordering of the calls does not matter. This is an intermediate lemma.
Lemma proj_pair_swap_LR i1 i2 c:
  proj_pair false L i1 (proj_pair false R i2 c)
  = proj_pair false R i2 (proj_pair false L i1 c).
Proof.
  induction c; simpl in *; auto.
  - destruct i1; destruct i2; reflexivity.
  - destruct s; simpl.
    + destruct i1; reflexivity.
    + destruct i2; reflexivity.
  - destruct s; simpl; reflexivity.
  - destruct s; simpl.
    + destruct (is_top c1).
      × subst. simpl. reflexivity.
      × simpl. reflexivity.
    + destruct (is_top c1).
      × subst. simpl. reflexivity.
      × simpl. reflexivity.
Qed.

When strong = false, if we call proj_pair twice in a row with distinct sides, then the ordering of the calls does not matter.
Lemma proj_pair_swap s1 i1 s2 i2 c:
  s1 ≠ s2 →
  proj_pair false s1 i1 (proj_pair false s2 i2 c)
  = proj_pair false s2 i2 (proj_pair false s1 i1 c).
Proof.
  intro Hneq.
  destruct s1; destruct s2; try congruence.
  - apply proj_pair_swap_LR.
  - symmetry. apply proj_pair_swap_LR.
Qed.

A call proj_pair strong L i c abstracts the operation of projecting the values on the left of the concretization of c on the component index of a pair.
Lemma concretize_corr_proj_pair_L strong ty1L ty1R ty2 i c:
  RelIncl
    (RelCompose (match i with
                 | One ⇒ RelPairR RelEqVal RelTopVal
                 | Two ⇒ RelPairR RelTopVal RelEqVal
                 end)
                (concretize_corr (TPair ty1L ty1R) ty2 c))
    (concretize_corr (match i with One ⇒ ty1L | Two ⇒ ty1R end) ty2
                     (proj_pair strong L i c)).
Proof.
  revert ty1L ty1R ty2.
  induction c; intros; simpl.
  - intros v1 v3 [v2 [H12 H23]].
    destruct i; destruct v2; simpl in *; try tauto.
    + destruct H12 as [[Heq H12'] H12]. subst.
      destruct H23 as [H23 [HwfL HwfR]].
      inversion HwfL; subst. tauto.
    + destruct H12 as [H12' [Heq H12]]. subst.
      destruct H23 as [H23 [HwfL HwfR]].
      inversion HwfL; subst. tauto.
  - intros v1 v3 [v2 [H12 H23]]. assumption.
  - intros v1 v3 [v2 [H12 H23]].
    destruct (ty_eq_dec (TPair ty1L ty1R) ty2); [ subst | contradiction ].
    destruct i; destruct v2; simpl in *; try tauto.
    + destruct (ty_eq_dec ty1L ty1L); [| contradiction ].
      simpl. intuition. subst. inversion H1; subst. tauto.
    + destruct (ty_eq_dec ty1R ty1R); [| contradiction ].
      simpl. intuition. subst. inversion H1; subst. tauto.
  - destruct i; destruct s.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; try contradiction.
      intuition. subst. assumption.
    + intros v1 v3 [v2 [H12 H23]]. destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      destruct v3; try contradiction.
      intuition; subst.
      × apply (IHc1 _ ty1R). simpl. ∃ (Pair v2_1 v2_2). tauto.
      × apply (IHc2 _ ty1R). simpl. ∃ (Pair v2_1 v2_2). tauto.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; try contradiction.
      intuition. subst. assumption.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      destruct v3; try contradiction.
      intuition; subst.
      × apply (IHc1 ty1L). simpl. ∃ (Pair v2_1 v2_2). tauto.
      × apply (IHc2 ty1L). simpl. ∃ (Pair v2_1 v2_2). tauto.
  - destruct i; destruct s.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; contradiction.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      destruct v3; try contradiction.
      × intuition; subst.
        apply (IHc1 _ ty1R). simpl. ∃ (Pair v2_1 v2_2). tauto.
      × intuition; subst.
        apply (IHc2 _ ty1R). simpl. ∃ (Pair v2_1 v2_2). tauto.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; contradiction.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      destruct v3; try contradiction.
      × intuition; subst.
        apply (IHc1 ty1L). simpl. ∃ (Pair v2_1 v2_2). tauto.
      × intuition; subst.
        apply (IHc2 ty1L). simpl. ∃ (Pair v2_1 v2_2). tauto.
  - destruct i; destruct s.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; try contradiction.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      intuition. subst. inversion H1; subst.
      destruct strong; [| simpl;tauto].
      destruct (is_top c1); subst.
      × simpl. split; [ split; [| split] | split]; auto.
        intros v w Happ [Hgood1 Hgood2].
        destruct (H8 _ _ Happ); [ simpl; tauto |].
        split; [ assumption |].
        apply (IHc3 _ ty1R). simpl.
        ∃ (Pair v2_1 v2_2). tauto.
      × simpl. tauto.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; try contradiction.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      intuition. subst. inversion H1; subst.
      destruct strong; [| simpl; tauto].
      destruct (is_top c1); subst.
      × simpl. split; [ split; [| split ] | split]; auto.
        intros v w Happ [Hgood1 Hgood2].
        destruct (H8 _ _ Happ); [ simpl; tauto |].
        split; [ assumption |].
        apply (IHc3 ty1L). simpl.
        ∃ (Pair v2_1 v2_2). tauto.
      × simpl. tauto.
Qed.

A call proj_pair strong R i c abstracts the operation of projecting the values on the right of the concretization of c on the component index of a pair.
Lemma concretize_corr_proj_pair_R strong ty1 ty2L ty2R i c:
  RelIncl
    (RelCompose (concretize_corr ty1 (TPair ty2L ty2R) c)
                (match i with
                 | One ⇒ RelPairL RelEqVal RelTopVal
                 | Two ⇒ RelPairL RelTopVal RelEqVal
                 end))
    (concretize_corr ty1 (match i with One ⇒ ty2L | Two ⇒ ty2R end)
                     (proj_pair strong R i c)).
Proof.
  apply RelInv_incl_reversed.
  rewrite RelInv_RelCompose.
  repeat rewrite <- concretize_corr_flip.
  rewrite proj_pair_flip.
  destruct i; rewrite RelInv_RelPairL; rewrite RelInv_RelEqVal;
    rewrite RelInv_RelTopVal.
  - rewrite <- concretize_corr_proj_pair_L with (i := One). reflexivity.
  - rewrite <- concretize_corr_proj_pair_L with (i := Two). reflexivity.
Qed.

Typing lemma for proj_pair strong strong L i c.
Lemma proj_pair_L_wf strong ty1L ty1R ty2 i c:
  wf_corr c (TPair ty1L ty1R) ty2 →
  wf_corr (proj_pair strong L i c) (match i with One ⇒ ty1L | Two ⇒ ty1R end) ty2.
Proof.
  revert ty1L ty1R ty2. induction c; intros ty1L ty1R ty2 Hwf; simpl in *; auto; subst.
  - destruct i; constructor; constructor.
  - destruct s; destruct i; try tauto; destruct ty2; try tauto;
      intuition; constructor; eauto.
  - destruct s; destruct i; try tauto; destruct ty2; try tauto;
      intuition; constructor; eauto.
  - destruct s; [ constructor |].
    destruct strong; [| constructor ].
    destruct (is_top c1); subst; [| constructor ].
    destruct ty2; try contradiction.
    intuition. constructor; auto.
Qed.

Typing lemma for proj_pair strong strong R i c.
Lemma proj_pair_R_wf strong ty1 ty2L ty2R i c:
  wf_corr c ty1 (TPair ty2L ty2R) →
  wf_corr (proj_pair strong R i c) ty1 (match i with One ⇒ ty2L | Two ⇒ ty2R end).
Proof.
  intro Hwf.
  rewrite <- (flip_corr_involution (proj_pair strong R i c)).
  apply flip_corr_wf.
  rewrite proj_pair_flip. apply proj_pair_L_wf.
  apply flip_corr_wf.
  assumption.
Qed.

Projection on sums

proj_sum strong s i c projects the correlation c on the case index of a sum on its side s. The boolean strong controls whether one should try to be more precise, at the cost of a loss of monotonicity. This is the Figure 13 of the ICFP'20 paper.
Fixpoint proj_sum (strong: bool) (s: side) (i: index) (c: corr): corr :=
  match c with
  | CTop as c | CBot as c ⇒ c
  | CEq ⇒
    match i with
    | One ⇒ CSum (flip_side s) CEq CBot
    | Two ⇒ CSum (flip_side s) CBot CEq
    end
  | CSum s' c1 c2 ⇒
    if side_eq_dec s s'
    then
      match i with
      | One ⇒ c1
      | Two ⇒ c2
      end
    else CSum s' (proj_sum strong s i c1) (proj_sum strong s i c2)
  | CPair s' c1 c2 ⇒
    if side_eq_dec s s'
    then
      if strong
      then CBot
      else CTop
    else CPair s' (proj_sum strong s i c1) (proj_sum strong s i c2)
  | CFun s' carg cinner couter ⇒
    if side_eq_dec s s'
    then CTop
    else
      if strong
      then
        if is_top carg
        then CFun s' (proj_sum strong s i carg) cinner (proj_sum strong s i couter)
        else CTop
      else CTop
  end.

proj_sum commutes with flip_corr. This is useful to factorize proofs.
Lemma proj_sum_flip strong s i c :
  flip_corr (proj_sum strong s i c)
  = proj_sum strong (flip_side s) i (flip_corr c).
Proof.
  induction c.
  - reflexivity.
  - reflexivity.
  - simpl. destruct i; reflexivity.
  - simpl flip_corr. simpl proj_sum.
    destruct (side_eq_dec s s0).
    + subst. destruct (side_eq_dec (flip_side s0) (flip_side s0)); try contradiction.
      destruct strong; reflexivity.
    + destruct (side_eq_dec (flip_side s) (flip_side s0)).
      × exfalso. auto using flip_side_injective.
      × rewrite <- IHc1. rewrite <- IHc2. reflexivity.
  - simpl flip_corr. simpl proj_sum.
    destruct (side_eq_dec s s0).
    + subst. destruct (side_eq_dec (flip_side s0) (flip_side s0)); try contradiction.
      destruct i; reflexivity.
    + destruct (side_eq_dec (flip_side s) (flip_side s0)).
      × exfalso. auto using flip_side_injective.
      × rewrite <- IHc1. rewrite <- IHc2. reflexivity.
  - simpl flip_corr. simpl proj_sum.
    destruct (side_eq_dec s s0).
    + subst. destruct (side_eq_dec (flip_side s0) (flip_side s0)); try contradiction.
      destruct i; reflexivity.
    + destruct (side_eq_dec (flip_side s) (flip_side s0)).
      × exfalso. auto using flip_side_injective.
      × { rewrite <- IHc1. rewrite <- IHc3.
          destruct strong; [| reflexivity].
          destruct (is_top c1).
          - subst. simpl. reflexivity.
          - destruct (is_top (flip_corr c1)).
            + exfalso. destruct c1; simpl in *; congruence.
            + reflexivity.
        }
Qed.

When strong = false, if we call proj_sum twice in a row with distinct sides, then the ordering of the calls does not matter. This is an intermediate lemma.
Lemma proj_sum_swap_LR i1 i2 c:
  proj_sum false L i1 (proj_sum false R i2 c)
  = proj_sum false R i2 (proj_sum false L i1 c).
Proof.
  induction c; simpl in *; auto.
  - destruct i1; destruct i2; reflexivity.
  - destruct s; simpl; reflexivity.
  - destruct s; simpl.
    + destruct i1; reflexivity.
    + destruct i2; reflexivity.
  - destruct s; destruct (is_top c1); subst; reflexivity.
Qed.

When strong = false, if we call proj_sum twice in a row with distinct sides, then the ordering of the calls does not matter.
Lemma proj_sum_swap s1 i1 s2 i2 c:
  s1 ≠ s2 →
  proj_sum false s1 i1 (proj_sum false s2 i2 c)
  = proj_sum false s2 i2 (proj_sum false s1 i1 c).
Proof.
  intro Hneq.
  destruct s1; destruct s2; try congruence.
  - apply proj_sum_swap_LR.
  - symmetry. apply proj_sum_swap_LR.
Qed.

A call proj_sum strong L i c abstracts the operation of projecting the values on the left of the concretization of c on the case index of a sum.
Lemma concretize_corr_proj_sum_L strong ty1L ty1R ty2 i c:
  RelIncl
    (RelCompose (match i with
                 | One ⇒ RelSumR RelEqVal RelBot
                 | Two ⇒ RelSumR RelBot RelEqVal
                 end)
                (concretize_corr (TSum ty1L ty1R) ty2 c))
    (concretize_corr (match i with One ⇒ ty1L | Two ⇒ ty1R end) ty2
                     (proj_sum strong L i c)).
Proof.
  revert ty1L ty1R ty2.
  induction c; intros; simpl.
  - intros v1 v3 [v2 [H12 H23]].
    destruct i; destruct v2; simpl in *; try tauto.
    + destruct H12 as [Heq H12]. subst.
      destruct H23 as [Hgood [HwfL HwfR]].
      inversion HwfL; subst. tauto.
    + destruct H12 as [Heq H12]. subst.
      destruct H23 as [Hgood [HwfL HwfR]].
      inversion HwfL; subst. tauto.
  - intros v1 v3 [v2 [H12 H23]]. assumption.
  - intros v1 v3 [v2 [H12 H23]].
    destruct i; destruct v2; simpl in *; try tauto;
      (destruct (ty_eq_dec (TSum ty1L ty1R) ty2); subst; [| contradiction ]);
      simpl in *; intuition; subst.
    + destruct (ty_eq_dec ty1L ty1L); [| contradiction ].
      inversion H1; subst. simpl. tauto.
    + destruct (ty_eq_dec ty1R ty1R); [| contradiction ].
      inversion H1; subst. simpl. tauto.
  - destruct i; destruct s.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; contradiction.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      destruct v3; try contradiction.
      intuition; subst.
      × apply (IHc1 _ ty1R). simpl. ∃ (InjL v2). tauto.
      × apply (IHc2 _ ty1R). simpl. ∃ (InjL v2). tauto.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; contradiction.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      destruct v3; try contradiction.
      intuition; subst.
      × apply (IHc1 ty1L). simpl. ∃ (InjR v2). tauto.
      × apply (IHc2 ty1L). simpl. ∃ (InjR v2). tauto.
  - destruct i; destruct s.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; try contradiction.
      intuition. subst. assumption.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      destruct v3; try contradiction.
      × intuition; subst.
        apply (IHc1 _ ty1R). simpl. ∃ (InjL v2). tauto.
      × intuition; subst.
        apply (IHc2 _ ty1R). simpl. ∃ (InjL v2). tauto.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; try contradiction.
      intuition. subst. assumption.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      destruct v3; try contradiction.
      × intuition; subst.
        apply (IHc1 ty1L). simpl. ∃ (InjR v2). tauto.
      × intuition; subst.
        apply (IHc2 ty1L). simpl. ∃ (InjR v2). tauto.
  - destruct i; destruct s.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; try contradiction.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      intuition. subst. inversion H1; subst.
      destruct strong; [| simpl; tauto].
      destruct (is_top c1); subst.
      × simpl. split; [ split; [| split ] | split]; auto.
        intros v w Happ [Hgood1 Hgood2].
        destruct (H6 _ _ Happ); [ simpl; tauto |].
        split; [ assumption |].
        apply (IHc3 _ ty1R). simpl.
        ∃ (InjL v2). tauto.
      × simpl. tauto.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct v2; try contradiction.
    + intros v1 v3 [v2 [H12 H23]]. simpl in ×.
      destruct ty2; try contradiction. simpl in ×.
      destruct v2; try contradiction.
      intuition. subst. inversion H1; subst.
      destruct strong; [| simpl; tauto].
      destruct (is_top c1); subst.
      × simpl. split; [ split; [| split ] | split]; auto.
        intros v w Happ [Hgood1 Hgood2].
        destruct (H6 _ _ Happ); [ simpl; tauto |].
        split; [ assumption |].
        apply (IHc3 ty1L). simpl.
        ∃ (InjR v2). tauto.
      × simpl. tauto.
Qed.

A call proj_sum strong R i c abstracts the operation of projecting the values on the right of the concretization of c on the case index of a sum.
Lemma concretize_corr_proj_sum_R strong ty1 ty2L ty2R i c:
  RelIncl
    (RelCompose (concretize_corr ty1 (TSum ty2L ty2R) c)
                (match i with
                 | One ⇒ RelSumL RelEqVal RelBot
                 | Two ⇒ RelSumL RelBot RelEqVal
                 end))
    (concretize_corr ty1 (match i with One ⇒ ty2L | Two ⇒ ty2R end)
                     (proj_sum strong R i c)).
Proof.
  apply RelInv_incl_reversed.
  rewrite RelInv_RelCompose.
  repeat rewrite <- concretize_corr_flip.
  rewrite proj_sum_flip.
  destruct i; rewrite RelInv_RelSumL; rewrite RelInv_RelEqVal;
    rewrite RelInv_RelBot.
  - rewrite <- concretize_corr_proj_sum_L with (i := One). reflexivity.
  - rewrite <- concretize_corr_proj_sum_L with (i := Two). reflexivity.
Qed.

Typing lemma for proj_sum strong strong L i c.
Lemma proj_sum_L_wf strong ty1L ty1R ty2 i c:
  wf_corr c (TSum ty1L ty1R) ty2 →
  wf_corr (proj_sum strong L i c) (match i with One ⇒ ty1L | Two ⇒ ty1R end) ty2.
Proof.
  revert ty1L ty1R ty2. induction c; intros ty1L ty1R ty2 Hwf; simpl in *; auto; subst.
  - destruct i; constructor; constructor.
  - destruct s; destruct i; try tauto; destruct ty2; try tauto;
      intuition; constructor; eauto.
  - destruct s; destruct i; try tauto; destruct ty2; try tauto;
      intuition; constructor; eauto.
  - destruct s; [ constructor |].
    destruct strong; [| constructor ].
    destruct (is_top c1); subst; [| constructor ].
    destruct ty2; try contradiction.
    intuition. constructor; auto.
Qed.

Typing lemma for proj_sum strong strong R i c.
Lemma proj_sum_R_wf strong ty1 ty2L ty2R i c:
  wf_corr c ty1 (TSum ty2L ty2R) →
  wf_corr (proj_sum strong R i c) ty1 (match i with One ⇒ ty2L | Two ⇒ ty2R end).
Proof.
  intro Hwf.
  rewrite <- (flip_corr_involution (proj_sum strong R i c)).
  apply flip_corr_wf.
  rewrite proj_sum_flip. apply proj_sum_L_wf.
  apply flip_corr_wf.
  assumption.
Qed.

Interplay between pair- and sum-projections

When calling proj_pair and proj_sum in sequence with different sides, the ordering does not matter. This is an intermediate lemma.
Lemma proj_pair_L_proj_sum_R_swap i1 i2 c:
  proj_pair false L i1 (proj_sum false R i2 c)
  = proj_sum false R i2 (proj_pair false L i1 c).
Proof.
  destruct c; simpl; auto.
  - destruct i1; destruct i2; reflexivity.
  - destruct s; destruct i1; reflexivity.
  - destruct s; destruct i2; reflexivity.
  - destruct s; destruct (is_top c1); subst; reflexivity.
Qed.

When calling proj_sum and proj_pair in sequence with different sides, the ordering does not matter. This is an intermediate lemma.
Lemma proj_pair_R_proj_sum_L_swap i1 i2 c:
  proj_pair false R i1 (proj_sum false L i2 c)
  = proj_sum false L i2 (proj_pair false R i1 c).
Proof.
  apply flip_corr_injective.
  rewrite proj_pair_flip.
  rewrite proj_sum_flip.
  rewrite proj_sum_flip.
  rewrite proj_pair_flip.
  apply proj_pair_L_proj_sum_R_swap.
Qed.

When calling proj_pair and proj_sum in sequence with different sides, the ordering does not matter.
Lemma proj_pair_proj_sum_swap s1 i1 s2 i2 c:
  s1 ≠ s2 →
  proj_pair false s1 i1 (proj_sum false s2 i2 c)
  = proj_sum false s2 i2 (proj_pair false s1 i1 c).
Proof.
  intro Hneq.
  destruct s1; destruct s2; try congruence.
  - apply proj_pair_L_proj_sum_R_swap.
  - apply proj_pair_R_proj_sum_L_swap.
Qed.

Projection on an path

An atomic path is either a projection on a side of a pair, or a projection on a case of a sum.
Inductive atomic_path : Type :=
| ProjPair (i: index)
| ProjSum (i: index)
.

A path is a list of atomic paths.
Definition path : Type := list atomic_path.

The projection proj_corr of a correlation on a path p is the iteration of the projections on each atomic path of p.
Definition proj_corr (strong: bool) (s: side) (p: path) (c: corr) : corr :=
  List.fold_left (fun acc p0 ⇒ match p0 with
                             | ProjPair i ⇒ proj_pair strong s i acc
                             | ProjSum i ⇒ proj_sum strong s i acc
                             end)
                 p c.

Commutation lemma on fold_left, that seems to be missing from Coq's standard libraey.
Lemma fold_left_commute {A B} (f: B → A → B) (l: list A) (acc: B) (g: B → B):
  (∀ a b, f (g b) a = g (f b a)) →
  g (List.fold_left f l acc) = List.fold_left f l (g acc).
Proof.
  intro Heq. revert acc. induction l; intros.
  - reflexivity.
  - simpl. rewrite Heq. rewrite IHl. reflexivity.
Qed.

When strong = false, when calling proj_corr twice in a row with different sides, the ordering of the calls does not matter. This is Lemma 5.5 of the ICFP'20 paper, that is generalized to general paths (i.e. lists of atomic paths).
Lemma proj_corr_swap s1 p1 s2 p2 c:
  s1 ≠ s2 →
  proj_corr false s1 p1 (proj_corr false s2 p2 c)
  = proj_corr false s2 p2 (proj_corr false s1 p1 c).
Proof.
  intro Hneq.
  unfold proj_corr. revert c. revert p2. induction p1; intros; simpl.
  - reflexivity.
  - destruct a.
    + rewrite <- IHp1. clear IHp1. rewrite fold_left_commute.
      × reflexivity.
      × { intros a b. destruct a.
          - auto using proj_pair_swap.
          - symmetry. auto using proj_pair_proj_sum_swap.
        }
    + rewrite <- IHp1. clear IHp1. rewrite fold_left_commute.
      × reflexivity.
      × { intros a b. destruct a.
          - auto using proj_pair_proj_sum_swap.
          - auto using proj_sum_swap.
        }
Qed.

Projecting a correlation c on p1, and then on p2 on the same side is equivalent to projecting c on p1 ++ p2.
Lemma proj_corr_app strong s p1 p2 c:
  proj_corr strong s p2 (proj_corr strong s p1 c) = proj_corr strong s (app p1 p2) c.
Proof.
  unfold proj_corr. symmetry. apply List.fold_left_app.
Qed.

The projection of CBot is always CBot.
Lemma proj_corr_bot strong s p:
  proj_corr strong s p CBot = CBot.
Proof.
  unfold proj_corr. induction p; simpl.
  - reflexivity.
  - destruct a; assumption.
Qed.

The projection of CTop is always CTop.
Lemma proj_corr_top strong s p:
  proj_corr strong s p CTop = CTop.
Proof.
  unfold proj_corr. induction p; simpl.
  - reflexivity.
  - destruct a; assumption.
Qed.

Commutation lemma for the projection of a pair correlation on its opposite side.
Lemma proj_corr_pair_other strong s1 p s2 c1 c2:
  s1 ≠ s2 →
  proj_corr strong s1 p (CPair s2 c1 c2) =
  CPair s2 (proj_corr strong s1 p c1) (proj_corr strong s1 p c2).
Proof.
  intro Hneq. revert c1 c2. unfold proj_corr. induction p; intros; simpl.
  - reflexivity.
  - destruct a; destruct (side_eq_dec s1 s2); try contradiction; auto.
Qed.

Commutation lemma for the projection of a sum correlation on its opposite side.
Lemma proj_corr_sum_other strong s1 p s2 c1 c2:
  s1 ≠ s2 →
  proj_corr strong s1 p (CSum s2 c1 c2) =
  CSum s2 (proj_corr strong s1 p c1) (proj_corr strong s1 p c2).
Proof.
  intro Hneq. revert c1 c2. unfold proj_corr. induction p; intros; simpl.
  - reflexivity.
  - destruct a; destruct (side_eq_dec s1 s2); try contradiction; auto.
Qed.

Commutation lemma for the projection of a function correlation on its opposite side.
Lemma proj_corr_fun_other strong s1 p s2 carg cinner cother:
  s1 ≠ s2 →
  p ≠ nil →
  proj_corr strong s1 p (CFun s2 carg cinner cother) =
  if strong
  then
    if is_top carg
    then CFun s2 (proj_corr strong s1 p carg) cinner (proj_corr strong s1 p cother)
    else CTop
  else CTop.
Proof.
  intros Hneq Hnil.
  revert carg cinner cother. unfold proj_corr. induction p; intros; simpl.
  - contradiction.
  - destruct a; destruct (side_eq_dec s1 s2); try contradiction.
    + destruct strong.
      × { destruct (is_top carg); subst; auto.
          - destruct p as [| a p].
            + reflexivity.
            + rewrite IHp; auto. congruence.
          - apply proj_corr_top.
        }
      × apply proj_corr_top.
    + destruct strong.
      × { destruct (is_top carg); subst; auto.
          - destruct p as [| a p].
            + reflexivity.
            + rewrite IHp; auto. congruence.
          - apply proj_corr_top.
        }
      × apply proj_corr_top.
Qed.

Comparison of correlations

Comparison (in terms of inclusion) of correlations. This is the Figure 11 of the ICFP'20 paper.
Inductive corr_leq: corr → corr → Prop :=
| CLeqBot: ∀ c, corr_leq CBot c
| CLeqTop: ∀ c, corr_leq c CTop
| CLeqEq: corr_leq CEq CEq
| CLeqPair: ∀ c s c1 c2,
    corr_leq (proj_pair false s One c) c1 →
    corr_leq (proj_pair false s Two c) c2 →
    corr_leq c (CPair s c1 c2)
| CLeqSum: ∀ c s c1 c2,
    corr_leq (proj_sum false s One c) c1 →
    corr_leq (proj_sum false s Two c) c2 →
    corr_leq c (CSum s c1 c2)
| CLeqFun: ∀ s carg1 cinner1 couter1 carg2 cinner2 couter2,
    corr_leq carg2 carg1 →
    corr_leq cinner1 cinner2 →
    corr_leq couter1 couter2 →
    corr_leq (CFun s carg1 cinner1 couter1) (CFun s carg2 cinner2 couter2)
.

flip_corr preserves and reflects corr_leq.
Lemma corr_leq_flip c1 c2:
  corr_leq c1 c2 ↔ corr_leq (flip_corr c1) (flip_corr c2).
Proof.
  revert c1 c2.
  assert (∀ c1 c2, corr_leq c1 c2 → corr_leq (flip_corr c1) (flip_corr c2)).
  { intros c1 c2 H.
    induction H; simpl;
      try solve [ constructor;
                  try rewrite proj_pair_flip in × |-;
                  try rewrite proj_sum_flip in × |-;
                  auto ].
  }
  intros c1 c2. split; intro Hleq; auto.
  apply H in Hleq. repeat rewrite flip_corr_involution in Hleq.
  assumption.
Qed.

Intermediate semantic lemmas used in the correctness of comparison

Unfolding lemma for correlations that hold pairs on their LHS.
Lemma RelPairL_incl tL1 tL2 tR R:
  good_vrel R →
  RelIncl R (RelTyped (TPair tL1 tL2) tR) →
  RelIncl R
    (RelPairL
       (RelCompose (RelPairR RelEqVal RelTopVal) R)
       (RelCompose (RelPairR RelTopVal RelEqVal) R)).
Proof.
  intros Hgood Htyped v1 v2 H.
  assert (good_value v1 ∧ good_value v2) as [Hgood1 Hgood2].
  { apply Hgood in H. assumption. }
  assert (is_value v1) as Hval1 by auto.
  assert (wf_term nil v1 (TPair tL1 tL2)) as Hwf1.
  { apply Htyped in H. simpl in H. tauto. }
  destruct v1; simpl in Hval1; try contradiction; inversion Hwf1; subst.
  assert (good_value v1_1) as Hgood11 by (eapply good_value_Pair_inv_L; eauto).
  assert (good_value v1_2) as Hgood12 by (eapply good_value_Pair_inv_R; eauto).
  split; ∃ (Pair v1_1 v1_2); simpl; tauto.
Qed.

Unfolding lemma for correlations that hold pairs on their RHS.
Lemma RelPairR_incl tL tR1 tR2 R:
  good_vrel R →
  RelIncl R (RelTyped tL (TPair tR1 tR2)) →
  RelIncl R
    (RelPairR
       (RelCompose R (RelPairL RelEqVal RelTopVal))
       (RelCompose R (RelPairL RelTopVal RelEqVal))).
Proof.
  intros Hgood Htyped.
  apply RelInv_RelIncl.
  rewrite RelInv_RelPairR.
  repeat rewrite RelInv_RelCompose.
  repeat rewrite RelInv_RelPairL.
  rewrite RelInv_RelEqVal. rewrite RelInv_RelTopVal.
  eapply RelPairL_incl; eauto.
  - rewrite <- RelInv_good_vrel. assumption.
  - apply RelInv_RelIncl in Htyped. rewrite RelInv_RelTyped in Htyped. eassumption.
Qed.

Unfolding lemma for correlations that hold sums on their LHS.
Lemma RelSumL_incl tL1 tL2 tR R:
  good_vrel R →
  RelIncl R (RelTyped (TSum tL1 tL2) tR) →
  RelIncl R
    (RelSumL
       (RelCompose (RelSumR RelEqVal RelBot) R)
       (RelCompose (RelSumR RelBot RelEqVal) R)).
Proof.
  intros Hgood Htyped v1 v2 H.
  assert (good_value v1 ∧ good_value v2) as [Hgood1 Hgood2].
  { apply Hgood in H. assumption. }
  assert (is_value v1) as Hval1 by auto.
  assert (wf_term nil v1 (TSum tL1 tL2)) as Hwf1.
  { apply Htyped in H. simpl in H. tauto. }
  destruct v1; simpl in Hval1; try contradiction; inversion Hwf1; subst.
  - assert (good_value v1) as Hgood11 by (eapply good_value_InjL_inv; eauto).
    ∃ (InjL v1). simpl. tauto.
  - assert (good_value v1) as Hgood11 by (eapply good_value_InjR_inv; eauto).
    ∃ (InjR v1). simpl. tauto.
Qed.

Unfolding lemma for correlations that hold sums on their RHS.
Lemma RelSumR_incl tL tR1 tR2 R:
  good_vrel R →
  RelIncl R (RelTyped tL (TSum tR1 tR2)) →
  RelIncl R
    (RelSumR
       (RelCompose R (RelSumL RelEqVal RelBot))
       (RelCompose R (RelSumL RelBot RelEqVal))).
Proof.
  intros Hgood Htyped.
  apply RelInv_RelIncl.
  rewrite RelInv_RelSumR.
  repeat rewrite RelInv_RelCompose.
  repeat rewrite RelInv_RelSumL.
  rewrite RelInv_RelEqVal. rewrite RelInv_RelBot.
  eapply RelSumL_incl; eauto.
  - rewrite <- RelInv_good_vrel. assumption.
  - apply RelInv_RelIncl in Htyped. rewrite RelInv_RelTyped in Htyped. eassumption.
Qed.

Correctness of comparison

Soundness lemma for corr_leq: if two correlations with the same types are included, then their concretizations are included. This is Lemma 5.8 of the ICFP'20 paper.
Lemma concretize_corr_leq tL tR c1 c2:
  wf_corr c1 tL tR →
  wf_corr c2 tL tR →
  corr_leq c1 c2 →
  RelIncl (concretize_corr tL tR c1) (concretize_corr tL tR c2).
Proof.
  intros Hwf1 Hwf2 Hleq. revert tL tR Hwf1 Hwf2. induction Hleq; intros.
  - apply RelBot_bot.
  - simpl. apply RelInter_glb.
    + apply concretize_corr_below_top.
    + apply concretize_corr_typed.
  - reflexivity.
  - simpl in Hwf2.
    destruct s; [destruct tL | destruct tR]; try contradiction.
    + destruct Hwf2 as [Hwf21 Hwf22]. simpl.
      rewrite <- IHHleq1;
        [| apply proj_pair_L_wf with (ty1R := tL2) (i := One); assumption | assumption].
      clear IHHleq1.
      rewrite <- concretize_corr_proj_pair_L with (ty1R := tL2) (i := One).
      rewrite <- IHHleq2;
        [| apply proj_pair_L_wf with (ty1L := tL1) (i := Two); assumption | assumption].
      clear IHHleq2.
      rewrite <- concretize_corr_proj_pair_L with (ty1L := tL1) (i := Two).
      eapply RelPairL_incl; eauto using concretize_corr_typed, concretize_corr_good.
    + destruct Hwf2 as [Hwf21 Hwf22]. simpl.
      rewrite <- IHHleq1;
        [| apply proj_pair_R_wf with (ty2R := tR2) (i := One); assumption | assumption].
      clear IHHleq1.
      rewrite <- concretize_corr_proj_pair_R with (ty2R := tR2) (i := One).
      rewrite <- IHHleq2;
        [| apply proj_pair_R_wf with (ty2L := tR1) (i := Two); assumption | assumption].
      clear IHHleq2.
      rewrite <- concretize_corr_proj_pair_R with (ty2L := tR1) (i := Two).
      eapply RelPairR_incl; eauto using concretize_corr_typed, concretize_corr_good.
  - simpl in Hwf2.
    destruct s; [destruct tL | destruct tR]; try contradiction.
    + destruct Hwf2 as [Hwf21 Hwf22]. simpl.
      rewrite <- IHHleq1;
        [| apply proj_sum_L_wf with (ty1R := tL2) (i := One); assumption | assumption].
      clear IHHleq1.
      rewrite <- concretize_corr_proj_sum_L with (ty1R := tL2) (i := One).
      rewrite <- IHHleq2;
        [| apply proj_sum_L_wf with (ty1L := tL1) (i := Two); assumption | assumption].
      clear IHHleq2.
      rewrite <- concretize_corr_proj_sum_L with (ty1L := tL1) (i := Two).
      eapply RelSumL_incl; eauto using concretize_corr_typed, concretize_corr_good.
    + destruct Hwf2 as [Hwf21 Hwf22]. simpl.
      rewrite <- IHHleq1;
        [| apply proj_sum_R_wf with (ty2R := tR2) (i := One); assumption | assumption].
      clear IHHleq1.
      rewrite <- concretize_corr_proj_sum_R with (ty2R := tR2) (i := One).
      rewrite <- IHHleq2;
        [| apply proj_sum_R_wf with (ty2L := tR1) (i := Two); assumption | assumption].
      clear IHHleq2.
      rewrite <- concretize_corr_proj_sum_R with (ty2L := tR1) (i := Two).
      eapply RelSumR_incl; eauto using concretize_corr_typed, concretize_corr_good.
  - simpl in Hwf2.
    destruct s; [ destruct tL | destruct tR ]; try contradiction; simpl in Hwf1.
    + destruct Hwf1 as [Hwfarg1 [Hwfinner1 Hwfouter1]].
      destruct Hwf2 as [Hwfarg2 [Hwfinner2 Hwfouter2]].
      simpl.
      rewrite IHHleq1; [| tauto | tauto]. clear IHHleq1.
      rewrite <- IHHleq2; [| tauto | tauto]. clear IHHleq2.
      rewrite <- IHHleq3; [| tauto | tauto]. clear IHHleq3.
      reflexivity.
    + destruct Hwf1 as [Hwfarg1 [Hwfinner1 Hwfouter1]].
      destruct Hwf2 as [Hwfarg2 [Hwfinner2 Hwfouter2]].
      simpl.
      rewrite IHHleq1; [| tauto | tauto]. clear IHHleq1.
      rewrite <- IHHleq2; [| tauto | tauto]. clear IHHleq2.
      rewrite <- IHHleq3; [| tauto | tauto]. clear IHHleq3.
      reflexivity.
Qed.

Preorder structure

corr_leq is a reflexive relation.
Lemma corr_leq_refl: ∀ c, corr_leq c c.
Proof.
  intro c. induction c.
  - apply CLeqTop.
  - apply CLeqBot.
  - apply CLeqEq.
  - apply CLeqPair; simpl; destruct (side_eq_dec s s); try contradiction; assumption.
  - apply CLeqSum; simpl; destruct (side_eq_dec s s); try contradiction; assumption.
  - apply CLeqFun; assumption.
Qed.

proj_corr false s p is monotonic wrt corr_leq. This is essential for the transitivity of corr_leq. This is Lemma 5.6 of the ICFP'20 paper, that is generalized to general paths (i.e. lists of atomic paths).
Lemma proj_corr_monotonic s p c1 c2:
  corr_leq c1 c2 →
  corr_leq (proj_corr false s p c1) (proj_corr false s p c2).
Proof.
  intro Hleq. revert s p. induction Hleq; intros.
  - simpl. rewrite proj_corr_bot. apply CLeqBot.
  - simpl. rewrite proj_corr_top. apply CLeqTop.
  - apply corr_leq_refl.
  - destruct (side_eq_dec s0 s); subst.
    + destruct p as [| [i|i] p]; simpl.
      × apply CLeqPair; assumption.
      × destruct (side_eq_dec s s); try contradiction.
        destruct i; auto.
      × destruct (side_eq_dec s s); try contradiction.
        rewrite proj_corr_top. apply CLeqTop.
    + rewrite proj_corr_pair_other; auto.
      apply CLeqPair.
      × replace (proj_pair false s One (proj_corr false s0 p c))
          with (proj_corr false s (List.cons (ProjPair One) nil) (proj_corr false s0 p c))
          by reflexivity.
        rewrite proj_corr_swap; auto.
      × replace (proj_pair false s Two (proj_corr false s0 p c))
          with (proj_corr false s (List.cons (ProjPair Two) nil) (proj_corr false s0 p c))
          by reflexivity.
        rewrite proj_corr_swap; auto.
  - destruct (side_eq_dec s0 s); subst.
    + destruct p as [| [i|i] p]; simpl.
      × apply CLeqSum; assumption.
      × destruct (side_eq_dec s s); try contradiction.
        rewrite proj_corr_top. apply CLeqTop.
      × destruct (side_eq_dec s s); try contradiction.
        destruct i; auto.
    + rewrite proj_corr_sum_other; auto.
      apply CLeqSum.
      × replace (proj_sum false s One (proj_corr false s0 p c))
          with (proj_corr false s (List.cons (ProjSum One) nil) (proj_corr false s0 p c))
          by reflexivity.
        rewrite proj_corr_swap; auto.
      × replace (proj_sum false s Two (proj_corr false s0 p c))
          with (proj_corr false s (List.cons (ProjSum Two) nil) (proj_corr false s0 p c))
          by reflexivity.
        rewrite proj_corr_swap; auto.
  - destruct (side_eq_dec s0 s); subst.
    + destruct p as [| [i|i] p]; simpl.
      × apply CLeqFun; assumption.
      × destruct (side_eq_dec s s); try contradiction.
        apply corr_leq_refl.
      × destruct (side_eq_dec s s); try contradiction.
        apply corr_leq_refl.
    + destruct p as [| a p].
      × simpl. apply CLeqFun; assumption.
      × repeat rewrite proj_corr_fun_other; auto; try congruence.
        apply corr_leq_refl.
Qed.

corr_leq is a transitive relation, when we consider correlations of the same types. This is Lemma 5.7 of the ICFP'20 paper.
Lemma corr_leq_trans: ∀ tL tR c1 c2 c3,
    wf_corr c1 tL tR →
    wf_corr c2 tL tR →
    wf_corr c3 tL tR →
    corr_leq c1 c2 →
    corr_leq c2 c3 →
    corr_leq c1 c3.
Proof.
  intros tL tR. remember (ty_size tL + ty_size tR) as n.
  assert (ty_size tL + ty_size tR ≤ n) as Hn by lia. clear Heqn.
  revert tL tR Hn.
  induction n; intros tL tR Hn c1 c2 c3 Hwf1 Hwf2 Hwf3 Hleq12 Hleq23; subst.
  - pose proof (ty_size_not_zero tL).
    pose proof (ty_size_not_zero tR).
    lia.
  - destruct Hleq23.
    + inversion Hleq12; subst. apply CLeqBot.
    + apply CLeqTop.
    + inversion Hleq12; subst.
      × apply CLeqBot.
      × apply CLeqEq.
    + simpl in Hwf3.
      destruct s; [ destruct tL | destruct tR ]; try contradiction;
        destruct Hwf3 as [Hwf31 Hwf32]; simpl in Hn.
      × { constructor.
          - apply (proj_corr_monotonic L (List.cons (ProjPair One) nil)) in Hleq12.
            simpl in Hleq12.
            simple refine (IHn tL1 tR _ (proj_pair false L One c1) (proj_pair false L One c) c0 _ _ _ _ _); eauto; try lia.
            + apply proj_pair_L_wf with (strong := false) (i := One) in Hwf1.
              assumption.
            + apply proj_pair_L_wf with (strong := false) (i := One) in Hwf2.
              assumption.
          - apply (proj_corr_monotonic L (List.cons (ProjPair Two) nil)) in Hleq12.
            simpl in Hleq12.
            simple refine (IHn tL2 tR _ (proj_pair false L Two c1) (proj_pair false L Two c) c2 _ _ _ _ _); eauto; try lia.
            + apply proj_pair_L_wf with (strong := false) (i := Two) in Hwf1.
              assumption.
            + apply proj_pair_L_wf with (strong := false) (i := Two) in Hwf2.
              assumption.
        }
      × { constructor.
          - apply (proj_corr_monotonic R (List.cons (ProjPair One) nil)) in Hleq12.
            simpl in Hleq12.
            simple refine (IHn tL tR1 _ (proj_pair false R One c1) (proj_pair false R One c) c0 _ _ _ _ _); eauto; try lia.
            + apply proj_pair_R_wf with (strong := false) (i := One) in Hwf1.
              assumption.
            + apply proj_pair_R_wf with (strong := false) (i := One) in Hwf2.
              assumption.
          - apply (proj_corr_monotonic R (List.cons (ProjPair Two) nil)) in Hleq12.
            simpl in Hleq12.
            simple refine (IHn tL tR2 _ (proj_pair false R Two c1) (proj_pair false R Two c) c2 _ _ _ _ _); eauto; try lia.
            + apply proj_pair_R_wf with (strong := false) (i := Two) in Hwf1.
              assumption.
            + apply proj_pair_R_wf with (strong := false) (i := Two) in Hwf2.
              assumption.
        }
    + simpl in Hwf3.
      destruct s; [ destruct tL | destruct tR ]; try contradiction;
        destruct Hwf3 as [Hwf31 Hwf32]; simpl in Hn.
      × { constructor.
          - apply (proj_corr_monotonic L (List.cons (ProjSum One) nil)) in Hleq12.
            simpl in Hleq12.
            simple refine (IHn tL1 tR _ (proj_sum false L One c1) (proj_sum false L One c) c0 _ _ _ _ _); eauto; try lia.
            + apply proj_sum_L_wf with (strong := false) (i := One) in Hwf1.
              assumption.
            + apply proj_sum_L_wf with (strong := false) (i := One) in Hwf2.
              assumption.
          - apply (proj_corr_monotonic L (List.cons (ProjSum Two) nil)) in Hleq12.
            simpl in Hleq12.
            simple refine (IHn tL2 tR _ (proj_sum false L Two c1) (proj_sum false L Two c) c2 _ _ _ _ _); eauto; try lia.
            + apply proj_sum_L_wf with (strong := false) (i := Two) in Hwf1.
              assumption.
            + apply proj_sum_L_wf with (strong := false) (i := Two) in Hwf2.
              assumption.
        }
      × { constructor.
          - apply (proj_corr_monotonic R (List.cons (ProjSum One) nil)) in Hleq12.
            simpl in Hleq12.
            simple refine (IHn tL tR1 _ (proj_sum false R One c1) (proj_sum false R One c) c0 _ _ _ _ _); eauto; try lia.
            + apply proj_sum_R_wf with (strong := false) (i := One) in Hwf1.
              assumption.
            + apply proj_sum_R_wf with (strong := false) (i := One) in Hwf2.
              assumption.
          - apply (proj_corr_monotonic R (List.cons (ProjSum Two) nil)) in Hleq12.
            simpl in Hleq12.
            simple refine (IHn tL tR2 _ (proj_sum false R Two c1) (proj_sum false R Two c) c2 _ _ _ _ _); eauto; try lia.
            + apply proj_sum_R_wf with (strong := false) (i := Two) in Hwf1.
              assumption.
            + apply proj_sum_R_wf with (strong := false) (i := Two) in Hwf2.
              assumption.
        }
    + inversion Hleq12; subst; [ apply CLeqBot |].
      simpl in Hwf1, Hwf2, Hwf3.
      destruct s; [ destruct tL | destruct tR ]; try contradiction;
        destruct Hwf1 as [Hwfarg1 [Hwfinner1 Hwfouter1]];
        destruct Hwf2 as [Hwfarg2 [Hwfinner2 Hwfouter2]];
        destruct Hwf3 as [Hwfarg3 [Hwfinner3 Hwfouter3]];
        simpl in Hn.
      × { constructor.
          - simple refine (IHn tL1 tR _ carg2 carg1 carg0 _ _ _ _ _); eauto. lia.
          - simple refine (IHn tL1 tL2 _ cinner0 cinner1 cinner2 _ _ _ _ _); eauto. lia.
          - simple refine (IHn tL2 tR _ couter0 couter1 couter2 _ _ _ _ _); eauto. lia.
        }
      × { constructor.
          - simple refine (IHn tL tR1 _ carg2 carg1 carg0 _ _ _ _ _); eauto. lia.
          - simple refine (IHn tR1 tR2 _ cinner0 cinner1 cinner2 _ _ _ _ _); eauto. lia.
          - simple refine (IHn tL tR2 _ couter0 couter1 couter2 _ _ _ _ _); eauto. lia.
        }
Qed.

Union of correlations

Specification of the union of correlations. This is Figure 14 of the ICFP'20 paper.
Inductive corr_union: corr → corr → corr → Prop :=
| CUnionTopL: ∀ c,
    corr_union c CTop CTop
| CUnionTopR: ∀ c,
    corr_union CTop c CTop
| CUnionBotL: ∀ c,
    corr_union c CBot c
| CUnionBotR: ∀ c,
    corr_union CBot c c
| CUnionEq:
    corr_union CEq CEq CEq
| CUnionPairL: ∀ s c1 c2 c c1' c2',
    corr_union c1 (proj_pair true s One c) c1' →
    corr_union c2 (proj_pair true s Two c) c2' →
    corr_union (CPair s c1 c2) c (CPair s c1' c2')
| CUnionPairR: ∀ s c1 c2 c c1' c2',
    corr_union (proj_pair true s One c) c1 c1' →
    corr_union (proj_pair true s Two c) c2 c2' →
    corr_union c (CPair s c1 c2) (CPair s c1' c2')
| CUnionSumL: ∀ s c1 c2 c c1' c2',
    corr_union c1 (proj_sum true s One c) c1' →
    corr_union c2 (proj_sum true s Two c) c2' →
    corr_union (CSum s c1 c2) c (CSum s c1' c2')
| CUnionSumR: ∀ s c1 c2 c c1' c2',
    corr_union (proj_sum true s One c) c1 c1' →
    corr_union (proj_sum true s Two c) c2 c2' →
    corr_union c (CSum s c1 c2) (CSum s c1' c2')
| CUnionFunLR_same_side_arg_left:
    ∀ s carg1 cinner1 couter1 carg2 cinner2 couter2 cinner couter,
    corr_leq carg1 carg2 →
    corr_union cinner1 cinner2 cinner →
    corr_union couter1 couter2 couter →
    corr_union (CFun s carg1 cinner1 couter1) (CFun s carg2 cinner2 couter2) (CFun s carg1 cinner couter)
| CUnionFunLR_same_side_arg_right:
    ∀ s carg1 cinner1 couter1 carg2 cinner2 couter2 cinner couter,
    corr_leq carg2 carg1 →
    corr_union cinner1 cinner2 cinner →
    corr_union couter1 couter2 couter →
    corr_union (CFun s carg1 cinner1 couter1) (CFun s carg2 cinner2 couter2) (CFun s carg2 cinner couter)
| CUnionFunLR_same_side_other:
    ∀ s carg1 cinner1 couter1 carg2 cinner2 couter2,
      not (corr_leq carg1 carg2) →
      not (corr_leq carg2 carg1) →
      corr_union (CFun s carg1 cinner1 couter1) (CFun s carg2 cinner2 couter2) CTop
| CUnionFunLR_other_side:
    ∀ s1 carg1 cinner1 couter1 s2 carg2 cinner2 couter2,
      s1 ≠ s2 →
      corr_union (CFun s1 carg1 cinner1 couter1) (CFun s2 carg2 cinner2 couter2) CTop
| CUnionFunEq: ∀ s carg cinner couter,
    corr_union (CFun s carg cinner couter) CEq CTop
| CUnionEqFun: ∀ s carg cinner couter,
    corr_union CEq (CFun s carg cinner couter) CTop
.

flip_corr commutes with corr_union.
Lemma flip_corr_union c1 c2 c3:
  corr_union c1 c2 c3 →
  corr_union (flip_corr c1) (flip_corr c2) (flip_corr c3).
Proof.
  intro H.
  induction H; simpl;
    try solve [ constructor;
                try rewrite proj_pair_flip in × |-;
                try rewrite proj_sum_flip in × |-;
                try (apply corr_leq_flip; try rewrite flip_corr_involution; simpl);
                auto ].
  - constructor; auto.
    apply corr_leq_flip in H. assumption.
  - constructor; auto.
    apply corr_leq_flip in H. assumption.
  - constructor; auto.
    + rewrite <- corr_leq_flip. assumption.
    + rewrite <- corr_leq_flip. assumption.
  - constructor; auto using flip_side_injective.
Qed.

The union of a correlation c with itself is c. (This is a sanity check)
Lemma corr_union_self c:
  corr_union c c c.
Proof.
  induction c;
    try solve [ constructor; auto using corr_leq_refl
              | constructor; simpl; (destruct (side_eq_dec s s); try contradiction); assumption
              ].
Qed.

Typing lemma for corr_union.
Lemma union_corr_wf tL tR c1 c2 c:
  corr_union c1 c2 c →
  wf_corr c1 tL tR →
  wf_corr c2 tL tR →
  wf_corr c tL tR.
Proof.
  intro H. revert tL tR.
  induction H; intros tL tR Hwf1 Hwf2; simpl in *;
    try solve [ auto
              | destruct s; constructor; tauto
              | destruct s; [ destruct tL | destruct tR ]; try tauto; intuition
              ].
  - destruct s; [ destruct tL | destruct tR ]; try tauto; intuition.
    + apply IHcorr_union1; auto.
      eapply proj_pair_L_wf with (i := One); eauto.
    + apply IHcorr_union2; auto.
      eapply proj_pair_L_wf with (i := Two); eauto.
    + apply IHcorr_union1; auto.
      eapply proj_pair_R_wf with (i := One); eauto.
    + apply IHcorr_union2; auto.
      eapply proj_pair_R_wf with (i := Two); eauto.
  - destruct s; [ destruct tL | destruct tR ]; try tauto; intuition.
    + apply IHcorr_union1; auto.
      eapply proj_pair_L_wf with (i := One); eauto.
    + apply IHcorr_union2; auto.
      eapply proj_pair_L_wf with (i := Two); eauto.
    + apply IHcorr_union1; auto.
      eapply proj_pair_R_wf with (i := One); eauto.
    + apply IHcorr_union2; auto.
      eapply proj_pair_R_wf with (i := Two); eauto.
  - destruct s; [ destruct tL | destruct tR ]; try tauto; intuition.
    + apply IHcorr_union1; auto.
      eapply proj_sum_L_wf with (i := One); eauto.
    + apply IHcorr_union2; auto.
      eapply proj_sum_L_wf with (i := Two); eauto.
    + apply IHcorr_union1; auto.
      eapply proj_sum_R_wf with (i := One); eauto.
    + apply IHcorr_union2; auto.
      eapply proj_sum_R_wf with (i := Two); eauto.
  - destruct s; [ destruct tL | destruct tR ]; try tauto; intuition.
    + apply IHcorr_union1; auto.
      eapply proj_sum_L_wf with (i := One); eauto.
    + apply IHcorr_union2; auto.
      eapply proj_sum_L_wf with (i := Two); eauto.
    + apply IHcorr_union1; auto.
      eapply proj_sum_R_wf with (i := One); eauto.
    + apply IHcorr_union2; auto.
      eapply proj_sum_R_wf with (i := Two); eauto.
Qed.

Intermediate semantic lemmas used in the correctness of union

Commutation lemma for the union of a left-sided pair relation.
Lemma RelPairL_union R1 R2 R ty1 ty2 ty:
  good_vrel R →
  RelIncl R (RelTyped (TPair ty1 ty2) ty) →
  RelIncl
    (RelUnion (RelPairL R1 R2) R)
    (RelPairL
       (RelUnion R1 (RelCompose (RelPairR RelEqVal RelTopVal) R))
       (RelUnion R2 (RelCompose (RelPairR RelTopVal RelEqVal) R))).
Proof.
  intros Hgood Hincl v1 v2 [H|H].
  - destruct v1; simpl in H; try contradiction. destruct H as [H1 H2].
    split; left; assumption.
  - assert (good_value v1) as Hv1good by eauto.
    assert (is_value v1) as Hv1val.
    { unfold good_value in Hv1good. tauto. }
    assert (wf_term nil v1 (TPair ty1 ty2)) as Hv1wf.
    { apply Hincl in H. simpl in H. tauto. }
    destruct v1; simpl in Hv1val; try contradiction; inversion Hv1wf; subst.
    assert (good_value v1_1) by eauto using good_value_Pair_inv_L.
    assert (good_value v1_2) by eauto using good_value_Pair_inv_R.
    split; right; ∃ (Pair v1_1 v1_2); simpl; tauto.
Qed.

Commutation lemma for the union of a right-sided pair relation.
Lemma RelPairR_union R1 R2 R ty ty1 ty2:
  good_vrel R →
  RelIncl R (RelTyped ty (TPair ty1 ty2)) →
  RelIncl
    (RelUnion (RelPairR R1 R2) R)
    (RelPairR
       (RelUnion R1 (RelCompose R (RelPairL RelEqVal RelTopVal)))
       (RelUnion R2 (RelCompose R (RelPairL RelTopVal RelEqVal)))).
Proof.
  intros Hgood Hincl.
  apply RelInv_RelIncl.
  rewrite RelInv_RelUnion. rewrite RelInv_RelPairR.
  rewrite RelInv_RelPairR. repeat rewrite RelInv_RelUnion.
  repeat rewrite RelInv_RelCompose.
  repeat rewrite RelInv_RelPairL.
  repeat rewrite RelInv_RelEqVal.
  repeat rewrite RelInv_RelTopVal.
  apply (RelPairL_union _ _ _ ty1 ty2 ty).
  - rewrite <- RelInv_good_vrel. assumption.
  - apply RelInv_RelIncl in Hincl.
    rewrite RelInv_RelTyped in Hincl.
    assumption.
Qed.

Commutation lemma for the union of a left-sided sum relation.
Lemma RelSumL_union R1 R2 R ty1 ty2 ty:
  good_vrel R →
  RelIncl R (RelTyped (TSum ty1 ty2) ty) →
  RelIncl
    (RelUnion (RelSumL R1 R2) R)
    (RelSumL
       (RelUnion R1 (RelCompose (RelSumR RelEqVal RelBot) R))
       (RelUnion R2 (RelCompose (RelSumR RelBot RelEqVal) R))).
Proof.
  intros Hgood Hincl v1 v2 [H|H].
  - destruct v1; simpl in H; try contradiction; left; assumption.
  - assert (good_value v1) as Hv1good by eauto.
    assert (is_value v1) as Hv1val.
    { unfold good_value in Hv1good. tauto. }
    assert (wf_term nil v1 (TSum ty1 ty2)) as Hv1wf.
    { apply Hincl in H. simpl in H. tauto. }
    destruct v1; simpl in Hv1val; try contradiction; inversion Hv1wf; subst.
    + assert (good_value v1) by eauto using good_value_InjL_inv.
      right. ∃ (InjL v1). simpl. tauto.
    + assert (good_value v1) by eauto using good_value_InjR_inv.
      right. ∃ (InjR v1). simpl. tauto.
Qed.

Commutation lemma for the union of a right-sided sum relation.
Lemma RelSumR_union R1 R2 R ty ty1 ty2:
  good_vrel R →
  RelIncl R (RelTyped ty (TSum ty1 ty2)) →
  RelIncl
    (RelUnion (RelSumR R1 R2) R)
    (RelSumR
       (RelUnion R1 (RelCompose R (RelSumL RelEqVal RelBot)))
       (RelUnion R2 (RelCompose R (RelSumL RelBot RelEqVal)))).
Proof.
  intros Hgood Hincl.
  apply RelInv_RelIncl.
  rewrite RelInv_RelUnion. rewrite RelInv_RelSumR.
  rewrite RelInv_RelSumR. repeat rewrite RelInv_RelUnion.
  repeat rewrite RelInv_RelCompose.
  repeat rewrite RelInv_RelSumL.
  repeat rewrite RelInv_RelEqVal.
  repeat rewrite RelInv_RelTopVal.
  apply (RelSumL_union _ _ _ ty1 ty2 ty).
  - rewrite <- RelInv_good_vrel. assumption.
  - apply RelInv_RelIncl in Hincl.
    rewrite RelInv_RelTyped in Hincl.
    assumption.
Qed.

Commutation lemma for the union of a left-sided function relation.
Lemma RelFUNvL_union Rarg Rarg1 Rarg2 Rinner1 Rinner2 Router1 Router2:
  RelIncl Rarg Rarg1 →
  RelIncl Rarg Rarg2 →
  RelIncl
    (RelUnion (FUNvL Rarg1 Rinner1 Router1) (FUNvL Rarg2 Rinner2 Router2))
    (FUNvL Rarg (RelUnion Rinner1 Rinner2) (RelUnion Router1 Router2)).
Proof.
  intros H1 H2 v1 v2 [[Hgood1 [Hgood2 Hfun]] | [Hgood1 [Hgood2 Hfun]]];
    (split; [ assumption | split; [ assumption |]]);
    intros w1 w2 Happ Harg.
  - apply H1 in Harg. specialize (Hfun _ _ Happ Harg). simpl. tauto.
  - apply H2 in Harg. specialize (Hfun _ _ Happ Harg). simpl. tauto.
Qed.

Commutation lemma for the union of a right-sided function relation.
Lemma RelFUNvR_union Rarg Rarg1 Rarg2 Rinner1 Rinner2 Router1 Router2:
  RelIncl Rarg Rarg1 →
  RelIncl Rarg Rarg2 →
  RelIncl
    (RelUnion (FUNvR Rarg1 Rinner1 Router1) (FUNvR Rarg2 Rinner2 Router2))
    (FUNvR Rarg (RelUnion Rinner1 Rinner2) (RelUnion Router1 Router2)).
Proof.
  intros H1 H2. apply RelInv_RelIncl.
  rewrite RelInv_RelUnion.
  repeat rewrite RelInv_FUNvR.
  rewrite RelInv_RelUnion.
  apply RelFUNvL_union; rewrite <- RelInv_RelIncl; assumption.
Qed.

Correctness of union

Correctness lemma for corr_union. This is bullet 1 of Lemma 5.9 of the ICFP'20 paper.
Lemma concretize_corr_union tL tR c1 c2 c:
  wf_corr c1 tL tR →
  wf_corr c2 tL tR →
  corr_union c1 c2 c →
  RelIncl
    (RelUnion (concretize_corr tL tR c1) (concretize_corr tL tR c2))
    (concretize_corr tL tR c).
Proof.
  intros Hwf1 Hwf2 H. revert tL tR Hwf1 Hwf2. induction H; intros tL tR Hwf1 Hwf2.
  - apply RelUnion_lub; [| reflexivity ].
    apply concretize_corr_leq; auto. constructor.
  - apply RelUnion_lub; [ reflexivity |].
    apply concretize_corr_leq; auto. constructor.
  - apply RelBot_neutral_union_right.
  - apply RelBot_neutral_union_left.
  - apply RelUnion_self.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_union1; [ | tauto | eapply proj_pair_L_wf with (i := One); eauto ].
      rewrite <- concretize_corr_proj_pair_L with (ty1R := tL2) (i := One).
      rewrite <- IHcorr_union2; [ | tauto | eapply proj_pair_L_wf with (i := Two); eauto ].
      rewrite <- concretize_corr_proj_pair_L with (ty1L := tL1) (i := Two).
      eapply RelPairL_union; eauto using concretize_corr_good, concretize_corr_typed.
    + rewrite <- IHcorr_union1; [ | tauto | eapply proj_pair_R_wf with (i := One); eauto ].
      rewrite <- concretize_corr_proj_pair_R with (ty2R := tR2) (i := One).
      rewrite <- IHcorr_union2; [ | tauto | eapply proj_pair_R_wf with (i := Two); eauto ].
      rewrite <- concretize_corr_proj_pair_R with (ty2L := tR1) (i := Two).
      eapply RelPairR_union; eauto using concretize_corr_good, concretize_corr_typed.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_union1; [ | eapply proj_pair_L_wf with (i := One); eauto | tauto ].
      rewrite <- concretize_corr_proj_pair_L with (ty1R := tL2) (i := One).
      rewrite <- IHcorr_union2; [ | eapply proj_pair_L_wf with (i := Two); eauto | tauto ].
      rewrite <- concretize_corr_proj_pair_L with (ty1L := tL1) (i := Two).
      rewrite RelUnion_comm at 1.
      rewrite RelPairL_union; eauto using concretize_corr_good, concretize_corr_typed.
      apply RelPairL_morphism_incl; rewrite RelUnion_comm; reflexivity.
    + rewrite <- IHcorr_union1; [ | eapply proj_pair_R_wf with (i := One); eauto | tauto ].
      rewrite <- concretize_corr_proj_pair_R with (ty2R := tR2) (i := One).
      rewrite <- IHcorr_union2; [ | eapply proj_pair_R_wf with (i := Two); eauto | tauto ].
      rewrite <- concretize_corr_proj_pair_R with (ty2L := tR1) (i := Two).
      rewrite RelUnion_comm at 1.
      rewrite RelPairR_union; eauto using concretize_corr_good, concretize_corr_typed.
      apply RelPairR_morphism_incl; rewrite RelUnion_comm; reflexivity.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_union1; [ | tauto | eapply proj_sum_L_wf with (i := One); eauto ].
      rewrite <- concretize_corr_proj_sum_L with (ty1R := tL2) (i := One).
      rewrite <- IHcorr_union2; [ | tauto | eapply proj_sum_L_wf with (i := Two); eauto ].
      rewrite <- concretize_corr_proj_sum_L with (ty1L := tL1) (i := Two).
      eapply RelSumL_union; eauto using concretize_corr_good, concretize_corr_typed.
    + rewrite <- IHcorr_union1; [ | tauto | eapply proj_sum_R_wf with (i := One); eauto ].
      rewrite <- concretize_corr_proj_sum_R with (ty2R := tR2) (i := One).
      rewrite <- IHcorr_union2; [ | tauto | eapply proj_sum_R_wf with (i := Two); eauto ].
      rewrite <- concretize_corr_proj_sum_R with (ty2L := tR1) (i := Two).
      eapply RelSumR_union; eauto using concretize_corr_good, concretize_corr_typed.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_union1; [ | eapply proj_sum_L_wf with (i := One); eauto | tauto ].
      rewrite <- concretize_corr_proj_sum_L with (ty1R := tL2) (i := One).
      rewrite <- IHcorr_union2; [ | eapply proj_sum_L_wf with (i := Two); eauto | tauto ].
      rewrite <- concretize_corr_proj_sum_L with (ty1L := tL1) (i := Two).
      rewrite RelUnion_comm at 1.
      rewrite RelSumL_union; eauto using concretize_corr_good, concretize_corr_typed.
      apply RelSumL_morphism_incl; rewrite RelUnion_comm; reflexivity.
    + rewrite <- IHcorr_union1; [ | eapply proj_sum_R_wf with (i := One); eauto | tauto ].
      rewrite <- concretize_corr_proj_sum_R with (ty2R := tR2) (i := One).
      rewrite <- IHcorr_union2; [ | eapply proj_sum_R_wf with (i := Two); eauto | tauto ].
      rewrite <- concretize_corr_proj_sum_R with (ty2L := tR1) (i := Two).
      rewrite RelUnion_comm at 1.
      rewrite RelSumR_union; eauto using concretize_corr_good, concretize_corr_typed.
      apply RelSumR_morphism_incl; rewrite RelUnion_comm; reflexivity.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_union1; [ | tauto | tauto ].
      rewrite <- IHcorr_union2; [ | tauto | tauto ].
      rewrite <- RelInter_RelUnion_distrib_right.
      rewrite RelFUNvL_union.
      × reflexivity.
      × reflexivity.
      × apply concretize_corr_leq; tauto.
    + rewrite <- IHcorr_union1; [ | tauto | tauto ].
      rewrite <- IHcorr_union2; [ | tauto | tauto ].
      rewrite <- RelInter_RelUnion_distrib_right.
      rewrite RelFUNvR_union.
      × reflexivity.
      × reflexivity.
      × apply concretize_corr_leq; tauto.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_union1; [ | tauto | tauto ].
      rewrite <- IHcorr_union2; [ | tauto | tauto ].
      rewrite <- RelInter_RelUnion_distrib_right.
      rewrite RelFUNvL_union.
      × reflexivity.
      × apply concretize_corr_leq; tauto.
      × reflexivity.
    + rewrite <- IHcorr_union1; [ | tauto | tauto ].
      rewrite <- IHcorr_union2; [ | tauto | tauto ].
      rewrite <- RelInter_RelUnion_distrib_right.
      rewrite RelFUNvR_union.
      × reflexivity.
      × apply concretize_corr_leq; tauto.
      × reflexivity.
  - apply RelUnion_lub; apply concretize_corr_leq; auto; constructor.
  - apply RelUnion_lub; apply concretize_corr_leq; auto; constructor.
  - apply RelUnion_lub; apply concretize_corr_leq; auto; constructor.
  - apply RelUnion_lub; apply concretize_corr_leq; auto; constructor.
Qed.

Intersection of correlations

Specification of the intersection of correlations. This is Figure 15 of the ICFP'20 paper.
Inductive corr_inter: corr → corr → corr → Prop :=
| CInterTopL: ∀ c,
    corr_inter c CTop c
| CInterTopR: ∀ c,
    corr_inter CTop c c
| CInterBotL: ∀ c,
    corr_inter c CBot CBot
| CInterBotR: ∀ c,
    corr_inter CBot c CBot
| CInterEq:
    corr_inter CEq CEq CEq
| CInterPairL: ∀ s c1 c2 c c1' c2',
    corr_inter c1 (proj_pair true s One c) c1' →
    corr_inter c2 (proj_pair true s Two c) c2' →
    corr_inter (CPair s c1 c2) c (CPair s c1' c2')
| CInterPairR: ∀ s c1 c2 c c1' c2',
    corr_inter (proj_pair true s One c) c1 c1' →
    corr_inter (proj_pair true s Two c) c2 c2' →
    corr_inter c (CPair s c1 c2) (CPair s c1' c2')
| CInterSumL: ∀ s c1 c2 c c1' c2',
    corr_inter c1 (proj_sum true s One c) c1' →
    corr_inter c2 (proj_sum true s Two c) c2' →
    corr_inter (CSum s c1 c2) c (CSum s c1' c2')
| CInterSumR: ∀ s c1 c2 c c1' c2',
    corr_inter (proj_sum true s One c) c1 c1' →
    corr_inter (proj_sum true s Two c) c2 c2' →
    corr_inter c (CSum s c1 c2) (CSum s c1' c2')
| CInterFunLR_same_side_arg_left:
    ∀ s carg1 cinner1 couter1 carg2 cinner2 couter2 cinner couter,
    corr_leq carg1 carg2 →
    corr_inter cinner1 cinner2 cinner →
    corr_inter couter1 couter2 couter →
    corr_inter (CFun s carg1 cinner1 couter1) (CFun s carg2 cinner2 couter2) (CFun s carg1 cinner couter)
| CInterFunLR_same_side_arg_right:
    ∀ s carg1 cinner1 couter1 carg2 cinner2 couter2 cinner couter,
    corr_leq carg2 carg1 →
    corr_inter cinner1 cinner2 cinner →
    corr_inter couter1 couter2 couter →
    corr_inter (CFun s carg1 cinner1 couter1) (CFun s carg2 cinner2 couter2) (CFun s carg2 cinner couter)
| CInterFunLR_same_side_other:
    ∀ s carg1 cinner1 couter1 carg2 cinner2 couter2,
      not (corr_leq carg1 carg2) →
      not (corr_leq carg2 carg1) →
      corr_inter (CFun s carg1 cinner1 couter1) (CFun s carg2 cinner2 couter2) CTop
| CInterFunLR_other_side:
    ∀ s1 carg1 cinner1 couter1 s2 carg2 cinner2 couter2,
      s1 ≠ s2 →
      corr_inter (CFun s1 carg1 cinner1 couter1) (CFun s2 carg2 cinner2 couter2) CTop
| CInterFunEq: ∀ s carg cinner couter,
    corr_inter (CFun s carg cinner couter) CEq (CFun s carg cinner couter)
| CInterEqFun: ∀ s carg cinner couter,
    corr_inter CEq (CFun s carg cinner couter) (CFun s carg cinner couter)
.

flip_corr commutes with corr_inter.
Lemma flip_corr_inter c1 c2 c3:
  corr_inter c1 c2 c3 →
  corr_inter (flip_corr c1) (flip_corr c2) (flip_corr c3).
Proof.
  intro H.
  induction H; simpl;
    try solve [ constructor;
                try rewrite proj_pair_flip in × |-;
                try rewrite proj_sum_flip in × |-;
                try (apply corr_leq_flip; try rewrite flip_corr_involution; simpl);
                auto ].
  - constructor; auto.
    apply corr_leq_flip in H. assumption.
  - constructor; auto.
    apply corr_leq_flip in H. assumption.
  - constructor; auto.
    + rewrite <- corr_leq_flip. assumption.
    + rewrite <- corr_leq_flip. assumption.
  - constructor; auto using flip_side_injective.
Qed.

The intersection of a correlation c with itself is c. (This is a sanity check)
Lemma corr_inter_self c:
  corr_inter c c c.
Proof.
  induction c;
    try solve [ constructor; auto using corr_leq_refl
              | constructor; simpl; (destruct (side_eq_dec s s); try contradiction); assumption
              ].
Qed.

Typing lemma for corr_inter.
Lemma inter_corr_wf tL tR c1 c2 c:
  corr_inter c1 c2 c →
  wf_corr c1 tL tR →
  wf_corr c2 tL tR →
  wf_corr c tL tR.
Proof.
  intro H. revert tL tR.
  induction H; intros tL tR Hwf1 Hwf2; simpl in *;
    try solve [ auto
              | destruct s; constructor; tauto
              | destruct s; [ destruct tL | destruct tR ]; try tauto; intuition
              ].
  - destruct s; [ destruct tL | destruct tR ]; try tauto; intuition.
    + apply IHcorr_inter1; auto.
      eapply proj_pair_L_wf with (i := One); eauto.
    + apply IHcorr_inter2; auto.
      eapply proj_pair_L_wf with (i := Two); eauto.
    + apply IHcorr_inter1; auto.
      eapply proj_pair_R_wf with (i := One); eauto.
    + apply IHcorr_inter2; auto.
      eapply proj_pair_R_wf with (i := Two); eauto.
  - destruct s; [ destruct tL | destruct tR ]; try tauto; intuition.
    + apply IHcorr_inter1; auto.
      eapply proj_pair_L_wf with (i := One); eauto.
    + apply IHcorr_inter2; auto.
      eapply proj_pair_L_wf with (i := Two); eauto.
    + apply IHcorr_inter1; auto.
      eapply proj_pair_R_wf with (i := One); eauto.
    + apply IHcorr_inter2; auto.
      eapply proj_pair_R_wf with (i := Two); eauto.
  - destruct s; [ destruct tL | destruct tR ]; try tauto; intuition.
    + apply IHcorr_inter1; auto.
      eapply proj_sum_L_wf with (i := One); eauto.
    + apply IHcorr_inter2; auto.
      eapply proj_sum_L_wf with (i := Two); eauto.
    + apply IHcorr_inter1; auto.
      eapply proj_sum_R_wf with (i := One); eauto.
    + apply IHcorr_inter2; auto.
      eapply proj_sum_R_wf with (i := Two); eauto.
  - destruct s; [ destruct tL | destruct tR ]; try tauto; intuition.
    + apply IHcorr_inter1; auto.
      eapply proj_sum_L_wf with (i := One); eauto.
    + apply IHcorr_inter2; auto.
      eapply proj_sum_L_wf with (i := Two); eauto.
    + apply IHcorr_inter1; auto.
      eapply proj_sum_R_wf with (i := One); eauto.
    + apply IHcorr_inter2; auto.
      eapply proj_sum_R_wf with (i := Two); eauto.
Qed.

Intermediate semantic lemmas used in the correctness of intersection

Commutation lemma for the intersection of a left-sided pair relation.
Lemma RelPairL_inter R1 R2 R ty1 ty2 ty:
  good_vrel R →
  RelIncl R (RelTyped (TPair ty1 ty2) ty) →
  RelIncl
    (RelInter (RelPairL R1 R2) R)
    (RelPairL
       (RelInter R1 (RelCompose (RelPairR RelEqVal RelTopVal) R))
       (RelInter R2 (RelCompose (RelPairR RelTopVal RelEqVal) R))).
Proof.
  intros Hgood Hincl v1 v2 [Hty HR].
  assert (good_value v1) as Hv1good by eauto.
  assert (is_value v1) as Hv1val.
  { unfold good_value in Hv1good. tauto. }
  assert (wf_term nil v1 (TPair ty1 ty2)) as Hv1wf.
  { apply Hincl in HR. simpl in HR. tauto. }
  destruct v1; simpl in Hty; try contradiction. destruct Hty as [H1 H2].
  assert (good_value v1_1) by eauto using good_value_Pair_inv_L.
  assert (good_value v1_2) by eauto using good_value_Pair_inv_R.
  split; split; auto; ∃ (Pair v1_1 v1_2); simpl; tauto.
Qed.

Commutation lemma for the intersection of a right-sided pair relation.
Lemma RelPairR_inter R1 R2 R ty ty1 ty2:
  good_vrel R →
  RelIncl R (RelTyped ty (TPair ty1 ty2)) →
  RelIncl
    (RelInter (RelPairR R1 R2) R)
    (RelPairR
       (RelInter R1 (RelCompose R (RelPairL RelEqVal RelTopVal)))
       (RelInter R2 (RelCompose R (RelPairL RelTopVal RelEqVal)))).
Proof.
  intros Hgood Hincl.
  apply RelInv_RelIncl.
  rewrite RelInv_RelInter. rewrite RelInv_RelPairR.
  rewrite RelInv_RelPairR. repeat rewrite RelInv_RelInter.
  repeat rewrite RelInv_RelCompose.
  repeat rewrite RelInv_RelPairL.
  repeat rewrite RelInv_RelEqVal.
  repeat rewrite RelInv_RelTopVal.
  apply (RelPairL_inter _ _ _ ty1 ty2 ty).
  - rewrite <- RelInv_good_vrel. assumption.
  - apply RelInv_RelIncl in Hincl.
    rewrite RelInv_RelTyped in Hincl.
    assumption.
Qed.

Commutation lemma for the intersection of a left-sided sum relation.
Lemma RelSumL_inter R1 R2 R ty1 ty2 ty:
  good_vrel R →
  RelIncl R (RelTyped (TSum ty1 ty2) ty) →
  RelIncl
    (RelInter (RelSumL R1 R2) R)
    (RelSumL
       (RelInter R1 (RelCompose (RelSumR RelEqVal RelBot) R))
       (RelInter R2 (RelCompose (RelSumR RelBot RelEqVal) R))).
Proof.
  intros Hgood Hincl v1 v2 [Hty HR].
  assert (good_value v1) as Hv1good by eauto.
  assert (is_value v1) as Hv1val.
  { unfold good_value in Hv1good. tauto. }
  assert (wf_term nil v1 (TSum ty1 ty2)) as Hv1wf.
  { apply Hincl in HR. simpl in HR. tauto. }
  destruct v1; simpl in Hv1val; try contradiction; inversion Hv1wf; subst.
  - assert (good_value v1) by eauto using good_value_InjL_inv.
    split; auto. ∃ (InjL v1). simpl. tauto.
  - assert (good_value v1) by eauto using good_value_InjR_inv.
    split; auto. ∃ (InjR v1). simpl. tauto.
Qed.

Commutation lemma for the intersection of a right-sided sum relation.
Lemma RelSumR_inter R1 R2 R ty ty1 ty2:
  good_vrel R →
  RelIncl R (RelTyped ty (TSum ty1 ty2)) →
  RelIncl
    (RelInter (RelSumR R1 R2) R)
    (RelSumR
       (RelInter R1 (RelCompose R (RelSumL RelEqVal RelBot)))
       (RelInter R2 (RelCompose R (RelSumL RelBot RelEqVal)))).
Proof.
  intros Hgood Hincl.
  apply RelInv_RelIncl.
  rewrite RelInv_RelInter. rewrite RelInv_RelSumR.
  rewrite RelInv_RelSumR. repeat rewrite RelInv_RelInter.
  repeat rewrite RelInv_RelCompose.
  repeat rewrite RelInv_RelSumL.
  repeat rewrite RelInv_RelEqVal.
  repeat rewrite RelInv_RelTopVal.
  apply (RelSumL_inter _ _ _ ty1 ty2 ty).
  - rewrite <- RelInv_good_vrel. assumption.
  - apply RelInv_RelIncl in Hincl.
    rewrite RelInv_RelTyped in Hincl.
    assumption.
Qed.

Commutation lemma for the intersection of a left-sided function relation.
Lemma RelFUNvL_inter Rarg Rarg1 Rarg2 Rinner1 Rinner2 Router1 Router2:
  RelIncl Rarg Rarg1 →
  RelIncl Rarg Rarg2 →
  RelIncl
    (RelInter (FUNvL Rarg1 Rinner1 Router1) (FUNvL Rarg2 Rinner2 Router2))
    (FUNvL Rarg (RelInter Rinner1 Rinner2) (RelInter Router1 Router2)).
Proof.
  intros H1 H2 v1 v2 [[Hgood11 [Hgood12 Hfun1]] [Hgood21 [Hgood22 Hfun2]]];
    (split; [ assumption | split; [ assumption |]]);
    intros w1 w2 Happ Harg. split; split.
  - apply H1 in Harg. specialize (Hfun1 _ _ Happ Harg). tauto.
  - apply H2 in Harg. specialize (Hfun2 _ _ Happ Harg). tauto.
  - apply H1 in Harg. specialize (Hfun1 _ _ Happ Harg). tauto.
  - apply H2 in Harg. specialize (Hfun2 _ _ Happ Harg). tauto.
Qed.

Commutation lemma for the intersection of a right-sided function relation.
Lemma RelFUNvR_inter Rarg Rarg1 Rarg2 Rinner1 Rinner2 Router1 Router2:
  RelIncl Rarg Rarg1 →
  RelIncl Rarg Rarg2 →
  RelIncl
    (RelInter (FUNvR Rarg1 Rinner1 Router1) (FUNvR Rarg2 Rinner2 Router2))
    (FUNvR Rarg (RelInter Rinner1 Rinner2) (RelInter Router1 Router2)).
Proof.
  intros H1 H2. apply RelInv_RelIncl.
  rewrite RelInv_RelInter.
  repeat rewrite RelInv_FUNvR.
  rewrite RelInv_RelInter.
  apply RelFUNvL_inter; rewrite <- RelInv_RelIncl; assumption.
Qed.

Correctness of intersection

Correctness lemma for corr_inter. This is bullet 2 of Lemma 5.9 of the ICFP'20 paper.
Lemma concretize_corr_inter tL tR c1 c2 c:
  wf_corr c1 tL tR →
  wf_corr c2 tL tR →
  corr_inter c1 c2 c →
  RelIncl
    (RelInter (concretize_corr tL tR c1) (concretize_corr tL tR c2))
    (concretize_corr tL tR c).
Proof.
  intros Hwf1 Hwf2 H. revert tL tR Hwf1 Hwf2. induction H; intros tL tR Hwf1 Hwf2.
  - apply RelInter_lb1.
  - apply RelInter_lb2.
  - apply RelInter_lb2.
  - apply RelInter_lb1.
  - apply RelInter_lb1.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_inter1; [ | tauto | eapply proj_pair_L_wf with (i := One); eauto ].
      rewrite <- concretize_corr_proj_pair_L with (ty1R := tL2) (i := One).
      rewrite <- IHcorr_inter2; [ | tauto | eapply proj_pair_L_wf with (i := Two); eauto ].
      rewrite <- concretize_corr_proj_pair_L with (ty1L := tL1) (i := Two).
      eapply RelPairL_inter; eauto using concretize_corr_good, concretize_corr_typed.
    + rewrite <- IHcorr_inter1; [ | tauto | eapply proj_pair_R_wf with (i := One); eauto ].
      rewrite <- concretize_corr_proj_pair_R with (ty2R := tR2) (i := One).
      rewrite <- IHcorr_inter2; [ | tauto | eapply proj_pair_R_wf with (i := Two); eauto ].
      rewrite <- concretize_corr_proj_pair_R with (ty2L := tR1) (i := Two).
      eapply RelPairR_inter; eauto using concretize_corr_good, concretize_corr_typed.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_inter1; [ | eapply proj_pair_L_wf with (i := One); eauto | tauto ].
      rewrite <- concretize_corr_proj_pair_L with (ty1R := tL2) (i := One).
      rewrite <- IHcorr_inter2; [ | eapply proj_pair_L_wf with (i := Two); eauto | tauto ].
      rewrite <- concretize_corr_proj_pair_L with (ty1L := tL1) (i := Two).
      rewrite RelInter_comm at 1.
      rewrite RelPairL_inter; eauto using concretize_corr_good, concretize_corr_typed.
      apply RelPairL_morphism_incl; rewrite RelInter_comm; reflexivity.
    + rewrite <- IHcorr_inter1; [ | eapply proj_pair_R_wf with (i := One); eauto | tauto ].
      rewrite <- concretize_corr_proj_pair_R with (ty2R := tR2) (i := One).
      rewrite <- IHcorr_inter2; [ | eapply proj_pair_R_wf with (i := Two); eauto | tauto ].
      rewrite <- concretize_corr_proj_pair_R with (ty2L := tR1) (i := Two).
      rewrite RelInter_comm at 1.
      rewrite RelPairR_inter; eauto using concretize_corr_good, concretize_corr_typed.
      apply RelPairR_morphism_incl; rewrite RelInter_comm; reflexivity.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_inter1; [ | tauto | eapply proj_sum_L_wf with (i := One); eauto ].
      rewrite <- concretize_corr_proj_sum_L with (ty1R := tL2) (i := One).
      rewrite <- IHcorr_inter2; [ | tauto | eapply proj_sum_L_wf with (i := Two); eauto ].
      rewrite <- concretize_corr_proj_sum_L with (ty1L := tL1) (i := Two).
      eapply RelSumL_inter; eauto using concretize_corr_good, concretize_corr_typed.
    + rewrite <- IHcorr_inter1; [ | tauto | eapply proj_sum_R_wf with (i := One); eauto ].
      rewrite <- concretize_corr_proj_sum_R with (ty2R := tR2) (i := One).
      rewrite <- IHcorr_inter2; [ | tauto | eapply proj_sum_R_wf with (i := Two); eauto ].
      rewrite <- concretize_corr_proj_sum_R with (ty2L := tR1) (i := Two).
      eapply RelSumR_inter; eauto using concretize_corr_good, concretize_corr_typed.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_inter1; [ | eapply proj_sum_L_wf with (i := One); eauto | tauto ].
      rewrite <- concretize_corr_proj_sum_L with (ty1R := tL2) (i := One).
      rewrite <- IHcorr_inter2; [ | eapply proj_sum_L_wf with (i := Two); eauto | tauto ].
      rewrite <- concretize_corr_proj_sum_L with (ty1L := tL1) (i := Two).
      rewrite RelInter_comm at 1.
      rewrite RelSumL_inter; eauto using concretize_corr_good, concretize_corr_typed.
      apply RelSumL_morphism_incl; rewrite RelInter_comm; reflexivity.
    + rewrite <- IHcorr_inter1; [ | eapply proj_sum_R_wf with (i := One); eauto | tauto ].
      rewrite <- concretize_corr_proj_sum_R with (ty2R := tR2) (i := One).
      rewrite <- IHcorr_inter2; [ | eapply proj_sum_R_wf with (i := Two); eauto | tauto ].
      rewrite <- concretize_corr_proj_sum_R with (ty2L := tR1) (i := Two).
      rewrite RelInter_comm at 1.
      rewrite RelSumR_inter; eauto using concretize_corr_good, concretize_corr_typed.
      apply RelSumR_morphism_incl; rewrite RelInter_comm; reflexivity.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_inter1; [ | tauto | tauto ].
      rewrite <- IHcorr_inter2; [ | tauto | tauto ].
      rewrite <- RelInter_RelInter_distrib_right.
      rewrite RelFUNvL_inter.
      × reflexivity.
      × reflexivity.
      × apply concretize_corr_leq; tauto.
    + rewrite <- IHcorr_inter1; [ | tauto | tauto ].
      rewrite <- IHcorr_inter2; [ | tauto | tauto ].
      rewrite <- RelInter_RelInter_distrib_right.
      rewrite RelFUNvR_inter.
      × reflexivity.
      × reflexivity.
      × apply concretize_corr_leq; tauto.
  - simpl. destruct s; [ destruct tL | destruct tR ]; simpl in *; try contradiction.
    + rewrite <- IHcorr_inter1; [ | tauto | tauto ].
      rewrite <- IHcorr_inter2; [ | tauto | tauto ].
      rewrite <- RelInter_RelInter_distrib_right.
      rewrite RelFUNvL_inter.
      × reflexivity.
      × apply concretize_corr_leq; tauto.
      × reflexivity.
    + rewrite <- IHcorr_inter1; [ | tauto | tauto ].
      rewrite <- IHcorr_inter2; [ | tauto | tauto ].
      rewrite <- RelInter_RelInter_distrib_right.
      rewrite RelFUNvR_inter.
      × reflexivity.
      × apply concretize_corr_leq; tauto.
      × reflexivity.
  - rewrite RelInter_lb1. apply concretize_corr_leq; auto; constructor.
  - rewrite RelInter_lb1. apply concretize_corr_leq; auto; constructor.
  - apply RelInter_lb1.
  - apply RelInter_lb2.
Qed.

Composition of correlations

Specification of the composition of correlations. This is Figure 16 of the ICFP'20 paper.
Inductive corr_compose: corr → corr → corr → Prop :=
| CComposeBotL: ∀ c,
    corr_compose CBot c CBot
| CComposeBotR: ∀ c,
    corr_compose c CBot CBot
| CComposeEqL: ∀ c,
    corr_compose CEq c c
| CComposeEqR: ∀ c,
    corr_compose c CEq c
| CComposeTop:
    corr_compose CTop CTop CTop
| CComposePairL: ∀ c1 c2 c c1' c2',
    corr_compose c1 c c1' →
    corr_compose c2 c c2' →
    corr_compose (CPair L c1 c2) c (CPair L c1' c2')
| CComposePairR: ∀ c c1 c2 c1' c2',
    corr_compose c c1 c1' →
    corr_compose c c2 c2' →
    corr_compose c (CPair R c1 c2) (CPair R c1' c2')
| CComposePair: ∀ cL1 cL2 cR1 cR2 c1 c2 c12,
    corr_compose cL1 cR1 c1 →
    corr_compose cL2 cR2 c2 →
    corr_inter c1 c2 c12 →
    corr_compose (CPair R cL1 cL2) (CPair L cR1 cR2) c12
| CComposePairTop: ∀ cL1 cL2 c1 c2 c12,
    corr_compose cL1 CTop c1 →
    corr_compose cL2 CTop c2 →
    corr_inter c1 c2 c12 →
    corr_compose (CPair R cL1 cL2) CTop c12
| CComposeTopPair: ∀ cR1 cR2 c1 c2 c12,
    corr_compose CTop cR1 c1 →
    corr_compose CTop cR2 c2 →
    corr_inter c1 c2 c12 →
    corr_compose CTop (CPair L cR1 cR2) c12
| CComposeSumL: ∀ c1 c2 c c1' c2',
    corr_compose c1 c c1' →
    corr_compose c2 c c2' →
    corr_compose (CSum L c1 c2) c (CSum L c1' c2')
| CComposeSumR: ∀ c c1 c2 c1' c2',
    corr_compose c c1 c1' →
    corr_compose c c2 c2' →
    corr_compose c (CSum R c1 c2) (CSum R c1' c2')
| CComposeSum: ∀ cL1 cL2 cR1 cR2 c1 c2 c12,
    corr_compose cL1 cR1 c1 →
    corr_compose cL2 cR2 c2 →
    corr_union c1 c2 c12 →
    corr_compose (CSum R cL1 cL2) (CSum L cR1 cR2) c12
| CComposeSumTop: ∀ cL1 cL2 c1 c2 c12,
    corr_compose cL1 CTop c1 →
    corr_compose cL2 CTop c2 →
    corr_union c1 c2 c12 →
    corr_compose (CSum R cL1 cL2) CTop c12
| CComposeTopSum: ∀ cR1 cR2 c1 c2 c12,
    corr_compose CTop cR1 c1 →
    corr_compose CTop cR2 c2 →
    corr_union c1 c2 c12 →
    corr_compose CTop (CSum L cR1 cR2) c12
| CComposeFunL_arg_good: ∀ carg cinner couter c carg' couter' carg'',
    corr_compose carg c carg' →
    corr_compose carg' (flip_corr c) carg'' →
    corr_leq carg'' carg →
    corr_compose couter c couter' →
    corr_compose (CFun L carg cinner couter) c (CFun L carg' cinner couter')
| CComposeFunL_arg_bad: ∀ carg cinner couter c carg' carg'',
    corr_compose carg c carg' →
    corr_compose carg' (flip_corr c) carg'' →
    not (corr_leq carg'' carg) →
    corr_compose (CFun L carg cinner couter) c CTop
| CComposeFunR_arg_good: ∀ c carg cinner couter carg' couter' carg'',
    corr_compose c carg carg' →
    corr_compose (flip_corr c) carg' carg'' →
    corr_leq carg'' carg →
    corr_compose c couter couter' →
    corr_compose c (CFun R carg cinner couter) (CFun R carg' cinner couter')
| CComposeFunR_arg_bad: ∀ c carg cinner couter carg' carg'',
    corr_compose c carg carg' →
    corr_compose (flip_corr c) carg' carg'' →
    not (corr_leq carg'' carg) →
    corr_compose c (CFun R carg cinner couter) CTop
| CComposeFun: ∀ carg1 cinner1 couter1 carg2 cinner2 couter2,
    corr_compose (CFun R carg1 cinner1 couter1) (CFun L carg2 cinner2 couter2) CTop
| CComposeFunTop: ∀ carg cinner couter,
    corr_compose (CFun R carg cinner couter) CTop CTop
| CComposeTopFun: ∀ carg cinner couter,
    corr_compose CTop (CFun L carg cinner couter) CTop
.

flip_corr commutes with corr_inter by reversing the arguments of the composition.
Lemma flip_corr_compose c1 c2 c3:
  corr_compose c1 c2 c3 →
  corr_compose (flip_corr c2) (flip_corr c1) (flip_corr c3).
Proof.
  intro H.
  induction H; simpl;
    try solve [ constructor; auto
              | econstructor; eauto using flip_corr_inter, flip_corr_union
              | econstructor; eauto; rewrite corr_leq_flip in H1; assumption
              ].
Qed.

Typing lemma for corr_compose.
Lemma compose_corr_wf tL tM tR c1 c2 c:
  corr_compose c1 c2 c →
  wf_corr c1 tL tM →
  wf_corr c2 tM tR →
  wf_corr c tL tR.
Proof.
  intro H. revert tL tM tR.
  induction H; intros tL tM tR Hwf1 Hwf2; simpl in *;
    try solve [ congruence
              | destruct tL; try contradiction; intuition eauto
              | destruct tR; try contradiction; intuition eauto
              | destruct tM; try contradiction;
                intuition eauto using inter_corr_wf, union_corr_wf
              ].
Qed.

Intermediate semantic lemmas used in the correctness of composition

The identity on values is smaller than the identity on terms.
Lemma RelEqVal_incl_RelEq:
  RelIncl RelEqVal RelEq.
Proof.
  intros v1 v2. simpl. tauto.
Qed.

The itendity of values is smaller than the full relation of values.
Lemma RelEqVal_incl_RelTopVal:
  RelIncl RelEqVal RelTopVal.
Proof.
  intros v1 v2. simpl. intros [? ?]; split; congruence.
Qed.

Composing the top relation for values is the top relation of values.
Lemma RelCompose_RelTopVal_self:
  RelEquiv (RelCompose RelTopVal RelTopVal) RelTopVal.
Proof.
  intros v1 v3; split; intro H.
  - destruct H as [v2 [H12 H23]]. simpl in ×. tauto.
  - ∃ v1. simpl in ×. tauto.
Qed.

Transitivity for the composition of the full typed relations. A sort of "Triangular inequality".
Lemma RelCompose_RelTyped t1 t2 t3:
  RelIncl (RelCompose (RelTyped t1 t2) (RelTyped t2 t3)) (RelTyped t1 t3).
Proof.
  intros v1 v3 [v2 [H12 H23]]. simpl in ×. tauto.
Qed.

Unfolding lemma for the composition on the LHS with a left-sided pair relation.
Lemma RelCompose_RelPairL {A B} (c1 c2: rel term A) (c: rel A B):
  RelIncl (RelCompose (RelPairL c1 c2) c)
          (RelPairL (RelCompose c1 c) (RelCompose c2 c)).
Proof.
  intros v1 v3 [v2 [H12 H]].
  destruct v1; simpl in H12; try contradiction.
  destruct H12 as [H1 H2]. split; ∃ v2; tauto.
Qed.

Unfolding lemma for the composition on the RHS with a right-sided pair relation.
Lemma RelCompose_RelPairR {A B} (c: rel A B) (c1 c2: rel B term):
  RelIncl (RelCompose c (RelPairR c1 c2))
          (RelPairR (RelCompose c c1) (RelCompose c c2)).
Proof.
  intros v1 v3 [v2 [H H23]].
  destruct v3; simpl in H23; try contradiction.
  destruct H23 as [H2 H3]. split; ∃ v2; tauto.
Qed.

Unfolding lemma for the composition of a right-sided pair relation with a left-sided pair relation.
Lemma RelCompose_RelPairR_RelPairL {A B} (c1 c2: rel A term) (c3 c4: rel term B):
  RelIncl (RelCompose (RelPairR c1 c2) (RelPairL c3 c4))
          (RelInter (RelCompose c1 c3) (RelCompose c2 c4)).
Proof.
  intros v1 v3 [v2 [H12 H23]]. destruct v2; simpl in H12, H23; try contradiction.
  split.
  - ∃ v2_1. tauto.
  - ∃ v2_2. tauto.
Qed.

Simplification for the left-sided pair corrrelation with CTop.
Lemma RelPairL_top_top tL1 tL2 tR:
  RelEquiv (RelInter RelTopVal (RelTyped (TPair tL1 tL2) tR))
           (RelPairL (concretize_corr tL1 tR CTop) (concretize_corr tL2 tR CTop)).
Proof.
  intros v1 v2. split; intro H.
  - destruct H as [[Hgood1 Hgood2] [Hwf1 Hwf2]].
    assert (is_value v1) as Hval1 by auto.
    destruct v1; simpl in Hval1; try contradiction; inversion Hwf1; subst.
    assert (good_value v1_1) by eauto using good_value_Pair_inv_L.
    assert (good_value v1_2) by eauto using good_value_Pair_inv_R.
    simpl. tauto.
  - destruct v1; simpl in H; try contradiction.
    simpl. intuition auto with good_rel.
    constructor; assumption.
Qed.

Simplification for the right-sided pair corrrelation with CTop.
Lemma RelPairR_top_top tL tR1 tR2:
  RelEquiv (RelInter RelTopVal (RelTyped tL (TPair tR1 tR2)))
           (RelPairR (concretize_corr tL tR1 CTop) (concretize_corr tL tR2 CTop)).
Proof.
  apply RelInv_RelEquiv.
  rewrite RelInv_RelInter. rewrite RelInv_RelTopVal. rewrite RelInv_RelTyped.
  rewrite RelInv_RelPairR. repeat rewrite <- concretize_corr_flip.
  simpl flip_corr.
  apply RelPairL_top_top.
Qed.

Unfolding lemma for the composition on the LHS with a left-sided sum relation.
Lemma RelCompose_RelSumL {A B} (c1 c2: rel term A) (c: rel A B):
  RelEquiv (RelCompose (RelSumL c1 c2) c)
           (RelSumL (RelCompose c1 c) (RelCompose c2 c)).
Proof.
  intros v1 v3; split; intro H.
  - destruct H as [v2 [H12 H]].
    destruct v1; simpl in H12; try contradiction; simpl; ∃ v2; tauto.
  - destruct v1; simpl in H; try contradiction; assumption.
Qed.

Unfolding lemma for the composition on the RHS with a right-sided pair relation.
Lemma RelCompose_RelSumR {A B} (c: rel A B) (c1 c2: rel B term):
  RelEquiv (RelCompose c (RelSumR c1 c2))
           (RelSumR (RelCompose c c1) (RelCompose c c2)).
Proof.
  intros v1 v3; split; intro H.
  - destruct H as [v2 [H H23]].
    destruct v3; simpl in H23; try contradiction; simpl; ∃ v2; tauto.
  - destruct v3; simpl in H; try contradiction; assumption.
Qed.

Unfolding lemma for the composition of a right-sided sum relation with a left-sided sum relation.
Lemma RelCompose_RelSumR_RelSumL {A B} (c1 c2: rel A term) (c3 c4: rel term B):
  RelEquiv (RelCompose (RelSumR c1 c2) (RelSumL c3 c4))
           (RelUnion (RelCompose c1 c3) (RelCompose c2 c4)).
Proof.
  intros v1 v3; split; intro H.
  - destruct H as [v2 [H12 H23]]. destruct v2; simpl in H12, H23; try contradiction.
    + left. ∃ v2; tauto.
    + right. ∃ v2; tauto.
  - destruct H as [[v2 [H12 H23]] | [v2 [H12 H23]]].
    + ∃ (InjL v2). simpl. tauto.
    + ∃ (InjR v2). simpl. tauto.
Qed.

Simplification for the left-sided sum corrrelation with CTop.
Lemma RelSumL_top_top tL1 tL2 tR:
  RelEquiv (RelInter RelTopVal (RelTyped (TSum tL1 tL2) tR))
           (RelSumL (concretize_corr tL1 tR CTop) (concretize_corr tL2 tR CTop)).
Proof.
  intros v1 v2. split; intro H.
  - destruct H as [[Hgood1 Hgood2] [Hwf1 Hwf2]].
    assert (is_value v1) as Hval1 by auto.
    destruct v1; simpl in Hval1; try contradiction; inversion Hwf1; subst.
    + assert (good_value v1) by eauto using good_value_InjL_inv.
      simpl. tauto.
    + assert (good_value v1) by eauto using good_value_InjR_inv.
      simpl. tauto.
  - destruct v1; simpl in H; try contradiction.
    + simpl. intuition auto with good_rel.
      constructor; assumption.
    + simpl. intuition auto with good_rel.
      constructor; assumption.
Qed.

Simplification for the right-sided sum corrrelation with CTop.
Lemma RelSumR_top_top tL tR1 tR2:
  RelEquiv (RelInter RelTopVal (RelTyped tL (TSum tR1 tR2)))
           (RelSumR (concretize_corr tL tR1 CTop) (concretize_corr tL tR2 CTop)).
Proof.
  apply RelInv_RelEquiv.
  rewrite RelInv_RelInter. rewrite RelInv_RelTopVal. rewrite RelInv_RelTyped.
  rewrite RelInv_RelSumR. repeat rewrite <- concretize_corr_flip.
  simpl flip_corr.
  apply RelSumL_top_top.
Qed.

Unfolding lemma for the composition on the LHS with a left-sided function relation.
Lemma RelCompose_FUNvL Rarg Rinner Router R R' :
  good_vrel R →
  RelIncl (RelCompose R' (RelInv R)) Rarg →
  RelIncl (RelCompose (FUNvL Rarg Rinner Router) R)
          (FUNvL R' Rinner (RelCompose Router R)).
Proof.
  intros Hgood Hincl v1 v3 [v2 [[Hgood1 [Hgood2 Hfun]] H]].
  split; [ assumption | split; [ eapply Hgood; eauto |]].
  intros w1 w3 Happ H'.
  assert (in_rel Rarg w1 v2) as Harg.
  { apply Hincl. ∃ v3. auto. }
  specialize (Hfun _ _ Happ Harg).
  destruct Hfun.
  split; [ assumption |]. ∃ v2. split; assumption.
Qed.

Unfolding lemma for the composition on the RHS with a right-sided function relation.
Lemma RelCompose_FUNvR R R' Rarg Rinner Router :
  good_vrel R →
  RelIncl (RelCompose (RelInv R) R') Rarg →
  RelIncl (RelCompose R (FUNvR Rarg Rinner Router))
          (FUNvR R' Rinner (RelCompose R Router)).
Proof.
  intros Hgood Hincl.
  apply RelInv_RelIncl. rewrite RelInv_RelCompose. repeat rewrite RelInv_FUNvR.
  repeat rewrite RelInv_RelCompose.
  apply RelCompose_FUNvL.
  - rewrite <- RelInv_good_vrel. assumption.
  - repeat rewrite <- RelInv_RelCompose. apply RelInv_RelIncl in Hincl. assumption.
Qed.

Correctness of composition

Correctness lemma for corr_compose. This is bullet 3 of Lemma 5.9 of the ICFP'20 paper.
Lemma concretize_corr_compose tL tM tR c1 c2 c:
  wf_corr c1 tL tM →
  wf_corr c2 tM tR →
  corr_compose c1 c2 c →
  RelIncl
    (RelCompose (concretize_corr tL tM c1) (concretize_corr tM tR c2))
    (concretize_corr tL tR c).
Proof.
  intros Hwf1 Hwf2 H. revert tL tM tR Hwf1 Hwf2. induction H; intros tL tM tR Hwf1 Hwf2.
  - apply RelBot_absorbant_compose_left.
  - apply RelBot_absorbant_compose_right.
  - simpl. destruct (ty_eq_dec tL tM); subst.
    + rewrite RelCompose_RelInter_left. rewrite RelInter_lb1.
      rewrite RelEqVal_incl_RelEq. rewrite RelEq_neutral_compose_left.
      reflexivity.
    + rewrite RelBot_absorbant_compose_left. apply RelBot_bot.
  - simpl. destruct (ty_eq_dec tM tR); subst.
    + rewrite RelCompose_RelInter_right. rewrite RelInter_lb1.
      rewrite RelEqVal_incl_RelEq. rewrite RelEq_neutral_compose_right.
      reflexivity.
    + rewrite RelBot_absorbant_compose_right. apply RelBot_bot.
  - simpl. rewrite RelCompose_RelInter_left.
    rewrite RelCompose_RelInter_right. rewrite RelCompose_RelInter_right.
    rewrite RelCompose_RelTopVal_self. rewrite RelInter_assoc1.
    apply RelInter_morphism_incl.
    + rewrite RelInter_lb1. apply RelInter_lb1.
    + apply RelCompose_RelTyped.
  - destruct tL; simpl in Hwf1; try contradiction. destruct Hwf1 as [Hwf11 Hwf12].
    simpl.
    rewrite <- IHcorr_compose1; eauto. clear IHcorr_compose1.
    rewrite <- IHcorr_compose2; eauto. clear IHcorr_compose2.
    apply RelCompose_RelPairL.
  - destruct tR; simpl in Hwf2; try contradiction. destruct Hwf2 as [Hwf21 Hwf22].
    simpl.
    rewrite <- IHcorr_compose1; eauto. clear IHcorr_compose1.
    rewrite <- IHcorr_compose2; eauto. clear IHcorr_compose2.
    apply RelCompose_RelPairR.
  - destruct tM; simpl in Hwf1, Hwf2; try contradiction.
    destruct Hwf1 as [Hwf11 Hwf12]. destruct Hwf2 as [Hwf21 Hwf22].
    simpl.
    rewrite <- (concretize_corr_inter _ _ c1 c2 c12); eauto using compose_corr_wf.
    rewrite <- IHcorr_compose1; eauto. clear IHcorr_compose1.
    rewrite <- IHcorr_compose2; eauto. clear IHcorr_compose2.
    rewrite RelCompose_RelPairR_RelPairL.
    reflexivity.
  - destruct tM; simpl in Hwf1, Hwf2; try contradiction.
    destruct Hwf1 as [Hwf11 Hwf12].
    simpl.
    rewrite <- (concretize_corr_inter _ _ c1 c2 c12); eauto using compose_corr_wf.
    rewrite <- IHcorr_compose1; eauto. clear IHcorr_compose1.
    rewrite <- IHcorr_compose2; eauto. clear IHcorr_compose2.
    rewrite <- RelCompose_RelPairR_RelPairL.
    rewrite RelPairL_top_top. reflexivity.
  - destruct tM; simpl in Hwf1, Hwf2; try contradiction.
    destruct Hwf2 as [Hwf21 Hwf22].
    simpl.
    rewrite <- (concretize_corr_inter _ _ c1 c2 c12); eauto using compose_corr_wf.
    rewrite <- IHcorr_compose1; eauto. clear IHcorr_compose1.
    rewrite <- IHcorr_compose2; eauto. clear IHcorr_compose2.
    rewrite <- RelCompose_RelPairR_RelPairL.
    rewrite RelPairR_top_top. reflexivity.
  - destruct tL; simpl in Hwf1; try contradiction. destruct Hwf1 as [Hwf11 Hwf12].
    simpl.
    rewrite <- IHcorr_compose1; eauto. clear IHcorr_compose1.
    rewrite <- IHcorr_compose2; eauto. clear IHcorr_compose2.
    rewrite RelCompose_RelSumL. reflexivity.
  - destruct tR; simpl in Hwf2; try contradiction. destruct Hwf2 as [Hwf21 Hwf22].
    simpl.
    rewrite <- IHcorr_compose1; eauto. clear IHcorr_compose1.
    rewrite <- IHcorr_compose2; eauto. clear IHcorr_compose2.
    rewrite RelCompose_RelSumR. reflexivity.
  - destruct tM; simpl in Hwf1, Hwf2; try contradiction.
    destruct Hwf1 as [Hwf11 Hwf12]. destruct Hwf2 as [Hwf21 Hwf22].
    simpl.
    rewrite <- (concretize_corr_union _ _ c1 c2 c12); eauto using compose_corr_wf.
    rewrite <- IHcorr_compose1; eauto. clear IHcorr_compose1.
    rewrite <- IHcorr_compose2; eauto. clear IHcorr_compose2.
    rewrite RelCompose_RelSumR_RelSumL.
    reflexivity.
  - destruct tM; simpl in Hwf1, Hwf2; try contradiction.
    destruct Hwf1 as [Hwf11 Hwf12].
    simpl.
    rewrite <- (concretize_corr_union _ _ c1 c2 c12); eauto using compose_corr_wf.
    rewrite <- IHcorr_compose1; eauto. clear IHcorr_compose1.
    rewrite <- IHcorr_compose2; eauto. clear IHcorr_compose2.
    rewrite <- RelCompose_RelSumR_RelSumL.
    rewrite RelSumL_top_top. reflexivity.
  - destruct tM; simpl in Hwf1, Hwf2; try contradiction.
    destruct Hwf2 as [Hwf21 Hwf22].
    simpl.
    rewrite <- (concretize_corr_union _ _ c1 c2 c12); eauto using compose_corr_wf.
    rewrite <- IHcorr_compose1; eauto. clear IHcorr_compose1.
    rewrite <- IHcorr_compose2; eauto. clear IHcorr_compose2.
    rewrite <- RelCompose_RelSumR_RelSumL.
    rewrite RelSumR_top_top. reflexivity.
  - destruct tL; simpl in Hwf1; try contradiction.
    destruct Hwf1 as [Hwfarg [Hwfinner Hwfouter]]. simpl.
    rewrite RelCompose_RelInter_left.
    rewrite RelCompose_FUNvL with (R' := concretize_corr tL1 tR carg');
      auto using concretize_corr_good.
    + rewrite IHcorr_compose3; auto.
      rewrite (concretize_corr_typed tM tR c). rewrite RelCompose_RelTyped.
      reflexivity.
    + apply (concretize_corr_leq tL1 tM) in H1;
        eauto using compose_corr_wf, flip_corr_wf.
      rewrite <- H1.
      rewrite <- concretize_corr_flip.
      apply IHcorr_compose2;
        eauto using compose_corr_wf, flip_corr_wf.
  - apply RelInter_glb.
    + repeat rewrite concretize_corr_below_top.
      rewrite RelCompose_RelTopVal_self. reflexivity.
    + repeat rewrite concretize_corr_typed.
      apply RelCompose_RelTyped.
  - destruct tR; simpl in Hwf2; try contradiction.
    destruct Hwf2 as [Hwfarg [Hwfinner Hwfouter]]. simpl.
    rewrite RelCompose_RelInter_right.
    rewrite RelCompose_FUNvR with (R' := concretize_corr tL tR1 carg');
      auto using concretize_corr_good.
    + rewrite IHcorr_compose3; auto.
      rewrite (concretize_corr_typed tL tM c). rewrite RelCompose_RelTyped.
      reflexivity.
    + apply (concretize_corr_leq tM tR1) in H1;
        eauto using compose_corr_wf, flip_corr_wf.
      rewrite <- H1.
      rewrite <- concretize_corr_flip.
      apply IHcorr_compose2;
        eauto using compose_corr_wf, flip_corr_wf.
  - apply RelInter_glb.
    + repeat rewrite concretize_corr_below_top.
      rewrite RelCompose_RelTopVal_self. reflexivity.
    + repeat rewrite concretize_corr_typed.
      apply RelCompose_RelTyped.
  - apply RelInter_glb.
    + repeat rewrite concretize_corr_below_top.
      rewrite RelCompose_RelTopVal_self. reflexivity.
    + repeat rewrite concretize_corr_typed.
      apply RelCompose_RelTyped.
  - apply RelInter_glb.
    + repeat rewrite concretize_corr_below_top.
      rewrite RelCompose_RelTopVal_self. reflexivity.
    + repeat rewrite concretize_corr_typed.
      apply RelCompose_RelTyped.
  - apply RelInter_glb.
    + repeat rewrite concretize_corr_below_top.
      rewrite RelCompose_RelTopVal_self. reflexivity.
    + repeat rewrite concretize_corr_typed.
      apply RelCompose_RelTyped.
Qed.

Application of correlations

Specification for the application of a correlation with an other one. This is the Figure 17 of the ICFP'20 paper.
Inductive corr_apply: corr → corr → corr → Prop :=
| CApplyTop1: ∀ c,
    corr_apply CTop c CTop
| CApplyEq1: ∀ c,
    corr_apply CEq c CTop
| CApplyBot1: ∀ c,
    corr_apply CBot c CBot
| CApplyBot2: ∀ c,
    corr_apply c CBot CBot
| CApplyFunRApplyGood: ∀ carg cinner couter c c' c'',
    corr_leq c carg →
    corr_compose c cinner c' →
    corr_inter c' couter c'' →
    corr_apply (CFun R carg cinner couter) c c''
| CApplyFunRApplyBad: ∀ carg cinner couter c,
    ¬ (corr_leq c carg) →
    corr_apply (CFun R carg cinner couter) c CTop
| CApplyFunL: ∀ carg cinner couter c,
    corr_apply (CFun L carg cinner couter) c CTop
| CApplyPairL1: ∀ c1 c2 c c1' c2',
    corr_apply c1 (proj_pair true L One c) c1' →
    corr_apply c2 (proj_pair true L Two c) c2' →
    corr_apply (CPair L c1 c2) c (CPair L c1' c2')
| CApplyPairR: ∀ c1 c2 c,
    corr_apply (CPair R c1 c2) c CBot
| CApplySumL1: ∀ c1 c2 c c1' c2',
    corr_apply c1 (proj_sum true L One c) c1' →
    corr_apply c2 (proj_sum true L Two c) c2' →
    corr_apply (CSum L c1 c2) c (CSum L c1' c2')
| CApplySumR: ∀ c1 c2 c,
    corr_apply (CSum R c1 c2) c CBot
| CApplyPairL2: ∀ c c1 c2 c1' c2',
    corr_apply (proj_pair true L One c) c1 c1' →
    corr_apply (proj_pair true L Two c) c2 c2' →
    corr_apply c (CPair L c1 c2) (CPair L c1' c2')
| CApplySumL2: ∀ c c1 c2 c1' c2',
    corr_apply (proj_sum true L One c) c1 c1' →
    corr_apply (proj_sum true L Two c) c2 c2' →
    corr_apply c (CSum L c1 c2) (CSum L c1' c2')
.

Typing lemma for apply_corr.
Lemma apply_corr_wf tL tR1 tR2 c1 c2 c:
  corr_apply c1 c2 c →
  wf_corr c1 tL (TFun tR2 tR1) →
  wf_corr c2 tL tR2 →
  wf_corr c tL tR1.
Proof.
  intro H. revert tL tR1 tR2.
  induction H; intros tL tR1 tR2 Hwf1 Hwf2;
    simpl in Hwf1; try solve [ inversion Hwf1 | constructor ].
  - destruct Hwf1 as [Hwarg [Hwfinner Hwfouter]].
    eauto using inter_corr_wf, compose_corr_wf.
  - destruct tL; try contradiction.
    destruct Hwf1 as [Hwf1L Hwf1R].
    constructor.
    + eapply IHcorr_apply1; eauto. eapply proj_pair_L_wf with (i := One); eauto.
    + eapply IHcorr_apply2; eauto. eapply proj_pair_L_wf with (i := Two); eauto.
  - destruct tL; try contradiction.
    destruct Hwf1 as [Hwf1L Hwf1R].
    constructor.
    + eapply IHcorr_apply1; eauto. eapply proj_sum_L_wf with (i := One); eauto.
    + eapply IHcorr_apply2; eauto. eapply proj_sum_L_wf with (i := Two); eauto.
  - destruct tL; try contradiction.
    destruct Hwf2 as [Hwf2L Hwf2R].
    constructor.
    + eapply IHcorr_apply1; eauto. eapply proj_pair_L_wf with (i := One); eauto.
    + eapply IHcorr_apply2; eauto. eapply proj_pair_L_wf with (i := Two); eauto.
  - destruct tL; try contradiction.
    destruct Hwf2 as [Hwf2L Hwf2R].
    constructor.
    + eapply IHcorr_apply1; eauto. eapply proj_sum_L_wf with (i := One); eauto.
    + eapply IHcorr_apply2; eauto. eapply proj_sum_L_wf with (i := Two); eauto.
Qed.

Intermediate semantic lemmas used in the correctness of application

Unfolding lemma for the application of an intersection of relations to some other relation.
Lemma APPv_RelInter_left {A} (R1 R2 R: rel A term):
  RelIncl (APPv (RelInter R1 R2) R) (RelInter (APPv R1 R) (APPv R2 R)).
Proof.
  intros v1 v2 [v3 [v4 [[H1 H2] [H Happ]]]]. split; ∃ v3, v4; auto.
Qed.

Unfolding lemma for the application of some relation to an intersection of relations.
Lemma APPv_RelInter_right {A} (R R1 R2: rel A term):
  RelIncl (APPv R (RelInter R1 R2)) (RelInter (APPv R R1) (APPv R R2)).
Proof.
  intros v1 v2 [v3 [v4 [H [[H1 H2] Happ]]]]. split; ∃ v3, v4; auto.
Qed.

The application of the full relation to itself is smaller than the top relation.
Lemma APPv_RelTopVal_self:
  RelIncl (APPv RelTopVal RelTopVal) RelTopVal.
Proof.
  intros v1 v2 [v3 [v4 [[H1 H3] [[H1' H4] Happ]]]].
  simpl in ×. split; auto.
  apply eval_good_value in Happ; auto.
  assert (fv v3 [<=] empty) by auto.
  assert (fv v4 [<=] empty) by auto.
  simpl. fsetdec.
Qed.

Unfolding lemma for the well-typed application of the full typed relation to the full typed relation.
Lemma APPv_RelTyped tL tR1 tR2:
  RelIncl (APPv (RelTyped tL (TFun tR2 tR1)) (RelTyped tL tR2)) (RelTyped tL tR1).
Proof.
  intros v1 v2 [v3 [v4 [[H1L H1R] [[H2L H2R] Happ]]]].
  split; auto.
  eapply preservation_eval; eauto.
  econstructor; eauto.
Qed.

The application of the empty relation is the empty relation.
Lemma APPv_RelBot_absorbant_left {A} (R: rel A term):
  RelIncl (APPv RelBot R) RelBot.
Proof.
  intros v1 v2 [w1 [w2 H]]. simpl in H. tauto.
Qed.

An application with the empty relation as argument is the empty relation.
Lemma APPv_RelBot_absorbant_right {A} (R: rel A term):
  RelIncl (APPv R RelBot) RelBot.
Proof.
  intros v1 v2 [w1 [w2 H]]. simpl in H. tauto.
Qed.

Unfolding lemma for the application of a right-sided relation to a compatible argument.
Lemma APPv_FUNvR Rarg Rinner Router R:
  RelIncl R Rarg →
  RelIncl (APPv (FUNvR Rarg Rinner Router) R)
          (RelInter (RelCompose R Rinner) Router).
Proof.
  intros Hincl v1 v2 [v3 [v4 [[Hgood1 [Hgood2 Hfun]] [H Happ]]]].
  apply Hfun in Happ; auto. destruct Happ as [Hinner Houter].
  split; auto. ∃ v4. auto.
Qed.

Unfolding lemma for the application of a pair of left-sided relations.
Lemma APPv_RelPairL1 R1 R2 R:
  good_vrel R1 →
  good_vrel R2 →
  RelIncl (APPv (RelPairL R1 R2) R)
          (RelPairL (APPv R1 (RelCompose (RelPairR RelEqVal RelTopVal) R))
                    (APPv R2 (RelCompose (RelPairR RelTopVal RelEqVal) R))).
Proof.
  intros Hgood1 Hgood2 v1 v2 [v3 [v4 [Hpair [H Happ]]]].
  destruct v1; simpl in Hpair; try contradiction. destruct Hpair as [H1 H2].
  assert (good_value v1_1) as Hgoodv11 by eauto.
  assert (good_value v1_2) as Hgoodv12 by eauto.
  split; ∃ v3, v4; (split; [| split]); auto; ∃ (Pair v1_1 v1_2); simpl; tauto.
Qed.

Unfolding lemma for the application to a pair of right-sided relations.
Lemma APPv_RelPairL2 R1 R2 R:
  good_vrel R1 →
  good_vrel R2 →
  RelIncl (APPv R (RelPairL R1 R2))
          (RelPairL (APPv (RelCompose (RelPairR RelEqVal RelTopVal) R) R1)
                    (APPv (RelCompose (RelPairR RelTopVal RelEqVal) R) R2)).
Proof.
  intros Hgood1 Hgood2 v1 v2 [v3 [v4 [H [Hpair Happ]]]].
  destruct v1; simpl in Hpair; try contradiction. destruct Hpair as [H1 H2].
  assert (good_value v1_1) as Hgoodv11 by eauto.
  assert (good_value v1_2) as Hgoodv12 by eauto.
  split; ∃ v3, v4; (split; [| split]); auto; ∃ (Pair v1_1 v1_2); simpl; tauto.
Qed.

Unfolding lemma for the application of a sum of left-sided relations.
Lemma APPv_RelSumL1 R1 R2 R:
  good_vrel R1 →
  good_vrel R2 →
  RelIncl (APPv (RelSumL R1 R2) R)
          (RelSumL (APPv R1 (RelCompose (RelSumR RelEqVal RelBot) R))
                   (APPv R2 (RelCompose (RelSumR RelBot RelEqVal) R))).
Proof.
  intros Hgood1 Hgood2 v1 v2 [v3 [v4 [Hpair [H Happ]]]].
  destruct v1; simpl in Hpair; try contradiction.
  - assert (good_value v1) as Hgoodv1 by eauto.
    ∃ v3, v4. split; [| split]; auto. ∃ (InjL v1). simpl. tauto.
  - assert (good_value v1) as Hgoodv1 by eauto.
    ∃ v3, v4. split; [| split]; auto. ∃ (InjR v1). simpl. tauto.
Qed.

Unfolding lemma for the application to a sum of right-sided relations.
Lemma APPv_RelSumL2 R1 R2 R:
  good_vrel R1 →
  good_vrel R2 →
  RelIncl (APPv R (RelSumL R1 R2))
          (RelSumL (APPv (RelCompose (RelSumR RelEqVal RelBot) R) R1)
                   (APPv (RelCompose (RelSumR RelBot RelEqVal) R) R2)).
Proof.
  intros Hgood1 Hgood2 v1 v2 [v3 [v4 [H [Hpair Happ]]]].
  destruct v1; simpl in Hpair; try contradiction.
  - assert (good_value v1) as Hgoodv1 by eauto.
    ∃ v3, v4. split; [| split]; auto. ∃ (InjL v1). simpl. tauto.
  - assert (good_value v1) as Hgoodv1 by eauto.
    ∃ v3, v4. split; [| split]; auto. ∃ (InjR v1). simpl. tauto.
Qed.

Unfolding lemma for the application of a left-sided function relation to a left-sided function relation.
Lemma APPv_FUNvL_FUNvL Rarg1 Rinner1 Router1 Rarg2 Rinner2 Router2 :
  good_vrel Rarg1 →
  good_vrel Rarg2 →
  RelIncl (RelCompose Rarg1 RelTopVal) Rarg1 →
  RelIncl (RelCompose Rarg2 RelTopVal) Rarg2 →
  RelIncl
    (APPv (FUNvL Rarg1 Rinner1 Router1) (FUNvL Rarg2 Rinner2 Router2))
    (FUNvL (APPv Rarg1 Rarg2) (RelInter Rinner1 Rinner2) (APPv Router1 Router2)).
Proof.
  intros Hgoodarg1 Hgoodarg2 Hincl1 Hincl2.
  intros v1 v2 [v3 [v4 [[Hgood1 [Hgood3 Hfun13]] [[Hgood1' [Hgood4 Hfun14]] Heval]]]].
  split; [ assumption | split].
  - apply eval_good_value in Heval; auto.
    assert (fv v3 [<=] empty) by auto.
    assert (fv v4 [<=] empty) by auto.
    simpl. fsetdec.
  - intros w1 w2 Heval' [w3 [w4 [Harg1 [Harg2 Heval'']]]].
    specialize (Hfun13 _ _ Heval').
    destruct Hfun13 as [Hinner1 Houter1];
      [ solve [ apply Hincl1; ∃ w3; split; [| split]; eauto ] |].
    specialize (Hfun14 _ _ Heval').
    destruct Hfun14 as [Hinner2 Houter2];
      [ solve [ apply Hincl2; ∃ w4; split; [| split]; eauto ] |].
    split; [ split |]; auto.
    ∃ v3, v4. tauto.
Qed.

Correctness of application

Correctness lemma for corr_apply. This is bullet 4 of Lemma 5.9 of the ICFP'20 paper.
Lemma concretize_corr_apply tL tR1 tR2 c1 c2 c:
    wf_corr c1 tL (TFun tR2 tR1) →
    wf_corr c2 tL tR2 →
    corr_apply c1 c2 c →
    RelIncl (APPv (concretize_corr tL (TFun tR2 tR1) c1) (concretize_corr tL tR2 c2))
            (concretize_corr tL tR1 c).
Proof.
  intros Hwf1 Hwf2 H. revert tL tR1 tR2 Hwf1 Hwf2. induction H; intros.
  - simpl. rewrite APPv_RelInter_left. apply RelInter_morphism_incl.
    + rewrite concretize_corr_below_top. apply APPv_RelTopVal_self.
    + rewrite concretize_corr_typed. apply APPv_RelTyped.
  - apply RelInter_glb.
    + repeat rewrite concretize_corr_below_top. apply APPv_RelTopVal_self.
    + repeat rewrite concretize_corr_typed. apply APPv_RelTyped.
  - apply APPv_RelBot_absorbant_left.
  - apply APPv_RelBot_absorbant_right.
  - simpl in Hwf1. destruct Hwf1 as [Hwfarg [Hwfinner Hwfouter]].
    eapply concretize_corr_inter in H1; eauto using compose_corr_wf.
    rewrite <- H1. clear H1.
    eapply concretize_corr_compose in H0; eauto.
    rewrite <- H0. clear H0.
    simpl. rewrite APPv_RelInter_left.
    rewrite RelInter_lb1.
    rewrite APPv_FUNvR; [ reflexivity |].
    apply concretize_corr_leq; auto.
  - apply RelInter_glb.
    + repeat rewrite concretize_corr_below_top. apply APPv_RelTopVal_self.
    + repeat rewrite concretize_corr_typed. apply APPv_RelTyped.
  - apply RelInter_glb.
    + repeat rewrite concretize_corr_below_top. apply APPv_RelTopVal_self.
    + repeat rewrite concretize_corr_typed. apply APPv_RelTyped.
  - simpl in Hwf1. destruct tL; try contradiction. destruct Hwf1 as [Hwf1L Hwf1R].
    simpl.
    rewrite <- IHcorr_apply1; eauto;
      [| solve [ eapply proj_pair_L_wf with (i := One); eauto ] ].
    clear IHcorr_apply1.
    rewrite <- concretize_corr_proj_pair_L with (ty1R := tL2) (i := One).
    rewrite <- IHcorr_apply2; eauto;
      [| solve [ eapply proj_pair_L_wf with (i := Two); eauto ] ].
    clear IHcorr_apply2.
    rewrite <- concretize_corr_proj_pair_L with (ty1L := tL1) (i := Two).
    rewrite APPv_RelPairL1; auto using concretize_corr_good.
    reflexivity.
  - simpl in Hwf1. contradiction.
  - simpl in Hwf1. destruct tL; try contradiction. destruct Hwf1 as [Hwf1L Hwf1R].
    simpl.
    rewrite <- IHcorr_apply1; eauto;
      [| solve [ eapply proj_sum_L_wf with (i := One); eauto ] ].
    clear IHcorr_apply1.
    rewrite <- concretize_corr_proj_sum_L with (ty1R := tL2) (i := One).
    rewrite <- IHcorr_apply2; eauto;
      [| solve [ eapply proj_sum_L_wf with (i := Two); eauto ] ].
    clear IHcorr_apply2.
    rewrite <- concretize_corr_proj_sum_L with (ty1L := tL1) (i := Two).
    rewrite APPv_RelSumL1; auto using concretize_corr_good.
    reflexivity.
  - simpl in Hwf1. contradiction.
  - simpl in Hwf2. destruct tL; try contradiction. destruct Hwf2 as [Hwf2L Hwf2R].
    simpl.
    rewrite <- IHcorr_apply1; eauto;
      [| solve [ eapply proj_pair_L_wf with (i := One); eauto ] ].
    clear IHcorr_apply1.
    rewrite <- concretize_corr_proj_pair_L with (ty1R := tL2) (i := One).
    rewrite <- IHcorr_apply2; eauto;
      [| solve [ eapply proj_pair_L_wf with (i := Two); eauto ] ].
    clear IHcorr_apply2.
    rewrite <- concretize_corr_proj_pair_L with (ty1L := tL1) (i := Two).
    rewrite APPv_RelPairL2; auto using concretize_corr_good.
    reflexivity.
  - simpl in Hwf2. destruct tL; try contradiction. destruct Hwf2 as [Hwf2L Hwf2R].
    simpl.
    rewrite <- IHcorr_apply1; eauto;
      [| solve [ eapply proj_sum_L_wf with (i := One); eauto ] ].
    clear IHcorr_apply1.
    rewrite <- concretize_corr_proj_sum_L with (ty1R := tL2) (i := One).
    rewrite <- IHcorr_apply2; eauto;
      [| solve [ eapply proj_sum_L_wf with (i := Two); eauto ] ].
    clear IHcorr_apply2.
    rewrite <- concretize_corr_proj_sum_L with (ty1L := tL1) (i := Two).
    rewrite APPv_RelSumL2; auto using concretize_corr_good.
    reflexivity.
Qed.