New example : init_prod.

_CoqProject

@@ -46,3 +46,4 @@ theories/typing/type_sum.v
 theories/typing/tests/get_x.v
 theories/typing/tests/rebor.v
 theories/typing/tests/unbox.v
+theories/typing/tests/init_prod.v

theories/typing/own.v

@@ -210,6 +210,21 @@ Section typing.
     typed_body E L C T (let: x := new [ #n ] in e).
   Proof. intros. eapply type_let. done. by apply type_new_instr. solve_typing. done. Qed.
 
+  Lemma type_new_subtype ty E L C T x (n : Z) e :
+    Closed (x :b: []) e →
+    0 ≤ n →
+    let n' := Z.to_nat n in
+    subtype E L (uninit n') ty →
+    (∀ (v : val), typed_body E L C ((v ◁ own n' ty) :: T) (subst' x v e)) →
+    typed_body E L C T (let: x := new [ #n ] in e).
+  Proof.
+    intros ???? Htyp. eapply type_let. done. by apply type_new_instr. solve_typing.
+    iIntros (v). iApply typed_body_mono; [done| |done|].
+    (* FIXME : why can't we iApply Htyp? *)
+    2:by iDestruct (Htyp v) as "$".
+    by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, own_mono.
+  Qed.
+
   Lemma type_delete_instr {E L} ty (n : Z) p :
     Z.of_nat (ty.(ty_size)) = n →
     typed_instruction E L [p ◁ own (ty.(ty_size)) ty] (delete [ #n; p])%E (λ _, []).

theories/typing/product_split.v

@@ -401,4 +401,6 @@ Hint Extern 0
      (tctx_extract_hasty _ _ _ _ (hasty_ptr_offsets _ _ _ _) _) =>
         cbn[hasty_ptr_offsets].
 
+Hint Extern 0 (tctx_extract_hasty _ _ _ _ (_ ++ _) _) => cbn[app].
+
 Hint Unfold extract_tyl : lrust_typing.

theories/typing/tests/init_prod.v

+From lrust.lifetime Require Import definitions.
+From lrust.lang Require Import new_delete.
+From lrust.typing Require Import programs product product_split own uniq_bor
+                    shr_bor int function lft_contexts uninit cont borrow.
+Set Default Proof Using "Type".
+
+Section rebor.
+  Context `{typeG Σ}.
+
+  Definition init_prod :=
+    (funrec: <> ["x"; "y"] :=
+       let: "x'" := !"x" in let: "y'" := !"y" in
+       let: "r" := new [ #2] in
+       "r" +ₗ #0 <- "x'";; "r" +ₗ #1 <- "y'";;
+       delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r":expr])%E.
+
+  Lemma init_prod_type :
+    typed_instruction_ty [] [] [] init_prod
+        (fn (λ _, []) (λ _, [# own 1 int; own 1 int])
+            (λ (_ : ()), own 2 (Π[int;int]))).
+  Proof.
+    apply type_fn; try apply _. move=> /= [] ret p. inv_vec p=>x y. simpl_subst.
+    eapply type_deref; try solve_typing; [apply read_own_move|done|]=>x'. simpl_subst.
+    eapply type_deref; try solve_typing; [apply read_own_move|done|]=>y'. simpl_subst.
+    eapply (type_new_subtype (Π[uninit 1; uninit 1])); [apply _|done| |].
+      { apply (uninit_product_subtype [] [] [1;1]%nat). }
+      intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
+    eapply (type_assign (own 2 (uninit 1))); try solve_typing. by apply write_own.
+    eapply (type_assign (own 2 (uninit 1))); try solve_typing. by apply write_own.
+    eapply type_delete; try solve_typing.
+    eapply type_delete; try solve_typing.
+    eapply (type_jump [_]); solve_typing.
+  Qed.
+End rebor.