Make the size of uninit compute.

theories/typing/own.v

@@ -155,7 +155,7 @@ Section typing.
   Context `{typeG Σ}.
 
   (** Typing *)
-  Lemma write_own E L ty ty' n :
+  Lemma write_own {E L} ty ty' n :
     ty.(ty_size) = ty'.(ty_size) → typed_write E L (own n ty') ty (own n ty).
   Proof.
     iIntros (Hsz p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
@@ -186,8 +186,8 @@ Section typing.
     iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
     { 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.
+    iExists _. iSplit; first done. iFrame "H†". iExists _. iFrame.
+    iApply uninit_own. auto.
   Qed.
 
   Lemma type_new {E L} (n : nat) :
@@ -196,13 +196,12 @@ Section typing.
     iIntros (tid eq) "#HEAP #LFT $ $ $ _".
     iApply (wp_new with "HEAP"); try done; first omega. iModIntro.
     iIntros (l vl) "(% & H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
-    iExists _. iSplit; first done. iNext. rewrite Nat2Z.id. iSplitR "H†".
-    - iExists vl. iFrame.
-      match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end.
-      apply (inj Z.of_nat) in Hlen. subst.
-      iInduction vl as [|v vl] "IH". done.
-      iExists [v], vl. iSplit. done. by iSplit.
-    - by rewrite uninit_sz freeable_sz_full.
+    iExists _. iSplit; first done. iNext. rewrite Nat2Z.id freeable_sz_full. iFrame.
+    iExists vl. iFrame.
+    match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end.
+    apply (inj Z.of_nat) in Hlen. subst.
+    iInduction vl as [|v vl] "IH". done.
+    iExists [v], vl. iSplit. done. by iSplit.
   Qed.
 
   Lemma type_delete {E L} ty n p :
@@ -265,7 +264,7 @@ Section typing.
         - eapply is_closed_subst. done. set_solver. }
       eapply type_let'.
       + apply subst_is_closed; last done. apply is_closed_of_val.
-      + eapply type_memcpy; try done. apply write_own, symmetry, uninit_sz.
+      + eapply type_memcpy; try done. by eapply (write_own _ (uninit _)).
       + solve_typing.
       + move=>//=.
   Qed.

theories/typing/type_sum.v

@@ -39,7 +39,7 @@ Section case.
         rewrite heap_mapsto_vec_singleton.
         iFrame. iExists [_], []. auto.
       + iExists _. iFrame. iSplit. done. iExists _. iFrame.
-      + rewrite -EQlen app_length minus_plus uninit_sz -(shift_loc_assoc_nat _ 1).
+      + rewrite -EQlen app_length minus_plus -(shift_loc_assoc_nat _ 1).
         iExists _. iFrame. iSplit. done. iExists _. iFrame. rewrite uninit_own. auto.
     - iExists _. iSplit. done.
       assert (EQf:=freeable_sz_split n 1). simpl in EQf. rewrite -EQf. clear EQf.

theories/typing/uninit.v

@@ -12,11 +12,27 @@ Section uninit.
   Global Instance uninit_1_send : Send uninit_1.
   Proof. iIntros (tid1 tid2 vl) "H". done. Qed.
 
-  Definition uninit (n : nat) : type :=
+  Definition uninit0 (n : nat) : type :=
     Π (replicate n uninit_1).
 
+  Lemma uninit0_sz n : ty_size (uninit0 n) = n.
+  Proof. induction n. done. simpl. by f_equal. Qed.
+
+  (* We redefine uninit as an alias of uninit0, so that the size
+     computes directly to [n] *)
+  Program Definition uninit (n : nat) : type :=
+    {| ty_size := n; ty_own := (uninit0 n).(ty_own);
+       ty_shr := (uninit0 n).(ty_shr) |}.
+  Next Obligation. intros. by rewrite ty_size_eq uninit0_sz. Qed.
+  Next Obligation. intros. by apply ty_share. Qed.
+  Next Obligation. intros. by apply ty_shr_mono. Qed.
+
   Global Instance uninit_copy n : Copy (uninit n).
-  Proof. apply product_copy, Forall_replicate, _. Qed.
+  Proof.
+    destruct (product_copy (replicate n uninit_1)) as [A B].
+      by apply Forall_replicate, _.
+    rewrite uninit0_sz in B. by split.
+  Qed.
 
   Global Instance uninit_send n : Send (uninit n).
   Proof. apply product_send, Forall_replicate, _. Qed.
@@ -24,14 +40,18 @@ Section uninit.
   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.
+  Lemma uninit_uninit0_eqtype E L n :
+    eqtype E L (uninit0 n) (uninit n).
+  Proof. apply equiv_eqtype; (split; first split)=>//=. apply uninit0_sz. Qed.
 
   Lemma uninit_product_eqtype E L ns :
     eqtype E L (uninit (foldr plus 0%nat ns)) (Π(uninit <$> ns)).
   Proof.
-    induction ns as [|n ns IH]. done. revert IH.
-    by rewrite /= /uninit replicate_plus prod_flatten_l -!prod_app=>->.
+    rewrite -uninit_uninit0_eqtype. etrans; last first.
+    { apply product_proper. eapply Forall2_fmap, Forall_Forall2, Forall_forall.
+      intros. by rewrite -uninit_uninit0_eqtype. }
+    induction ns as [|n ns IH]=>//=. revert IH.
+    by rewrite /= /uninit0 replicate_plus prod_flatten_l -!prod_app=>->.
   Qed.
   Lemma uninit_product_eqtype' E L ns :
     eqtype E L (Π(uninit <$> ns)) (uninit (foldr plus 0%nat ns)).
@@ -47,7 +67,7 @@ Section uninit.
     (uninit n).(ty_own) tid vl ⊣⊢ ⌜length vl = n⌝.
   Proof.
     iSplit.
-    - iIntros "?". rewrite -{2}(uninit_sz n). by iApply ty_size_eq.
+    - rewrite ty_size_eq. auto.
     - iInduction vl as [|v vl] "IH" forall (n).
       + iIntros "%". destruct n; done.
       + iIntros (Heq). destruct n; first done. simpl.

[Ralf Jung]

Why this? Looks like it overall complicates things.

I'd really prefer for (uninit n).(ty_own) to be just "test the length", and for (uninit n).(ty_shr) to be the simple sharing protocol based on that ty_own... but unfortunately, that doesn't work :/ . It at least breaks "uninit 0" to be a unit with respect to product.