From d2372b490d3bcb4aa49c55b8b37c4eb0ff25a685 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 May 2020 15:18:55 +0200
Subject: [PATCH] Avoid inconsistent sealing of subtyping. Instead give better
 type class precedences.

---
 theories/logrel/subtyping.v       |  13 +---
 theories/logrel/subtyping_rules.v | 110 +++++++++++-------------------
 2 files changed, 40 insertions(+), 83 deletions(-)

diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 93d98ec..6a7c3c9 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -5,17 +5,10 @@ having both [A <: B] and [B <: A]. Finally, the notion of a *copyable type* is
 defined in terms of subtyping: a type [A] is copyable when [A <: copy A]. *)
 From actris.logrel Require Export model term_types.
 
-Definition lsty_le_def {Σ} (P1 P2 : lsty Σ) :=
-  iProto_le (lsty_car P1) (lsty_car P2).
-Definition lsty_le_aux : seal (@lsty_le_def). by eexists. Qed.
-Definition lsty_le := lsty_le_aux.(unseal).
-Definition lsty_le_eq : @lsty_le = @lsty_le_def := lsty_le_aux.(seal_eq).
-Arguments lsty_le {_} _ _.
-
 Definition lty_le {Σ k} : lty Σ k → lty Σ k → iProp Σ :=
   match k with
   | tty_kind => λ A1 A2, ■ ∀ v, ltty_car A1 v -∗ ltty_car A2 v
-  | lty_kind => λ P1 P2, ■ lsty_le P1 P2
+  | lty_kind => λ P1 P2, ■ iProto_le (lsty_car P1) (lsty_car P2)
   end%I.
 Arguments lty_le : simpl never.
 Infix "<:" := lty_le (at level 70) : bi_scope.
@@ -40,9 +33,7 @@ Section subtyping.
   Proof. rewrite /lty_bi_le /=. apply _. Qed.
 
   Global Instance lty_le_ne : NonExpansive2 (@lty_le Σ k).
-  Proof.
-    rewrite /lty_le lsty_le_eq. destruct k; rewrite ?/lsty_le_def; solve_proper.
-  Qed.
+  Proof. destruct k; solve_proper. Qed.
   Global Instance lty_le_proper {k} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ k).
   Proof. apply (ne_proper_2 _). Qed.
   Global Instance lty_bi_le_ne {k} : NonExpansive2 (@lty_bi_le Σ k).
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 8acf256..4f70e9f 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -12,14 +12,12 @@ Section subtyping_rules.
 
   (** Generic rules *)
   Lemma lty_le_refl {k} (M : lty Σ k) : ⊢ M <: M.
-  Proof. destruct k. by iIntros (v) "!> H".
-         rewrite /lty_le lsty_le_eq /lsty_le_def. by iModIntro. Qed.
+  Proof. destruct k. by iIntros (v) "!> H". by iModIntro. Qed.
   Lemma lty_le_trans {k} (M1 M2 M3 : lty Σ k) : M1 <: M2 -∗ M2 <: M3 -∗ M1 <: M3.
   Proof.
     destruct k.
     - iIntros "#H1 #H2" (v) "!> H". iApply "H2". by iApply "H1".
-    - iIntros "#H1 #H2 !>".
-      rewrite /lty_le lsty_le_eq /lsty_le_def. by iApply iProto_le_trans.
+    - iIntros "#H1 #H2 !>". by iApply iProto_le_trans.
   Qed.
 
   Lemma lty_bi_le_refl {k} (M : lty Σ k) : ⊢ M <:> M.
@@ -131,11 +129,9 @@ Section subtyping_rules.
   Lemma lty_copyable_prod A B :
     lty_copyable A -∗ lty_copyable B -∗ lty_copyable (A * B).
   Proof.
-    iIntros "#HcpA #HcpB". rewrite /lty_copyable /tc_opaque.
+    iIntros "#HcpA #HcpB". rewrite /lty_copyable /=.
     iApply lty_le_r; last by iApply lty_le_prod_copy.
-    iApply lty_le_prod.
-    - iApply "HcpA".
-    - iApply "HcpB".
+    iApply lty_le_prod. iApply "HcpA". iApply "HcpB".
   Qed.
 
   Lemma lty_le_sum A11 A12 A21 A22 :
@@ -156,11 +152,9 @@ Section subtyping_rules.
   Lemma lty_copyable_sum A B :
     lty_copyable A -∗ lty_copyable B -∗ lty_copyable (A + B).
   Proof.
-    iIntros "#HcpA #HcpB". rewrite /lty_copyable /tc_opaque.
+    iIntros "#HcpA #HcpB". rewrite /lty_copyable /=.
     iApply lty_le_r; last by iApply lty_le_sum_copy.
-    iApply lty_le_sum.
-    - iApply "HcpA".
-    - iApply "HcpB".
+    iApply lty_le_sum. iApply "HcpA". iApply "HcpB".
   Qed.
 
   Lemma lty_le_forall C1 C2 :
@@ -169,7 +163,7 @@ Section subtyping_rules.
   Proof.
     iIntros "#Hle" (v) "!> H". iIntros (w).
     iApply (wp_step_fupd); first done.
-    { iIntros "!>!>!>". iExact "Hle". }
+    { iIntros "!> !> !>". iExact "Hle". }
     iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
     by iApply "Hle'".
   Qed.
@@ -241,8 +235,7 @@ Section subtyping_rules.
     ▷ (S1 <: S2) -∗ chan S1 <: chan S2.
   Proof.
     iIntros "#Hle" (v) "!> H".
-    iApply (iProto_mapsto_le with "H [Hle]").
-    rewrite /lty_le lsty_le_eq. eauto.
+    iApply (iProto_mapsto_le with "H [Hle]"). eauto.
   Qed.
 
   (** Session subtyping *)
@@ -250,7 +243,6 @@ Section subtyping_rules.
     ▷ (A2 <: A1) -∗ ▷ (S1 <: S2) -∗
     (<!!> TY A1 ; S1) <: (<!!> TY A2 ; S2).
   Proof.
-    rewrite /lty_le lsty_le_eq.
     iIntros "#HAle #HSle !>" (v) "H". iExists v.
     iDestruct ("HAle" with "H") as "$". by iModIntro.
   Qed.
@@ -259,7 +251,6 @@ Section subtyping_rules.
     ▷ (A1 <: A2) -∗ ▷ (S1 <: S2) -∗
     (<??> TY A1 ; S1) <: (<??> TY A2 ; S2).
   Proof.
-    rewrite /lty_le lsty_le_eq.
     iIntros "#HAle #HSle !>" (v) "H". iExists v.
     iDestruct ("HAle" with "H") as "$". by iModIntro.
   Qed.
@@ -268,7 +259,6 @@ Section subtyping_rules.
     (∀ (A : lty Σ k), (<??> M A) <: S) -∗
     (<?? (A : lty Σ k)> M A) <: S.
   Proof.
-    rewrite /lty_le lsty_le_eq.
     iIntros "#Hle !>". iApply (iProto_le_exist_elim_l_inhabited M). auto.
   Qed.
 
@@ -276,23 +266,16 @@ Section subtyping_rules.
     (∀ (A : lty Σ k), S <: (<!!> M A)) -∗
     S <: (<!! (A : lty Σ k)> M A).
   Proof.
-    rewrite /lty_le lsty_le_eq.
     iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto.
   Qed.
 
   Lemma lty_le_exist_intro_l k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
     ⊢ (<!! X> M X) <: (<!!> M A).
-  Proof.
-    rewrite /lty_le lsty_le_eq.
-    iIntros "!>". iApply (iProto_le_exist_intro_l).
-  Qed.
+  Proof. iIntros "!>". iApply (iProto_le_exist_intro_l). Qed.
 
   Lemma lty_le_exist_intro_r k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
     ⊢ (<??> M A) <: (<?? X> M X).
-  Proof.
-    rewrite /lty_le lsty_le_eq.
-    iIntros "!>". iApply (iProto_le_exist_intro_r).
-  Qed.
+  Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
 
   Lemma lty_le_texist_elim_l {kt} (M : ltys Σ kt → lmsg Σ) S :
     (∀ Xs, (<??> M Xs) <: S) -∗
@@ -329,7 +312,6 @@ Section subtyping_rules.
   Lemma lty_le_swap_recv_send A1 A2 S :
     ⊢ (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
   Proof.
-    rewrite /lty_le lsty_le_eq.
     iIntros "!>" (v1 v2).
     iApply iProto_le_trans;
       [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ v2)|].
@@ -341,7 +323,6 @@ Section subtyping_rules.
   Lemma lty_le_swap_recv_select A Ss :
     ⊢ (<??> TY A; lty_select Ss) <: lty_select ((λ S, <??> TY A; S) <$> Ss)%lty.
   Proof.
-    rewrite /lty_le lsty_le_eq.
     iIntros "!>" (v1 x2).
     iApply iProto_le_trans;
       [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
@@ -355,7 +336,6 @@ Section subtyping_rules.
   Lemma lty_le_swap_branch_send A Ss :
     ⊢ lty_branch ((λ S, <!!> TY A; S) <$> Ss)%lty <: (<!!> TY A; lty_branch Ss).
   Proof.
-    rewrite /lty_le lsty_le_eq.
     iIntros "!>" (x1 v2).
     iApply iProto_le_trans;
       [|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ x1)]; simpl.
@@ -370,7 +350,6 @@ Section subtyping_rules.
     ▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
     lty_select Ss1 <: lty_select Ss2.
   Proof.
-    rewrite /lty_le lsty_le_eq.
     iIntros "#H !>" (x); iMod 1 as %[S2 HSs2]. iExists x.
     iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
     assert (is_Some (Ss1 !! x)) as [S1 HSs1] by naive_solver.
@@ -382,7 +361,6 @@ Section subtyping_rules.
     Ss2 ⊆ Ss1 →
     ⊢ lty_select Ss1 <: lty_select Ss2.
   Proof.
-    rewrite /lty_le lsty_le_eq.
     intros; iIntros "!>" (x); iMod 1 as %[S HSs2]. iExists x.
     assert (Ss1 !! x = Some S) as HSs1 by eauto using lookup_weaken.
     rewrite HSs1. iSplitR; [by eauto|].
@@ -393,7 +371,6 @@ Section subtyping_rules.
     ▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
     lty_branch Ss1 <: lty_branch Ss2.
   Proof.
-    rewrite /lty_le lsty_le_eq.
     iIntros "#H !>" (x); iMod 1 as %[S1 HSs1]. iExists x.
     iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
     assert (is_Some (Ss2 !! x)) as [S2 HSs2] by naive_solver.
@@ -405,7 +382,6 @@ Section subtyping_rules.
     Ss1 ⊆ Ss2 →
     ⊢ lty_branch Ss1 <: lty_branch Ss2.
   Proof.
-    rewrite /lty_le lsty_le_eq.
     intros; iIntros "!>" (x); iMod 1 as %[S HSs1]. iExists x.
     assert (Ss2 !! x = Some S) as HSs2 by eauto using lookup_weaken.
     rewrite HSs2. iSplitR; [by eauto|].
@@ -416,29 +392,25 @@ Section subtyping_rules.
   Lemma lty_le_app S11 S12 S21 S22 :
     (S11 <: S21) -∗ (S12 <: S22) -∗
     (S11 <++> S12) <: (S21 <++> S22).
-  Proof. rewrite /lty_le lsty_le_eq.
-         iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
+  Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
 
   Lemma lty_le_app_id_l S : ⊢ (END <++> S) <:> S.
-  Proof. rewrite /lty_app left_id.
-         iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iModIntro. Qed.
+  Proof. rewrite /lty_app left_id. iSplit; by iModIntro. Qed.
   Lemma lty_le_app_id_r S : ⊢ (S <++> END) <:> S.
-  Proof. rewrite /lty_app right_id.
-         iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iModIntro. Qed.
+  Proof. rewrite /lty_app right_id. iSplit; by iModIntro. Qed.
   Lemma lty_le_app_assoc S1 S2 S3 :
     ⊢ (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
-  Proof. rewrite /lty_app assoc.
-         iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iModIntro. Qed.
+  Proof. rewrite /lty_app assoc. iSplit; by iModIntro. Qed.
 
   Lemma lty_le_app_send A S1 S2 : ⊢ (<!!> TY A; S1) <++> S2 <:> (<!!> TY A; S1 <++> S2).
   Proof.
     rewrite /lty_app iProto_app_message iMsg_app_exist. setoid_rewrite iMsg_app_base.
-    iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iIntros "!> /=".
+    iSplit; by iIntros "!> /=".
   Qed.
   Lemma lty_le_app_recv A S1 S2 : ⊢ (<??> TY A; S1) <++> S2 <:> (<??> TY A; S1 <++> S2).
   Proof.
     rewrite /lty_app iProto_app_message iMsg_app_exist. setoid_rewrite iMsg_app_base.
-    iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iIntros "!> /=".
+    iSplit; by iIntros "!> /=".
   Qed.
 
   Lemma lty_le_app_choice a (Ss : gmap Z (lsty Σ)) S2 :
@@ -447,7 +419,7 @@ Section subtyping_rules.
     rewrite /lty_app /lty_choice iProto_app_message iMsg_app_exist;
       setoid_rewrite iMsg_app_base; setoid_rewrite lookup_total_alt;
       setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
-    iSplit; rewrite /lty_le lsty_le_eq; iIntros "!> /="; destruct a;
+    iSplit; iIntros "!> /="; destruct a;
       iIntros (x); iExists x; iMod 1 as %[S ->]; iSplitR; eauto.
   Qed.
   Lemma lty_le_app_select A Ss S2 :
@@ -458,13 +430,11 @@ Section subtyping_rules.
   Proof. apply lty_le_app_choice. Qed.
 
   Lemma lty_le_dual S1 S2 : S2 <: S1 -∗ lty_dual S1 <: lty_dual S2.
-  Proof. rewrite /lty_le lsty_le_eq. iIntros "#H !>". by iApply iProto_le_dual. Qed.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
   Lemma lty_le_dual_l S1 S2 : lty_dual S2 <: S1 -∗ lty_dual S1 <: S2.
-  Proof. rewrite /lty_le lsty_le_eq. iIntros "#H !>".
-         by iApply iProto_le_dual_l. Qed.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual_l. Qed.
   Lemma lty_le_dual_r S1 S2 : S2 <: lty_dual S1 -∗ S1 <: lty_dual S2.
-  Proof. rewrite /lty_le lsty_le_eq. iIntros "#H !>".
-           by iApply iProto_le_dual_r. Qed.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual_r. Qed.
 
   Lemma lty_le_dual_end : ⊢ lty_dual (Σ:=Σ) END <:> END.
   Proof. rewrite /lty_dual iProto_dual_end=> /=. apply lty_bi_le_refl. Qed.
@@ -473,8 +443,7 @@ Section subtyping_rules.
     ⊢ lty_dual (lty_message a (TY A; S)) <:> lty_message (action_dual a) (TY A; (lty_dual S)).
   Proof.
     rewrite /lty_dual iProto_dual_message iMsg_dual_exist.
-    setoid_rewrite iMsg_dual_base.
-    iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iIntros "!> /=".
+    setoid_rewrite iMsg_dual_base. iSplit; by iIntros "!> /=".
   Qed.
   Lemma lty_le_dual_send A S : ⊢ lty_dual (<!!> TY A; S) <:> (<??> TY A; lty_dual S).
   Proof. apply lty_le_dual_message. Qed.
@@ -487,7 +456,7 @@ Section subtyping_rules.
     rewrite /lty_dual /lty_choice iProto_dual_message iMsg_dual_exist;
       setoid_rewrite iMsg_dual_base; setoid_rewrite lookup_total_alt;
       setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
-    iSplit; rewrite /lty_le lsty_le_eq; iIntros "!> /="; destruct a;
+    iSplit; iIntros "!> /="; destruct a;
       iIntros (x); iExists x; iMod 1 as %[S ->]; iSplitR; eauto.
   Qed.
 
@@ -498,46 +467,43 @@ Section subtyping_rules.
     ⊢ lty_dual (lty_branch Ss) <:> lty_select (lty_dual <$> Ss).
   Proof. iApply lty_le_dual_choice. Qed.
 
+  (** The instances below make it possible to use the tactics [iIntros],
+  [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [lty_le] goals.
+  These instances have higher precedence than the ones in [proto.v] to avoid
+  needless unfolding of the subtyping relation. *)
   Global Instance lty_le_from_forall_l k (M : lty Σ k → lmsg Σ) (S : lsty Σ) :
-    FromForall (lty_le (<?? X> M X) S)%lty (λ X, (lty_le (<??> M X) S)%lty) | 10.
+    FromForall ((<?? X> M X) <: S) (λ X, (<??> M X) <: S)%I | 0.
   Proof. apply lty_le_exist_elim_l. Qed.
   Global Instance lty_le_from_forall_r k (S : lsty Σ) (M : lty Σ k → lmsg Σ) :
-    FromForall (lty_le S (<!! X> M X))%lty (λ X, (lty_le S (<!!> M X))%lty) | 11.
+    FromForall (S <: (<!! X> M X)) (λ X, S <: (<!!> M X))%I | 1.
   Proof. apply lty_le_exist_elim_r. Qed.
 
   Global Instance lty_le_from_exist_l k (M : lty Σ k → lmsg Σ) S :
-    FromExist ((<!! X> M X) <: S) (λ X, (<!!> M X) <: S)%I | 10.
+    FromExist ((<!! X> M X) <: S) (λ X, (<!!> M X) <: S)%I | 0.
   Proof.
     rewrite /FromExist. iDestruct 1 as (x) "H".
     iApply (lty_le_trans with "[] H"). iApply lty_le_exist_intro_l.
   Qed.
   Global Instance lty_le_from_exist_r k (M : lty Σ k → lmsg Σ) S :
-    FromExist (S <: <?? X> M X) (λ X, S <: (<??> M X))%I | 11.
+    FromExist (S <: <?? X> M X) (λ X, S <: (<??> M X))%I | 1.
   Proof.
     rewrite /FromExist. iDestruct 1 as (x) "H".
     iApply (lty_le_trans with "H"). iApply lty_le_exist_intro_r.
   Qed.
 
-  Lemma lty_le_base_send A (S1 S2 : lsty Σ) :
-    ▷ (S1 <: S2) -∗
-    (<!!> TY A ; S1) <: (<!!> TY A ; S2).
-  Proof. iIntros "H". iApply lty_le_send. iApply lty_le_refl. eauto. Qed.
-
   Global Instance lty_le_from_modal_send A (S1 S2 : lsty Σ) :
     FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
-              ((<!!> TY A; S1) <: (<!!> TY A; S2)) (S1 <: S2).
-  Proof. apply lty_le_base_send. Qed.
-
-  Lemma lty_le_base_recv A (S1 S2 : lsty Σ) :
-    ▷ (S1 <: S2) -∗
-    (<??> TY A ; S1) <: (<??> TY A ; S2).
-  Proof. iIntros "H". iApply lty_le_recv. iApply lty_le_refl. eauto. Qed.
+              ((<!!> TY A; S1) <: (<!!> TY A; S2)) (S1 <: S2) | 0.
+  Proof.
+    rewrite /FromModal. iIntros "H". iApply lty_le_send. iApply lty_le_refl. done.
+  Qed.
 
   Global Instance lty_le_from_modal_recv A (S1 S2 : lsty Σ) :
     FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
-              ((<??> TY A; S1) <: (<??> TY A; S2)) (S1 <: S2).
-  Proof. apply lty_le_base_recv. Qed.
-
+              ((<??> TY A; S1) <: (<??> TY A; S2)) (S1 <: S2) | 0.
+  Proof.
+    rewrite /FromModal. iIntros "H". iApply lty_le_recv. iApply lty_le_refl. done.
+  Qed.
 End subtyping_rules.
 
 Hint Extern 0 (environments.envs_entails _ (?x <: ?y)) =>
-- 
GitLab