From 87916dfb1611d6d928c15552e330972b0e1e65c0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2023 16:15:07 +0100
Subject: [PATCH] More use of `iDestruct .. gives`.

---
 theories/examples/symbol.v      | 11 +++---
 theories/examples/ticket_lock.v |  4 +-
 theories/examples/various.v     |  4 +-
 theories/logic/spec_rules.v     | 68 ++++++++++++++++-----------------
 4 files changed, 42 insertions(+), 45 deletions(-)

diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 1be8990..22f7b55 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -63,8 +63,7 @@ Section rules.
     ⌜m ≤ n⌝.
   Proof.
     iIntros "Hn Hm".
-    by iDestruct (own_valid_2 with "Hn Hm")
-      as %[?%max_nat_included _]%auth_both_valid_discrete.
+    by iCombine "Hn Hm" gives %[?%max_nat_included _]%auth_both_valid_discrete.
   Qed.
 
   Lemma same_size (n m : nat) :
@@ -152,8 +151,8 @@ Section proof.
         "(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & #Hls)" "Hcl".
     iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
     rel_load_r. rel_pure_r. rel_pure_r.
-    iDestruct (own_valid_2 with "Ha Hn")
-      as %[?%max_nat_included _]%auth_both_valid_discrete; simpl in *.
+    iCombine "Ha Hn"
+      gives %[?%max_nat_included _]%auth_both_valid_discrete; simpl in *.
     rel_op_l. rel_op_r. rewrite bool_decide_true; last lia.
     rel_pure_r. rel_load_r. rel_op_r.
     iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
@@ -189,8 +188,8 @@ Section proof.
     rel_load_l_atomic.
     iInv sizeN as (m ls) "(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & Hls)" "Hcl".
     iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
-    iDestruct (own_valid_2 with "Ha Hn")
-      as %[?%max_nat_included _]%auth_both_valid_discrete; simpl in *.
+    iCombine "Ha Hn"
+      gives %[?%max_nat_included _]%auth_both_valid_discrete; simpl in *.
     iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
     { iNext. iExists _,_. by iFrame. }
     clear ls. repeat rel_pure_l.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index ae23fda..b8949c2 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -45,8 +45,8 @@ Section refinement.
 
   Lemma ticket_nondup γ n : ticket γ n -∗ ticket γ n -∗ False.
   Proof.
-    iIntros "Ht1 Ht2". iDestruct (own_valid_2 with "Ht1 Ht2")
-      as %?%auth_frag_op_valid_1%gset_disj_valid_op.
+    iIntros "Ht1 Ht2". iCombine "Ht1 Ht2"
+      gives %?%auth_frag_op_valid_1%gset_disj_valid_op.
     set_solver.
   Qed.
 
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 2c79266..b35c5d8 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -55,9 +55,7 @@ Section proofs.
   Lemma shot_not_pending γ `{oneshotG Σ} :
     shot γ -∗ pending γ -∗ False.
   Proof.
-    iIntros "Hs Hp".
-    iPoseProof (own_valid_2 with "Hs Hp") as "H".
-    iDestruct "H" as %[].
+    iIntros "Hs Hp". iCombine "Hs Hp" gives %[].
   Qed.
 
   Lemma refinement2 `{oneshotG Σ} :
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 09c1d8f..3834f8a 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -51,8 +51,8 @@ Section rules.
     iDestruct "Hspec" as (ρ) "Hspec".
     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 ?]%auth_both_valid_discrete.
+    iCombine "Hown Hj"
+      gives %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { eapply auth_update, prod_local_update_1.
       by eapply (singleton_local_update _ j (Excl (fill K e))),
@@ -96,8 +96,8 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
     iDestruct "Hinv" as (ρ) "Hinv".
     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.
     destruct (exist_fresh (used_proph_id σ)) as [p Hp].
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1,
@@ -117,8 +117,8 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
     iDestruct "Hinv" as (ρ) "Hinv".
     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.
     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 #()))). }
@@ -139,8 +139,8 @@ Section rules.
     iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     destruct (exist_fresh (dom (heap σ))) 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 (#l)%E))). }
@@ -167,10 +167,10 @@ Section rules.
     iDestruct "Hinv" as (ρ) "Hinv".
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
     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)))). }
@@ -191,10 +191,10 @@ Section rules.
     iDestruct "Hinv" as (ρ) "Hinv".
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
     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 #()))). }
@@ -222,10 +222,10 @@ Section rules.
     iDestruct "Hinv" as (ρ) "Hinv".
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
     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 (of_val v')))). }
@@ -256,10 +256,10 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iDestruct "Hinv" as (ρ) "Hinv".
     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)%V))). }
@@ -283,10 +283,10 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iDestruct "Hinv" as (ρ) "Hinv".
     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)%V))). }
@@ -314,10 +314,10 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iDestruct "Hinv" as (ρ) "Hinv".
     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 (# i1)))). }
@@ -344,8 +344,8 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
     iDestruct "Hspec" as (ρ) "Hspec".
     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