Inclusion of permissions. In order to make type inclusion working, I had to...

Inclusion of permissions. In order to make type inclusion working, I had to change the inclusion of types also.

_CoqProject

@@ -14,3 +14,4 @@ lifetime.v
 type.v
 type_incl.v
 perm.v
+perm_incl.v

perm.v

 From iris.program_logic Require Import thread_local.
+From iris.proofmode Require Import invariants.
 From lrust Require Export type.
 
 Delimit Scope perm_scope with P.
@@ -8,9 +9,10 @@ Module Perm.
 
 Section perm.
 
-  Context `{lifetimeG Σ}.
+  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
 
-  (* TODO : define valuable expressions ν in order to define ν ◁ τ. *)
+  Definition has_type (v : val) (ty : type) : perm :=
+    λ tid, ty.(ty_own) tid [v].
 
   Definition extract (κ : lifetime) (ρ : perm) : perm :=
     λ tid, (κ ∋ ρ tid)%I.
@@ -27,7 +29,7 @@ Section perm.
   Definition sep (ρ1 ρ2 : perm) : @perm Σ :=
     λ tid, (ρ1 tid ★ ρ2 tid)%I.
 
-  Definition top : @perm Σ :=
+  Global Instance top : Top (@perm Σ) :=
     λ _, True%I.
 
 End perm.
@@ -36,6 +38,9 @@ End Perm.
 
 Import Perm.
 
+Notation "v ◁ ty" := (has_type v ty)
+  (at level 75, right associativity) : perm_scope.
+
 Notation "κ ∋ ρ" := (extract κ ρ)
   (at level 75, right associativity) : perm_scope.
 
@@ -47,8 +52,3 @@ Notation "∃ x .. y , P" :=
   (exist (λ x, .. (exist (λ y, P)) ..)) : perm_scope.
 
 Infix "★" := sep (at level 80, right associativity) : perm_scope.
-
-Notation "⊤" := top : perm_scope.
-
-Definition perm_incl {Σ} (ρ1 ρ2 : @perm Σ) :=
-  ∀ tid, ρ1 tid ⊢ ρ2 tid.
\ No newline at end of file

perm_incl.v

+From iris.algebra Require Import upred_big_op.
+From iris.program_logic Require Import thread_local.
+From lrust Require Export type perm.
+
+Section perm_incl.
+
+  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+
+  Definition perm_incl (ρ1 ρ2 : perm) :=
+    ∀ tid, ρ1 tid ={⊤}=> ρ2 tid.
+
+  Lemma perm_incl_top ρ : perm_incl ρ ⊤.
+  Proof. iIntros (tid) "H". eauto. Qed.
+
+  Global Instance perm_incl_refl : Reflexive perm_incl.
+  Proof. iIntros (? tid) "H". eauto. Qed.
+
+  Global Instance perm_incl_trans : Transitive perm_incl.
+  Proof.
+    iIntros (??? H12 H23 tid) "H". iVs (H12 with "H") as "H". by iApply H23.
+  Qed.
+
+  Lemma perm_incl_frame_l ρ ρ1 ρ2 :
+    perm_incl ρ1 ρ2 → perm_incl (ρ ★ ρ1) (ρ ★ ρ2).
+  Proof. iIntros (Hρ tid) "[$?]". by iApply Hρ. Qed.
+
+  Lemma perm_incl_frame_r ρ ρ1 ρ2 :
+    perm_incl ρ1 ρ2 → perm_incl (ρ1 ★ ρ) (ρ2 ★ ρ).
+  Proof. iIntros (Hρ tid) "[?$]". by iApply Hρ. Qed.
+
+End perm_incl.
+
+Section duplicable.
+
+  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+
+  Class Duplicable (ρ : perm) :=
+    perm_incl_duplicable : perm_incl ρ (ρ ★ ρ).
+
+  Lemma has_type_dup v ty : ty.(ty_dup) → Duplicable (v ◁ ty).
+  Proof. iIntros (Hdup tid) "H!==>". by iApply ty_dup_dup. Qed.
+
+  Global Instance lft_incl_dup κ κ' : Duplicable (κ ⊑ κ').
+  Proof. iIntros (tid) "#H!==>". by iSplit. Qed.
+
+  Global Instance sep_dup P Q :
+    Duplicable P → Duplicable Q → Duplicable (P ★ Q).
+  Proof.
+    iIntros (HP HQ tid) "[HP HQ]".
+    iVs (HP with "HP") as "[$$]". by iApply HQ.
+  Qed.
+
+  Global Instance top_dup : Duplicable ⊤.
+  Proof. iIntros (tid) "_!==>". by iSplit. Qed.
+
+End duplicable.
+
+Hint Extern 0 (Duplicable (_ ◁ _)) => apply has_type_dup; exact I.
+
+Section perm_equiv.
+
+  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+
+  Definition perm_equiv ρ1 ρ2 := perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
+
+  Global Instance perm_equiv_refl : Reflexive perm_equiv.
+  Proof. by split. Qed.
+
+  Global Instance perm_equiv_trans : Transitive perm_equiv.
+  Proof. intros x y z [] []. split; by transitivity y. Qed.
+
+  Global Instance perm_equiv_sym : Symmetric perm_equiv.
+  Proof. by intros x y []; split. Qed.
+
+  Global Instance perm_incl_proper :
+    Proper (perm_equiv ==> perm_equiv ==> iff) perm_incl.
+  Proof. intros ??[??]??[??]; split; eauto using perm_incl_trans. Qed.
+
+  Global Instance sep_assoc : Assoc perm_equiv Perm.sep.
+  Proof. intros ???; split. by iIntros (tid) "[$[$$]]". by iIntros (tid) "[[$$]$]". Qed.
+
+  Global Instance sep_comm : Comm perm_equiv Perm.sep.
+  Proof. intros ??; split; by iIntros (tid) "[$$]". Qed.
+
+  Global Instance top_right_id : RightId perm_equiv ⊤ Perm.sep.
+  Proof. intros ρ; split. by iIntros (tid) "[? _]". by iIntros (tid) "$". Qed.
+
+  Global Instance top_left_id : LeftId perm_equiv ⊤ Perm.sep.
+  Proof. intros ρ. by rewrite comm right_id. Qed.
+
+End perm_equiv.
\ No newline at end of file

type.v

@@ -419,7 +419,7 @@ Section types.
     size_eq : Forall ((= n) ∘ ty_size) tyl.
   Instance LstTySize_nil n : LstTySize n nil := List.Forall_nil _.
   Hint Extern 1 (LstTySize _ (_ :: _)) =>
-    apply List.Forall_cons; [reflexivity|].
+    apply List.Forall_cons; [reflexivity|] : typeclass_instances.
 
   Lemma sum_size_eq n tid i tyl vl {Hn : LstTySize n tyl} :
     ty_own (nth i tyl bot) tid vl ⊢ length vl = n.
@@ -490,32 +490,35 @@ Section types.
       iApply ("Hclose'" with "Hownq").
   Qed.
 
-  Program Definition undef (n : nat) :=
+  Program Definition uninit (n : nat) :=
     ty_of_st {| st_size := n; st_own tid vl := (length vl = n)%I |}.
   Next Obligation. done. Qed.
 
-  Program Definition cont {n : nat} (perm : vec val n → perm (Σ := Σ)):=
+  (* TODO : For now, functions and closures are not Sync nor
+     Send. This means they cannot be called in another thread than the
+     one that created it.
+     We will need Send and Sync closures when dealing with
+     multithreading (spawn needs a Send closure). *)
+  Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
     {| ty_size := 1; ty_dup := false;
-       ty_own tid vl := (∃ f xl e Hcl, vl = [@RecV f xl e Hcl] ★
-          ∀ vl tid, perm vl tid -★ tl_own tid ⊤
-                    -★ WP e (map of_val (vec_to_list vl)) {{λ _, False}})%I;
+       ty_own tid vl := (∃ f, vl = [f] ★
+          ∀ vl, ▷ ρ vl tid -★ tl_own tid ⊤
+                 -★ WP f (map of_val vl) {{λ _, False}})%I;
        ty_shr κ tid N l := True%I |}.
   Next Obligation.
-    iIntros (n perm tid vl) "H". iDestruct "H" as (f xl e Hcl) "[% _]". by subst.
+    iIntros (n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
   Next Obligation. done. Qed.
   Next Obligation. intros. by iIntros "_ $". Qed.
   Next Obligation. intros. by iIntros "_ _". Qed.
   Next Obligation. done. Qed.
 
-  Program Definition fn {n : nat} (perm : vec val n → perm (Σ := Σ)):=
+  Program Definition fn {n : nat} (ρ : vec val n → @perm Σ):=
     ty_of_st {| st_size := 1;
-       st_own tid vl := (∃ f xl e Hcl, vl = [@RecV f xl e Hcl] ★
-          ∀ vl tid, {{ perm vl tid ★ tl_own tid ⊤ }}
-                      e (map of_val (vec_to_list vl))
-                    {{λ _, False}})%I |}.
+       st_own tid vl := (∃ f, vl = [f] ★
+          ∀ vl, {{ ▷ ρ vl tid ★ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
   Next Obligation.
-    iIntros (n perm tid vl) "H". iDestruct "H" as (f xl e Hcl) "[% _]". by subst.
+    iIntros (n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
 
   (* TODO *)
@@ -545,11 +548,13 @@ Notation "&uniq{ κ } ty" := (uniq_borrow κ ty)
   (format "&uniq{ κ } ty", at level 20, right associativity) : lrust_type_scope.
 Notation "&shr{ κ } ty" := (shared_borrow κ ty)
   (format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
+
+(* FIXME : these notations do not work. *)
 Notation "( ty1 * ty2 * .. * tyn )" :=
   (product (cons ty1 (cons ty2 ( .. (cons tyn nil) .. ))))
-  (format "( ty1 * ty2 * .. * tyn )") : lrust_type_scope.
+  (format "( ty1  *  ty2  *  ..  *  tyn )") : lrust_type_scope.
 Notation "( ty1 + ty2 + .. + tyn )" :=
   (sum (cons ty1 (cons ty2 ( .. (cons tyn nil) .. ))))
-  (format "( ty1 + ty2 + .. + tyn )") : lrust_type_scope.
+  (format "( ty1  +  ty2  +  ..  +  tyn )") : lrust_type_scope.
 
 (* TODO : notation for forall *)
\ No newline at end of file

type_incl.v

 From iris.algebra Require Import upred_big_op.
 From iris.program_logic Require Import thread_local.
-From lrust Require Export type perm.
+From lrust Require Export type perm_incl.
 
 Import Types.
 
@@ -9,111 +9,218 @@ Section ty_incl.
   Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
 
   Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
-    ∀ tid,
-      ρ tid ⊢
-      (□ ∀ tid vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ∧
-      (□ ∀ κ tid E l, ty1.(ty_shr) κ tid E l →
-                      ty2.(ty_shr) κ tid E l
+    ∀ tid, ρ tid ={⊤}=>
+      (□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ★
+      (□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
        (* [ty_incl] needs to prove something about the length of the
           object when it is shared. We place this property under the
-          hypothesis that [ty2.(ty_shr)] holds, so that the [!]  type
+          hypothesis that [ty2.(ty_shr)] holds, so that the [!] type
           is still included in any other. *)
-                    ★ ty1.(ty_size) = ty2.(ty_size)).
+                  ty2.(ty_shr) κ tid E l ★ ty1.(ty_size) = ty2.(ty_size)).
 
-  Lemma ty_incl_refl ρ ty : ty_incl ρ ty ty.
-  Proof. iIntros (tid0) "_". iSplit; iIntros "!#"; eauto. Qed.
+  Global Instance ty_incl_refl ρ : Reflexive (ty_incl ρ).
+  Proof.
+    iIntros (ty tid) "_!==>". iSplit; iIntros "!#"; eauto.
+  Qed.
 
-  Lemma ty_incl_trans ρ ty1 ty2 ty3 :
-    ty_incl ρ ty1 ty2 → ty_incl ρ ty2 ty3 → ty_incl ρ ty1 ty3.
+  Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
+    ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ★ θ) ty1 ty3.
   Proof.
-    iIntros (H12 H23 tid0) "H".
-    iDestruct (H12 with "H") as "[#H12 #H12']".
-    iDestruct (H23 with "H") as "[#H23 #H23']".
-    iSplit; iIntros "{H}!#*H1".
+    iIntros (H12 H23 tid) "[H1 H2]".
+    iVs (H12 with "H1") as "[#H12 #H12']".
+    iVs (H23 with "H2") as "[#H23 #H23']".
+    iVsIntro; iSplit; iIntros "!#*H1".
     - by iApply "H23"; iApply "H12".
-    - iDestruct ("H12'" $! _ _ _ _ with "H1") as "[H2 %]".
-      iDestruct ("H23'" $! _ _ _ _ with "H2") as "[$ %]".
+    - iDestruct ("H12'" $! _ _ _ with "H1") as "[H2 %]".
+      iDestruct ("H23'" $! _ _ _ with "H2") as "[$ %]".
       iPureIntro. congruence.
   Qed.
 
-  Lemma ty_weaken ρ θ ty1 ty2 :
+  Lemma ty_incl_weaken ρ θ ty1 ty2 :
     perm_incl ρ θ → ty_incl θ ty1 ty2 → ty_incl ρ ty1 ty2.
-  Proof. iIntros (Hρθ Hθ tid) "H". iApply Hθ. by iApply Hρθ. Qed.
+  Proof. iIntros (Hρθ Hρ' tid) "H". iVs (Hρθ with "H"). by iApply Hρ'. Qed.
+
+  Global Instance ty_incl_trans' ρ: Duplicable ρ → Transitive (ty_incl ρ).
+  Proof. intros ??????. eauto using ty_incl_weaken, ty_incl_trans. Qed.
 
   Lemma ty_incl_bot ρ ty : ty_incl ρ ! ty.
-  Proof. iIntros (tid0) "_". iSplit; iIntros "!#*/=[]". Qed.
+  Proof. iIntros (tid) "_!==>". iSplit; iIntros "!#*/=[]". Qed.
 
   Lemma ty_incl_own ρ ty1 ty2 q :
     ty_incl ρ ty1 ty2 → ty_incl ρ (own q ty1) (own q ty2).
   Proof.
-    iIntros (Hincl tid0) "H/=". iDestruct (Hincl with "H") as "[#Howni #Hshri]".
-    iClear "H". iSplit; iIntros "!#*H".
+    iIntros (Hincl tid) "H/=". iVs (Hincl with "H") as "[#Howni #Hshri]".
+    iVsIntro. iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "(%&H†&Hmt)". subst. iExists _. iSplit. done.
       iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
       iDestruct (ty_size_eq with "Hown") as %<-.
-      iDestruct ("Howni" $! _ _ with "Hown") as "Hown".
+      iDestruct ("Howni" $! _ with "Hown") as "Hown".
       iDestruct (ty_size_eq with "Hown") as %<-. iFrame.
       iExists _. by iFrame.
     - iDestruct "H" as (l') "[Hfb #Hvs]". iSplit; last done. iExists l'. iFrame.
       iIntros (q') "!#Hκ".
       iVs ("Hvs" $! _ with "Hκ") as "Hvs'". iIntros "!==>!>".
       iVs "Hvs'" as "[Hshr $]". iVsIntro.
-      by iDestruct ("Hshri" $! _ _ _ _ with "Hshr") as "[$ _]".
+      by iDestruct ("Hshri" $! _ _ _ with "Hshr") as "[$ _]".
   Qed.
 
-  Lemma lft_incl_ty_incl_uniq_borrow ρ ty κ1 κ2 :
-    perm_incl ρ (κ1 ⊑ κ2) → ty_incl ρ (&uniq{κ2}ty) (&uniq{κ1}ty).
+  Lemma lft_incl_ty_incl_uniq_borrow ty κ1 κ2 :
+    ty_incl (κ1 ⊑ κ2) (&uniq{κ2}ty) (&uniq{κ1}ty).
   Proof.
-    iIntros (Hκκ' tid0) "H". iDestruct (Hκκ' with "H") as "#Hκκ'". iClear "H".
-    iSplit; iIntros "!#*H".
+    iIntros (tid) "#Hincl!==>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
-      by iApply (lft_borrow_incl with "Hκκ'").
+      by iApply (lft_borrow_incl with "Hincl").
     - admit. (* TODO : fix the definition before *)
   Admitted.
 
-  Lemma lft_incl_ty_incl_shared_borrow ρ ty κ1 κ2 :
-    perm_incl ρ (κ1 ⊑ κ2) → ty_incl ρ (&shr{κ2}ty) (&shr{κ1}ty).
+  Lemma lft_incl_ty_incl_shared_borrow ty κ1 κ2 :
+    ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
   Proof.
-    iIntros (Hκκ' tid0) "H". iDestruct (Hκκ' with "H") as "#Hκκ'". iClear "H".
-    iSplit; iIntros "!#*H".
+    iIntros (tid) "#Hincl!==>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
-      by iApply (ty.(ty_shr_mono) with "Hκκ'").
+      by iApply (ty.(ty_shr_mono) with "Hincl").
     - iDestruct "H" as (vl) "#[Hfrac Hty]". iSplit; last done.
       iExists vl. iFrame "#". iNext.
       iDestruct "Hty" as (l0) "[% Hty]". subst. iExists _. iSplit. done.
-      by iApply (ty_shr_mono with "Hκκ' Hty").
+      by iApply (ty_shr_mono with "Hincl Hty").
   Qed.
 
   Lemma ty_incl_prod ρ tyl1 tyl2 :
-    Forall2 (ty_incl ρ) tyl1 tyl2 → ty_incl ρ (product tyl1) (product tyl2).
+    Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 →
+    ty_incl ρ (product tyl1) (product tyl2).
   Proof.
-    rewrite {2}/ty_incl /product /=. iIntros (HFA tid0) "Hρ". iSplit.
-    - assert (Himpl : ρ tid0 ⊢
-         □ (∀ tid vll, length tyl1 = length vll →
+    intros Hρ HFA. eapply ty_incl_weaken. apply Hρ.
+    iIntros (tid) "[Hρ1 Hρ2]". iSplitL "Hρ1".
+    - assert (Himpl : ρ tid ={⊤}=>
+         □ (∀ vll, length tyl1 = length vll →
                ([★ list] tyvl ∈ combine tyl1 vll, ty_own (tyvl.1) tid (tyvl.2))
              → ([★ list] tyvl ∈ combine tyl2 vll, ty_own (tyvl.1) tid (tyvl.2)))).
       { induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH].
-        - iIntros "_!#* _ _". by rewrite big_sepL_nil.
-        - iIntros "Hρ". iDestruct (IH with "Hρ") as "#Hqimpl".
-          iDestruct (Hincl with "Hρ") as "[#Hhimpl _]". iIntros "!#*%".
-          destruct vll as [|vlh vllq]. discriminate. rewrite !big_sepL_cons.
+        - iIntros "_!==>!#* _ _". by rewrite big_sepL_nil.
+        - iIntros "Hρ". iVs (Hρ with "Hρ") as "[Hρ1 Hρ2]".
+          iVs (IH with "Hρ1") as "#Hqimpl". iVs (Hincl with "Hρ2") as "[#Hhimpl _]".
+          iIntros "!==>!#*%". destruct vll as [|vlh vllq]. done. rewrite !big_sepL_cons.
           iIntros "[Hh Hq]". iSplitL "Hh". by iApply "Hhimpl".
           iApply ("Hqimpl" with "[] Hq"). iPureIntro. simpl in *. congruence. }
-      iDestruct (Himpl with "Hρ") as "#Himpl". iIntros "{Hρ}!#*H".
+      iVs (Himpl with "Hρ1") as "#Himpl". iIntros "!==>!#*H".
       iDestruct "H" as (vll) "(%&%&H)". iExists _. iSplit. done. iSplit.
       by rewrite -(Forall2_length _ _ _ HFA). by iApply ("Himpl" with "[] H").
-    - iRevert "Hρ". generalize O.
+    - rewrite /product /=. iRevert "Hρ2". generalize O.
       change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O.
       induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH].
-      + iIntros (i offs) "_!#* _". rewrite big_sepL_nil. eauto.
-      + iIntros (i offs) "Hρ". iDestruct (IH with "[] Hρ") as "#Hqimpl". done.
-        iDestruct (Hincl with "Hρ") as "[_ #Hhimpl]". iIntros "!#*".
+      + iIntros (i offs) "_!==>!#*_/=". rewrite big_sepL_nil. eauto.
+      + iIntros (i offs) "Hρ". iVs (Hρ with "Hρ") as "[Hρ1 Hρ2]".
+        iVs (IH with "[] Hρ1") as "#Hqimpl".
+        done. (* TODO : get rid of this done by doing induction in the proof mode. *)
+        iVs (Hincl with "Hρ2") as "[_ #Hhimpl]". iIntros "!==>!#*".
         rewrite !big_sepL_cons. iIntros "[Hh Hq]".
         setoid_rewrite <-Nat.add_succ_comm.
-        iDestruct ("Hhimpl" $! _ _ _ _ with "Hh") as "[$ %]".
+        iDestruct ("Hhimpl" $! _ _ _ with "Hh") as "[$ %]".
         replace ty2.(ty_size) with ty1.(ty_size) by done.
-        iDestruct ("Hqimpl" $! _ _ _ _ with "Hq") as "[$ %]".
+        iDestruct ("Hqimpl" $! _ _ _ with "Hq") as "[$ %]".
         iIntros "!%/=". congruence.
   Qed.
 
+  Lemma ty_incl_prod_cons_l ρ ty tyl :
+    ty_incl ρ (product (ty :: tyl)) (product [ty ; product tyl]).
+  Proof.
+    iIntros (tid) "_!==>". iSplit; iIntros "!#/=".
+    - iIntros (vl) "H". iDestruct "H" as ([|vlh vllq]) "(%&%&H)". done. subst.
+      iExists [_;_]. iSplit. by rewrite /= app_nil_r. iSplit. done.
+      rewrite !big_sepL_cons big_sepL_nil right_id. iDestruct "H" as "[$ H]".
+      iExists _. repeat iSplit; try done. iPureIntro. simpl in *; congruence.
+    - iIntros (κ E l) "H". iSplit; last (iPureIntro; lia).
+      rewrite !big_sepL_cons big_sepL_nil right_id. iDestruct "H" as "[$ H]".
+      (* FIXME : namespaces do not match. *)
+      admit.
+  Admitted.
+
+  (* TODO *)
+  Lemma ty_incl_prod_flatten ρ tyl1 tyl2 tyl3 :
+    ty_incl ρ (product (tyl1 ++ product tyl2 :: tyl3))
+              (product (tyl1 ++ tyl2 ++ tyl3)).
+  Admitted.
+
+  Lemma ty_incl_sum ρ n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) :
+    Duplicable ρ →
+    Forall2 (ty_incl ρ) tyl1 tyl2 → ty_incl ρ (sum tyl1) (sum tyl2).
+  Proof.
+    iIntros (DUP FA tid) "Hρ". rewrite /sum /=.
+    iVs (DUP with "Hρ") as "[Hρ1 Hρ2]". iSplitR "Hρ2".
+    - assert (Hincl : ρ tid ={⊤}=>
+         (□ ∀ i vl, (nth i tyl1 !%T).(ty_own) tid vl
+                  → (nth i tyl2 !%T).(ty_own) tid vl)).
+      { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
+        - iIntros "_!==>*!#". eauto.
+        - iIntros "Hρ". iVs (DUP with "Hρ") as "[Hρ1 Hρ2]".
+          iVs (IH with "Hρ1") as "#IH". iVs (Hincl with "Hρ2") as "[#Hh _]".
+          iIntros "!==>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
+      iVs (Hincl with "Hρ1") as "#Hincl". iIntros "!==>!#*H".
+      iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
+        by iApply "Hincl".
+    - assert (Hincl : ρ tid ={⊤}=>
+         (□ ∀ i κ E l, (nth i tyl1 !%T).(ty_shr) κ tid E l
+                     → (nth i tyl2 !%T).(ty_shr) κ tid E l)).
+      { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
+        - iIntros "_!==>*!#". eauto.
+        - iIntros "Hρ". iVs (DUP with "Hρ") as "[Hρ1 Hρ2]".
+          iVs (IH with "Hρ1") as "#IH". iVs (Hincl with "Hρ2") as "[_ #Hh]".
+          iIntros "!==>*!#*Hown". destruct i as [|i]; last by iApply "IH".
+          by iDestruct ("Hh" $! _ _ _ with "Hown") as "[$ _]". }
+      iVs (Hincl with "Hρ2") as "#Hincl". iIntros "!==>!#*H". iSplit; last done.
+      iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
+  Qed.
+
+  Lemma ty_incl_uninit_split ρ n1 n2 :
+    ty_incl ρ (uninit (n1+n2)) (product [uninit n1; uninit n2]).
+  Proof.
+    iIntros (tid) "_!==>". iSplit; iIntros "!#*H".
+    - iDestruct "H" as %Hlen. iExists [take n1 vl; drop n1 vl].
+      repeat iSplit. by rewrite /= app_nil_r take_drop. done.
+      rewrite big_sepL_cons big_sepL_singleton. iSplit; iPureIntro.
+      apply take_length_le. lia. rewrite drop_length. lia.
+    - iSplit; last (iPureIntro; simpl; lia). iDestruct "H" as (vl) "[#Hf #Hlen]".
+      rewrite /= big_sepL_cons big_sepL_singleton. iSplit.
+      + iExists (take n1 vl). iSplit.
+        (* FIXME : cannot split the fractured borrow. *)
+        admit.
+        iNext. iDestruct "Hlen" as %Hlen. rewrite /= take_length_le //. lia.
+      + iExists (drop n1 vl). iSplit.
+        (* FIXME : cannot split the fractured borrow. *)
+        admit.
+        iNext. iDestruct "Hlen" as %Hlen. rewrite /= drop_length. iPureIntro. lia.
+  Admitted.
+
+  Lemma ty_incl_uninit_combine ρ n1 n2 :
+    ty_incl ρ (product [uninit n1; uninit n2]) (uninit (n1+n2)).
+  Proof.
+  (* FIXME : idem : cannot combine the fractured borrow. *)
+  Admitted.
+
+  (* Lemma ty_incl_cont_frame {n} ρ ρ1 ρ2 : *)
+  (*   Duplicable ρ → (∀ vl : vec val n, perm_incl (ρ ★ ρ2 vl) (ρ1 vl)) → *)
+  (*   ty_incl ρ (cont ρ1) (cont ρ2). *)
+  (* Proof. *)
+  (*   iIntros (? Hρ1ρ2 tid) "Hρ". *)
+  (*   iVs (inv_alloc lrustN _ (ρ tid) with "[Hρ]") as "#INV". by auto. *)
+  (*   iIntros "!==>". iSplit; iIntros "!#*H"; last by auto. *)
+  (*   iDestruct "H" as (f xl e ?) "[% Hwp]". subst. iExists _, _, _, _. iSplit. done. *)
+  (*   iIntros (vl) "Htl Hown". *)
+  (*   iApply pvs_wp. iInv lrustN as "Hρ" "Hclose". *)
+
+  (*   iSplit; last by iIntros "{Hρ}!#*_"; auto. *)
+  (*   (* FIXME : I do not know how to prove this. Should we put this *)
+  (*      under a view modality and then put Hρ in an invariant? *) *)
+  (*   admit. *)
+  (* Admitted. *)
+
+  (* Lemma ty_incl_fn_frame {n} ρ ρ1 ρ2 : *)
+  (*   Duplicable ρ → (∀ vl : vec val n, perm_incl (ρ ★ ρ2 vl) (ρ1 vl)) → *)
+  (*   ty_incl ρ (fn ρ1) (fn ρ2). *)
+  (*   (* FIXME : idem. *) *)
+  (*   admit. *)
+  (* Admitted. *)
+
+  (* TODO : forall, when we will have figured out the right definition. *)
+
 End ty_incl.
\ No newline at end of file