product and sum preserve Send/Sync

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 _.

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