From 64e94f3fbddf616a85b914234f80201a5220ab83 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 14 Sep 2020 16:51:17 +0200
Subject: [PATCH] Removed later from payloads in session types

---
 theories/logrel/examples/double.v   |  4 ++--
 theories/logrel/session_types.v     | 13 ++++---------
 theories/logrel/subtyping_rules.v   | 22 +++++++++++-----------
 theories/logrel/term_typing_rules.v |  2 +-
 4 files changed, 18 insertions(+), 23 deletions(-)

diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index ff514a1..7bf2260 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -131,8 +131,8 @@ Section double.
     iIntros (c) "Hc".
     iApply (wp_prog (λ v1 v2, ltty_car lty_int v1 ∗ ltty_car lty_int v2)%I with "[Hc]").
     { iApply (iProto_mapsto_le _ (lsty_car (<??> TY lty_int; <??> TY lty_int; END)) with "Hc").
-      iIntros "!> !>" (v1). iMod 1 as %[x1 ->]. iExists #x1.
-      iIntros "!>" (v2). iMod 1 as %[x2 ->]. iExists #x2. iSplitL; last done.
+      iIntros "!> !>" (v1). iDestruct 1 as %[x1 ->]. iExists #x1.
+      iIntros "!>" (v2). iDestruct 1 as %[x2 ->]. iExists #x2. iSplitL; last done.
       rewrite /ltty_car /=. auto. }
     iIntros "!>" (v1 v2 [[[k1 ->] [k2 ->]]|[[k1 ->] [k2 ->]]]);
       iExists _, _; iSplit; by eauto.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 8e8b6d7..8466ecb 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -12,7 +12,7 @@ Delimit Scope lmsg_scope with lmsg.
 Bind Scope lmsg_scope with lmsg.
 
 Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
-  (∃ v, MSG v {{ ▷ ltty_car A v}} ; (lsty_car S))%msg.
+  (∃ v, MSG v {{ ltty_car A v}} ; (lsty_car S))%msg.
 
 Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ :=
   (∃ X, M X)%msg.
@@ -27,7 +27,7 @@ Definition lty_message {Σ} (a : action) (M : lmsg Σ) : lsty Σ :=
   Lsty (<a> M).
 
 Definition lty_choice {Σ} (a : action) (Ss : gmap Z (lsty Σ)) : lsty Σ :=
-  Lsty (<a@(x : Z)> MSG #x {{ ▷ ⌜is_Some (Ss !! x)⌝ }}; lsty_car (Ss !!! x)).
+  Lsty (<a@(x : Z)> MSG #x {{ ⌜is_Some (Ss !! x)⌝ }}; lsty_car (Ss !!! x)).
 
 Definition lty_dual {Σ} (S : lsty Σ) : lsty Σ :=
   Lsty (iProto_dual (lsty_car S)).
@@ -94,8 +94,8 @@ Section session_types.
   Global Instance lty_msg_base_proper :
     Proper ((≡) ==> (≡) ==> (≡)) (@lty_msg_base Σ).
   Proof. rewrite /lty_msg_base. apply ne_proper_2, _. Qed.
-  Global Instance lty_msg_base_contractive n :
-    Proper (dist_later n ==> dist_later n ==> dist n) (@lty_msg_base Σ).
+  Global Instance lty_msg_base_contractive n A :
+    Proper (dist_later n ==> dist n) (@lty_msg_base Σ A).
   Proof. solve_contractive. Qed.
 
   Global Instance lty_message_ne a : NonExpansive (@lty_message Σ a).
@@ -107,11 +107,6 @@ Section session_types.
   Proof. solve_proper. Qed.
   Global Instance lty_choice_proper a : Proper ((≡) ==> (≡)) (@lty_choice Σ a).
   Proof. apply ne_proper, _. Qed.
-  Global Instance lty_choice_contractive a : Contractive (@lty_choice Σ a).
-  Proof.
-    intros n Ss Ts Heq. rewrite /lty_choice.
-    do 4 f_equiv; f_contractive; [ f_contractive | ]; by rewrite Heq.
-  Qed.
   Global Instance lty_dual_ne : NonExpansive (@lty_dual Σ).
   Proof. solve_proper. Qed.
   Global Instance lty_dual_proper : Proper ((≡) ==> (≡)) (@lty_dual Σ).
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 0b70449..db0c667 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -242,7 +242,7 @@ Section subtyping_rules.
 
   (** Session subtyping *)
   Lemma lty_le_send A1 A2 S1 S2 :
-    ▷ (A2 <: A1) -∗ ▷ (S1 <: S2) -∗
+    (A2 <: A1) -∗ ▷ (S1 <: S2) -∗
     (<!!> TY A1 ; S1) <: (<!!> TY A2 ; S2).
   Proof.
     iIntros "#HAle #HSle !>" (v) "H". iExists v.
@@ -250,7 +250,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_recv A1 A2 S1 S2 :
-    ▷ (A1 <: A2) -∗ ▷ (S1 <: S2) -∗
+    (A1 <: A2) -∗ ▷ (S1 <: S2) -∗
     (<??> TY A1 ; S1) <: (<??> TY A2 ; S2).
   Proof.
     iIntros "#HAle #HSle !>" (v) "H". iExists v.
@@ -329,7 +329,7 @@ Section subtyping_rules.
     iApply iProto_le_trans;
       [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
     iApply iProto_le_payload_elim_r.
-    iMod 1 as %HSs. revert HSs.
+    iDestruct 1 as %HSs. revert HSs.
     rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
     iApply iProto_le_trans; [iApply iProto_le_base_swap|]. iSplitL; [by eauto|].
     iModIntro. by iExists v1.
@@ -342,7 +342,7 @@ Section subtyping_rules.
     iApply iProto_le_trans;
       [|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ x1)]; simpl.
     iApply iProto_le_payload_elim_l.
-    iMod 1 as %HSs. revert HSs.
+    iDestruct 1 as %HSs. revert HSs.
     rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
     iApply iProto_le_trans; [|iApply iProto_le_base_swap]. iSplitL; [by eauto|].
     iModIntro. by iExists v2.
@@ -358,7 +358,7 @@ Section subtyping_rules.
     intros Hin.
     iIntros "!>" (v1 v2).
     rewrite !lookup_fmap !fmap_is_Some !lookup_total_alt !lookup_fmap.
-    iIntros ">% >%".
+    iIntros "H1 H2". iDestruct "H1" as %H1. iDestruct "H2" as %H2.
     destruct H1 as [Ss1' Heq1]. destruct H2 as [Ss2' Heq2].
     rewrite Heq1 Heq2 /=.
     destruct (Hin v1 v2 Ss1' Ss2' Heq1 Heq2) as (Hin1 & Hin2 & Heq).
@@ -374,7 +374,7 @@ Section subtyping_rules.
     ▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
     lty_select Ss1 <: lty_select Ss2.
   Proof.
-    iIntros "#H !>" (x); iMod 1 as %[S2 HSs2]. iExists x.
+    iIntros "#H !>" (x); iDestruct 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.
     rewrite HSs1. iSplitR; [by eauto|].
@@ -385,7 +385,7 @@ Section subtyping_rules.
     Ss2 ⊆ Ss1 →
     ⊢ lty_select Ss1 <: lty_select Ss2.
   Proof.
-    intros; iIntros "!>" (x); iMod 1 as %[S HSs2]. iExists x.
+    intros; iIntros "!>" (x); iDestruct 1 as %[S HSs2]. iExists x.
     assert (Ss1 !! x = Some S) as HSs1 by eauto using lookup_weaken.
     rewrite HSs1. iSplitR; [by eauto|].
     iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
@@ -395,7 +395,7 @@ Section subtyping_rules.
     ▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
     lty_branch Ss1 <: lty_branch Ss2.
   Proof.
-    iIntros "#H !>" (x); iMod 1 as %[S1 HSs1]. iExists x.
+    iIntros "#H !>" (x); iDestruct 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.
     rewrite HSs2. iSplitR; [by eauto|].
@@ -406,7 +406,7 @@ Section subtyping_rules.
     Ss1 ⊆ Ss2 →
     ⊢ lty_branch Ss1 <: lty_branch Ss2.
   Proof.
-    intros; iIntros "!>" (x); iMod 1 as %[S HSs1]. iExists x.
+    intros; iIntros "!>" (x); iDestruct 1 as %[S HSs1]. iExists x.
     assert (Ss2 !! x = Some S) as HSs2 by eauto using lookup_weaken.
     rewrite HSs2. iSplitR; [by eauto|].
     iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
@@ -446,7 +446,7 @@ Section subtyping_rules.
       setoid_rewrite iMsg_app_base; setoid_rewrite lookup_total_alt;
       setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
     iSplit; iIntros "!> /="; destruct a;
-      iIntros (x); iExists x; iMod 1 as %[S ->]; iSplitR; eauto.
+      iIntros (x); iExists x; iDestruct 1 as %[S ->]; iSplitR; eauto.
   Qed.
   Lemma lty_le_app_select A Ss S2 :
     ⊢ lty_select Ss <++> S2 <:> lty_select ((.<++> S2) <$> Ss)%lty.
@@ -483,7 +483,7 @@ Section subtyping_rules.
       setoid_rewrite iMsg_dual_base; setoid_rewrite lookup_total_alt;
       setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
     iSplit; iIntros "!> /="; destruct a;
-      iIntros (x); iExists x; iMod 1 as %[S ->]; iSplitR; eauto.
+      iIntros (x); iExists x; iDestruct 1 as %[S ->]; iSplitR; eauto.
   Qed.
 
   Lemma lty_le_dual_select (Ss : gmap Z (lsty Σ)) :
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index b348a2d..3730b0c 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -509,7 +509,7 @@ Section properties.
       { by apply lookup_insert. }
       rewrite Hxc.
       iAssert (c ↣ <? (Xs : ltys Σ kt) (v : val)>
-        MSG v {{ â–· ltty_car (ktele_app A Xs) v }}; lsty_car (ktele_app S Xs)) with "[Hc]" as "Hc".
+        MSG v {{ ltty_car (ktele_app A Xs) v }}; lsty_car (ktele_app S Xs)) with "[Hc]" as "Hc".
       { iApply (iProto_mapsto_le with "Hc"); iIntros "!>". rewrite HM.
         iApply iProto_le_lmsg_texist. }
       wp_recv (Xs v) as "HA". wp_pures.
-- 
GitLab