diff --git a/_CoqProject b/_CoqProject
index e410b9bf41d57605a5eb7b95194e91440a6970c4..1136854b641f59ee534bf3d5eb965000cc80246c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -14,3 +14,4 @@ lifetime.v
type.v
type_incl.v
perm.v
+perm_incl.v
diff --git a/perm.v b/perm.v
index c6c254bcef6628b85819c38f6ee7357a310bf79c..9f948d3a1b02739287a773cbe0fa46686f76e3ab 100644
--- a/perm.v
+++ b/perm.v
@@ -1,4 +1,5 @@
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
diff --git a/perm_incl.v b/perm_incl.v
new file mode 100644
index 0000000000000000000000000000000000000000..086bd19823482baa749760cce25ea6b03b99dd5c
--- /dev/null
+++ b/perm_incl.v
@@ -0,0 +1,91 @@
+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
diff --git a/type.v b/type.v
index c82c9431da7194c15d13fce406092da7a674c922..1440f1231636a812647787c43c1b0c2c28f1bb6b 100644
--- a/type.v
+++ b/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
diff --git a/type_incl.v b/type_incl.v
index fd3dbc5821a381a39d40f95dfc2c13bf49749ab2..126442db4c5fbd624d97e2c4859a213c5e2fb116 100644
--- a/type_incl.v
+++ b/type_incl.v
@@ -1,6 +1,6 @@
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