From e0d15199c89efa61d921dd1af07aeedbb2ee0d82 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 16 Sep 2020 14:20:00 +0200
Subject: [PATCH] Refactoring - Moved spar to own file and renamed as par_start

---
 _CoqProject                         |  1 +
 theories/logrel/lib/par_start.v     | 48 +++++++++++++++++++++++++++++
 theories/logrel/term_typing_rules.v | 48 ++---------------------------
 3 files changed, 51 insertions(+), 46 deletions(-)
 create mode 100644 theories/logrel/lib/par_start.v

diff --git a/_CoqProject b/_CoqProject
index 62de521..392a033 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -36,6 +36,7 @@ theories/logrel/term_typing_judgment.v
 theories/logrel/subtyping_rules.v
 theories/logrel/term_typing_rules.v
 theories/logrel/lib/mutex.v
+theories/logrel/lib/par_start.v
 theories/logrel/examples/double.v
 theories/logrel/examples/pair.v
 theories/logrel/examples/rec_subtyping.v
diff --git a/theories/logrel/lib/par_start.v b/theories/logrel/lib/par_start.v
new file mode 100644
index 0000000..ca7db42
--- /dev/null
+++ b/theories/logrel/lib/par_start.v
@@ -0,0 +1,48 @@
+From actris.logrel Require Export term_typing_rules environments.
+From actris.channel Require Import proofmode.
+
+Section properties.
+  Context `{heapG Σ}.
+  Context `{chanG Σ}.
+  Context `{spawnG Σ}.
+
+  Definition par_start : expr :=
+    (λ: "e1" "e2",
+     let: "c" := new_chan #() in
+     let: "c1" := Fst "c" in
+     let: "c2" := Snd "c" in
+     ("e1" "c1") ||| ("e2" "c2"))%E.
+
+  Lemma ltyped_par_start Γ S A B :
+    ⊢ Γ ⊨ par_start : ((chan S) ⊸ A) ⊸ (chan (lty_dual S) ⊸ B) ⊸ A * B.
+  Proof.
+    iApply ltyped_lam; [ iApply env_split_id_l | ].
+    iApply ltyped_lam; [ iApply env_split_id_r | ].
+    iApply ltyped_let.
+    { iApply ltyped_app; [ iApply ltyped_unit | iApply ltyped_new_chan ]. }
+    iApply ltyped_let; [ by iApply ltyped_fst | ].
+    rewrite insert_insert.
+    iApply ltyped_let; [ by iApply ltyped_snd | ].
+    rewrite /binder_insert (insert_commute _ "c1" "c") // insert_insert.
+    iApply (ltyped_par).
+    - iApply env_split_right; last first.
+      { rewrite (insert_commute _ "c1" "e2"); [ | eauto ].
+        rewrite (insert_commute _ "c" "e2"); [ | eauto ].
+        iApply env_split_right; last by iApply env_split_id_r.
+        eauto. eauto. }
+      eauto. eauto.
+    - iApply ltyped_app; by iApply ltyped_var.
+    - iApply ltyped_app; by iApply ltyped_var.
+    - rewrite insert_insert.
+      rewrite (insert_commute _ "c2" "e2") // insert_insert.
+      rewrite (insert_commute _ "c1" "c") // insert_insert.
+      rewrite (insert_commute _ "c1" "e1") //
+              (insert_commute _ "c" "e1") // insert_insert.
+      iApply env_split_left=> //; last first.
+      iApply env_split_left=> //; last first.
+      iApply env_split_left=> //; last first.
+      iApply env_split_id_l.
+      eauto. eauto. eauto.
+  Qed.
+
+End properties.
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 9ec3989..aa33282 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -6,7 +6,8 @@ From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import metatheory.
 From iris.heap_lang.lib Require Export spawn par assert.
-From actris.logrel Require Export subtyping term_typing_judgment operators session_types.
+From actris.logrel Require Export subtyping term_typing_judgment operators
+     session_types.
 From actris.logrel Require Import environments.
 From actris.utils Require Import switch.
 From actris.channel Require Import proofmode.
@@ -468,51 +469,6 @@ Section properties.
       iExists c1, c2. iSplit=>//. iFrame "Hp1 Hp2".
     Qed.
 
-    Section with_spawn.
-      Context `{spawnG Σ}.
-
-      Definition spar : expr :=
-        (λ: "e1" "e2",
-         let: "c" := new_chan #() in
-         let: "c1" := Fst "c" in
-         let: "c2" := Snd "c" in
-         ("e1" "c1") ||| ("e2" "c2"))%E.
-
-      Lemma ltyped_spar Γ S A B :
-        ⊢ Γ ⊨ spar : ((chan S) ⊸ A) ⊸ (chan (lty_dual S) ⊸ B) ⊸ A * B.
-      Proof.
-        rewrite /spar.
-        iApply ltyped_lam; [ iApply env_split_id_l | ].
-        iApply ltyped_lam; [ iApply env_split_id_r | ].
-        iApply ltyped_let.
-        { iApply ltyped_app; [ iApply ltyped_unit | iApply ltyped_new_chan ]. }
-        iApply ltyped_let; [ by iApply ltyped_fst | ].
-        rewrite insert_insert.
-        iApply ltyped_let; [ by iApply ltyped_snd | ].
-        rewrite /binder_insert (insert_commute _ "c1" "c") // insert_insert.
-        iApply (ltyped_par).
-        - iApply env_split_right; last first.
-          { rewrite (insert_commute _ "c1" "e2"); [ | eauto ].
-            rewrite (insert_commute _ "c" "e2"); [ | eauto ].
-            iApply env_split_right; last by iApply env_split_id_r.
-            eauto. eauto. }
-          eauto. eauto.
-        - iApply ltyped_app; by iApply ltyped_var.
-        - iApply ltyped_app; by iApply ltyped_var.
-        - rewrite insert_insert.
-          rewrite (insert_commute _ "c2" "e2") // insert_insert.
-          rewrite (insert_commute _ "c1" "c") // insert_insert.
-          rewrite (insert_commute _ "c1" "e1") //
-                  (insert_commute _ "c" "e1") // insert_insert.
-          iApply env_split_left=> //; last first.
-          iApply env_split_left=> //; last first.
-          iApply env_split_left=> //; last first.
-          iApply env_split_id_l.
-          eauto. eauto. eauto.
-      Qed.
-
-    End with_spawn.
-
     Lemma ltyped_send Γ Γ' (x : string) e A S :
       Γ' !! x = Some (chan (<!!> TY A; S))%lty →
       (Γ ⊨ e : A ⫤ Γ') -∗
-- 
GitLab