From ce6097e898b08507537a40bce0c7bbdb3a8b097a Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 16 Apr 2020 12:01:06 +0200
Subject: [PATCH] Changed the meta letter for session types from P to S

---
 theories/logrel/session_types.v | 48 +++++++++++++-------------
 theories/logrel/subtyping.v     | 60 ++++++++++++++++-----------------
 theories/logrel/types.v         | 30 ++++++++---------
 3 files changed, 69 insertions(+), 69 deletions(-)

diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 372f36c..3f1e67d 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -10,21 +10,21 @@ Section protocols.
 
   Definition lsty_end : lsty Σ := Lsty END.
 
-  Definition lsty_message (a : action) (A : lty Σ) (P : lsty Σ) : lsty Σ :=
-    Lsty (<a> v, MSG v {{ A v }}; lsty_car P).
+  Definition lsty_message (a : action) (A : lty Σ) (S : lsty Σ) : lsty Σ :=
+    Lsty (<a> v, MSG v {{ A v }}; lsty_car S).
 
-  Definition lsty_send (A : lty Σ) (P : lsty Σ) : lsty Σ :=
-    lsty_message Send A P.
-  Definition lsty_recv (A : lty Σ) (P : lsty Σ) : lsty Σ :=
-    lsty_message Recv A P.
+  Definition lsty_send (A : lty Σ) (S : lsty Σ) : lsty Σ :=
+    lsty_message Send A S.
+  Definition lsty_recv (A : lty Σ) (S : lsty Σ) : lsty Σ :=
+    lsty_message Recv A S.
 
-  Definition lsty_choice (a : action) (Ps : gmap Z (lsty Σ)) : lsty Σ :=
-    Lsty (<a> x : Z, MSG #x {{ ⌜is_Some (Ps !! x)⌝ }}; lsty_car (Ps !!! x)).
+  Definition lsty_choice (a : action) (Ss : gmap Z (lsty Σ)) : lsty Σ :=
+    Lsty (<a> x : Z, MSG #x {{ ⌜is_Some (Ss !! x)⌝ }}; lsty_car (Ss !!! x)).
 
-  Definition lsty_select (Ps : gmap Z (lsty Σ)) : lsty Σ :=
-    lsty_choice Send Ps.
-  Definition lsty_branch (Ps : gmap Z (lsty Σ)) : lsty Σ :=
-    lsty_choice Recv Ps.
+  Definition lsty_select (Ss : gmap Z (lsty Σ)) : lsty Σ :=
+    lsty_choice Send Ss.
+  Definition lsty_branch (Ss : gmap Z (lsty Σ)) : lsty Σ :=
+    lsty_choice Recv Ss.
 
   Definition lsty_rec1 (C : lsty Σ → lsty Σ) `{!Contractive C}
     (rec : lsty Σ) : lsty Σ := Lsty (C rec).
@@ -33,22 +33,22 @@ Section protocols.
   Definition lsty_rec (C : lsty Σ → lsty Σ) `{!Contractive C} : lsty Σ :=
     fixpoint (lsty_rec1 C).
 
-  Definition lsty_dual (P : lsty Σ) : lsty Σ :=
-    Lsty (iProto_dual P).
+  Definition lsty_dual (S : lsty Σ) : lsty Σ :=
+    Lsty (iProto_dual S).
 
-  Definition lsty_app (P1 P2 : lsty Σ) : lsty Σ :=
-    Lsty (P1 <++> P2).
+  Definition lsty_app (S1 S2 : lsty Σ) : lsty Σ :=
+    Lsty (S1 <++> S2).
 End protocols.
 
 Section Propers.
   Context `{heapG Σ, protoG Σ}.
 
   Global Instance lsty_message_ne a : NonExpansive2 (@lsty_message Σ a).
-  Proof. intros n A A' ? P P' ?. by apply iProto_message_ne; simpl. Qed.
+  Proof. intros n A A' ? S S' ?. by apply iProto_message_ne; simpl. Qed.
   Global Instance lsty_message_contractive n a :
     Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_message Σ a).
   Proof.
-    intros A A' ? P P' ?.
+    intros A A' ? S S' ?.
     apply iProto_message_contractive; simpl; done || by destruct n.
   Qed.
 
@@ -66,11 +66,11 @@ Section Propers.
 
   Global Instance lsty_choice_ne a : NonExpansive (@lsty_choice Σ a).
   Proof.
-    intros n Ps1 Ps2 Pseq. apply iProto_message_ne; simpl; solve_proper.
+    intros n Ss1 Ss2 Pseq. apply iProto_message_ne; simpl; solve_proper.
   Qed.
   Global Instance lsty_choice_contractive a : Contractive (@lsty_choice Σ a).
   Proof.
-    intros ? Ps1 Ps2 ?.
+    intros ? Ss1 Ss2 ?.
     apply iProto_message_contractive; destruct n; simpl; done || solve_proper.
   Qed.
 
@@ -91,8 +91,8 @@ Section Propers.
 End Propers.
 
 Notation "'END'" := lsty_end : lsty_scope.
-Notation "<!!> A ; P" :=
-  (lsty_send A P) (at level 20, A, P at level 200) : lsty_scope.
-Notation "<??> A ; P" :=
-  (lsty_recv A P) (at level 20, A, P at level 200) : lsty_scope.
+Notation "<!!> A ; S" :=
+  (lsty_send A S) (at level 20, A, S at level 200) : lsty_scope.
+Notation "<??> A ; S" :=
+  (lsty_recv A S) (at level 20, A, S at level 200) : lsty_scope.
 Infix "<++>" := lsty_app (at level 60) : lsty_scope.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 9073812..f864d2e 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -18,7 +18,7 @@ Proof. solve_proper. Qed.
 Definition lsty_le {Σ} (P1 P2 : lsty Σ) : iProp Σ :=
   â–¡ iProto_le P1 P2.
 Arguments lsty_le {_} _%lsty _%lsty.
-Infix "<p:" := lsty_le (at level 70).
+Infix "<s:" := lsty_le (at level 70).
 Instance: Params (@lsty_le) 1 := {}.
 
 Instance lsty_le_ne {Σ} : NonExpansive2 (@lsty_le Σ).
@@ -29,9 +29,9 @@ Proof. solve_proper. Qed.
 Section subtype.
   Context `{heapG Σ, chanG Σ}.
   Implicit Types A : lty Σ.
-  Implicit Types P : lsty Σ.
+  Implicit Types S : lsty Σ.
 
-  Lemma lty_le_refl A : ⊢ A <: A.
+  Lemma lty_le_refl (A : lty Σ) : ⊢ A <: A.
   Proof. by iIntros (v) "!> H". Qed.
 
   Lemma lty_le_trans A1 A2 A3 : A1 <: A2 -∗ A2 <: A3 -∗ A1 <: A3.
@@ -169,15 +169,15 @@ Section subtype.
     - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
   Qed.
 
-  Lemma lsty_le_refl P : ⊢ P <p: P.
+  Lemma lsty_le_refl (S : lsty Σ) : ⊢ S <s: S.
   Proof. iApply iProto_le_refl. Qed.
 
-  Lemma lsty_le_trans P1 P2 P3 : P1 <p: P2 -∗ P2 <p: P3 -∗ P1 <p: P3.
+  Lemma lsty_le_trans S1 S2 S3 : S1 <s: S2 -∗ S2 <s: S3 -∗ S1 <s: S3.
   Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_trans. Qed.
 
-  Lemma lsty_send_le A1 A2 P1 P2 :
-    ▷ (A2 <: A1) -∗ ▷ (P1 <p: P2) -∗
-    (<!!> A1 ; P1) <p: (<!!> A2 ; P2).
+  Lemma lsty_send_le A1 A2 S1 S2 :
+    ▷ (A2 <: A1) -∗ ▷ (S1 <s: S2) -∗
+    (<!!> A1 ; S1) <s: (<!!> A2 ; S2).
   Proof.
     iIntros "#HAle #HPle !>".
     iApply iProto_le_send=> /=.
@@ -186,9 +186,9 @@ Section subtype.
     eauto with iFrame.
   Qed.
 
-  Lemma lsty_recv_le A1 A2 P1 P2 :
-    ▷ (A1 <: A2) -∗ ▷ (P1 <p: P2) -∗
-    (<??> A1 ; P1) <p: (<??> A2 ; P2).
+  Lemma lsty_recv_le A1 A2 S1 S2 :
+    ▷ (A1 <: A2) -∗ ▷ (S1 <s: S2) -∗
+    (<??> A1 ; S1) <s: (<??> A2 ; S2).
   Proof.
     iIntros "#HAle #HPle !>".
     iApply iProto_le_recv; simpl.
@@ -198,23 +198,23 @@ Section subtype.
   Qed.
 
   Lemma lsty_swap_le (A1 A2 : lty Σ) (P : lsty Σ) :
-    ⊢ (<??> A1 ; <!!> A2 ; P) <p: (<!!> A2 ; <??> A1 ; P).
+    ⊢ (<??> A1 ; <!!> A2 ; P) <s: (<!!> A2 ; <??> A1 ; P).
   Proof.
     iIntros "!>".
-    iApply iProto_le_swap. iIntros (x1 x2) "/= HP1 HP2".
+    iApply iProto_le_swap. iIntros (x1 x2) "/= HS1 HS2".
     iExists _, _,
       (tele_app (TT:=[tele _]) (λ x2, (x2, A2 x2, (P:iProto Σ)))),
       (tele_app (TT:=[tele _]) (λ x1, (x1, A1 x1, (P:iProto Σ)))),
       x2, x1; simpl.
     do 2 (iSplit; [done|]).
-    iFrame "HP1 HP2".
+    iFrame "HS1 HS2".
     iModIntro.
     do 2 (iSplitR; [iApply iProto_le_refl|]). by iFrame.
   Qed.
 
   Lemma lsty_select_le_subseteq (Ps1 Ps2 : gmap Z (lsty Σ)) :
     Ps2 ⊆ Ps1 →
-    ⊢ lsty_select Ps1 <p: lsty_select Ps2.
+    ⊢ lsty_select Ps1 <s: lsty_select Ps2.
   Proof.
     iIntros (Hsub) "!>".
     iApply iProto_le_send; simpl.
@@ -231,8 +231,8 @@ Section subtype.
   Qed.
 
   Lemma lsty_select_le (Ps1 Ps2 : gmap Z (lsty Σ)) :
-    (▷ [∗ map] i ↦ P1;P2 ∈ Ps1; Ps2, P1 <p: P2) -∗
-    lsty_select Ps1 <p: lsty_select Ps2.
+    (▷ [∗ map] i ↦ S1;S2 ∈ Ps1; Ps2, S1 <s: S2) -∗
+    lsty_select Ps1 <s: lsty_select Ps2.
   Proof.
     iIntros "#H1 !>".
     iApply iProto_le_send; simpl.
@@ -250,7 +250,7 @@ Section subtype.
 
   Lemma lsty_branch_le_subseteq (Ps1 Ps2 : gmap Z (lsty Σ)) :
     Ps1 ⊆ Ps2 →
-    ⊢ lsty_branch Ps1 <p: lsty_branch Ps2.
+    ⊢ lsty_branch Ps1 <s: lsty_branch Ps2.
   Proof.
     iIntros (Hsub) "!>".
     iApply iProto_le_recv; simpl.
@@ -267,8 +267,8 @@ Section subtype.
   Qed.
 
   Lemma lsty_branch_le (Ps1 Ps2 : gmap Z (lsty Σ)) :
-    (▷ [∗ map] i ↦ P1;P2 ∈ Ps1; Ps2, P1 <p: P2) -∗
-    lsty_branch Ps1 <p: lsty_branch Ps2.
+    (▷ [∗ map] i ↦ S1;S2 ∈ Ps1; Ps2, S1 <s: S2) -∗
+    lsty_branch Ps1 <s: lsty_branch Ps2.
   Proof.
     iIntros "#H1 !>". iApply iProto_le_recv.
     iIntros (x) ">H !>"; iDestruct "H" as %Hsome.
@@ -283,30 +283,30 @@ Section subtype.
       + iPureIntro. by apply lookup_lookup_total; naive_solver.
   Qed.
 
-  Lemma lsty_app_le P11 P12 P21 P22 :
-    (P11 <p: P21) -∗ (P12 <p: P22) -∗
-    (P11 <++> P12) <p: (P21 <++> P22).
+  Lemma lsty_app_le S11 S12 S21 S22 :
+    (S11 <s: S21) -∗ (S12 <s: S22) -∗
+    (S11 <++> S12) <s: (S21 <++> S22).
   Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
 
-  Lemma lsty_dual_le P1 P2 : P2 <p: P1 -∗ lsty_dual P1 <p: lsty_dual P2.
+  Lemma lsty_dual_le S1 S2 : S2 <s: S1 -∗ lsty_dual S1 <s: lsty_dual S2.
   Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
 
   Lemma lsty_rec_le_1 (C : lsty Σ → lsty Σ) `{!Contractive C} :
-    ⊢ lsty_rec C <p: C (lsty_rec C).
+    ⊢ lsty_rec C <s: C (lsty_rec C).
   Proof.
     rewrite {1}/lsty_rec {1}fixpoint_unfold {1}/lsty_rec1.
     iApply lsty_le_refl.
   Qed.
   Lemma lsty_rec_le_2 (C : lsty Σ → lsty Σ) `{!Contractive C} :
-    ⊢ C (lsty_rec C) <p: lsty_rec C.
+    ⊢ C (lsty_rec C) <s: lsty_rec C.
   Proof.
     rewrite {2}/lsty_rec {1}fixpoint_unfold {1}/lsty_rec1.
     iApply lsty_le_refl.
   Qed.
 
   Lemma lsty_rec_le `{Contractive C1, Contractive C2} :
-    (□ ∀ P P', ▷ (P <p: P') -∗ C1 P <p: C2 P') -∗
-    lsty_rec C1 <p: lsty_rec C2.
+    (□ ∀ S S', ▷ (S <s: S') -∗ C1 S <s: C2 S') -∗
+    lsty_rec C1 <s: lsty_rec C2.
   Proof.
     iIntros "#Hle !>".
     iLöb as "IH".
@@ -318,8 +318,8 @@ Section subtype.
     iNext. iApply "IH".
   Qed.
 
-  Lemma lty_chan_le P1 P2 :
-    ▷ (P1 <p: P2) -∗ chan P1 <: chan P2.
+  Lemma lty_chan_le S1 S2 :
+    ▷ (S1 <s: S2) -∗ chan S1 <: chan S2.
   Proof.
     iIntros "#Hle" (v) "!> H".
     iApply (iProto_mapsto_le with "H [Hle]"). eauto.
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index d456a3c..01670e0 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -699,8 +699,8 @@ Section properties.
     Proof. solve_proper. Qed.
 
     Definition chanalloc : val := λ: "u", let: "cc" := new_chan #() in "cc".
-    Lemma ltyped_chanalloc P:
-      ⊢ ∅ ⊨ chanalloc : () → (chan P * chan (lsty_dual P)).
+    Lemma ltyped_chanalloc S:
+      ⊢ ∅ ⊨ chanalloc : () → (chan S * chan (lsty_dual S)).
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
       iIntros "!>" (u) ">->". rewrite /chanalloc. wp_pures.
@@ -710,8 +710,8 @@ Section properties.
     Qed.
 
     Definition chansend : val := λ: "chan" "val", send "chan" "val";; "chan".
-    Lemma ltyped_chansend A P:
-      ⊢ ∅ ⊨ chansend : chan (<!!> A; P) → A ⊸ chan P.
+    Lemma ltyped_chansend A S:
+      ⊢ ∅ ⊨ chansend : chan (<!!> A; S) → A ⊸ chan S.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
       iIntros "!>" (c) "Hc". rewrite /chansend. wp_pures.
@@ -720,8 +720,8 @@ Section properties.
     Qed.
 
     Definition chanrecv : val := λ: "chan", (recv "chan", "chan").
-    Lemma ltyped_chanrecv A P:
-      ⊢ ∅ ⊨ chanrecv : chan (<??> A; P) → A * chan P.
+    Lemma ltyped_chanrecv A S:
+      ⊢ ∅ ⊨ chanrecv : chan (<??> A; S) → A * chan S.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
       iIntros "!>" (c) "Hc". rewrite /chanrecv. wp_pures.
@@ -730,17 +730,17 @@ Section properties.
     Qed.
 
     Definition chanselect : val := λ: "c" "i", send "c" "i";; "c".
-    Lemma ltyped_chanselect Γ (c : val) (i : Z) P Ps :
-      Ps !! i = Some P →
-      (Γ ⊨ c : chan (lsty_select Ps)) -∗
-      Γ ⊨ chanselect c #i : chan P.
+    Lemma ltyped_chanselect Γ (c : val) (i : Z) S Ss :
+      Ss !! i = Some S →
+      (Γ ⊨ c : chan (lsty_select Ss)) -∗
+      Γ ⊨ chanselect c #i : chan S.
     Proof.
       iIntros (Hin) "#Hc !>".
       iIntros (vs) "H /=".
       rewrite /chanselect.
       iMod (wp_value_inv with "(Hc H)") as "Hc'".
       wp_send with "[]"; [by eauto|].
-      rewrite (lookup_total_correct Ps i P)=> //.
+      rewrite (lookup_total_correct Ss i S)=> //.
       by wp_pures.
     Qed.
 
@@ -749,10 +749,10 @@ Section properties.
       let: "y" := recv "c" in
       switch_body "y" 0 xs (assert: #false) $ λ i, ("f" +:+ pretty i) "c".
 
-    Lemma ltyped_chanbranch Ps A xs :
-      (∀ x, x ∈ xs ↔ is_Some (Ps !! x)) →
-      ⊢ ∅ ⊨ chanbranch xs : chan (lsty_branch Ps) ⊸
-        lty_arr_list ((λ x, (chan (Ps !!! x) ⊸ A)%lty) <$> xs) A.
+    Lemma ltyped_chanbranch Ss A xs :
+      (∀ x, x ∈ xs ↔ is_Some (Ss !! x)) →
+      ⊢ ∅ ⊨ chanbranch xs : chan (lsty_branch Ss) ⊸
+        lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A.
     Proof.
       iIntros (Hdom) "!>". iIntros (vs) "Hvs".
       iApply wp_value. iIntros (c) "Hc". wp_lam.
-- 
GitLab