From 26b7ab260b79ffeff8a16a866aeb00ee37a8fb67 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2023 16:04:12 +0100
Subject: [PATCH] More uses of `iCombine .. gives`.
---
theories/barrier/proof.v | 8 +--
theories/hocap/lib/oneshot.v | 3 +-
theories/lecture_notes/coq_intro_example_2.v | 6 +-
.../locks/array_based_queuing_lock/abql.v | 4 +-
theories/logatom/treiber2.v | 4 +-
theories/logrel/F_mu_ref_conc/binary/rules.v | 68 +++++++++----------
6 files changed, 46 insertions(+), 47 deletions(-)
diff --git a/theories/barrier/proof.v b/theories/barrier/proof.v
index bcbad09d..148223e9 100644
--- a/theories/barrier/proof.v
+++ b/theories/barrier/proof.v
@@ -86,8 +86,8 @@ Proof.
{ iExists false, γsps. iFrame. }
wp_pures. by wp_apply ("IH" with "[$] [$]"). }
iSpecialize ("HRs" with "[//]"). wp_load.
- iDestruct (own_valid_2 with "H● H◯")
- as %[Hvalid%gset_disj_included%elem_of_subseteq_singleton _]%auth_both_valid_discrete.
+ iCombine "H● H◯"
+ gives %[Hvalid%gset_disj_included%elem_of_subseteq_singleton _]%auth_both_valid_discrete.
iDestruct (big_sepS_delete with "HRs") as "[HR'' HRs]"; first done.
iDestruct "HR''" as (R'') "[#Hsp' HR'']".
iDestruct (saved_prop_agree with "Hsp Hsp'") as "#Heq".
@@ -106,8 +106,8 @@ Proof.
rename P1 into R1; rename P2 into R2.
iIntros (?). iDestruct 1 as (γ P R' γsp) "(#Hinv & HR & H◯ & #Hsp)".
iInv N as (b γsps) "(>Hl & >H● & HRs)".
- iDestruct (own_valid_2 with "H● H◯")
- as %[Hvalid%gset_disj_included%elem_of_subseteq_singleton _]%auth_both_valid_discrete.
+ iCombine "H● H◯"
+ gives %[Hvalid%gset_disj_included%elem_of_subseteq_singleton _]%auth_both_valid_discrete.
iMod (own_update_2 with "H● H◯") as "H●".
{ apply (auth_update_dealloc _ _ (GSet (γsps ∖ {[ γsp ]}))).
apply gset_disj_dealloc_local_update. }
diff --git a/theories/hocap/lib/oneshot.v b/theories/hocap/lib/oneshot.v
index 2527c932..05fc171a 100644
--- a/theories/hocap/lib/oneshot.v
+++ b/theories/hocap/lib/oneshot.v
@@ -25,8 +25,7 @@ Lemma shot_not_pending `{oneshotG Σ} γ v q :
shot γ v -∗ pending γ q -∗ False.
Proof.
iIntros "Hs Hp".
- iPoseProof (own_valid_2 with "Hs Hp") as "H".
- iDestruct "H" as %[].
+ iCombine "Hs Hp" gives %[].
Qed.
Lemma shot_agree `{oneshotG Σ} γ (v w: val) :
shot γ v -∗ shot γ w -∗ ⌜v = w⌝.
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index 1affbc1b..b9eb89cd 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -313,7 +313,7 @@ Section monotone_counter.
wp_bind (! _)%E.
iInv N as (m) ">[Hpt HOwnAuth]" "HClose".
wp_load.
- iDestruct (@own_valid_2 _ _ _ γ with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag.
+ iCombine "HOwnAuth HOwnFrag" gives %H%mcounterRA_valid_auth_frag.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists m; iFrame. }
iModIntro.
@@ -491,7 +491,7 @@ Section monotone_counter'.
wp_lam.
iInv N as (m) ">[Hpt HOwnAuth]" "HClose".
wp_load.
- iDestruct (@own_valid_2 _ _ _ γ with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag'.
+ iCombine "HOwnAuth HOwnFrag" gives %H%mcounterRA_valid_auth_frag'.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists m; iFrame. }
iModIntro.
@@ -509,7 +509,7 @@ Section monotone_counter'.
wp_bind (! _)%E.
iInv N as (m) ">[Hpt HOwnAuth]" "HClose".
wp_load.
- iDestruct (@own_valid_2 _ _ _ γ with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag'.
+ iCombine "HOwnAuth HOwnFrag" gives %H%mcounterRA_valid_auth_frag'.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists m; iFrame. }
iModIntro.
diff --git a/theories/locks/array_based_queuing_lock/abql.v b/theories/locks/array_based_queuing_lock/abql.v
index a0af4571..d19cfef7 100644
--- a/theories/locks/array_based_queuing_lock/abql.v
+++ b/theories/locks/array_based_queuing_lock/abql.v
@@ -474,8 +474,8 @@ Section proof.
* (* The case where the lock is closed. *)
rewrite xsEq in xsLookup. apply nth_list_with_one in xsLookup.
assert (t = o) as ->. { apply (mod_fact _ _ i (cap)); auto. }
- iDestruct (own_valid_2 with "Ticket Ticket2")
- as % [_ ?%gset_disj_valid_op]%auth_frag_op_valid_1.
+ iCombine "Ticket Ticket2"
+ gives % [_ ?%gset_disj_valid_op]%auth_frag_op_valid_1.
set_solver.
- iMod ("Close" with "[nextPts isArr Inv Auth Part]") as "_".
{ iNext. iExists o, i, xs. iFrame. auto. }
diff --git a/theories/logatom/treiber2.v b/theories/logatom/treiber2.v
index c9243229..84afa0ef 100644
--- a/theories/logatom/treiber2.v
+++ b/theories/logatom/treiber2.v
@@ -150,8 +150,8 @@ Qed.
Lemma auth_agree γ xs ys :
own γ (● (Excl' xs)) -∗ own γ (◯ (Excl' ys)) -∗ ⌜xs = ys⌝.
Proof.
- iIntros "Hγ● Hγ◯". by iDestruct (own_valid_2 with "Hγ● Hγ◯")
- as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
+ iIntros "Hγ● Hγ◯". by iCombine "Hγ● Hγ◯"
+ gives %[<-%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
Qed.
(** The view of the authority can be updated together with the local view. *)
diff --git a/theories/logrel/F_mu_ref_conc/binary/rules.v b/theories/logrel/F_mu_ref_conc/binary/rules.v
index b5a9e31b..08e0d8bd 100644
--- a/theories/logrel/F_mu_ref_conc/binary/rules.v
+++ b/theories/logrel/F_mu_ref_conc/binary/rules.v
@@ -235,8 +235,8 @@ Section cfg.
rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose".
iDestruct "Hrtc" as %Hrtc.
- iDestruct (own_valid_2 with "Hown Hj")
- as %[[Htpj%tpool_singleton_included' _]%prod_included ?]
+ iCombine "Hown Hj" gives
+ %[[Htpj%tpool_singleton_included' _]%prod_included ?]
%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
@@ -284,9 +284,9 @@ Section cfg.
rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
destruct (exist_fresh (dom σ)) as [l Hl%not_elem_of_dom].
- iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included ?]
- %auth_both_valid_discrete.
+ iCombine "Hown Hj"
+ gives %[[?%tpool_singleton_included' _]%prod_included ?]
+ %auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
singleton_local_update, (exclusive_local_update _ (Excl (fill K (Loc l)))). }
@@ -308,10 +308,10 @@ Section cfg.
iIntros (?) "(#Hinv & Hj & Hl)". iDestruct "Hinv" as (ρ) "Hinv".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
- iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
- iDestruct (own_valid_2 with "Hown Hl")
- as %[[? ?%heap_singleton_included]%prod_included ?]%auth_both_valid_discrete.
+ iCombine "Hown Hj"
+ gives %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
+ iCombine "Hown Hl"
+ gives %[[? ?%heap_singleton_included]%prod_included ?]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (of_val v)))). }
@@ -329,12 +329,12 @@ Section cfg.
iIntros (??) "(#Hinv & Hj & Hl)". iDestruct "Hinv" as (ρ) "Hinv".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
- iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]
+ iCombine "Hown Hj"
+ gives %[[?%tpool_singleton_included' _]
%prod_included _]%auth_both_valid_discrete.
- iDestruct (own_valid_2 with "Hown Hl")
- as %[[_ Hl%heap_singleton_included]%prod_included _]
- %auth_both_valid_discrete.
+ iCombine "Hown Hl"
+ gives %[[_ Hl%heap_singleton_included]%prod_included _]
+ %auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K Unit))). }
@@ -356,11 +356,11 @@ Section cfg.
iIntros (????) "(#Hinv & Hj & Hl)". iDestruct "Hinv" as (ρ) "Hinv".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
- iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included ?]
- %auth_both_valid_discrete.
- iDestruct (own_valid_2 with "Hown Hl")
- as %[[_ ?%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
+ iCombine "Hown Hj"
+ gives %[[?%tpool_singleton_included' _]%prod_included ?]
+ %auth_both_valid_discrete.
+ iCombine "Hown Hl"
+ gives %[[_ ?%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (#♭ false)))). }
@@ -378,12 +378,12 @@ Section cfg.
iIntros (????) "(#Hinv & Hj & Hl)"; subst. iDestruct "Hinv" as (ρ) "Hinv".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
- iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included _]
- %auth_both_valid_discrete.
- iDestruct (own_valid_2 with "Hown Hl")
- as %[[_ Hl%heap_singleton_included]%prod_included _]
- %auth_both_valid_discrete.
+ iCombine "Hown Hj"
+ gives %[[?%tpool_singleton_included' _]%prod_included _]
+ %auth_both_valid_discrete.
+ iCombine "Hown Hl"
+ gives %[[_ Hl%heap_singleton_included]%prod_included _]
+ %auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (#♭ true)))). }
@@ -405,12 +405,12 @@ Section cfg.
iIntros (??) "(#Hinv & Hj & Hl)"; subst. iDestruct "Hinv" as (ρ) "Hinv".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
- iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _]%prod_included _]
- %auth_both_valid_discrete.
- iDestruct (own_valid_2 with "Hown Hl")
- as %[[_ Hl%heap_singleton_included]%prod_included _]
- %auth_both_valid_discrete.
+ iCombine "Hown Hj"
+ gives %[[?%tpool_singleton_included' _]%prod_included _]
+ %auth_both_valid_discrete.
+ iCombine "Hown Hl"
+ gives %[[_ Hl%heap_singleton_included]%prod_included _]
+ %auth_both_valid_discrete.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (#n m)))). }
@@ -508,9 +508,9 @@ Section cfg.
iIntros (?) "[#Hinv Hj]". iDestruct "Hinv" as (ρ) "Hinv".
rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
- iDestruct (own_valid_2 with "Hown Hj")
- as %[[?%tpool_singleton_included' _] %prod_included ?]
- %auth_both_valid_discrete.
+ iCombine "Hown Hj"
+ gives %[[?%tpool_singleton_included' _] %prod_included ?]
+ %auth_both_valid_discrete.
assert (j < length tp) by eauto using lookup_lt_Some.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
--
GitLab