From 39f063107e736883ed799adf3ccc9732275f26ce Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 14 Sep 2016 21:06:13 +0200
Subject: [PATCH] Duplicable is defined as persistent in the model. This makes
 [ty_incl_fn] provable.

---
 perm.v      | 32 ++++++++++++++++++++--
 perm_incl.v | 29 ++++----------------
 type.v      | 57 ++++++++++++++++----------------------
 type_incl.v | 79 +++++++++++++++++++++++++++--------------------------
 4 files changed, 100 insertions(+), 97 deletions(-)

diff --git a/perm.v b/perm.v
index 9f948d3a..5880427f 100644
--- a/perm.v
+++ b/perm.v
@@ -5,14 +5,19 @@ From lrust Require Export type.
 Delimit Scope perm_scope with P.
 Bind Scope perm_scope with perm.
 
+(* TODO : find a better place for this. *)
+Definition valuable := option val.
+Definition proj_valuable (n : Z) :=
+  (≫= λ v, match v with LitV (LitLoc l) => Some (shift_loc l n) | _ => None end).
+
 Module Perm.
 
 Section perm.
 
   Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
 
-  Definition has_type (v : val) (ty : type) : perm :=
-    λ tid, ty.(ty_own) tid [v].
+  Definition has_type (v : valuable) (ty : type) : perm :=
+    λ tid, from_option (λ v, ty.(ty_own) tid [v]) False%I v.
 
   Definition extract (κ : lifetime) (ρ : perm) : perm :=
     λ tid, (κ ∋ ρ tid)%I.
@@ -52,3 +57,26 @@ Notation "∃ x .. y , P" :=
   (exist (λ x, .. (exist (λ y, P)) ..)) : perm_scope.
 
 Infix "★" := sep (at level 80, right associativity) : perm_scope.
+
+Section duplicable.
+
+  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+
+  Class Duplicable (ρ : @perm Σ) :=
+    duplicable_persistent tid : PersistentP (ρ tid).
+  Global Existing Instance duplicable_persistent.
+
+  Global Instance has_type_dup v ty : ty.(ty_dup) → Duplicable (v ◁ ty).
+  Proof. intros Hdup tid. apply _. Qed.
+
+  Global Instance lft_incl_dup κ κ' : Duplicable (κ ⊑ κ').
+  Proof. intros tid. apply _. Qed.
+
+  Global Instance sep_dup P Q :
+    Duplicable P → Duplicable Q → Duplicable (P ★ Q).
+  Proof. intros HP HQ tid. apply _. Qed.
+
+  Global Instance top_dup : Duplicable ⊤.
+  Proof. intros tid. apply _. Qed.
+
+End duplicable.
\ No newline at end of file
diff --git a/perm_incl.v b/perm_incl.v
index b1909f7a..d46618ba 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -15,9 +15,6 @@ Section defs.
   Global Instance perm_equiv : Equiv perm :=
     λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
 
-  Class Duplicable (ρ : @perm Σ) :=
-    perm_incl_duplicable : perm_incl ρ (ρ ★ ρ).
-
 End defs.
 
 Infix "⇒" := perm_incl (at level 95, no associativity) : C_scope.
@@ -76,6 +73,9 @@ Section props.
   Global Instance perm_top_left_id : LeftId (⇔) ⊤ sep.
   Proof. intros ρ. by rewrite comm right_id. Qed.
 
+  Lemma perm_incl_duplicable ρ (_ : Duplicable ρ) : ρ ⇒ ρ ★ ρ.
+  Proof. iIntros (tid) "#H!==>". by iSplit. Qed.
+
   Lemma perm_tok_plus κ q1 q2 :
     tok κ q1 ★ tok κ q2 ⇔ tok κ (q1 + q2).
   Proof.
@@ -92,30 +92,13 @@ Section props.
   Lemma perm_incl_share v κ ty :
     v ◁ &uniq{κ} ty ⇒ v ◁ &shr{κ} ty.
   Proof.
-    iIntros (tid) "Huniq". iDestruct "Huniq" as (l) "[% Hown]".
-    (* FIXME : we nee some tokens here. *)
+    iIntros (tid) "Huniq". destruct v; last done.
+    iDestruct "Huniq" as (l) "[% Hown]".
+    (* FIXME : we need some tokens here. *)
     iAssert (∃ q, [κ]{q})%I as "Htok". admit.
     iDestruct "Htok" as (q) "Htok".
     iVs (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown _]".
     admit. set_solver. iVsIntro. iExists _. iSplit. done. done.
   Admitted.
 
-  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 props.
-
-Hint Extern 0 (Duplicable (_ ◁ _)) => apply has_type_dup; exact I.
diff --git a/type.v b/type.v
index 5c363775..bbdad947 100644
--- a/type.v
+++ b/type.v
@@ -19,11 +19,10 @@ Section defs.
          used with anything else than namespaces. *)
       ty_shr : lifetime → thread_id → namespace → loc → iProp Σ;
 
+      ty_dup_persistent tid vl : ty_dup → PersistentP (ty_own tid vl);
       ty_shr_persistent κ tid N l : PersistentP (ty_shr κ tid N l);
 
       ty_size_eq tid vl : ty_own tid vl ⊢ length vl = ty_size;
-      ty_dup_dup tid vl E :
-        ty_dup → ty_own tid vl ={E}=> ty_own tid vl ★ ty_own tid vl;
       (* The mask for starting the sharing does /not/ include the
          namespace N, for allowing more flexibility for the user of
          this type (typically for the [own] type). AFAIK, there is no
@@ -43,7 +42,7 @@ Section defs.
           [κ]{q} ★ tl_own tid N ={E}=> ∃ q', ▷l ↦★{q'}: ty_own tid ★
              (▷l ↦★{q'}: ty_own tid ={E}=★ [κ]{q} ★ tl_own tid N)
     }.
-  Global Existing Instance ty_shr_persistent.
+  Global Existing Instances ty_shr_persistent ty_dup_persistent.
 
   Record simple_type :=
     { st_size : nat;
@@ -60,7 +59,6 @@ Section defs.
                  (∃ vl, (&frac{κ} λ q, l ↦★{q} vl) ★ ▷ st.(st_own) tid vl)%I
     |}.
   Next Obligation. apply st_size_eq. Qed.
-  Next Obligation. iIntros (st tid vl E _) "H". eauto. Qed.
   Next Obligation.
     intros st E N κ l tid q ??. iIntros "Hmt Htok".
     iVs (lft_borrow_exists with "Hmt Htok") as (vl) "[Hmt Htok]". set_solver.
@@ -106,7 +104,6 @@ Section types.
     {| ty_size := 0; ty_dup := true;
        ty_own tid vl := False%I; ty_shr κ tid N l := False%I |}.
   Next Obligation. iIntros (tid vl) "[]". Qed.
-  Next Obligation. iIntros (????) "[]". Qed.
   Next Obligation.
     iIntros (????????) "Hb Htok".
     iVs (lft_borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
@@ -145,10 +142,10 @@ Section types.
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ★
             ∀ q', [κ]{q'} ={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ tid N l' ★ [κ]{q'})%I
     |}.
+  Next Obligation. done. Qed.
   Next Obligation.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
-  Next Obligation. done. Qed.
   Next Obligation.
     intros q ty E N κ l tid q' ?? =>/=. iIntros "Hshr Htok".
     iVs (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
@@ -197,10 +194,10 @@ Section types.
             ∀ q' κ'', κ'' ⊑ κ ★ κ'' ⊑ κ' ★ [κ'']{q'}
                ={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ'' tid N l' ★ [κ'']{q'})%I
     |}.
+  Next Obligation. done. Qed.
   Next Obligation.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
-  Next Obligation. done. Qed.
   Next Obligation.
     intros κ ty E N κ' l tid q' ?? =>/=. iIntros "Hshr Htok".
     iVs (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
@@ -338,23 +335,17 @@ Section types.
            tyoffs.1.(ty_shr) κ tid (N .@ i) (shift_loc l (tyoffs.2)))%I
     |}.
   Next Obligation.
-    iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (vll) "(%&%&Hown)".
-    subst. by iApply (list_ty_type_eq with "Hown").
+    intros tyl tid vl Hfa.
+    cut (∀ vll, PersistentP ([★ list] tyvl ∈ combine tyl vll,
+                             ty_own (tyvl.1) tid (tyvl.2))). by apply _.
+    clear vl. induction tyl as [|ty tyl IH]=>[|[|vl vll]]; try by apply _.
+    edestruct andb_prop_elim as [Hduph Hdupq]. by apply Hfa.
+    rewrite /PersistentP /= big_sepL_cons.
+    iIntros "?". by iApply persistentP.
   Qed.
   Next Obligation.
-    induction tyl as [|ty tyq IH]; iIntros (tid vl E Hfa) "H";
-      iDestruct "H" as ([|vl0 vlq]) "(%&#Hlen&Hown)"; subst vl;
-      iDestruct "Hlen" as %Hlen; inversion Hlen; simpl in *.
-    - iIntros "!==>". iSplit; iExists []; by repeat iSplit.
-    - apply andb_prop_elim in Hfa. destruct Hfa as [Hfah Hfaq].
-      iDestruct (big_sepL_cons with "Hown") as "[Hh Hq]".
-      iVs (ty_dup_dup with "Hh") as "[Hh1 Hh2]". done.
-      iVs (IH tid (concat vlq) _ Hfaq with "[Hq]") as "[Hq1 Hq2]". by eauto.
-      iVsIntro. iSplitL "Hh1 Hq1".
-      + iDestruct "Hq1" as (vllq) "(%&%&?)". iExists (vl0::vllq).
-        rewrite big_sepL_cons/=. iFrame. iSplit; iPureIntro; congruence.
-      + iDestruct "Hq2" as (vllq) "(%&%&?)". iExists (vl0::vllq).
-        rewrite big_sepL_cons/=. iFrame. iSplit; iPureIntro; congruence.
+    iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (vll) "(%&%&Hown)".
+    subst. by iApply (list_ty_type_eq with "Hown").
   Qed.
   Next Obligation.
     intros tyl E N κ l tid q ??. rewrite split_prod_mt.
@@ -385,7 +376,7 @@ Section types.
       iIntros (q i offs) "#Hshr!#([Htokh Htokq]&Htlf&Htlh&Htlq)".
       rewrite big_sepL_cons Nat.add_0_r.
       iDestruct "Hshr" as "[Hshrh Hshrq]". setoid_rewrite <-Nat.add_succ_comm.
-      iVs (IH with "Hshrq [Htokq Htlf Htlq]") as (q'q) "[Hownq Hcloseq]". done. by iFrame.
+      iVs (IH with "Hshrq [Htokq Htlf Htlq]") as (q'q) "[Hownq Hcloseq]". by iFrame.
       iVs (tyh.(ty_shr_acc) with "Hshrh [Htokh Htlh]") as (q'h) "[Hownh Hcloseh]"; try done.
       by pose proof (nclose_subseteq N i); set_solver. by iFrame.
       destruct (Qp_lower_bound q'h q'q) as (q' & q'0h & q'0q & -> & ->).
@@ -440,16 +431,14 @@ Section types.
                (nth i tyl bot).(ty_shr) κ tid N (shift_loc l 1))%I
     |}.
   Next Obligation.
-    iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)". subst.
-    simpl. by iDestruct (sum_size_eq with "Hown") as %->.
+    intros n tyl Hn tid vl Hdup%Is_true_eq_true.
+    cut (∀ i vl', PersistentP (ty_own (nth i tyl bot) tid vl')). apply _.
+    intros. apply ty_dup_persistent. edestruct nth_in_or_default as [| ->]; last done.
+    rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left.
   Qed.
   Next Obligation.
-    iIntros (n tyl Hn tid vl E Hdup%Is_true_eq_true) "Hown".
-    iDestruct "Hown" as (i vl') "[% Hown]". subst.
-    iVs ((nth i tyl bot).(ty_dup_dup) with "Hown") as "[Hown1 Hown2]".
-    - edestruct nth_in_or_default as [| ->]; last done.
-      rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left.
-    - iSplitR "Hown1"; eauto.
+    iIntros (n tyl Hn tid vl) "Hown". iDestruct "Hown" as (i vl') "(%&Hown)". subst.
+    simpl. by iDestruct (sum_size_eq with "Hown") as %->.
   Qed.
   Next Obligation.
     intros n tyl Hn E N κ l tid q ??. iIntros "Hown Htok". rewrite split_sum_mt.
@@ -503,13 +492,13 @@ Section types.
   Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
     {| ty_size := 1; ty_dup := false;
        ty_own tid vl := (∃ f, vl = [f] ★
-          ∀ vl, ▷ ρ vl tid -★ tl_own tid ⊤
+          ∀ vl, ρ vl tid -★ tl_own tid ⊤
                  -★ WP f (map of_val vl) {{λ _, False}})%I;
        ty_shr κ tid N l := True%I |}.
+  Next Obligation. done. Qed.
   Next Obligation.
     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.
@@ -517,7 +506,7 @@ Section types.
   Program Definition fn {n : nat} (ρ : vec val n → @perm Σ):=
     ty_of_st {| st_size := 1;
        st_own tid vl := (∃ f, vl = [f] ★
-          ∀ vl, {{ ▷ ρ vl tid ★ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
+          ∀ vl, {{ ρ vl tid ★ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
   Next Obligation.
     iIntros (n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
diff --git a/type_incl.v b/type_incl.v
index d7b293fe..0332cb25 100644
--- a/type_incl.v
+++ b/type_incl.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import upred_big_op.
-From iris.program_logic Require Import thread_local.
+From iris.program_logic Require Import thread_local hoare.
 From lrust Require Export type perm_incl.
 
 Import Types.
@@ -40,9 +40,8 @@ Section ty_incl.
 
   Global Instance ty_incl_preorder ρ: Duplicable ρ → PreOrder (ty_incl ρ).
   Proof.
-    split.
-    - apply _.
-    - intros ?????. eauto using ty_incl_weaken, ty_incl_trans.
+    split. apply _.
+    eauto using ty_incl_weaken, ty_incl_trans, perm_incl_duplicable.
   Qed.
 
   Lemma ty_incl_bot ρ ty : ty_incl ρ ! ty.
@@ -87,34 +86,37 @@ Section ty_incl.
       by iApply (ty_shr_mono with "Hincl Hty").
   Qed.
 
+  (* We have the additional hypothesis that ρ should be duplicable.
+     The only way I can see to circumvent this limitation is to deeply
+     embed permissions (and their inclusion). Not sure this is worth it. *)
   Lemma ty_incl_prod ρ tyl1 tyl2 :
     Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 →
     ty_incl ρ (product tyl1) (product tyl2).
   Proof.
-    intros Hρ HFA. eapply ty_incl_weaken. apply Hρ.
-    iIntros (tid) "[Hρ1 Hρ2]". iSplitL "Hρ1".
+    intros Hρ HFA. iIntros (tid) "#Hρ". iSplitL "".
     - 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ρ". 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 "#Hρ". iVs (IH with "Hρ") as "#Hqimpl".
+          iVs (Hincl with "Hρ") 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. }
-      iVs (Himpl with "Hρ1") as "#Himpl". iIntros "!==>!#*H".
+      iVs (Himpl with "Hρ") as "#Himpl". iIntros "!==>!#*H".
       iDestruct "H" as (vll) "(%&%&H)". iExists _. iSplit. done. iSplit.
       by rewrite -(Forall2_length _ _ _ HFA). by iApply ("Himpl" with "[] H").
-    - rewrite /product /=. iRevert "Hρ2". generalize O.
+    - rewrite /product /=. iRevert "Hρ". 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ρ". 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 "!==>!#*".
+      + iIntros (i offs) "#Hρ". iVs (IH with "[] []") as "#Hqimpl".
+          by iClear "Hρ". (* TODO : get rid of this by doing induction in the proof mode. *)
+          done.
+        iVs (Hincl with "Hρ") as "[_ #Hhimpl]". iIntros "!==>!#*".
         rewrite !big_sepL_cons. iIntros "[Hh Hq]".
         setoid_rewrite <-Nat.add_succ_comm.
         iDestruct ("Hhimpl" $! _ _ _ with "Hh") as "[$ %]".
@@ -144,20 +146,18 @@ Section ty_incl.
   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).
+    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".
+    iIntros (DUP FA tid) "#Hρ". rewrite /sum /=. iSplitR "".
     - 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 "#Hρ".  iVs (IH with "Hρ") as "#IH". iVs (Hincl with "Hρ") as "[#Hh _]".
           iIntros "!==>*!#*Hown". destruct i as [|i]. by iApply "Hh". by iApply "IH". }
-      iVs (Hincl with "Hρ1") as "#Hincl". iIntros "!==>!#*H".
+      iVs (Hincl with "Hρ") as "#Hincl". iIntros "!==>!#*H".
       iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
         by iApply "Hincl".
     - assert (Hincl : ρ tid ={⊤}=>
@@ -165,11 +165,11 @@ Section ty_incl.
                      → (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 "#Hρ".
+          iVs (IH with "Hρ") as "#IH". iVs (Hincl with "Hρ") 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.
+      iVs (Hincl with "Hρ") as "#Hincl". iIntros "!==>!#*H". iSplit; last done.
       iDestruct "H" as (i) "[??]". iExists _. iSplit. done. by iApply "Hincl".
   Qed.
 
@@ -203,23 +203,26 @@ Section ty_incl.
     Duplicable ρ → (∀ vl : vec val n, ρ ★ ρ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.
+    iIntros (? Hρ1ρ2 tid) "#Hρ!==>". iSplit; iIntros "!#*H"; last by auto.
     iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-    iIntros (vl) "Htl Hown".
-    iApply pvs_wp. iInv lrustN as "Hρ" "Hclose".
-    (* FIXME : we need some kind of "Invariant of duplicable
-       propositions" that we can open several times. *)
-    admit.
-  Admitted.
+    iIntros (vl) "Hρ2 Htl". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+    by iApply ("Hwp" with "[-Htl] Htl").
+  Qed.
 
   Lemma ty_incl_fn {n} ρ ρ1 ρ2 :
     Duplicable ρ → (∀ vl : vec val n, ρ ★ ρ2 vl ⇒ ρ1 vl) →
     ty_incl ρ (fn ρ1) (fn ρ2).
-    (* FIXME : idem. *)
-    admit.
-  Admitted.
+  Proof.
+    iIntros (? Hρ1ρ2 tid) "#Hρ!==>". iSplit; iIntros "!#*#H".
+    - iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
+      iIntros (vl) "!#[Hρ2 Htl]". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+      iApply "Hwp". by iFrame.
+    - iSplit; last done. simpl. iDestruct "H" as (vl0) "[? Hvl]".
+      iExists vl0. iFrame "#". iNext. iDestruct "Hvl" as (f) "[% Hwp]".
+      iExists f. iSplit. done.
+      iIntros (vl) "!#[Hρ2 Htl]". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+      iApply "Hwp". by iFrame.
+  Qed.
 
   Lemma ty_incl_fn_cont {n} ρ ρf : ty_incl ρ (fn ρf) (cont (n:=n) ρf).
   Proof.
@@ -234,7 +237,7 @@ Section ty_incl.
     ty_incl ρ ty1 ty2 → ρ ★ v ◁ ty1 ⇒ v ◁ ty2.
   Proof.
     iIntros (Hincl tid) "[Hρ Hty1]". iVs (Hincl with "Hρ") as "[#Hownincl _]".
-    by iApply "Hownincl".
+    destruct v; last done. by iApply "Hownincl".
   Qed.
 
 End ty_incl.
\ No newline at end of file
-- 
GitLab