WIP.

theories/typing/lft_contexts.v

@@ -173,9 +173,11 @@ Section lft_contexts.
     ∀ F qL, ↑lftN ⊆ F → elctx_interp E -∗ llctx_interp L qL ={F}=∗
           ∃ q', q'.[κ] ∗ (q'.[κ] ={F}=∗ llctx_interp L qL).
 
-  Lemma lctx_lft_alive_tok κ :
-    lctx_lft_alive κ → lctx_lft_alive κ.
-  Proof. done. Qed.
+  Lemma lctx_lft_alive_tok κ F q :
+    ↑lftN ⊆ F →
+    lctx_lft_alive κ → elctx_interp E -∗ llctx_interp L q ={F}=∗
+      ∃ q', q'.[κ] ∗ llctx_interp L (q / 2) ∗ (q'.[κ] ={F}=∗ llctx_interp L (q / 2)).
+  Proof. iIntros (? Hal) "#HE [$ HL]". by iApply Hal. Qed.
 
   Lemma lctx_lft_alive_static : lctx_lft_alive static.
   Proof.

theories/typing/lib/refcell/ref.v

@@ -76,19 +76,19 @@ Section ref.
   Global Instance ref_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) ref.
   Proof.
-    iIntros (α1 α2 Hα ty1 ty2 Hty) "#HE #HL".
-    iDestruct (Hty with "HE HL") as "(%&#Ho&#Hs)".
-    iDestruct (Hα with "HE HL") as "Hα1α2".
-    iSplit; [|iSplit; iAlways].
+    iIntros (α1 α2 Hα ty1 ty2 Hty q) "HL".
+    iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
     - done.
     - iIntros (tid [|[[]|][|[[]|][]]]) "H"; try done.
-      iDestruct "H" as (ν q γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
-      iExists ν, q, γ, β, ty'. iFrame "∗#". iSplit.
+      iDestruct "H" as (ν q' γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
+      iExists ν, q', γ, β, ty'. iFrame "∗#". iSplit.
       + iApply ty_shr_mono; last by iApply "Hs".
         iApply lft_intersect_mono. done. iApply lft_incl_refl.
       + by iApply lft_incl_trans.
-    - iIntros (κ tid l) "H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
-      iExists ν, q, γ, β, ty', lv, lrc. iDestruct "H" as "#($&$&?&?&$&$)". iSplit.
+    - iIntros (κ tid l) "H". iDestruct "H" as (ν q' γ β ty' lv lrc) "H".
+      iExists ν, q', γ, β, ty', lv, lrc. iDestruct "H" as "#($&$&?&?&$&$)". iSplit.
       + iApply ty_shr_mono; last by iApply "Hs".
         iApply lft_intersect_mono. done. iApply lft_incl_refl.
       + by iApply lft_incl_trans.

theories/typing/lib/refcell/ref_code.v

@@ -56,17 +56,23 @@ Section ref_functions.
      See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
   Lemma ref_clone_type ty :
     typed_val ref_clone
-      (fn (fun '(α, β) => FP [α; β]%EL [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
+              (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
+                                     [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x').
-    iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
+
+Typeclasses Opaque llctx_interp.
+    iIntros (tid) "#LFT HE Hna [HL1 HL2] Hk HT".
+
+
+    simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hβδ & Hinv & H◯inv)".
-    wp_op. rewrite {1}/elctx_interp big_sepL_cons big_sepL_singleton.
-    iDestruct "HE" as "[[Hα1 Hα2] Hβ]".
+    wp_op.
+    iMod (lctx_lft_alive_tok _ _ β with "HE HL") as (q') "[Hβ Hclose1]"; [solve_typing..|].
     iMod (lft_incl_acc with "Hβδ Hβ") as (qδ) "[Hδ Hcloseβ]". done.
     iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
     iMod (na_bor_acc with "LFT Hinv Hδ Hna") as "(INV & Hna & Hcloseδ)"; [done..|].

theories/typing/lib/refcell/refmut.v

@@ -80,11 +80,10 @@ Section refmut.
   Global Instance refmut_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> eqtype E L ==> subtype E L) refmut.
   Proof.
-    iIntros (α1 α2 Hα ty1 ty2 Hty) "#HE #HL".
-    pose proof Hty as Hty'%eqtype_unfold.
-    iDestruct (Hty' with "HE HL") as "(%&#Ho&#Hs)".
-    iDestruct (Hα with "HE HL") as "Hα1α2".
-    iSplit; [|iSplit; iAlways].
+    intros α1 α2 Hα ty1 ty2. rewrite eqtype_unfold=>Hty. iIntros (q) "HL".
+    iDestruct (Hty with "HL") as "#Hty". iDestruct (Hα with "HL") as "#Hα".
+    iIntros "!# #HE". iDestruct ("Hα" with "HE") as "Hα1α2".
+    iDestruct ("Hty" with "HE") as "(%&#Ho&#Hs)". iSplit; [|iSplit; iAlways].
     - done.
     - iIntros (tid [|[[]|][|[[]|][]]]) "H"; try done.
       iDestruct "H" as (ν γ β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".