From 7c4dc90cba598c5dd91054e715a9bcea33692489 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 24 Dec 2016 11:40:06 +0100
Subject: [PATCH] Fixpoint type. There are still a few TODO for the
 non-expansiveness of sums, products and functions.

---
 _CoqProject                     |   1 +
 opam.pins                       |   2 +-
 theories/lifetime/definitions.v |   6 ++
 theories/typing/bool.v          |   3 +-
 theories/typing/borrow.v        |   3 +-
 theories/typing/fixpoint.v      |  67 +++++++++++++++
 theories/typing/function.v      |   3 +
 theories/typing/own.v           |  12 ++-
 theories/typing/product.v       |  14 +++-
 theories/typing/shr_bor.v       |  14 +++-
 theories/typing/sum.v           |   3 +
 theories/typing/type.v          | 144 +++++++++++++++++++++++++++++++-
 theories/typing/uninit.v        |   4 +-
 theories/typing/uniq_bor.v      |  23 +++--
 14 files changed, 278 insertions(+), 21 deletions(-)
 create mode 100644 theories/typing/fixpoint.v

diff --git a/_CoqProject b/_CoqProject
index 5098d4b6..e0d8ab8b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -40,3 +40,4 @@ theories/typing/function.v
 theories/typing/programs.v
 theories/typing/borrow.v
 theories/typing/cont.v
+theories/typing/fixpoint.v
diff --git a/opam.pins b/opam.pins
index cf8bb509..5c7302b3 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9c55bc2cb196512e08ad8756722ac127e539a1da
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 34eefd91027b10f99c930cbc15999fb7175a4168
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index f93130b6..d98f4dd1 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -281,16 +281,22 @@ Proof. apply (ne_proper_2 _). Qed.
 
 Global Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
 Proof. solve_proper. Qed.
+Global Instance idx_bor_contractive κ i : Contractive (idx_bor κ i).
+Proof. solve_contractive. Qed.
 Global Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
 Proof. apply (ne_proper _). Qed.
 
 Global Instance raw_bor_ne i n : Proper (dist n ==> dist n) (raw_bor i).
 Proof. solve_proper. Qed.
+Global Instance raw_bor_contractive i : Contractive (raw_bor i).
+Proof. solve_contractive. Qed.
 Global Instance raw_bor_proper i : Proper ((≡) ==> (≡)) (raw_bor i).
 Proof. apply (ne_proper _). Qed.
 
 Global Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
 Proof. solve_proper. Qed.
+Global Instance bor_contractive κ : Contractive (bor κ).
+Proof. solve_contractive. Qed.
 Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
 Proof. apply (ne_proper _). Qed.
 
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 65de7b92..ea832478 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -27,8 +27,7 @@ Section typing.
     typed_body E L C T e1 → typed_body E L C T e2 →
     typed_body E L C (TCtx_hasty p bool :: T) (if: p then e1 else e2).
   Proof.
-    (* FIXME why can't I merge these two iIntros? *)
-    iIntros (He1 He2). iIntros (tid qE) "#HEAP #LFT Htl HE HL HC".
+    iIntros (He1 He2 tid qE) "#HEAP #LFT Htl HE HL HC".
     rewrite tctx_interp_cons. iIntros "[Hp HT]".
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (b) "Hv". iDestruct "Hv" as %[=->].
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 5b1c1824..c61c6696 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -44,7 +44,7 @@ Section borrow.
       iMod (bor_sep _ _ _ (l' ↦∗: ty_own ty tid) with "LFT Hbor") as "[_ Hbor]". done.
       iMod ("Hclose" with "Htok") as "($ & $)".
       rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _, _.
-      iFrame. iSplitR. done. by rewrite -uPred.iff_refl.
+      iFrame. iSplitR. done. rewrite -uPred.iff_refl. auto.
     - iFrame "H↦ H† Hown".
     - iIntros "!>(?&?&?)!>". iNext. iExists _.
       rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
@@ -123,5 +123,4 @@ Section borrow.
       rewrite tctx_interp_singleton tctx_hasty_val' //.
       iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT Hincl' Hshr").
   Qed.
-
 End borrow.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
new file mode 100644
index 00000000..4d527fd0
--- /dev/null
+++ b/theories/typing/fixpoint.v
@@ -0,0 +1,67 @@
+From lrust.lifetime Require Import definitions.
+From lrust.typing Require Export type bool.
+
+Section fixpoint.
+  Context `{typeG Σ}.
+
+  Global Instance type_inhabited : Inhabited type := populate bool.
+
+  Context (T : type → type) `{Contractive T}.
+
+  (* FIXME : Contrarily to the rule on paper, these rules are
+     coinductive: they let one assume [ty] is [Copy]/[Send]/[Sync] to
+     prove that [T ty] is [Copy]/[Send]/[Sync]. *)
+  Global Instance fixpoint_copy :
+    (∀ `(!Copy ty), Copy (T ty)) → Copy (fixpoint T).
+  Proof.
+    intros ?. apply fixpoint_ind.
+    - intros ??[[EQsz%leibniz_equiv EQown]EQshr].
+      specialize (λ tid vl, EQown tid vl). specialize (λ κ tid l, EQshr κ tid l).
+      simpl in *=>-[Hp Hsh]; (split; [intros ??|intros ???]).
+      + revert Hp. by rewrite /PersistentP -EQown.
+      + intros F l q. rewrite -EQsz -EQshr. setoid_rewrite <-EQown. auto.
+    - exists bool. apply _.
+    - done.
+    - intros c Hc. split.
+      + intros tid vl. apply uPred.equiv_entails, equiv_dist=>n.
+        by rewrite conv_compl uPred.always_always.
+      + intros κ tid E F l q ? ?.
+        apply uPred.entails_equiv_and, equiv_dist=>n. etrans.
+        { apply equiv_dist, uPred.entails_equiv_and, (copy_shr_acc κ tid E F)=>//.
+          by rewrite -conv_compl. }
+        do 2 f_equiv; first by rewrite conv_compl. do 8 (f_contractive || f_equiv).
+        * by rewrite -conv_compl.
+        * destruct n. done. by setoid_rewrite conv_compl.
+        * by rewrite -conv_compl.
+        * f_equiv. f_contractive. unfold dist_later. destruct n=>//.
+          by setoid_rewrite conv_compl.
+  Qed.
+
+  Global Instance fixpoint_send :
+    (∀ `(!Send ty), Send (T ty)) → Send (fixpoint T).
+  Proof.
+    intros ?. apply fixpoint_ind.
+    - intros ?? EQ ????. by rewrite -EQ.
+    - exists bool. apply _.
+    - done.
+    - intros c Hc ???. apply uPred.entails_equiv_and, equiv_dist=>n.
+      rewrite conv_compl. apply equiv_dist, uPred.entails_equiv_and; apply Hc.
+  Qed.
+
+  Global Instance fixpoint_sync :
+    (∀ `(!Sync ty), Sync (T ty)) → Sync (fixpoint T).
+  Proof.
+    intros ?. apply fixpoint_ind.
+    - intros ?? EQ ?????. by rewrite -EQ.
+    - exists bool. apply _.
+    - done.
+    - intros c Hc ????. apply uPred.entails_equiv_and, equiv_dist=>n.
+      rewrite conv_compl. apply equiv_dist, uPred.entails_equiv_and; apply Hc.
+  Qed.
+
+  Lemma fixpoint_unfold_eqtype E L : eqtype E L (fixpoint T) (T (fixpoint T)).
+  Proof.
+    unfold eqtype, subtype, type_incl. setoid_rewrite <-fixpoint_unfold.
+    split; iIntros "_ _ _"; (iSplit; first done); iSplit; iIntros "!#*$".
+  Qed.
+End fixpoint.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index eeea31fa..76c6fe6b 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -4,6 +4,9 @@ From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
 
+(* TODO : prove contractiveness.
+   Prerequisite : cofe structure on lists and vectors. *)
+
 Section fn.
   Context `{typeG Σ}.
 
diff --git a/theories/typing/own.v b/theories/typing/own.v
index e02642a1..9bec068d 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -116,6 +116,17 @@ Section own.
     Proper (eqtype E L ==> eqtype E L) (own n).
   Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
 
+  Global Instance own_contractive n : Contractive (own n).
+  Proof.
+    intros m ?? EQ. split; [split|]; simpl.
+    - done.
+    - destruct m=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
+    - intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance own_ne n m : Proper (dist m ==> dist m) (own n).
+  Proof. apply contractive_ne, _. Qed.
+
   Global Instance own_send n ty :
     Send ty → Send (own n ty).
   Proof.
@@ -198,5 +209,4 @@ Section typing.
     iApply (wp_delete with "[-]"); try (by auto); [].
     rewrite freeable_sz_full. by iFrame.
   Qed.
-
 End typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index e1d8f2ce..bc59d38f 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -2,6 +2,9 @@ From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
 
+(* TODO : prove contractiveness.
+   Prerequisite : cofe structure on lists and vectors. *)
+
 Section product.
   Context `{typeG Σ}.
 
@@ -66,6 +69,16 @@ Section product.
     iSplitL "H1"; by iApply (ty_shr_mono with "LFT H⊑").
   Qed.
 
+  Global Instance product2_ne n:
+    Proper (dist n ==> dist n ==> dist n) product2.
+  Proof.
+    intros ?? EQ1 ?? EQ2. split; [split|]; simpl.
+    - by rewrite EQ1 EQ2.
+    - f_contractive. destruct n=>// tid vl.
+        by setoid_rewrite EQ1; setoid_rewrite EQ2.
+    - intros ???. by rewrite EQ1 EQ2.
+  Qed.
+
   Global Instance product2_mono E L:
     Proper (subtype E L ==> subtype E L ==> subtype E L) product2.
   Proof.
@@ -216,5 +229,4 @@ Section typing.
   Lemma prod_app E L tyl1 tyl2 :
     eqtype E L (Π[Π tyl1; Π tyl2]) (Π(tyl1 ++ tyl2)).
   Proof. by rewrite -prod_flatten_r -prod_flatten_l. Qed.
-
 End typing.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index eb7f2f4c..be026233 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -8,8 +8,7 @@ Section shr_bor.
   Context `{typeG Σ}.
 
   Program Definition shr_bor (κ : lft) (ty : type) : type :=
-    {| st_own tid vl :=
-         (∃ (l:loc), ⌜vl = [ #l ]⌝ ∗ ty.(ty_shr) κ tid l)%I |}.
+    {| st_own tid vl := (∃ (l:loc), ⌜vl = [ #l ]⌝ ∗ ty.(ty_shr) κ tid l)%I |}.
   Next Obligation.
     iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
@@ -20,7 +19,7 @@ Section shr_bor.
     intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
     iIntros (??) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
     iDestruct "H" as (l) "(% & H)". subst. iExists _. iSplit. done.
-    iApply (ty2.(ty_shr_mono) with "LFT Hκ"). 
+    iApply (ty2.(ty_shr_mono) with "LFT Hκ").
     iDestruct (Hty with "* [] [] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
     by iApply "Hs1".
   Qed.
@@ -31,6 +30,15 @@ Section shr_bor.
     Proper (eqtype E L ==> eqtype E L) (shr_bor κ).
   Proof. intros ??[]. by split; apply subtype_shr_bor_mono. Qed.
 
+  Global Instance shr_contractive κ : Contractive (shr_bor κ).
+  Proof.
+    intros n ?? EQ. apply ty_of_st_ne. apply Next_contractive.
+    destruct n=>// tid vl /=. apply uPred.exist_ne.
+    repeat (apply EQ || f_contractive || f_equiv).
+  Qed.
+  Global Instance shr_ne κ n : Proper (dist n ==> dist n) (shr_bor κ).
+  Proof. apply contractive_ne, _. Qed.
+
   Global Instance shr_send κ ty :
     Sync ty → Send (shr_bor κ ty).
   Proof.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index a55d5ee1..2f33dc40 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -3,6 +3,9 @@ From iris.base_logic Require Import fractional.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
 
+(* TODO : prove contractiveness.
+   Prerequisite : cofe structure on lists and vectors. *)
+
 Section sum.
   Context `{typeG Σ}.
 
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 51a4d8c9..3d3ddae3 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -35,7 +35,7 @@ Section type.
          invariants, which does not need the mask.  Moreover, it is
          more consistent with thread-local tokens, which we do not
          give any.
- 
+
          The lifetime token is needed (a) to make the definition of simple types
          nicer (they would otherwise require a "∨ □|=>[†κ]"), and (b) so that
          we can have emp == sum [].
@@ -62,7 +62,7 @@ Section type.
     - rewrite -Nat.add_1_l Nat2Z.inj_add /= IHn shift_loc_assoc.
       set_solver+.
   Qed.
-  
+
   Lemma shr_locsE_disj l n m :
     shr_locsE l n ⊥ shr_locsE (shift_loc l n) m.
   Proof.
@@ -202,6 +202,146 @@ Coercion ty_of_st : simple_type >-> type.
 Delimit Scope lrust_type_scope with T.
 Bind Scope lrust_type_scope with type.
 
+(* OFE and COFE structures on types and simple types. *)
+Section ofe.
+  Context `{typeG Σ}.
+
+  Section def.
+    Definition tuple_of_type (ty : type) : prodC (prodC _ _) _ :=
+      (ty.(ty_size),
+       Next (ty.(ty_own) : _ -c> _ -c> _),
+       ty.(ty_shr) :  _ -c> _ -c> _ -c> _).
+
+    Instance type_equiv : Equiv type := λ ty1 ty2,
+       tuple_of_type ty1 ≡ tuple_of_type ty2.
+    Instance type_dist : Dist type := λ n ty1 ty2,
+       tuple_of_type ty1 ≡{n}≡ tuple_of_type ty2.
+
+    Definition type_ofe_mixin : OfeMixin type.
+    Proof.
+      split; [|split|]; unfold equiv, dist, type_equiv, type_dist.
+      - intros. apply equiv_dist.
+      - by intros ?.
+      - by intros ???.
+      - by intros ???->.
+      - by intros ????; apply dist_S.
+    Qed.
+
+    Canonical Structure typeC : ofeT := OfeT type type_ofe_mixin.
+
+    Instance st_equiv : Equiv simple_type := λ st1 st2,
+      @Next (_ -c> _ -c> _) st1.(st_own) ≡ Next st2.(st_own).
+    Instance st_dist : Dist simple_type := λ n st1 st2,
+      @Next (_ -c> _ -c> _) st1.(st_own) ≡{n}≡ Next st2.(st_own).
+
+    Definition st_ofe_mixin : OfeMixin simple_type.
+    Proof.
+      split; [|split|]; unfold equiv, dist, st_equiv, st_dist.
+      - intros. apply equiv_dist.
+      - by intros ?.
+      - by intros ???.
+      - by intros ???->.
+      - by intros ????; apply dist_S.
+    Qed.
+
+    Canonical Structure simple_typeC : ofeT := OfeT simple_type st_ofe_mixin.
+  End def.
+
+  Global Instance ty_size_proper_d n:
+    Proper (dist n ==> eq) ty_size.
+  Proof. intros ?? EQ. apply EQ. Qed.
+  Global Instance ty_size_proper_e :
+    Proper ((≡) ==> eq) ty_size.
+  Proof. intros ?? EQ. apply EQ. Qed.
+  Global Instance ty_own_ne n:
+    Proper (dist (S n) ==> eq ==> eq ==> dist n) ty_own.
+  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+  Global Instance ty_own_proper_e:
+    Proper ((≡) ==> eq ==> eq ==> (≡)) ty_own.
+  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+  Global Instance ty_shr_ne n:
+    Proper (dist n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
+  Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
+  Global Instance ty_shr_proper_e :
+    Proper ((≡) ==> eq ==> eq ==> eq ==> (≡)) ty_shr.
+  Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
+  Global Instance st_own_ne n:
+    Proper (dist (S n) ==> eq ==> eq ==> dist n) st_own.
+  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+  Global Instance st_own_proper_e :
+    Proper ((≡) ==> eq ==> eq ==> (≡)) st_own.
+  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+
+  Global Program Instance type_cofe : Cofe typeC :=
+    {| compl c :=
+         let '(ty_size, Next ty_own, ty_shr) :=
+             compl {| chain_car := tuple_of_type ∘ c |}
+         in
+         {| ty_size := ty_size; ty_own := ty_own; ty_shr := ty_shr |}
+    |}.
+  Next Obligation. intros [c Hc]. apply Hc. Qed.
+  Next Obligation.
+    simpl. intros c _ _ shr [=_ _ ->] κ tid l.
+    apply uPred.equiv_entails, equiv_dist=>n.
+    by rewrite (λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c κ tid l) /=
+               uPred.always_always.
+  Qed.
+  Next Obligation.
+    simpl. intros c sz own _ [=-> -> _] tid vl.
+    apply uPred.entails_equiv_and, equiv_dist=>n.
+    rewrite (λ c, conv_compl (A:=_ -c> _ -c> _) n c tid vl) /= conv_compl /=.
+    apply equiv_dist, uPred.entails_equiv_and, ty_size_eq.
+  Qed.
+  Next Obligation.
+    simpl. intros c _ own shr [=_ -> ->] E κ l tid q ?.
+    apply uPred.entails_equiv_and, equiv_dist=>n.
+    rewrite (λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c κ tid l) /=.
+    setoid_rewrite (λ c vl, conv_compl (A:=_ -c> _ -c> _) n c tid vl). simpl.
+    etrans. { by apply equiv_dist, uPred.entails_equiv_and, (c n).(ty_share). }
+    simpl. destruct n; repeat (simpl; (f_contractive || f_equiv)).
+    rewrite (c.(chain_cauchy) (S n) (S (S n))) //. lia.
+  Qed.
+  Next Obligation.
+    simpl. intros c _ _ shr [=_ _ ->] κ κ' tid l.
+    apply uPred.entails_equiv_and, equiv_dist=>n.
+    rewrite !(λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c _ tid l) /=.
+    apply equiv_dist, uPred.entails_equiv_and. apply ty_shr_mono.
+  Qed.
+  Next Obligation.
+    intros n c. split; [split|]; simpl; try by rewrite conv_compl.
+    f_contractive. destruct n; first done. rewrite /= conv_compl //.
+  Qed.
+
+  Global Program Instance simple_type_cofe : Cofe simple_typeC :=
+    {| compl c :=
+         let 'Next st_own := compl
+                {| chain_car := Next ∘ (st_own : _ -> _ -c> _ -c> _) ∘ c |} in
+         {| st_own := st_own |}
+    |}.
+  Next Obligation. intros [c Hc]. apply Hc. Qed.
+  Next Obligation.
+    simpl. intros c own [=->] tid vl.
+    apply uPred.entails_equiv_and, equiv_dist=>n.
+    rewrite (λ c, conv_compl (A:=_ -c> _ -c> _) n c tid vl) /=.
+    apply equiv_dist, uPred.entails_equiv_and, st_size_eq.
+  Qed.
+  Next Obligation.
+    simpl. intros c own [=->] tid vl.
+    apply uPred.equiv_entails, equiv_dist=>n.
+    by rewrite (λ c, conv_compl (A:=_ -c> _ -c> _) n c tid vl) /=
+               uPred.always_always.
+  Qed.
+  Next Obligation.
+    intros n c. apply Next_contractive. destruct n=>//=. rewrite conv_compl //.
+  Qed.
+
+  Global Instance ty_of_st_ne n : Proper (dist n ==> dist n) ty_of_st.
+  Proof.
+    intros [][]EQ. split;[split|]=>//= κ tid l.
+    repeat (f_contractive || f_equiv). apply EQ.
+  Qed.
+End ofe.
+
 Section subtyping.
   Context `{typeG Σ}.
   Definition type_incl (ty1 ty2 : type) : iProp Σ :=
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index f25c3d1f..6153466d 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -11,7 +11,7 @@ Section uninit.
 
   Global Instance uninit_1_send : Send uninit_1.
   Proof. iIntros (tid1 tid2 vl) "H". done. Qed.
-    
+
   Definition uninit (n : nat) : type :=
     Π (replicate n uninit_1).
 
@@ -44,5 +44,5 @@ Section uninit.
       + iIntros (Heq). destruct n; first done. simpl.
         iExists [v], vl. iSplit; first done. iSplit; first done.
         iApply "IH". by inversion Heq.
-  Qed. 
+  Qed.
 End uninit.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 1f2ca93a..3d216196 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -20,7 +20,7 @@ Section uniq_bor.
           The trouble with this definition is that bor_unnest as proven is too
           weak. The original unnesting with open borrows was strong enough. *)
        ty_own tid vl :=
-         (∃ (l:loc) P, (⌜vl = [ #l ]⌝ ∗ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
+         (∃ (l:loc) P, (⌜vl = [ #l ]⌝ ∗ ▷ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
        ty_shr κ' tid l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
             □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ∪κ']
@@ -81,7 +81,7 @@ Section uniq_bor.
     iSplit; iAlways.
     - iIntros (??) "H". iDestruct "H" as (l P) "[[% #HPiff] Hown]". subst.
       iExists _, _. iSplitR; last by iApply (bor_shorten with "Hκ"). iSplit. done.
-      iIntros "!#". iSplit; iIntros "H".
+      iNext. iIntros "!#". iSplit; iIntros "H".
       + iDestruct ("HPiff" with "H") as (vl) "[??]". iExists vl. iFrame.
         by iApply "Ho1".
       + iDestruct "H" as (vl) "[??]". iApply "HPiff". iExists vl. iFrame.
@@ -104,11 +104,21 @@ Section uniq_bor.
     Proper (eqtype E L ==> eqtype E L) (uniq_bor κ).
   Proof. split; by apply subtype_uniq_mono. Qed.
 
+  Global Instance uniq_contractive κ : Contractive (uniq_bor κ).
+  Proof.
+    intros n ?? EQ. split; [split|]; simpl.
+    - done.
+    - destruct n=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
+    - intros κ' tid l. repeat (apply EQ || f_contractive || f_equiv).
+  Qed.
+  Global Instance uniq_ne κ n : Proper (dist n ==> dist n) (uniq_bor κ).
+  Proof. apply contractive_ne, _. Qed.
+
   Global Instance uniq_send κ ty :
     Send ty → Send (uniq_bor κ ty).
   Proof.
     iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (l P) "[[% #HPiff] H]".
-    iExists _, _. iFrame "H". iSplit; first done. iAlways. iSplit.
+    iExists _, _. iFrame "H". iSplit; first done. iNext. iAlways. iSplit.
     - iIntros "HP". iApply (heap_mapsto_pred_wand with "[HP]").
       { by iApply "HPiff". }
       clear dependent vl. iIntros (vl) "?". by iApply Hsend.
@@ -138,14 +148,14 @@ Section typing.
     iIntros (Hκ ???) "#LFT HE HL Huniq".
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
     rewrite /tctx_interp !big_sepL_singleton /=.
-    iDestruct "Huniq" as (v) "[% Huniq]". 
+    iDestruct "Huniq" as (v) "[% Huniq]".
     iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
     iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
     iMod (ty.(ty_share) with "LFT H↦ Htok") as "[Hown Htok]"; [solve_ndisj|].
     iMod ("Hclose" with "Htok") as "[$ $]". iExists _. iFrame "%".
     iIntros "!>/=". eauto.
   Qed.
-  
+
   Lemma tctx_reborrow_uniq E L p ty κ κ' :
     lctx_lft_incl E L κ' κ →
     tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)]
@@ -185,7 +195,7 @@ Section typing.
   Lemma write_uniq E L κ ty :
     lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
-    iIntros (Halive p tid F qE qL ?) "#LFT HE HL Hown". 
+    iIntros (Halive p tid F qE qL ?) "#LFT HE HL Hown".
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     iDestruct "Hown" as (l P) "[[EQ #HP] H↦]". iDestruct "EQ" as %[=->].
     iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
@@ -197,5 +207,4 @@ Section typing.
     iMod ("Hclose" with "Htok") as "($ & $ & $)".
     iExists _, _. erewrite <-uPred.iff_refl. auto.
   Qed.
-
 End typing.
-- 
GitLab