From 19acb9ad8efae506a1e9a67e40396bf2e92a69ec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 17 Jun 2019 16:05:57 +0200
Subject: [PATCH] =?UTF-8?q?More=20renaming,=20use=20=CE=A6=20for=20predica?=
 =?UTF-8?q?tes=20as=20we=20do=20in=20Iris.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proto/proto_def.v   | 88 ++++++++++++++++++------------------
 theories/proto/proto_enc.v   | 38 ++++++++--------
 theories/proto/proto_specs.v | 82 ++++++++++++++++-----------------
 3 files changed, 103 insertions(+), 105 deletions(-)

diff --git a/theories/proto/proto_def.v b/theories/proto/proto_def.v
index a494aa4..06221e2 100644
--- a/theories/proto/proto_def.v
+++ b/theories/proto/proto_def.v
@@ -22,7 +22,7 @@ Instance proto_inhabited V PROP : Inhabited (proto V PROP) := populate TEnd.
 CoFixpoint dual_proto {V PROP} (prot : proto V PROP) : proto V PROP :=
   match prot with
   | TEnd => TEnd
-  | TSR a P prot => TSR (dual_action a) P (λ v, dual_proto (prot v))
+  | TSR a Φ prot => TSR (dual_action a) Φ (λ v, dual_proto (prot v))
   end.
 Instance: Params (@dual_proto) 2.
 
@@ -39,9 +39,9 @@ Notation "<!> x , prot" := (<!> x @ True, prot%proto)%proto
   (at level 200, x pattern, prot at level 200) : proto_scope.
 Notation "<?> x , prot" := (<?> x @ True, prot%proto)%proto
   (at level 200, x pattern, prot at level 200) : proto_scope.
-Notation "<!> @ P , prot" := (<!> x @ P x, prot x)%proto
+Notation "<!> @ Φ , prot" := (TSR Send Φ prot)%proto
   (at level 200, prot at level 200) : proto_scope.
-Notation "<?> @ P , prot" := (<?> x @ P x, prot x)%proto
+Notation "<?> @ Φ , prot" := (TSR Receive Φ prot)%proto
   (at level 200, prot at level 200) : proto_scope.
 
 Section proto_ofe.
@@ -50,52 +50,52 @@ Section proto_ofe.
 
   CoInductive proto_equiv : Equiv (proto V PROP) :=
     | TEnd_equiv : TEnd ≡ TEnd
-    | TSR_equiv a P1 P2 prot1 prot2 :
-       pointwise_relation V (≡) P1 P2 →
+    | TSR_equiv a Φ1 Φ2 prot1 prot2 :
+       pointwise_relation V (≡) Φ1 Φ2 →
        pointwise_relation V (≡) prot1 prot2 →
-       TSR a P1 prot1 ≡ TSR a P2 prot2.
+       TSR a Φ1 prot1 ≡ TSR a Φ2 prot2.
   Existing Instance proto_equiv.
 
   CoInductive proto_dist : Dist (proto V PROP) :=
     | TEnd_dist n : TEnd ≡{n}≡ TEnd
-    | TSR_dist_0 a P1 P2 prot1 prot2 :
-       pointwise_relation V (dist 0) P1 P2 →
-       TSR a P1 prot1 ≡{0}≡ TSR a P2 prot2
-    | TSR_dist_S n a P1 P2 prot1 prot2 :
-       pointwise_relation V (dist (S n)) P1 P2 →
+    | TSR_dist_0 a Φ1 Φ2 prot1 prot2 :
+       pointwise_relation V (dist 0) Φ1 Φ2 →
+       TSR a Φ1 prot1 ≡{0}≡ TSR a Φ2 prot2
+    | TSR_dist_S n a Φ1 Φ2 prot1 prot2 :
+       pointwise_relation V (dist (S n)) Φ1 Φ2 →
        pointwise_relation V (dist n) prot1 prot2 →
-       TSR a P1 prot1 ≡{S n}≡ TSR a P2 prot2.
+       TSR a Φ1 prot1 ≡{S n}≡ TSR a Φ2 prot2.
   Existing Instance proto_dist.
 
-  Lemma TSR_dist n a P1 P2 prot1 prot2 :
-    pointwise_relation V (dist n) P1 P2 →
+  Lemma TSR_dist n a Φ1 Φ2 prot1 prot2 :
+    pointwise_relation V (dist n) Φ1 Φ2 →
     pointwise_relation V (dist_later n) prot1 prot2 →
-    TSR a P1 prot1 ≡{n}≡ TSR a P2 prot2.
+    TSR a Φ1 prot1 ≡{n}≡ TSR a Φ2 prot2.
   Proof. destruct n; by constructor. Defined.
 
   Definition proto_ofe_mixin : OfeMixin (proto V PROP).
   Proof.
     split.
     - intros prot1 prot2. split.
-      + revert prot1 prot2. cofix IH; destruct 1 as [|a P1 P2 prot1' prot2' HP]=> n.
+      + revert prot1 prot2. cofix IH; destruct 1 as [|a Φ1 Φ2 prot1' prot2' HΦ]=> n.
         { constructor. }
         destruct n as [|n].
-        * constructor=> v. apply equiv_dist, HP.
-        * constructor=> v. apply equiv_dist, HP. by apply IH.
-      + revert prot1 prot2. cofix IH=> -[|a1 P1 prot1] -[|a2 P2 prot2] Hprot;
+        * constructor=> v. apply equiv_dist, HΦ.
+        * constructor=> v. apply equiv_dist, HΦ. by apply IH.
+      + revert prot1 prot2. cofix IH=> -[|a1 Φ1 prot1] -[|a2 Φ2 prot2] Hprot;
           feed inversion (Hprot O); subst; constructor=> v.
         * apply equiv_dist=> n. feed inversion (Hprot n); auto.
         * apply IH=> n. feed inversion (Hprot (S n)); auto.
     - intros n. split.
-      + revert n. cofix IH=> -[|n] [|a P prot]; constructor=> v; auto.
+      + revert n. cofix IH=> -[|n] [|a Φ prot]; constructor=> v; auto.
       + revert n. cofix IH; destruct 1; constructor=> v; symmetry; auto.
       + revert n. cofix IH; destruct 1; inversion 1; constructor=> v; etrans; eauto.
     - cofix IH=> -[|n]; inversion 1; constructor=> v; try apply dist_S; auto.
   Qed.
   Canonical Structure protoC : ofeT := OfeT (proto V PROP) proto_ofe_mixin.
 
-  Definition proto_head (d : V -c> PROP) (prot : proto V PROP) : V -c> PROP :=
-    match prot with TEnd => d | TSR a P prot => P end.
+  Definition proto_head (dΦ : V -c> PROP) (prot : proto V PROP) : V -c> PROP :=
+    match prot with TEnd => dΦ | TSR a Φ prot => Φ end.
   Definition proto_tail (v : V) (prot : protoC) : later protoC :=
     match prot with TEnd => Next TEnd | TSR a P prot => Next (prot v) end.
   Global Instance proto_head_ne d : NonExpansive (proto_head d).
@@ -106,7 +106,7 @@ Section proto_ofe.
   Definition proto_force (prot : proto V PROP) : proto V PROP :=
     match prot with
     | TEnd => TEnd
-    | TSR a P prot => TSR a P prot
+    | TSR a Φ prot => TSR a Φ prot
     end.
   Lemma proto_force_eq prot : proto_force prot = prot.
   Proof. by destruct prot. Defined.
@@ -114,8 +114,8 @@ Section proto_ofe.
   CoFixpoint proto_compl_go `{!Cofe PROP} (c : chain protoC) : protoC :=
     match c O with
     | TEnd => TEnd
-    | TSR a P prot => TSR a
-       (compl (chain_map (proto_head P) c) : V → PROP)
+    | TSR a Φ prot => TSR a
+       (compl (chain_map (proto_head Φ) c) : V → PROP)
        (λ v, proto_compl_go (later_chain (chain_map (proto_tail v) c)))
     end.
 
@@ -124,16 +124,16 @@ Section proto_ofe.
   Next Obligation.
     intros ? n c; rewrite /compl. revert c n. cofix IH=> c n.
     rewrite -(proto_force_eq (proto_compl_go c)) /=.
-    destruct (c O) as [|a P prot'] eqn:Hc0.
+    destruct (c O) as [|a Φ prot'] eqn:Hc0.
     - assert (c n ≡{0}≡ TEnd) as Hcn.
       { rewrite -Hc0 -(chain_cauchy c 0 n) //. lia. }
       by inversion Hcn.
-    - assert (c n ≡{0}≡ TSR a P prot') as Hcn.
+    - assert (c n ≡{0}≡ TSR a Φ prot') as Hcn.
       { rewrite -Hc0 -(chain_cauchy c 0 n) //. lia. }
-      inversion Hcn as [|? P' ? prot'' ? HP|]; subst.
+      inversion Hcn as [|? P' ? prot'' ? HΦ|]; subst.
       destruct n as [|n]; constructor.
-      + intros v. by rewrite (conv_compl 0 (chain_map (proto_head P) c) v) /= -H.
-      + intros v. by rewrite (conv_compl _ (chain_map (proto_head P) c) v) /= -H.
+      + intros v. by rewrite (conv_compl 0 (chain_map (proto_head Φ) c) v) /= -H.
+      + intros v. by rewrite (conv_compl _ (chain_map (proto_head Φ) c) v) /= -H.
       + intros v. assert (prot'' v = later_car (proto_tail v (c (S n)))) as ->.
         { by rewrite -H /=. }
         apply IH.
@@ -147,7 +147,7 @@ Section proto_ofe.
     Proper (pointwise_relation _ (dist n) ==>
             pointwise_relation _ (dist n) ==> dist n) (TSR a).
   Proof.
-    intros P1 P2 HP prot1 prot2 Hst. apply TSR_proto_contractive=> //.
+    intros Φ1 Φ2 HΦ prot1 prot2 Hst. apply TSR_proto_contractive=> //.
     destruct n as [|n]=> // v /=. by apply dist_S.
   Qed.
   Global Instance TSR_proto_proper a :
@@ -175,8 +175,8 @@ Section proto_ofe.
     prot1 ≡ prot2 ⊣⊢@{uPredI M}
         match prot1, prot2 with
         | TEnd, TEnd => True
-        | TSR a1 P1 prot1, TSR a2 P2 prot2 =>
-          ⌜ a1 = a2 ⌝ ∧ (∀ v, P1 v ≡ P2 v) ∧ ▷ (∀ v, prot1 v ≡ prot2 v)
+        | TSR a1 Φ1 prot1, TSR a2 Φ2 prot2 =>
+          ⌜ a1 = a2 ⌝ ∧ (∀ v, Φ1 v ≡ Φ2 v) ∧ ▷ (∀ v, prot1 v ≡ prot2 v)
         | _, _ => False
         end.
   Proof.
@@ -185,16 +185,16 @@ Section proto_ofe.
     by intros [[= ->] [??]]; destruct n; constructor.
   Qed.
 
-  Lemma proto_later_equiv M prot a P2 prot2 :
-    ▷ (prot ≡ TSR a P2 prot2) -∗
-    ◇ (∃ P1 prot1, prot ≡ TSR a P1 prot1 ∗
-                 ▷ (∀ v, P1 v ≡ P2 v) ∗
+  Lemma proto_later_equiv M prot a Φ2 prot2 :
+    ▷ (prot ≡ TSR a Φ2 prot2) -∗
+    ◇ (∃ Φ1 prot1, prot ≡ TSR a Φ1 prot1 ∗
+                 ▷ (∀ v, Φ1 v ≡ Φ2 v) ∗
                  ▷ ▷ (∀ v, prot1 v ≡ prot2 v) : uPred M).
   Proof.
-    iIntros "Heq". destruct prot as [|a' P1 prot1].
+    iIntros "Heq". destruct prot as [|a' Φ1 prot1].
     - iDestruct (proto_equivI with "Heq") as ">[]".
-    - iDestruct (proto_equivI with "Heq") as "(>-> & HPeq & Hsteq)".
-      iExists P1, prot1. auto.
+    - iDestruct (proto_equivI with "Heq") as "(>-> & HΦeq & Hsteq)".
+      iExists Φ1, prot1. auto.
   Qed.
 
   Lemma dual_proto_flip {M} prot1 prot2 :
@@ -212,7 +212,7 @@ CoFixpoint proto_map {V PROP PROP'} (f : PROP → PROP')
     (prot : proto V PROP) : proto V PROP' :=
   match prot with
   | TEnd => TEnd
-  | TSR a P prot => TSR a (λ v, f (P v)) (λ v, proto_map f (prot v))
+  | TSR a Φ prot => TSR a (λ v, f (Φ v)) (λ v, proto_map f (prot v))
   end.
 Lemma proto_map_ext_ne {V PROP} {PROP' : ofeT}
     (f g : PROP → PROP') (prot : proto V PROP) n :
@@ -220,7 +220,7 @@ Lemma proto_map_ext_ne {V PROP} {PROP' : ofeT}
 Proof.
   revert n prot. cofix IH=> n prot Hf.
   rewrite -(proto_force_eq (proto_map f prot)) -(proto_force_eq (proto_map g prot)).
-  destruct prot as [|a P prot], n as [|n]; constructor=> v //. apply IH; auto using dist_S.
+  destruct prot as [|a Φ prot], n as [|n]; constructor=> v //. apply IH; auto using dist_S.
 Qed.
 Lemma proto_map_ext {V PROP} {B : ofeT} (f g : PROP → B) (prot : proto V PROP) :
   (∀ x, f x ≡ g x) → proto_map f prot ≡ proto_map g prot.
@@ -305,10 +305,10 @@ Section DualProto.
   Global Instance is_dual_end : IsDualProto (TEnd : proto V PROP) TEnd.
   Proof. by rewrite /IsDualProto -(proto_force_eq (dual_proto _)). Qed.
 
-  Global Instance is_dual_tsr a1 a2 P (prot1 prot2 : V → proto V PROP) :
+  Global Instance is_dual_tsr a1 a2 Φ (prot1 prot2 : V → proto V PROP) :
     IsDualAction a1 a2 →
     (∀ x, IsDualProto (prot1 x) (prot2 x)) →
-    IsDualProto (TSR a1 P prot1) (TSR a2 P prot2).
+    IsDualProto (TSR a1 Φ prot1) (TSR a2 Φ prot2).
   Proof.
     rewrite /IsDualAction /IsDualProto. intros <- Hst.
     rewrite /IsDualProto -(proto_force_eq (dual_proto _)) /=.
diff --git a/theories/proto/proto_enc.v b/theories/proto/proto_enc.v
index 2ef46d5..f9e5bd1 100644
--- a/theories/proto/proto_enc.v
+++ b/theories/proto/proto_enc.v
@@ -5,16 +5,16 @@ Section DualProtoEnc.
   Context `{ValEncDec V} {PROP: bi} .
 
   Definition TSR'
-      (a : action) (P : V → PROP) (prot : V → proto val PROP) : proto val PROP :=
+      (a : action) (Φ : V → PROP) (prot : V → proto val PROP) : proto val PROP :=
     TSR a
-      (λ v, if val_decode v is Some x then P x else False)%I
+      (λ v, if val_decode v is Some x then Φ x else False)%I
       (λ v, if val_decode v is Some x then prot x else TEnd (* dummy *)).
   Global Instance: Params (@TSR') 3.
 
-  Global Instance is_dual_tsr' a1 a2 P (st1 st2 : V → proto val PROP) :
+  Global Instance is_dual_tsr' a1 a2 Φ (st1 st2 : V → proto val PROP) :
     IsDualAction a1 a2 →
     (∀ x, IsDualProto (st1 x) (st2 x)) →
-    IsDualProto (TSR' a1 P st1) (TSR' a2 P st2).
+    IsDualProto (TSR' a1 Φ st1) (TSR' a2 Φ st2).
   Proof.
     rewrite /IsDualAction /IsDualProto. intros <- Hst.
     rewrite -(proto_force_eq (dual_proto _)).
@@ -33,41 +33,39 @@ Notation "<!> x , prot" := (<!> x @ True, (prot x))%proto
   (at level 200, x pattern, prot at level 200) : proto_scope.
 Notation "<?> x , prot" := (<?> x @ True, (prot x))%proto
   (at level 200, x pattern, prot at level 200) : proto_scope.
-Notation "<!> @ P , prot" := (<!> dummy__ @ P dummy__, prot dummy__)%proto
+Notation "<!> @ Φ , prot" := (TSR' Send Φ prot)
   (at level 200, prot at level 200) : proto_scope.
-Notation "<?> @ P , prot" := (<?> dummy__ @ P dummy__, prot dummy__)%proto
+Notation "<?> @ Φ , prot" := (TSR' Receive Φ prot)
   (at level 200, prot at level 200) : proto_scope.
 
 Section proto_enc_specs.
   Context `{!heapG Σ, !logrelG val Σ} `{ValEncDec A} (N : namespace).
 
-  Lemma send_st_spec prot γ c s (P : A → iProp Σ) w :
-    {{{ P w ∗ ⟦ c @ s : <!> @ P, prot ⟧{N,γ} }}}
+  Lemma send_st_spec prot γ c s (Φ : A → iProp Σ) w :
+    {{{ Φ w ∗ ⟦ c @ s : <!> @ Φ, prot ⟧{N,γ} }}}
       send c #s (val_encode w)
     {{{ RET #(); ⟦ c @ s : prot w ⟧{N,γ} }}}.
   Proof.
-    iIntros (Φ) "[HP Hsend] HΦ".
-    iApply (send_st_spec with "[HP $Hsend]").
+    iIntros (Ψ) "[HΦ Hsend] HΨ".
+    iApply (send_st_spec with "[HΦ $Hsend]").
     { by rewrite val_encode_decode. }
     iNext. rewrite val_encode_decode.
-    by iApply "HΦ".
+    by iApply "HΨ".
   Qed.
 
-  Lemma recv_st_spec prot γ c s (P : A → iProp Σ) :
-    {{{ ⟦ c @ s : <?> @ P, prot ⟧{N,γ} }}}
+  Lemma recv_st_spec prot γ c s (Φ : A → iProp Σ) :
+    {{{ ⟦ c @ s : <?> @ Φ, prot ⟧{N,γ} }}}
       recv c #s
-    {{{ v, RET (val_encode v); ⟦ c @ s : prot v ⟧{N,γ} ∗ P v }}}.
+    {{{ v, RET (val_encode v); ⟦ c @ s : prot v ⟧{N,γ} ∗ Φ v }}}.
   Proof.
-    iIntros (Φ) "Hrecv HΦ".
+    iIntros (Ψ) "Hrecv HΨ".
     iApply (recv_st_spec with "Hrecv").
-    iNext. iIntros (v).
-    iIntros "[H HP]".
-    iAssert (∃ w, ⌜val_decode v = Some w⌝ ∗ P w)%I with "[HP]" as (w Hw) "HP".
+    iIntros "!>" (v) "[H HΦ]".
+    iAssert (∃ w, ⌜val_decode v = Some w⌝ ∗ Φ w)%I with "[HΦ]" as (w Hw) "HΦ".
     { destruct (val_decode v) as [x|]; last done.
       iExists x. by iFrame. }
-    iSpecialize ("HΦ" $!w).
     apply val_decode_encode in Hw as <-.
-    iApply "HΦ". iFrame "HP".
+    iApply ("HΨ" $!w). iFrame "HΦ".
     by rewrite val_encode_decode.
   Qed.
 End proto_enc_specs.
diff --git a/theories/proto/proto_specs.v b/theories/proto/proto_specs.v
index cd99fde..cef54d1 100644
--- a/theories/proto/proto_specs.v
+++ b/theories/proto/proto_specs.v
@@ -20,7 +20,7 @@ Fixpoint prot_eval `{!logrelG val Σ} (vs : list val) (prot1 prot2 : proto val (
   match vs with
   | [] => prot1 ≡ dual_proto prot2
   | v::vs => match prot2 with
-             | TSR Receive P prot2  => P v ∗ ▷ prot_eval vs prot1 (prot2 v)
+             | TSR Receive Φ prot2  => Φ v ∗ ▷ prot_eval vs prot1 (prot2 v)
              | _ => False
              end
   end%I.
@@ -67,7 +67,7 @@ Section proto.
   Global Instance prot_eval_ne : NonExpansive2 (prot_eval vs).
   Proof.
     induction vs as [|v vs IH];
-      destruct 2 as [n|[] P1 P2 prot1 prot2|n [] P1 P2 prot1 prot2]=> //=.
+      destruct 2 as [n|[] Φ1 Φ2 prot1 prot2|n [] Φ1 Φ2 prot1 prot2]=> //=.
     - by repeat f_equiv.
     - f_equiv. done. f_equiv. by constructor.
     - f_equiv. done. f_equiv. by constructor.
@@ -114,24 +114,24 @@ Section proto.
     by rewrite own_op.
   Qed.
 
-  Lemma prot_eval_send (P : val →iProp Σ) prot vs v protr :
-    P v -∗ prot_eval vs (<!> @ P, prot) protr -∗ prot_eval (vs ++ [v]) (prot v) protr.
+  Lemma prot_eval_send (Φ : val → iProp Σ) prot vs v protr :
+    Φ v -∗ prot_eval vs (<!> @ Φ, prot) protr -∗ prot_eval (vs ++ [v]) (prot v) protr.
   Proof.
-    iIntros "HP".
+    iIntros "HΦ".
     iRevert (protr).
     iInduction vs as [|v' vs] "IH"; iIntros (protr) "Heval".
     - iDestruct (dual_proto_flip with "Heval") as "Heval".
       iRewrite -"Heval"; simpl.
       rewrite dual_proto_involutive.
       by iFrame.
-    - destruct protr as [|[] P' protr]=> //=.
+    - destruct protr as [|[] Φ' protr]=> //=.
       iDestruct "Heval" as "[$ Heval]".
-      by iApply ("IH" with "HP").
+      by iApply ("IH" with "HΦ").
   Qed.
 
-  Lemma prot_eval_recv (P : val → iProp Σ) prot1 l prot2 v :
-     prot_eval (v :: l) prot1 (<?> @ P, prot2) -∗ ▷ prot_eval l prot1 (prot2 v) ∗ P v.
-  Proof. iDestruct 1 as "[HP Heval]". iFrame. Qed.
+  Lemma prot_eval_recv (Φ : val → iProp Σ) prot1 l prot2 v :
+     prot_eval (v :: l) prot1 (<?> @ Φ, prot2) -∗ ▷ prot_eval l prot1 (prot2 v) ∗ Φ v.
+  Proof. iDestruct 1 as "[HΦ Heval]". iFrame. Qed.
 
   Lemma new_chan_vs prot E c cγ :
     is_chan N cγ c ∗
@@ -175,11 +175,11 @@ Section proto.
     by iFrame.
   Qed.
 
-  Lemma send_vs c γ s (P : val → iProp Σ) prot E :
+  Lemma send_vs c γ s (Φ : val → iProp Σ) prot E :
     ↑N ⊆ E →
-    ⟦ c @ s : TSR Send P prot ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
+    ⟦ c @ s : <!> @ Φ, prot ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
       chan_own (prot_c_name γ) s vs ∗
-      ▷ ∀ v, P v -∗
+      ▷ ∀ v, Φ v -∗
              chan_own (prot_c_name γ) s (vs ++ [v]) ={E∖↑N,E}=∗
              ⟦ c @ s : prot v ⟧{N,γ}.
   Proof.
@@ -188,7 +188,7 @@ Section proto.
     iModIntro.
     destruct s.
     - iExists _.
-      iIntros "{$Hclf} !>" (v) "HP Hclf".
+      iIntros "{$Hclf} !>" (v) "HΦ Hclf".
       iRename "Hstf" into "Hstlf".
       iDestruct (prot_excl_eq with "Hstla Hstlf") as "#Heq".
       iMod (prot_excl_update _ _ _ _ (prot v) with "Hstla Hstlf") as "[Hstla Hstlf]".
@@ -198,14 +198,14 @@ Section proto.
         iLeft.
         iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
         - iSplit=> //.
-          iApply (prot_eval_send with "HP").
+          iApply (prot_eval_send with "HΦ").
           by iRewrite "Heq" in "Heval".
         - iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //=.
           iSplit; first done.
-          iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_proto_involutive. }
+          iRewrite "Heval". simpl. iFrame "HΦ". by rewrite dual_proto_involutive. }
       iModIntro. iFrame. auto.
     - iExists _.
-      iIntros "{$Hcrf} !>" (v) "HP Hcrf".
+      iIntros "{$Hcrf} !>" (v) "HΦ Hcrf".
       iRename "Hstf" into "Hstrf".
       iDestruct (prot_excl_eq with "Hstra Hstrf") as "#Heq".
       iMod (prot_excl_update _ _ _ _ (prot v) with "Hstra Hstrf") as "[Hstra Hstrf]".
@@ -216,38 +216,38 @@ Section proto.
         iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
         - iRewrite "Heq" in "Heval". destruct l as [|vl l]=> //.
           iSplit; first done. simpl.
-          iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_proto_involutive.
+          iRewrite "Heval". simpl. iFrame "HΦ". by rewrite dual_proto_involutive.
         - iSplit=> //.
-          iApply (prot_eval_send with "HP").
+          iApply (prot_eval_send with "HΦ").
           by iRewrite "Heq" in "Heval". }
       iModIntro. iFrame. auto.
   Qed.
 
-  Lemma send_st_spec prot γ c s (P : val → iProp Σ) v :
-    {{{ P v ∗ ⟦ c @ s : <!> @ P , prot ⟧{N,γ} }}}
+  Lemma send_st_spec prot γ c s (Φ : val → iProp Σ) v :
+    {{{ Φ v ∗ ⟦ c @ s : <!> @ Φ, prot ⟧{N,γ} }}}
       send c #s v
     {{{ RET #(); ⟦ c @ s : prot v ⟧{N,γ} }}}.
   Proof.
-    iIntros (Φ) "[HP Hsend] HΦ".
+    iIntros (Ψ) "[HΦ Hsend] HΨ".
     iApply (send_spec with "[#]").
     { iDestruct "Hsend" as "[? [$ ?]]". }
     iMod (send_vs with "Hsend") as (vs) "[Hch H]"; first done.
     iModIntro. iExists vs. iFrame "Hch".
-    iIntros "!> Hupd". iApply "HΦ".
-    iApply ("H" $! v with "HP"). by destruct s.
+    iIntros "!> Hupd". iApply "HΨ".
+    iApply ("H" $! v with "HΦ"). by destruct s.
   Qed.
 
-  Lemma try_recv_vs c γ s (P : val → iProp Σ) prot E :
+  Lemma try_recv_vs c γ s (Φ : val → iProp Σ) prot E :
     ↑N ⊆ E →
-    ⟦ c @ s : TSR Receive P prot ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
+    ⟦ c @ s : TSR Receive Φ prot ⟧{N,γ} ={E,E∖↑N}=∗ ∃ vs,
       chan_own (prot_c_name γ) (dual_side s) vs ∗
       ▷ ((⌜vs = []⌝ -∗
            chan_own (prot_c_name γ) (dual_side s) vs ={E∖↑N,E}=∗
-           ⟦ c @ s : TSR Receive P prot ⟧{N,γ}) ∧
+           ⟦ c @ s : <?> @ Φ, prot ⟧{N,γ}) ∧
          (∀ v vs',
            ⌜vs = v :: vs'⌝ -∗
            chan_own (prot_c_name γ) (dual_side s) vs' ={E∖↑N,E}=∗
-           ⟦ c @ s : (prot v) ⟧{N,γ} ∗ ▷ P v)).
+           ⟦ c @ s : prot v ⟧{N,γ} ∗ ▷ Φ v)).
   Proof.
     iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
     iInv N as (l r protl protr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
@@ -295,13 +295,13 @@ Section proto.
         iNext. by iRewrite -("HPeq" $! v).
   Qed.
 
-  Lemma try_recv_st_spec prot γ c s (P : val → iProp Σ) :
-    {{{ ⟦ c @ s : <?> @ P , prot ⟧{N,γ} }}}
+  Lemma try_recv_st_spec prot γ c s (Φ : val → iProp Σ) :
+    {{{ ⟦ c @ s : <?> @ Φ, prot ⟧{N,γ} }}}
       try_recv c #s
-    {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : <?> @ P, prot ⟧{N,γ}) ∨
-                  (∃ w, ⌜v = SOMEV w⌝ ∧ ⟦ c @ s : prot w ⟧{N,γ} ∗ ▷ P w)}}}.
+    {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : <?> @ Φ, prot ⟧{N,γ}) ∨
+                  (∃ w, ⌜v = SOMEV w⌝ ∧ ⟦ c @ s : prot w ⟧{N,γ} ∗ ▷ Φ w)}}}.
   Proof.
-    iIntros (Φ) "Hrecv HΦ".
+    iIntros (Ψ) "Hrecv HΨ".
     iApply (try_recv_spec with "[#]").
     { iDestruct "Hrecv" as "[? [$ ?]]". }
     iMod (try_recv_vs with "Hrecv") as (vs) "[Hch H]"; first done.
@@ -312,27 +312,27 @@ Section proto.
       iDestruct "H" as "[H _]".
       iMod ("H" $!Hvs with "Hown") as "H".
       iModIntro.
-      iApply "HΦ"=> //.
+      iApply "HΨ"=> //.
       eauto with iFrame.
     - iIntros (v vs' Hvs) "Hown".
       iDestruct "H" as "[_ H]".
       iMod ("H" $!v vs' Hvs with "Hown") as "H".
       iModIntro.
-      iApply "HΦ"; eauto with iFrame.
+      iApply "HΨ"; eauto with iFrame.
   Qed.
 
-  Lemma recv_st_spec prot γ c s (P : val → iProp Σ) :
-    {{{ ⟦ c @ s : <?> @ P ,  prot ⟧{N,γ} }}}
+  Lemma recv_st_spec prot γ c s (Φ : val → iProp Σ) :
+    {{{ ⟦ c @ s : <?> @ Φ,  prot ⟧{N,γ} }}}
       recv c #s
-    {{{ v, RET v; ⟦ c @ s : prot v ⟧{N,γ} ∗ P v }}}.
+    {{{ v, RET v; ⟦ c @ s : prot v ⟧{N,γ} ∗ Φ v }}}.
   Proof.
-    iIntros (Φ) "Hrecv HΦ".
+    iIntros (Ψ) "Hrecv HΨ".
     iLöb as "IH". wp_rec.
     wp_apply (try_recv_st_spec with "Hrecv").
     iIntros (v) "H".
     iDestruct "H" as "[[-> H]| H]".
     - wp_pures. by iApply ("IH" with "[H]").
-    - iDestruct "H" as (w ->) "[H HP]".
-      wp_pures. iApply "HΦ". iFrame.
+    - iDestruct "H" as (w ->) "[H HΦ]".
+      wp_pures. iApply "HΨ". iFrame.
   Qed.
 End proto. 
-- 
GitLab