From 02ef8176f01f8de0563a2f5a8e1444bb9ee01b6d Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Mon, 19 Dec 2016 22:25:41 +0100
Subject: [PATCH] product and sum preserve Send/Sync

---
 theories/typing/product.v | 25 ++++++++++++++++++++++++-
 theories/typing/sum.v     | 24 +++++++++++++++++++++++-
 2 files changed, 47 insertions(+), 2 deletions(-)

diff --git a/theories/typing/product.v b/theories/typing/product.v
index 1881e598..98e13124 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -18,6 +18,12 @@ Section product.
     iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto.
   Qed.
 
+  Global Instance unit_send : Send unit.
+  Proof. iIntros (tid1 tid2 vl) "H". done. Qed.
+
+  Global Instance unit_sync : Sync unit.
+  Proof. iIntros (????) "_". done. Qed.
+
   Lemma split_prod_mt tid ty1 ty2 q l :
     (l ↦∗{q}: λ vl,
        ∃ vl1 vl2, ⌜vl = vl1 ++ vl2⌝ ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
@@ -77,7 +83,7 @@ Section product.
     Proper (eqtype E L ==> eqtype E L ==> eqtype E L) product2.
   Proof. by intros ??[]??[]; split; apply product2_mono. Qed.
 
-  Global Instance product2_copy `(!Copy ty1) `(!Copy ty2) :
+  Global Instance product2_copy `{!Copy ty1} `{!Copy ty2} :
     Copy (product2 ty1 ty2).
   Proof.
     split; first (intros; apply _).
@@ -115,6 +121,19 @@ Section product.
       iMod ("Hclose2" with "[H2 H↦2]") as "[$$]". by iExists _; iFrame. done.
   Qed.
 
+  Global Instance product2_send `{!Send ty1} `{!Send ty2} :
+    Send (product2 ty1 ty2).
+  Proof.
+    iIntros (tid1 tid2 vl) "H". iDestruct "H" as (vl1 vl2) "(% & Hown1 & Hown2)".
+    iExists _, _. iSplit; first done. iSplitL "Hown1"; by iApply @send_change_tid.
+  Qed.
+
+  Global Instance product2_sync `{!Sync ty1} `{!Sync ty2} :
+    Sync (product2 ty1 ty2).
+  Proof.
+    iIntros (κ tid1 ti2 l) "[#Hshr1 #Hshr2]". iSplit; by iApply @sync_change_tid.
+  Qed.
+
   Definition product := foldr product2 unit.
 
   Global Instance product_mono E L:
@@ -125,6 +144,10 @@ Section product.
   Proof. intros ??. induction 1. done. by simpl; f_equiv. Qed.
   Global Instance product_copy tys : LstCopy tys → Copy (product tys).
   Proof. induction 1; apply _. Qed.
+  Global Instance product_send tys : LstSend tys → Send (product tys).
+  Proof. induction 1; apply _. Qed.
+  Global Instance product_sync tys : LstSync tys → Sync (product tys).
+  Proof. induction 1; apply _. Qed.
 
   Definition product_cons ty tyl :
     product (ty :: tyl) = product2 ty (product tyl) := eq_refl _.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 5288a061..4cc51413 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -30,6 +30,12 @@ Section sum.
     iIntros (????????) "? []".
   Qed.
 
+  Global Instance emp_send : Send ∅.
+  Proof. iIntros (???) "[]". Qed.
+
+  Global Instance emp_sync : Sync ∅.
+  Proof. iIntros (????) "[]". Qed.
+
   Definition list_max (l : list nat) := foldr max 0%nat l.
 
   Definition is_pad i tyl (vl : list val) : iProp Σ :=
@@ -149,7 +155,7 @@ Section sum.
       rewrite nth_empty. by iDestruct "Hshr" as "[]".
   Qed.
 
-  Global Instance sum_copy tyl: LstCopy tyl → Copy (sum tyl).
+  Global Instance sum_copy tyl : LstCopy tyl → Copy (sum tyl).
   Proof.
     intros HFA. split.
     - intros tid vl.
@@ -182,6 +188,22 @@ Section sum.
         iMod ("Hclose'" with "[$HownC1 $HownC2]").
         iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
   Qed.
+
+  Global Instance sum_send tyl : LstSend tyl → Send (sum tyl).
+  Proof.
+    iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
+    iExists _, _, _. iSplit; first done. iSplit; first done. iApply @send_change_tid; last done.
+    edestruct nth_in_or_default as [| ->]; last by apply _.
+          by eapply List.Forall_forall.
+  Qed.
+
+  Global Instance sum_sync tyl : LstSync tyl → Sync (sum tyl).
+  Proof.
+    iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (i) "[Hframe Hown]".
+    iExists _. iFrame "Hframe". iApply @sync_change_tid; last done.
+    edestruct nth_in_or_default as [| ->]; last by apply _.
+          by eapply List.Forall_forall.
+  Qed.
 End sum.
 
 (* Σ is commonly used for the current functor. So it cannot be defined
-- 
GitLab