From 4aba48572e02f9a90d006a03c13df2fac7f93088 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 29 Apr 2020 16:54:14 +0200
Subject: [PATCH] Added a typing rule for select using the post-context

---
 theories/logrel/term_typing_rules.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 753a584..ec7821c 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -525,6 +525,26 @@ Section properties.
       wp_pures. iFrame.
     Qed.
 
+    Definition select : val := λ: "c" "i", send "c" "i".
+    Lemma ltyped_select Γ (c : string) (i : Z) (S : lsty Σ) Ss :
+      Ss !! i = Some S →
+      ⊢ <[c := (chan (lty_select Ss))%lty]>Γ ⊨ select c #i : () ⫤
+        <[c := (chan S)%lty]>Γ.
+    Proof.
+      iIntros (Hin).
+      iIntros "!>" (vs) "HΓ /=".
+      iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".
+      { by apply lookup_insert. }
+      rewrite Heq /select.
+      wp_send with "[]".
+      { eauto. }
+      iSplitR; first done.
+      iDestruct (env_ltyped_insert _ _ c (chan _) with "[Hc //] HΓ")
+        as "HΓ'"=> /=.
+      rewrite insert_delete insert_insert (insert_id vs)=> //.
+      by rewrite lookup_total_alt Hin.
+    Qed.
+
     Definition chanbranch (xs : list Z) : val := λ: "c",
       switch_lams "f" 0 (length xs) $
       let: "y" := recv "c" in
-- 
GitLab