From 627eb7152502e3e2b56d52f55048643e678c9de2 Mon Sep 17 00:00:00 2001
From: Hai Dang <hai@bedrocksystems.com>
Date: Fri, 5 May 2023 00:26:40 +0200
Subject: [PATCH] update dependency

---
 coq-lambda-rust.opam                 |  2 +-
 theories/lang/arc.v                  | 11 +++++++----
 theories/lifetime/frac_borrow.v      |  2 +-
 theories/lifetime/model/borrow.v     |  4 +++-
 theories/lifetime/model/borrow_sep.v |  6 ++++--
 theories/lifetime/model/boxes.v      |  2 +-
 theories/lifetime/model/creation.v   | 21 +++++++++++++--------
 theories/lifetime/model/primitive.v  | 16 ++++++++--------
 theories/lifetime/model/reborrow.v   |  6 ++++--
 theories/typing/fixpoint.v           |  2 +-
 theories/typing/lft_contexts.v       |  4 ++--
 theories/typing/lib/arc.v            | 12 ++++++------
 theories/typing/lib/rwlock/rwlock.v  | 11 ++++++-----
 theories/typing/programs.v           |  2 +-
 theories/typing/sum.v                |  2 +-
 theories/typing/type.v               | 18 +++++++++---------
 theories/typing/type_context.v       |  2 +-
 17 files changed, 69 insertions(+), 54 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 748c8e27..aacd92be 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2023-05-02.2.34a8bf9d") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-05-03.1.44a343ae") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index c2f5d1d4..c8fb1519 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -2124,7 +2124,8 @@ Section arc.
       iIntros "!>".
       iDestruct (GPS_SWSharedReaders_join with "R' SR'") as "R'".
       iDestruct (StrDowns_join with "[$SD $SD']") as "SD".
-      iCombine "oW" "oW'" as "oW". iCombine "HP1" "HP2" as "HP". rewrite HPn.
+      iCombine "oW" "oW'" as "oW". iCombine "HP1" "HP2" as "HP".
+      rewrite (bi.wand_entails _ _ (HPn _ _)).
       iCombine "SeenD" "SeenD'" as "SeenD'".
       iDestruct (SeenActs_join with "SeenD'") as "SeenD'".
       case (decide (n = 1%positive)) => nEq.
@@ -2294,7 +2295,8 @@ Section arc.
       iApply step_fupd_intro; [solve_ndisj|]. iIntros "!>".
       iDestruct (GPS_SWSharedReaders_join with "R' SR'") as "R'".
       iDestruct (StrDowns_join with "[$SD $SD']") as "SD".
-      iCombine "oW" "oW'" as "oW". iCombine "HP1" "HP2" as "HP". rewrite HPn.
+      iCombine "oW" "oW'" as "oW". iCombine "HP1" "HP2" as "HP".
+      rewrite (bi.wand_entails _ _ (HPn _ _)).
       iCombine "SeenD" "SeenD'" as "SeenD'".
       iDestruct (SeenActs_join with "SeenD'") as "SeenD'".
       iSplitR "SA"; last first. { iExists None. by iFrame "SA". }
@@ -2482,7 +2484,8 @@ Section arc.
         iDestruct (GPS_SWSharedReaders_join with "SR' SR") as "SR'".
         iDestruct (StrMoves_agree with "[$SM $SM']") as %?. subst Mt2.
         iCombine "SM" "SM'" as "SM". iCombine "HP1" "HP2" as "HP".
-        iCombine "tok" "tok'" as "tok". rewrite HPn Qp.add_comm -Qp.div_add_distr Eq''.
+        iCombine "tok" "tok'" as "tok".
+        rewrite (bi.wand_entails _ _ (HPn _ _)) Qp.add_comm -Qp.div_add_distr Eq''.
         iCombine "tok" "tokW" as "tok". iDestruct ("FR" with "tok VR") as "#$".
         by iFrame "SR' SMA WUA SM HP tok VR".
       - (* it's impossible to read 1 with only F_read *)
@@ -2680,7 +2683,7 @@ Section arc.
     iDestruct (StrDowns_join with "[$SD $SD']") as "SD".
     iCombine "SeenD" "SeenD'" as "SeenD'". iClear "SeenD".
     iDestruct (SeenActs_join with "SeenD'") as "SeenD".
-    rewrite HPn Eq.
+    rewrite (bi.wand_entails _ _ (HPn _ _)) Eq.
     iAssert (SeenActs γs l (Mt ∪ {[t']}))%I with "[SW MAX]" as "#SeenM".
     { iExists _, _. iDestruct (GPS_SWWriter_Reader with "SW") as "$".
       by iFrame "MAX". } iClear "rTrue R MAX". clear Vb MAX t2 v2 t v.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 67bf1b2d..0853bfd8 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -112,7 +112,7 @@ Section frac_bor.
     iIntros (?) "#LFT Hfrac Hκ".
     iDestruct "Hfrac" as (γ κ' V0 φ') "#(Hκκ' & HV0 & Hφ' & Hfrac & Hshr)".
     iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[Hκ Hclose]". { done. }
-    rewrite -{1}(Qp.div_2 qκ'). rewrite lft_tok_split_obj.
+    rewrite -{1}(Qp.div_2 qκ'). rewrite (bi.wand_entails _ _ (lft_tok_split_obj _ _ _)).
     iDestruct "Hκ" as "[Hκ1 Hκ2]".
     iMod (in_at_bor_acc with "LFT Hshr Hκ1") as (Vb) "[H Hclose']"; try done.
     iCombine "H HV0" as "HH".
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 5abdccb6..afb8da0b 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -44,7 +44,9 @@ Proof.
   iSpecialize ("Hclose'" with "[Hvs Hinh HboxB HB● HB]").
   { iNext. iExists _. iFrame "%". iLeft. rewrite lft_inv_alive_unfold /lft_inv.
     iExists (P' ∗ Pb)%I, (P' ∗ Pi)%I.
-    iFrame "Hinh". rewrite -lft_vs_frame /lft_bor_alive. iFrame. iExists _.
+    iFrame "Hinh".
+    rewrite -(bi.wand_entails _ _ (lft_vs_frame _ _ _ _)) /lft_bor_alive.
+    iFrame. iExists _.
     iFrame "HboxB HB●". rewrite big_sepM_insert /=; [|by destruct (B !! γB)].
     iFrame. auto with lat. }
   iMod ("Hclose" with "[HA HI Hclose']") as "_".
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index b84379aa..74579407 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -7,6 +7,7 @@ From iris.prelude Require Import options.
 Lemma uPred_and_split {M} (P Q1 Q2 : uPred M) :
   P ∧ (Q1 ∗ Q2) -∗ ∃ P1 P2, bi_persistently (P1 ∗ P2 → P) ∗ (Q1 ∧ P1) ∗ (Q2 ∧ P2).
 Proof.
+  apply bi.entails_wand.
   uPred.unseal. split. intros ? x ?[HP(a1&a2&Hx&HQ1&HQ2)].
   exists (uPred_ownM a1), (uPred_ownM a2). uPred.unseal.
   eexists ε, _. rewrite left_id. split; [done|]. split.
@@ -22,7 +23,7 @@ Lemma monPred_and_split {M I} (P Q1 Q2 : monPred I (uPredI M)) :
   P ∧ (Q1 ∗ Q2) -∗
   ∃ P1 P2, bi_persistently (⎡P1 ∗ P2⎤ → P) ∗ (Q1 ∧ ⎡P1⎤) ∗ (Q2 ∧ ⎡P2⎤).
 Proof.
-  iStartProof (uPred _). iIntros (i). rewrite uPred_and_split.
+  iStartProof (uPred _). iIntros (i). rewrite (bi.wand_entails _ _ (uPred_and_split _ _ _)).
   iDestruct 1 as (P1 P2) "(#? & H1 & H2)". iExists P1, P2.
   iSplit; [by iIntros (? ->) "!>"|iFrame].
 Qed.
@@ -65,7 +66,8 @@ Proof.
   { rewrite lookup_fmap EQB //. }
   iAssert (▷ (⎡P' V'⎤ ∧ (P ∗ Q)))%I with "[HP']" as "HP'".
   { iNext. iSplit; [done|]. iApply "HPP'". by iApply monPred_in_elim. }
-  rewrite monPred_and_split. iDestruct "HP'" as (P0 Q0) "(#HP' & HP & HQ)".
+  rewrite (bi.wand_entails _ _ (monPred_and_split _ _ _)).
+  iDestruct "HP'" as (P0 Q0) "(#HP' & HP & HQ)".
   iCombine "HP HQ HV' HPP'" as "HH". iClear "HPP'".
   iDestruct (monPred_in_intro with "HH") as (V) "(#HV & HP & HQ & % & #HPP')".
   set (P1 := (((monPred_in V) ∨ ⎡P0⎤) ∧ (monPred_in V → P))%I).
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 0b5fd532..7b9d0c88 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -103,7 +103,7 @@ Lemma box_own_auth_update γ o1 o2 o3 :
   ==∗ box_own_auth γ (●E o3) ∗ box_own_auth γ (◯E o3).
 Proof.
   rewrite /box_own_auth -!own_op -pair_op left_id.
-  apply own_update, prod_update; last done.
+  apply bi.entails_wand, own_update, prod_update; last done.
   by apply excl_auth_update.
 Qed.
 
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 52ac3b87..00e13c7e 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -169,8 +169,11 @@ Proof.
   iMod ("Hclose" with "[HA HI Hinv]") as "_".
   { iNext. rewrite /lfts_inv /own_alft_auth.
     iExists (<[Λ:=(true, bot)]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
-    rewrite big_sepS_impl. iApply "Hinv".
-    rewrite /lft_inv. iIntros (κ ?) "!> !> H". iDestruct "H" as (Vκ) "[Hhv H]".
+    iCombine "LFT Hinv" as "Hinv".
+    iApply (embed_mono with "Hinv").
+    iIntros "[#LFT Hinv]".
+    iApply (big_sepS_impl with "Hinv").
+    rewrite /lft_inv. iIntros "!#" (κ ?) "H". iDestruct "H" as (Vκ) "[Hhv H]".
     iDestruct "Hhv" as %Hhv. iExists Vκ. iSplit.
     - iPureIntro. intros Λ' HΛ'. specialize (Hhv Λ' HΛ').
       rewrite lookup_insert_ne //. intros <-. by rewrite HΛ in Hhv.
@@ -228,11 +231,13 @@ Proof.
     - left. destruct Hd as (Λ'&?&?). exists Λ'. split; [|done].
       by eapply gmultiset_elem_of_subseteq.
     - right. by eapply gmultiset_elem_of_subseteq. }
-  { rewrite big_sepS_impl. iApply "HinvD".
-    iIntros "!> !>" (κ [[? _]_]%elem_of_filter) "[[$ _]|[_ %]]".
+  { iApply (embed_mono with "HinvD"). iApply big_sepS_mono.
+    iIntros (κ [[? _]_]%elem_of_filter) "[[$ _]|[_ %]]".
     by edestruct @lft_alive_and_dead_in. }
-  { rewrite big_sepS_impl. iApply "HinvK".
-    iIntros "!> !>" (κ [_ Hκ]%elem_of_K) "[[H %]|H]"; [iLeft|iRight]; iFrame "H %".
+  { iCombine "HΛ HinvK" as "H".
+    iApply (embed_mono with "H"). iIntros "[#HΛ HinvK]".
+    iApply (big_sepS_impl with "HinvK").
+    iIntros "!>" (κ [_ Hκ]%elem_of_K) "[[H %]|H]"; [iLeft|iRight]; iFrame "H %".
     rewrite /lft_dead /=. iExists _, _, _. iIntros "{$HΛ} !%". split; [|done].
     case Hκ=>// Hd. by destruct (lft_alive_and_dead_in A κ). }
   iModIntro. iMod ("Hclose" with "[-]") as "_"; last first.
@@ -251,11 +256,11 @@ Proof.
   iModIntro. iModIntro. iExists A', I.
   rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
   rewrite HI !big_sepS_union //. iSplitL "HinvD".
-  - rewrite big_sepS_impl. iApply "HinvD".
+  - iApply (big_sepS_impl with "HinvD").
     iIntros "!>" (κ [[??]?]%elem_of_filter) "Halive".
     rewrite /lft_inv. iExists (Vs κ). iSplitR; [by auto|].
     iLeft. iFrame "Halive". iPureIntro. by apply lft_alive_in_insert_false.
-  - rewrite big_sepS_impl /lft_inv. iApply "HinvK".
+  - iApply (big_sepS_impl with "HinvK").
     iIntros "!>" (κ [? HκK]%elem_of_K) "Hdead". iExists (Vs κ). iSplitR; [by auto|].
     iRight. iFrame. iPureIntro. destruct HκK.
     + by apply lft_dead_in_insert_false. + by apply lft_dead_in_insert_false'.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 73491d98..2df819b8 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -79,7 +79,7 @@ Proof. rewrite /IsOp /IntoSep=>->. by rewrite own_bor_op. Qed.
 Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_bor_valid_2 κ x y : own_bor κ x -∗ own_bor κ y -∗ ✓ (x ⋅ y).
-Proof. apply bi.wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
+Proof. apply bi.entails_wand, bi.wand_intro_r. rewrite -own_bor_op. iApply own_bor_valid. Qed.
 Lemma own_bor_update κ x y : x ~~> y → own_bor κ x ==∗ own_bor κ y.
 Proof.
   iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
@@ -87,7 +87,7 @@ Qed.
 Lemma own_bor_update_2 κ x1 x2 y :
   x1 ⋅ x2 ~~> y → own_bor κ x1 ⊢ own_bor κ x2 ==∗ own_bor κ y.
 Proof.
-  intros. apply bi.wand_intro_r. rewrite -own_bor_op. by apply own_bor_update.
+  intros. apply bi.wand_intro_r. rewrite -own_bor_op. by iApply own_bor_update.
 Qed.
 
 Lemma own_cnt_auth I κ x : own_ilft_auth I -∗ own_cnt κ x -∗ ⌜κ ∈ dom I⌝.
@@ -113,7 +113,7 @@ Qed.
 Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_cnt_valid_2 κ x y : own_cnt κ x -∗ own_cnt κ y -∗ ✓ (x ⋅ y).
-Proof. apply bi.wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
+Proof. apply bi.entails_wand, bi.wand_intro_r. rewrite -own_cnt_op. iApply own_cnt_valid. Qed.
 Lemma own_cnt_update κ x y : x ~~> y → own_cnt κ x ==∗ own_cnt κ y.
 Proof.
   iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
@@ -121,7 +121,7 @@ Qed.
 Lemma own_cnt_update_2 κ x1 x2 y :
   x1 ⋅ x2 ~~> y → own_cnt κ x1 -∗ own_cnt κ x2 ==∗ own_cnt κ y.
 Proof.
-  intros. apply bi.wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
+  intros. apply bi.entails_wand, bi.wand_intro_r. rewrite -own_cnt_op. by iApply own_cnt_update.
 Qed.
 
 Lemma own_inh_auth I κ x : own_ilft_auth I -∗ own_inh κ x -∗ ⌜κ ∈ dom I⌝.
@@ -147,7 +147,7 @@ Qed.
 Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_inh_valid_2 κ x y : own_inh κ x -∗ own_inh κ y -∗ ✓ (x ⋅ y).
-Proof. apply bi.wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
+Proof. apply bi.entails_wand, bi.wand_intro_r. rewrite -own_inh_op. iApply own_inh_valid. Qed.
 Lemma own_inh_update κ x y : x ~~> y → own_inh κ x ==∗ own_inh κ y.
 Proof.
   iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
@@ -155,7 +155,7 @@ Qed.
 Lemma own_inh_update_2 κ x1 x2 y :
   x1 ⋅ x2 ~~> y → own_inh κ x1 ⊢ own_inh κ x2 ==∗ own_inh κ y.
 Proof.
-  intros. apply bi.wand_intro_r. rewrite -own_inh_op. by apply own_inh_update.
+  intros. apply bi.wand_intro_r. rewrite -own_inh_op. by iApply own_inh_update.
 Qed.
 
 (** Alive and dead *)
@@ -334,7 +334,7 @@ Lemma lft_tok_split_obj `{LatBottom Lat bot} q1 q2 κ :
   (q1 + q2).[κ] -∗ q1.[κ] ∗ <obj> q2.[κ].
 Proof.
   rewrite /lft_tok. rewrite -monPred_objectively_big_sepMS_entails -big_sepMS_sep.
-  apply big_sepMS_mono=>// Λ ?. iStartProof (iProp _). iDestruct 1 as (V) "[#? H]".
+  iApply big_sepMS_mono=>// Λ ?. iStartProof (iProp _). iDestruct 1 as (V) "[#? H]".
   rewrite (fin_maps.singletonM_proper Λ _ (Cinl (_, to_latT V ⋅ to_latT bot))); last first.
   { rewrite lat_op_join' right_id //. } rewrite pair_op Cinl_op -singleton_op.
   iDestruct "H" as "[Hp Hq]". iSplitL "Hp"; [by auto|]. iIntros (?). iExists bot. auto.
@@ -353,7 +353,7 @@ Qed.
 Lemma lft_incl_intro κ κ' :
   □ (∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ]))
     -∗ κ ⊑ κ'.
-Proof. reflexivity. Qed.
+Proof. iIntros "?". done. Qed.
 
 Lemma lft_intersect_incl_l κ κ' : ⊢ κ ⊓ κ' ⊑ κ.
 Proof.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 15ff1a3c..9a2c56b9 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -7,6 +7,7 @@ From iris.prelude Require Import options.
 Lemma and_extract_ownM {M} σ (P : uPred M) :
   uPred_ownM σ ∧ P -∗ uPred_ownM σ ∗ (uPred_ownM σ -∗ P).
 Proof.
+  apply bi.entails_wand.
   uPred.unseal. split=>?? Hv[[σ' Hσ']]. revert Hv. move:Hσ'=>->. exists σ, σ'.
   split; [done|split].
   - exists ε. by rewrite right_id.
@@ -21,8 +22,9 @@ Proof. rewrite own.own_eq. apply and_extract_ownM. Qed.
 Lemma and_extract_own_bor `{lftG Σ Lat userE} κ σ (P : iProp Σ) :
   own_bor κ σ ∧ P -∗ own_bor κ σ ∗ (own_bor κ σ -∗ P).
 Proof.
+  apply bi.entails_wand.
   rewrite /own_bor bi.and_exist_r bi.exist_elim=>// γ.
-  rewrite bi.sep_and -(assoc bi_and) (and_extract_own _ _ P).
+  rewrite bi.sep_and -(assoc bi_and) (bi.wand_entails _ _ (and_extract_own _ _ P)).
   iIntros "(#Hag & Hσ & Hclose)". iSplitL "Hσ"; [by auto|]. iIntros "H".
   iApply "Hclose". iDestruct "H" as (γ') "[#Hag' H]".
   iDestruct (own_valid_2 with "Hag Hag'") as %Hγs. move : Hγs.
@@ -58,7 +60,7 @@ Proof.
     iApply "HQ"; auto. }
   rewrite {2}/idx_bor_own monPred_at_exist /= bi.and_exist_r.
   iDestruct "Hi" as (V0) "Hi". rewrite monPred_at_sep monPred_at_embed monPred_at_in.
-  rewrite (bi.sep_and ⌜V0 ⊑ V⌝%I) -(assoc bi_and) and_extract_own_bor.
+  rewrite (bi.sep_and ⌜V0 ⊑ V⌝%I) -(assoc bi_and) (bi.wand_entails _ _ (and_extract_own_bor _ _ _)).
   iDestruct "Hi" as "(% & Hi & HcloseQ)".
   iDestruct (own_bor_auth with "HI Hi") as %?.
   assert (κ ⊆ κ') by (by apply strict_include).
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 0389062d..2e5c1b52 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -61,7 +61,7 @@ Section fixpoint.
       { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
       apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
       + apply bi.limit_preserving_Persistent; solve_proper.
-      + apply limit_preserving_impl', bi.limit_preserving_entails;
+      + apply limit_preserving_impl', bi.limit_preserving_emp_valid;
         solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
 
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 494c6b5c..7e28f6f8 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -75,7 +75,7 @@ Section lft_contexts.
   Qed.
 
   Lemma llctx_elt_interp_acc_noend qmax x :
-    llctx_elt_interp qmax x -∗
+    llctx_elt_interp qmax x ⊢
     llctx_elt_interp_noend qmax x 1 ∗ (llctx_elt_interp_noend qmax x 1 -∗ llctx_elt_interp qmax x).
   Proof.
     destruct x as [κ κs].
@@ -145,7 +145,7 @@ Section lft_contexts.
   Context (E : elctx) (L : llctx).
 
   Definition lctx_lft_incl κ κ' : Prop :=
-    ∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ ⌜κ ⊑ˢʸⁿ κ'⌝)%I.
+    ∀ qmax qL, llctx_interp_noend qmax L qL ⊢ □ (elctx_interp E -∗ ⌜κ ⊑ˢʸⁿ κ'⌝)%I.
 
   Definition lctx_lft_eq κ κ' : Prop :=
     lctx_lft_incl κ κ' ∧ lctx_lft_incl κ' κ.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 7c208d38..e04a4162 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -62,7 +62,7 @@ Section arc.
   Qed.
 
   Lemma arc_persist_send tid tid' ν γi γs γw γsw l ty `{!Send ty,!Sync ty} :
-    arc_persist tid ν γi γs γw γsw l ty -∗ arc_persist tid' ν γi γs γw γsw l ty.
+    arc_persist tid ν γi γs γw γsw l ty ⊢ arc_persist tid' ν γi γs γw γsw l ty.
   Proof.
     iIntros "#($ & ? & Hvs)". rewrite sync_change_tid. iFrame "#".
     iIntros "!> Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
@@ -359,7 +359,7 @@ Section arc.
   Proof. apply type_contractive_ne, _. Qed.
 
   Lemma weak_subtype ty1 ty2 :
-    type_incl ty1 ty2 -∗ type_incl (weak ty1) (weak ty2).
+    type_incl ty1 ty2 ⊢ type_incl (weak ty1) (weak ty2).
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
     iSplit; first done. iSplit; iModIntro.
@@ -859,7 +859,7 @@ Section arc.
     iDestruct "Hrc'" as (γi γs γw γsw ν t q) "(#Hpersist & Htok & Hν)".
     wp_bind (drop_arc _). iApply (drop_arc_spec with "[] [Htok Hν]");
       [| |by iDestruct "Hpersist" as "[$?]"| |];
-      [move => ??; by rewrite fractional| solve_ndisj|
+      [move => ??; rewrite fractional; auto| solve_ndisj|
       iSplitL "Htok"; [by iExists _|done]|].
     iNext. iIntros (b) "Hdrop". wp_bind (if: _ then _ else _)%E.
     iApply (wp_wand _ _ _ (λ _, ty_own (box (option ty)) tid [r])%I with "[Hdrop Hr]").
@@ -969,7 +969,7 @@ Section arc.
     iDestruct "Hrc'" as (γi γs γw γsw ν t q) "(#Hpersist & Htok & Hν)".
     wp_apply (try_unwrap_spec with "[] [Hν Htok]");
       [| |by iDestruct "Hpersist" as "[$?]"|iFrame; by iExists _|];
-      [move => ??; by rewrite fractional|solve_ndisj|..].
+      [move => ??; rewrite fractional; auto|solve_ndisj|..].
     iIntros ([]) "H"; wp_if.
     - iDestruct "H" as "[Hν Hend]". rewrite -(lock [r]). destruct r as [[|r|]|]=>//=.
       iDestruct "Hr" as "[Hr >Hfree]". iDestruct "Hr" as (vl0) "[>Hr Hown]".
@@ -1054,7 +1054,7 @@ Section arc.
     { iDestruct "Hrc" as "[Hrc|$]"=>//. by iApply arc_own_share. }
     iDestruct "Hrc" as (γi γs γw γsw ν t q') "[#(Hi & Hs & #Hc) [Htok1 Htok2]]".
     wp_apply (is_unique_spec with "Hi [Htok1 $Htok2]");
-      [move => ??; by rewrite fractional|solve_ndisj|by iExists _|].
+      [move => ??; rewrite fractional; auto|solve_ndisj|by iExists _|].
     iIntros ([]) "H"; wp_if.
     - iDestruct "H" as "(Hrc & Hrc1 & Hν)". iSpecialize ("Hc" with "Hν"). wp_bind Skip.
       iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [done..|set_solver|].
@@ -1141,7 +1141,7 @@ Section arc.
     { iDestruct "Hrc" as "[Hrc|$]"=>//. by iApply arc_own_share. }
     iDestruct "Hrc" as (γi γs γw γsw ν t q') "[#(Hi & Hs & #Hc) [Htok1 Htok2]]". wp_let.
     wp_apply (try_unwrap_full_spec with "Hi [Htok1 $Htok2]");
-      [move =>??; by rewrite fractional|solve_ndisj|by iExists _|..]. iIntros (x).
+      [move =>??; rewrite fractional; auto|solve_ndisj|by iExists _|..]. iIntros (x).
     pose proof (fin_to_nat_lt x). destruct (fin_to_nat x) as [|[|[]]]; last lia.
     - iIntros "(Hrc0 & Hrc1 & HP1)". wp_case. wp_bind (_ +â‚— _)%E.
       iSpecialize ("Hc" with "HP1").
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index fcc9a5c7..9d3c4c8e 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -55,7 +55,7 @@ Section rwlock_inv.
   Lemma rwown_update_write_read ν γs :
     let st' : rwlock_st := Some (inr (ν, (1/2)%Qp, 1%positive)) in
     rwown γs (st_global None)
-    ==∗ rwown γs (st_global st') ∗ rwown γs (reading_st (1/2)%Qp ν).
+    ⊢ |==> rwown γs (st_global st') ∗ rwown γs (reading_st (1/2)%Qp ν).
   Proof.
     iIntros (st') "g". rewrite -embed_sep -own_op.
     iMod (own_update with "g") as "$"; [|done]. apply auth_update_alloc.
@@ -67,10 +67,11 @@ Section rwlock_inv.
     let st : rwlock_st := (Some (inr (ν, q, n))) in
     let st': rwlock_st := Some (inr (ν, (q + (q'/2)%Qp)%Qp, (n + 1)%positive)) in
     rwown γs (st_global st)
-    ==∗ rwown γs (st_global st') ∗ rwown γs (reading_st (q'/2)%Qp ν).
+    ⊢ |==> rwown γs (st_global st') ∗ rwown γs (reading_st (q'/2)%Qp ν).
   Proof.
-    iIntros (st') "g". rewrite -embed_sep -own_op.
+    iIntros (st st') "g". rewrite -embed_sep -own_op.
     iMod (own_update with "g") as "$"; [|done]. apply auth_update_alloc.
+    subst st st'.
     rewrite Pos.add_comm Qp.add_comm -pos_op_add /=
             -{2}(agree_idemp (to_agree _)) -frac_op
             2!pair_op Cinr_op Some_op.
@@ -83,7 +84,7 @@ Section rwlock_inv.
 
   Lemma rwown_update_write γs :
     let st' : rwlock_st := Some (inl ()) in
-    rwown γs (st_global None) ==∗ rwown γs (st_global st') ∗ rwown γs writing_st.
+    rwown γs (st_global None) ⊢ |==> rwown γs (st_global st') ∗ rwown γs writing_st.
   Proof.
     iIntros (st') "g". rewrite -embed_sep -own_op.
     iMod (own_update with "g") as "$"; [|done]. apply auth_update_alloc.
@@ -92,7 +93,7 @@ Section rwlock_inv.
 
   Lemma rwown_update_write_dealloc γs :
     let st : rwlock_st := Some (inl ()) in
-    rwown γs (st_global st) -∗ rwown γs writing_st ==∗ rwown γs (st_global None).
+    rwown γs (st_global st) ⊢ rwown γs writing_st ==∗ rwown γs (st_global None).
   Proof.
     iIntros (st) "g w". iCombine "g" "w" as "gw".
     iMod (own_update with "gw") as "$"; [|done]. apply auth_update_dealloc.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 295463e8..9eab149f 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -119,7 +119,7 @@ Section typing_rules.
   (* This lemma is helpful when switching from proving unsafe code in Iris
      back to proving it in the type system. *)
   Lemma type_type E L C T e :
-    typed_body E L C T e -∗ typed_body E L C T e.
+    typed_body E L C T e ⊢ typed_body E L C T e.
   Proof. done. Qed.
 
   (** This lemma can replace [κ1] by [κ2] and vice versa in positions that
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 19d9cb58..5f05f2d5 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -201,7 +201,7 @@ Section sum.
         - apply shr_locsE_subseteq. lia.
         - set_solver+. }
       destruct (Qp.lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
-      rewrite -(heap_mapsto_pred_combine _ q' q'02); last (by intros; apply ty_size_eq).
+      rewrite -(heap_mapsto_pred_combine _ q' q'02); last (by intros; iApply ty_size_eq).
       rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).
       iDestruct "HownC" as "[HownC1 HownC2]". iDestruct "Hown" as "[Hown1 Hown2]".
       iExists q'. iModIntro. iSplitL "Hown1 HownC1".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 8d7789d0..400c3d22 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -30,7 +30,7 @@ Record type `{!typeG Σ} :=
 
     ty_shr_persistent κ tid l : Persistent (ty_shr κ tid l);
 
-    ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_size⌝;
+    ty_size_eq tid vl : ty_own tid vl ⊢ ⌜length vl = ty_size⌝;
     (* 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
@@ -119,7 +119,7 @@ Qed.
 
 Record simple_type `{!typeG Σ} :=
   { st_own : thread_id → list val → vProp Σ;
-    st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
+    st_size_eq tid vl : st_own tid vl ⊢ ⌜length vl = 1%nat⌝;
     st_own_persistent tid vl : Persistent (st_own tid vl) }.
 Global Existing Instance st_own_persistent.
 Global Instance: Params (@st_own) 2 := {}.
@@ -176,7 +176,7 @@ Section ofe.
     (lft -d> thread_id -d> loc -d> vPropO Σ).
   Let P (x : T) : Prop :=
     (∀ κ tid l, Persistent (x.2 κ tid l)) ∧
-    (∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1⌝) ∧
+    (∀ tid vl, x.1.2 tid vl ⊢ ⌜length vl = x.1.1⌝) ∧
     (∀ E κ l tid q, ↑lftN ⊆ E →
       ⎡lft_ctx⎤ -∗ &{κ} (l ↦∗: λ vs, x.1.2 tid vs) -∗
       q.[κ] ={E}=∗ x.2 κ tid l ∗ q.[κ]) ∧
@@ -221,9 +221,9 @@ Section ofe.
     - (* TODO: automate this *)
       repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?).
       + apply bi.limit_preserving_Persistent=> n ty1 ty2 Hty; apply Hty.
-      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; [apply Hty|by rewrite Hty].
-      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
-      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
+      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; last by rewrite Hty. apply Hty.
+      + apply bi.limit_preserving_emp_valid=> n ty1 ty2 Hty. repeat f_equiv; apply Hty.
+      + apply bi.limit_preserving_emp_valid=> n ty1 ty2 Hty. repeat f_equiv; apply Hty.
   Qed.
 
   Inductive st_equiv' (ty1 ty2 : simple_type) : Prop :=
@@ -415,7 +415,7 @@ Global Instance lst_copy_cons `{!typeG Σ} ty tys :
   Copy ty → ListCopy tys → ListCopy (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Send `{!typeG Σ} (t : type) :=
-  send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
+  send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl ⊢ t.(ty_own) tid2 vl.
 Global Instance: Params (@Send) 2 := {}.
 
 Class ListSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
@@ -425,7 +425,7 @@ Global Instance lst_send_cons `{!typeG Σ} ty tys :
   Send ty → ListSend tys → ListSend (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Sync `{!typeG Σ} (t : type) :=
-  sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
+  sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l ⊢ t.(ty_shr) κ tid2 l.
 Global Instance: Params (@Sync) 2 := {}.
 
 Class ListSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
@@ -552,7 +552,7 @@ Definition type_equal `{!typeG Σ} (ty1 ty2 : type) : vProp Σ :=
 Global Instance: Params (@type_equal) 2 := {}.
 
 Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
-  ∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
+  ∀ qmax qL, llctx_interp_noend qmax L qL ⊢ □ (elctx_interp E -∗ type_incl ty1 ty2).
 Global Instance: Params (@subtype) 4 := {}.
 
 (* TODO: The prelude should have a symmetric closure. *)
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 9f82fffa..8ae9561d 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -150,7 +150,7 @@ Section type_context.
 
   (** Send typing contexts *)
   Class SendC (T : tctx) :=
-    sendc_change_tid tid1 tid2 : tctx_interp tid1 T -∗ tctx_interp tid2 T.
+    sendc_change_tid tid1 tid2 : tctx_interp tid1 T ⊢ tctx_interp tid2 T.
 
   Global Instance tctx_nil_send : SendC [].
   Proof. done. Qed.
-- 
GitLab