From f79b4f65a14622ed078fc33df65714ea6dd8c68a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2023 15:38:04 +0100
Subject: [PATCH] Bump Iris (beautify code for `iCombine .. gives`).

---
 coq-lambda-rust.opam                          |  2 +-
 theories/lang/heap.v                          |  6 ++--
 theories/lang/lib/arc.v                       |  8 ++---
 theories/lifetime/model/borrow_sep.v          |  2 +-
 theories/lifetime/model/primitive.v           | 29 +++++++++++++++----
 theories/typing/lib/brandedvec.v              |  2 +-
 theories/typing/lib/ghostcell.v               |  8 ++---
 theories/typing/lib/rc/rc.v                   | 10 +++----
 theories/typing/lib/rc/weak.v                 |  8 ++---
 theories/typing/lib/refcell/refmut_code.v     |  4 +--
 .../typing/lib/rwlock/rwlockreadguard_code.v  |  2 +-
 .../typing/lib/rwlock/rwlockwriteguard_code.v |  2 +-
 12 files changed, 51 insertions(+), 32 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index b5d1f3e6..862ba524 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2023-03-07.1.7e127436") | (= "dev") }
+  "coq-iris" { (= "dev.2023-03-09.0.f91e8eab") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 0ce57d17..4836e47f 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -412,7 +412,7 @@ Section heap.
   Proof.
     iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
     iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
-    iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid_discrete.
+    iCombine "HhF Hf" gives % [Hl Hv]%auth_both_valid_discrete.
     move: Hl=> /singleton_included_l [[q qs] [/leibniz_equiv_iff Hl Hq]].
     apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
     { move: (Hv (l.1)). rewrite Hl. by intros [??]. }
@@ -435,7 +435,7 @@ Section heap.
         σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
   Proof.
     iIntros "H● H◯".
-    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid_discrete.
+    iCombine "H● H◯" gives %[Hl?]%auth_both_valid_discrete.
     iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
     rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
@@ -454,7 +454,7 @@ Section heap.
     ⌜σ !! l = Some (ls, v)⌝.
   Proof.
     iIntros "H● H◯".
-    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid_discrete.
+    iCombine "H● H◯" gives %[Hl?]%auth_both_valid_discrete.
     iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
     rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 264a45ae..305e4000 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -208,7 +208,7 @@ Section arc.
                              if decide (strong = xH) then q = q' ∧ wlock = None
                              else ∃ q'', q' = (q + q'')%Qp⌝.
   Proof.
-    iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
+    iIntros "H● Htok". iCombine "H● Htok" gives
         %[[Hincl%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
     destruct st, Hincl as [[=]|(?&?&[= <-]&?&[Hincl|Hincl%csum_included])];
       simpl in *; subst.
@@ -333,7 +333,7 @@ Section arc.
   Lemma weak_tok_auth_val γ st :
     own γ (● st) -∗ weak_tok γ -∗ ⌜∃ st' weak, st = (st', S weak) ∧ ✓ st'⌝.
   Proof.
-    iIntros "H● Htok". iDestruct (own_valid_2 with "H● Htok") as
+    iIntros "H● Htok". iCombine "H● Htok" gives
         %[[Hincl%option_included Hincl'%nat_included]%prod_included [Hval _]]
          %auth_both_valid_discrete.
     destruct st as [?[]], Hincl as [_|(?&?&[=]&?)]; simpl in *; try lia. eauto.
@@ -588,7 +588,7 @@ Section arc.
                  (alloc_option_local_update (Excl ())). }
       iMod ("Hclose" with "[-HΦ HP1 H◯]") as "_"; first by iExists _; eauto with iFrame.
       iModIntro. wp_case. wp_bind (!ˢᶜ_)%E. iInv N as ([st ?]) "[>H● H]" "Hclose".
-      iDestruct (own_valid_2 with "H● H◯") as
+      iCombine "H● H◯" gives
         %[[[[=]|Hincl]%option_included _]%prod_included [? _]]%auth_both_valid_discrete.
       simpl in Hincl. destruct Hincl as (? & ? & [=<-] & -> & [|Hincl]); last first.
       + apply csum_included in Hincl. destruct Hincl as [->|[Hincl|(?&?&[=]&?)]]=>//.
@@ -598,7 +598,7 @@ Section arc.
         iMod ("Hclose" with "[-HΦ H◯ HP1]") as "_"; first by iExists _; auto with iFrame.
         iModIntro. wp_let. wp_op; case_bool_decide; [lia|]. wp_let. wp_op. wp_bind (_ <-ˢᶜ _)%E.
         iInv N as ([st w]) "[>H● H]" "Hclose".
-        iDestruct (own_valid_2 with "H● H◯") as
+        iCombine "H● H◯" gives
            %[[[[=]|Hincl]%option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
         simpl in Hincl. destruct Hincl as (x1 & x2 & [=<-] & -> & Hincl); last first.
         assert (∃ q p, x2 = Cinl (q, p, Excl' ())) as (? & ? & ->).
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 227c668a..816b02fd 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -97,7 +97,7 @@ Proof.
     iDestruct (own_bor_valid_2 with "Hown Hbor2")
         as %[EQB2%to_borUR_included _]%auth_both_valid_discrete.
     iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
-    { iIntros (->). iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2.
+    { iIntros (->). iCombine "Hbor1 Hbor2" gives %Hj1j2.
       exfalso; revert Hj1j2.
       rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid.
       by intros [[]]. }
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index aa235d8d..51db9d35 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -47,7 +47,7 @@ Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
     own alft_name (◯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some b⌝.
 Proof.
   iIntros "HA HΛ".
-  iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid_discrete.
+  iCombine "HA HΛ" gives %[HA _]%auth_both_valid_discrete.
   iPureIntro. move: HA=> /singleton_included_l [qs [/leibniz_equiv_iff]].
   rewrite lookup_fmap fmap_Some=> -[b' [? ->]] /Some_included.
   move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
@@ -65,7 +65,7 @@ Proof.
   { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
-  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
+  iCombine "Hγs Hγs'" gives %Hγs. move : Hγs.
   rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
@@ -78,6 +78,13 @@ 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 wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
+Global Instance own_bor_sep_gives κ x y :
+  CombineSepGives (own_bor κ x) (own_bor κ y) (✓ (x ⋅ y)).
+Proof.
+  rewrite /CombineSepGives. iIntros "[H1 H2]".
+  iDestruct (own_bor_valid_2 with "H1 H2") as "#?"; auto.
+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.
@@ -99,7 +106,7 @@ Proof.
   { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
-  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
+  iCombine "Hγs Hγs'" gives %Hγs. move: Hγs.
   rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L=> <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
@@ -112,6 +119,12 @@ 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 wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
+Global Instance own_cnt_sep_gives κ x y :
+  CombineSepGives (own_cnt κ x) (own_cnt κ y) (✓ (x ⋅ y)).
+Proof.
+  rewrite /CombineSepGives. iIntros "[H1 H2]".
+  iDestruct (own_cnt_valid_2 with "H1 H2") as "#?"; auto.
+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.
@@ -133,7 +146,7 @@ Proof.
   { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
   iIntros "[Hx Hy]".
   iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
-  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
+  iCombine "Hγs Hγs'" gives %Hγs. move: Hγs.
   rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L=> <-.
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
@@ -146,6 +159,12 @@ 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 wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
+Global Instance own_inh_sep_gives κ x y :
+  CombineSepGives (own_inh κ x) (own_inh κ y) (✓ (x ⋅ y)).
+Proof.
+  rewrite /CombineSepGives. iIntros "[H1 H2]".
+  iDestruct (own_inh_valid_2 with "H1 H2") as "#?"; auto.
+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.
@@ -276,7 +295,7 @@ Lemma lft_tok_dead q κ : q.[κ] -∗ [† κ] -∗ False.
 Proof.
   rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
   iDestruct (@big_sepMS_elem_of _ _ _ _ _ _ Λ' with "H") as "H"=> //.
-  iDestruct (own_valid_2 with "H H'") as %Hvalid.
+  iCombine "H H'" gives %Hvalid.
   move: Hvalid=> /auth_frag_valid /=; by rewrite singleton_op singleton_valid.
 Qed.
 
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 1a104e77..94e4ad98 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -151,7 +151,7 @@ Section brandedvec.
     iDestruct "Hn" as (γn) "(Hidx1 & Hn)".
     iDestruct "Hm" as (γm) "(Hidx2 & Hm)".
     iDestruct (lft_meta_agree with "Hidx1 Hidx2") as %<-.
-    iDestruct (own_valid_2 with "Hn Hm") as %[?%max_nat_included ?]%auth_both_valid_discrete.
+    iCombine "Hn Hm" gives %[?%max_nat_included ?]%auth_both_valid_discrete.
     iPureIntro. simpl in *. lia.
   Qed.
 
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index d5ea8279..bb868034 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -552,7 +552,7 @@ Section ghostcell.
         destruct rw as[|].
         { iDestruct "Hst'" as (κ'0) "(Hbor & Hdead)".
           iMod (bor_acc_atomic with "LFT Hbor") as "[[> Hst' Hcloseb]|[H† Hcloseb]]"; first done.
-          - iDestruct (own_valid_2 with "Hset Hst'") as %[].
+          - iCombine "Hset Hst'" gives %[].
           - iMod "Hcloseb" as "_".
             iMod ("Hdead" with "H†") as "Hst'".
             iMod ("Hcloses" with "Hset") as "Hβ2".
@@ -579,7 +579,7 @@ Section ghostcell.
           iExists l, (Vector.cons #lc Vector.nil).
           by iFrame "Hshr Hl Hfree". }
         iDestruct "Hsucc" as (q'0) "[>Hownκ'0 Hcloseκ'0]".
-        iDestruct (own_valid_2 with "Hset Hownκ'0") as %Hvalidκ'0.
+        iCombine "Hset Hownκ'0" gives %Hvalidκ'0.
         (* Argue that we have the same κ' here as the already existing sharing protocol. *)
         assert (Hκ'κ'0 : κ' = κ'0).
         { move: Hvalidκ'0. rewrite /ghosttoken_st_to_R /=.
@@ -683,7 +683,7 @@ Section ghostcell.
         { iDestruct "Hst'" as (κ'0) "(Hbor & Hdead)".
           iMod (bor_acc_atomic with "LFT Hbor") as "[[> Hst' Hcloseb]|[H† Hcloseb]]";
             first done.
-          { iDestruct (own_valid_2 with "Hset Hst'") as %[]. }
+          { iCombine "Hset Hst'" gives %[]. }
           iMod "Hcloseb" as "_".
           iMod ("Hdead" with "H†") as "Hst'".
           iFrame. done. }
@@ -692,7 +692,7 @@ Section ghostcell.
         iClear "Hshrκ".
         iMod (frac_bor_atomic_acc with "LFT Hκ'0bor") as "[Hsucc|[H Hcloseb]]"; first done.
         { iDestruct "Hsucc" as (q) "[>Htok _]".
-          iDestruct (own_valid_2 with "Hset Htok") as %[]. }
+          iCombine "Hset Htok" gives %[]. }
         iMod "Hcloseb" as "_".
         iMod ("Hνκ" with "H") as "$".
         iMod "Hclose".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 6a397b3d..bf265d14 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -280,7 +280,7 @@ Section code.
       iPoseProof "Hpersist" as (ty') "(Hincl & Hinv & _ & #Hνend)".
       iMod (na_inv_acc with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
       iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
-      iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
+      iCombine "Hst Htok" gives %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
         %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
       simpl in EQst'. subst st. destruct Hincl as [Hincl|Hincl].
       + destruct st' as [[]| |]; try by inversion Hincl. apply (inj Cinl) in Hincl.
@@ -344,7 +344,7 @@ Section code.
           iIntros "!> Hna". iClear "Hνend". clear q' Hqq' weak Hval.
           iMod (na_inv_acc with "Hinv Hna") as "(Hproto & Hna & Hclose)"; [solve_ndisj..|].
           iDestruct "Hproto" as ([st weak]) "[>Hst Hproto]".
-          iDestruct (own_valid_2 with "Hst Htok") as %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
+          iCombine "Hst Htok" gives %[[[[=]|(?&st'&[=<-]&EQst'&Hincl)]
             %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete.
           simpl in EQst'. subst st. destruct Hincl as [Hincl|Hincl]; first last.
           { apply csum_included in Hincl. destruct Hincl as
@@ -415,7 +415,7 @@ Section code.
     iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
-    iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
+    iCombine "Hrc● Hrctok" gives %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
                %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl].
@@ -475,7 +475,7 @@ Section code.
     iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
-    iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
+    iCombine "Hrc● Hrctok" gives %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
                %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl].
@@ -581,7 +581,7 @@ Section code.
     iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weak]) "[>Hrc● Hrcst]".
-    iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
+    iCombine "Hrc● Hrctok" gives %[[[[=]|(?&[[q0 s0]| |]&[=<-]&?&Hincl)]
                %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl].
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 2680ceac..2239d898 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -156,7 +156,7 @@ Section code.
     iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
     iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
-    iDestruct (own_valid_2 with "Hrc● Hwtok") as
+    iCombine "Hrc● Hwtok" gives
       %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
     destruct st as [[[q'' strong]| |]|]; try done.
     - (* Success case. *)
@@ -257,7 +257,7 @@ Section code.
     iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
     iMod (na_bor_acc with "LFT Hrctokb Hα1 Hna") as "(>Hrctok & Hna & Hclose3)"; [solve_ndisj..|].
     iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
-    iDestruct (own_valid_2 with "Hrc● Hrctok") as %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
+    iCombine "Hrc● Hrctok" gives %[[[[=]|(?&[[q0 weak0]| |]&[=<-]&?&Hincl)]
                %option_included _]%prod_included [Hval _]]%auth_both_valid_discrete;
     setoid_subst; try done; last first.
     { exfalso. destruct Hincl as [Hincl|Hincl].
@@ -324,7 +324,7 @@ Section code.
     { iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose2)"; [solve_ndisj..|].
       iMod (na_bor_acc with "LFT Hwtokb Hα1 Hna") as "(>Hwtok & Hna & Hclose3)"; [solve_ndisj..|].
       iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
-      iDestruct (own_valid_2 with "Hrc● Hwtok") as
+      iCombine "Hrc● Hwtok" gives
         %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
       iMod (own_update with "Hrc●") as "[Hrc● $]".
       { by apply auth_update_alloc, prod_local_update_2,
@@ -397,7 +397,7 @@ Section code.
       iDestruct "Hszeq" as %Hszeq.
       iMod (na_inv_acc with "Hinv Hna") as "(Hrcproto & Hna & Hclose)"; [solve_ndisj..|].
       iDestruct "Hrcproto" as ([st weakc]) "[>Hrc● Hrcst]".
-      iDestruct (own_valid_2 with "Hrc● Hwtok") as
+      iCombine "Hrc● Hwtok" gives
           %[[_ Hweak%nat_included]%prod_included [Hval _]]%auth_both_valid_discrete.
       destruct weakc as [|weakc]; first by simpl in *; lia.
       iMod (own_update_2 with "Hrc● Hwtok") as "Hrc●".
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 8aba2dc7..ccc5f4dc 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -129,7 +129,7 @@ Section refmut_functions.
     iDestruct "INV" as (st) "(H↦lrc & H● & INV)". wp_read. wp_let. wp_op. wp_write.
     iAssert (|={↑lftN ∪ lft_userE}[lft_userE]▷=> refcell_inv tid lrc γ β ty')%I
       with "[H↦lrc H● H◯ Hν INV]" as "INV".
-    { iDestruct (own_valid_2 with "H● H◯") as
+    { iCombine "H● H◯" gives
         %[[[=]|(? & [[? q'] ?] & [= <-] & Hst & INCL)]%option_included _]
          %auth_both_valid_discrete.
       destruct st as [[[[??]?]?]|]; [|done]. move: Hst=>-[= ???]. subst.
@@ -302,7 +302,7 @@ Section refmut_functions.
     iMod (na_bor_acc with "LFT Hinv Hβ Hna") as "(INV & Hna & Hclosena)"; [done..|].
     wp_seq. wp_op. wp_read.
     iDestruct "INV" as (st) "(Hlrc & H● & Hst)".
-    iDestruct (own_valid_2 with "H● Hγ") as %[Hst _]%auth_both_valid_discrete.
+    iCombine "H● Hγ" gives %[Hst _]%auth_both_valid_discrete.
     destruct st as [[[[??]?]?]|]; last by destruct Hst as [[?|] Hst]; inversion Hst.
     move:Hst=>/Some_pair_included [/Some_pair_included_total_1
               [/to_agree_included /(leibniz_equiv _ _) [= <- <-] _] _].
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 5659b7a6..c796ae0b 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -86,7 +86,7 @@ Section rwlockreadguard_functions.
     + iAssert (|={⊤ ∖ ↑rwlockN}[⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ lft_userE]▷=>
                (lx' ↦ #(Z_of_rwlock_st st'-1) ==∗ rwlock_inv tid_own tid lx' γ β ty))%I
         with "[H● H◯ Hx' Hν Hst H†]" as "INV".
-      { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
+      { iCombine "H● H◯" gives %[[[=]| (? & st0 & [=<-] & -> & [Heq|Hle])]
            %option_included Hv]%auth_both_valid_discrete.
         - destruct st0 as [|[[agν q']n]|]; try by inversion Heq. revert Heq. simpl.
           intros [[EQ <-%leibniz_equiv]%(inj2 pair) <-%leibniz_equiv]
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 3c9ac622..33d062b8 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -127,7 +127,7 @@ Section rwlockwriteguard_functions.
     iMod (at_bor_acc_tok with "LFT Hinv Hβ") as "[INV Hcloseβ]"; [done..|].
     iDestruct "INV" as (st) "(H↦ & H● & INV)". wp_write.
     iMod ("Hcloseβ" with "[> H↦ H● H◯ INV Hx']") as "Hβ".
-    { iDestruct (own_valid_2 with "H● H◯") as %[[[=]| (? & st0 & [=<-] & -> &
+    { iCombine "H● H◯" gives %[[[=]| (? & st0 & [=<-] & -> &
          [Heq|Hle])]%option_included Hv]%auth_both_valid_discrete;
       last by destruct (exclusive_included _ _ Hle).
       destruct st0 as [[[]|]| |]; try by inversion Heq.
-- 
GitLab