prove read_own_move

theories/typing/own.v

@@ -159,39 +159,19 @@ Section typing.
     iExists _. iSplit; first done. iFrame "H†". iExists _. by iFrame.
   Qed.
 
-  (* Old Typing *)
-  Lemma consumes_copy_own ty n:
-    Copy ty → consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n ty)%P.
+  Lemma read_own_move E L ty n :
+    typed_read E L (own n ty) ty (own n $ uninit ty.(ty_size)).
   Proof.
-    iIntros (? ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
-    iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
-    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
-    iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
+    iIntros (p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
-      by rewrite ty.(ty_size_eq).
-    iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
-    rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
-  Qed.
-
-
-  Lemma consumes_move ty n:
-    consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n (uninit ty.(ty_size)))%P.
-  Proof.
-    iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "H◁").
-    iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
-    rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
-    iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">Hlen".
-      by rewrite ty.(ty_size_eq). iDestruct "Hlen" as %Hlen.
-    iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
-    rewrite /has_type Hνv. iExists _. iSplit. done. iSplitR "H†".
-    - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear.
-      iInduction vl as [|v vl] "IH". done.
-      iExists [v], vl. iSplit. done. by iSplit.
-    - rewrite uninit_sz; auto.
+    { by iApply ty_size_eq. }
+    iModIntro. iExists l, vl, _. iSplit; first done. iFrame "∗#". iIntros "Hl !>".
+    iExists _. iSplit; first done. rewrite uninit_sz. iFrame "H†". iExists _.
+    iFrame. iApply uninit_own. auto.
   Qed.
 
-
+  (* Old Typing *)
   Lemma typed_new ρ (n : nat):
     0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own n (uninit n)).
   Proof.

theories/typing/uninit.v

+From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import product.
 
@@ -8,12 +9,21 @@ Section uninit.
     {| st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
   Next Obligation. done. Qed.
 
+  Global Instance uninit_1_send : Send uninit_1.
+  Proof. iIntros (tid1 tid2 vl) "H". done. Qed.
+    
   Definition uninit (n : nat) : type :=
     Π (replicate n uninit_1).
 
   Global Instance uninit_copy n : Copy (uninit n).
   Proof. apply product_copy, Forall_replicate, _. Qed.
 
+  Global Instance uninit_send n : Send (uninit n).
+  Proof. apply product_send, Forall_replicate, _. Qed.
+
+  Global Instance uninit_sync n : Sync (uninit n).
+  Proof. apply product_sync, Forall_replicate, _. Qed.
+
   Lemma uninit_sz n : ty_size (uninit n) = n.
   Proof. induction n. done. simpl. by f_equal. Qed.
 
@@ -23,4 +33,16 @@ Section uninit.
     induction ns as [|n ns IH]. done. revert IH.
     by rewrite /= /uninit replicate_plus prod_flatten_l -!prod_app=>->.
   Qed.
+
+  Lemma uninit_own n tid vl :
+    (uninit n).(ty_own) tid vl ⊣⊢ ⌜length vl = n⌝.
+  Proof.
+    iSplit.
+    - iIntros "?". rewrite -{2}(uninit_sz n). by iApply ty_size_eq.
+    - iInduction vl as [|v vl] "IH" forall (n).
+      + iIntros "%". destruct n; done.
+      + iIntros (Heq). destruct n; first done. simpl.
+        iExists [v], vl. iSplit; first done. iSplit; first done.
+        iApply "IH". by inversion Heq.
+  Qed. 
 End uninit.