Bump Iris (beautify code for `iCombine .. gives`).

cca1fa39 · Robbert Krebbers · 5eb90084 · cca1fa39 · cca1fa39 · cca1fa39
Commit cca1fa39 authored 2 years ago by Robbert Krebbers
--- a/coq-simuliris.opam
+++ b/coq-simuliris.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/simuliris.git"
 synopsis: "Local Simulation proofs, the Iris style"

 depends: [
-  "coq-iris" { (= "dev.2022-11-29.1.c44ce4c9") | (= "dev") }
+  "coq-iris" { (= "dev.2023-03-09.0.f91e8eab") | (= "dev") }
  "coq-equations" { (= "1.2.4+8.12") | (= "1.3+8.14") | (= "1.3+8.15") | (= "1.3+8.16") }
 ]


--- a/theories/base_logic/gen_sim_heap.v
+++ b/theories/base_logic/gen_sim_heap.v
@@ -108,6 +108,12 @@ Section gen_heap.
  Proof. split; [done|]. apply _. Qed.
  Global Instance mapsto_persistent l v : Persistent (l ↦□ v).
  Proof. rewrite mapsto_eq. apply _. Qed.
+  Global Instance mapsto_combine_sep_gives l dq1 dq2 v1 v2 :
+    CombineSepGives (l ↦{dq1} v1) (l ↦{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝ | 20.
+  Proof.
+    rewrite /CombineSepGives mapsto_eq. iIntros "[H1 H2]".
+    iCombine "H1 H2" gives %[??]%gmap_view_frag_op_valid_L; auto.
+  Qed.

  Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝%Qp.
  Proof.
@@ -115,18 +121,10 @@ Section gen_heap.
    iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done.
  Qed.
  Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
-  Proof.
-    rewrite mapsto_eq. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
-    auto.
-  Qed.
+  Proof. iIntros "H1 H2". by iCombine "H1 H2" gives %[]. Qed.
  (** Almost all the time, this is all you really need. *)
  Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
-  Proof.
-    iIntros "H1 H2".
-    iDestruct (mapsto_valid_2 with "H1 H2") as %[_ ?].
-    done.
-  Qed.
+  Proof. iIntros "H1 H2". by iCombine "H1 H2" gives %[]. Qed.

  Lemma mapsto_combine l dq1 dq2 v1 v2 :
    l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
@@ -141,7 +139,7 @@ Section gen_heap.
    ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
  Proof.
    iIntros (?) "Hl1 Hl2"; iIntros (->).
-    by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
+    by iCombine "Hl1 Hl2" gives %[??].
  Qed.
  Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
  Proof. apply mapsto_frac_ne. intros ?%exclusive_l; [done|apply _]. Qed.
@@ -171,8 +169,8 @@ Section gen_heap.
  Proof.
    rewrite meta_token_eq /meta_token_def.
    iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
-    iDestruct (own_valid_2 with "Hγm1 Hγm2") as %[_ ->]%gmap_view_frag_op_valid_L.
-    iDestruct (own_valid_2 with "Hm1 Hm2") as %?%reservation_map_token_valid_op.
+    iCombine "Hγm1 Hγm2" gives %[_ ->]%gmap_view_frag_op_valid_L.
+    iCombine "Hm1 Hm2" gives %?%reservation_map_token_valid_op.
    iExists γm2. iFrame "Hγm2". rewrite reservation_map_token_union //. by iSplitL "Hm1".
  Qed.
  Lemma meta_token_union l E1 E2 :
@@ -194,8 +192,8 @@ Section gen_heap.
  Proof.
    rewrite meta_eq /meta_def.
    iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
-    iDestruct (own_valid_2 with "Hγm1 Hγm2") as %[_ ->]%gmap_view_frag_op_valid_L.
-    iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
+    iCombine "Hγm1 Hγm2" gives %[_ ->]%gmap_view_frag_op_valid_L.
+    iCombine "Hm1 Hm2" gives %Hγ; iPureIntro.
    move: Hγ. rewrite -reservation_map_data_op reservation_map_data_valid.
    move=> /to_agree_op_inv_L. naive_solver.
  Qed.
@@ -248,7 +246,7 @@ Section gen_heap.
  Proof.
    iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
    rewrite /gen_heap_interp mapsto_eq.
-    by iDestruct (own_valid_2 with "Hσ Hl") as %[??]%gmap_view_both_valid_L.
+    by iCombine "Hσ Hl" gives %[??]%gmap_view_both_valid_L.
  Qed.

  Lemma gen_heap_update σ l v1 v2 :
@@ -256,7 +254,7 @@ Section gen_heap.
  Proof.
    iDestruct 1 as (m Hσm) "[Hσ Hm]".
    iIntros "Hl". rewrite /gen_heap_interp mapsto_eq /mapsto_def.
-    iDestruct (own_valid_2 with "Hσ Hl") as %[_ Hl]%gmap_view_both_valid_L.
+    iCombine "Hσ Hl" gives %[_ Hl]%gmap_view_both_valid_L.
    iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
    { eapply gmap_view_update. }
    iModIntro. iFrame "Hl". iExists m. iFrame.

--- a/theories/base_logic/gen_sim_prog.v
+++ b/theories/base_logic/gen_sim_prog.v
@@ -67,7 +67,7 @@ Section gen_prog.
  Lemma has_prog_agree p1 p2 : has_prog p1 -∗ has_prog p2 -∗ ⌜p1 = p2⌝.
  Proof.
    iIntros "Hp1 Hp2".
-    iDestruct (own_valid_2 with "Hp1 Hp2") as %Hval.
+    iCombine "Hp1 Hp2" gives %Hval.
    setoid_rewrite to_agree_op_valid_L in Hval. done.
  Qed.


--- a/theories/simulang/logical_heap.v
+++ b/theories/simulang/logical_heap.v
@@ -155,7 +155,7 @@ Section globals.
    heap_globals γ gs1 -∗ heap_globals γ gs2 -∗ ⌜gs1 = gs2⌝.
  Proof.
    rewrite heap_globals_eq. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %Hvalid.
+    iCombine "H1 H2" gives %Hvalid.
    move: Hvalid => /to_agree_op_valid. by fold_leibniz.
  Qed.

@@ -350,7 +350,7 @@ Section heap.
  Proof.
    rewrite heap_block_size_eq.
    iIntros (?) "(%&->&Hl1) (%&->&Hl2)"; simplify_eq/=.
-    by iDestruct (ghost_map_elem_valid_2 with "Hl1 Hl2") as %[? ?].
+    by iCombine "Hl1 Hl2" gives %[? ?].
  Qed.

  Lemma heap_block_size_rel_stable σ h l p :
@@ -567,7 +567,7 @@ Section heap.
        h !! 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.
@@ -586,7 +586,7 @@ Section heap.
    ⌜h !! 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.

--- a/theories/stacked_borrows/tkmap_view.v
+++ b/theories/stacked_borrows/tkmap_view.v
@@ -618,26 +618,25 @@ Section lemmas.
    - rewrite big_opM_own //. iIntros "?". done.
  Qed.

-  Lemma tkmap_elem_valid_2 k γ tk1 tk2 v1 v2 :
-    k ↪[γ]{tk1} v1 -∗ k ↪[γ]{tk2} v2 -∗ ⌜✓ (to_tgkR tk1 ⋅ to_tgkR tk2) ∧ v1 = v2⌝.
+  Global Instance tkmap_elem_combine_sep_gives k γ tk1 tk2 v1 v2 :
+    CombineSepGives (k ↪[γ]{tk1} v1) (k ↪[γ]{tk2} v2)
+      ⌜✓ (to_tgkR tk1 ⋅ to_tgkR tk2) ∧ v1 = v2⌝.
  Proof.
-    unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %?%tkmap_view_frag_op_valid_L.
-    done.
+    rewrite /CombineSepGives. unseal. iIntros "[H1 H2]".
+    iCombine "H1 H2" gives %[??]%tkmap_view_frag_op_valid_L; auto.
  Qed.
+  Lemma tkmap_elem_valid_2 k γ tk1 tk2 v1 v2 :
+    k ↪[γ]{tk1} v1 -∗ k ↪[γ]{tk2} v2 -∗ ⌜✓ (to_tgkR tk1 ⋅ to_tgkR tk2) ∧ v1 = v2⌝.
+  Proof. iIntros "Helem1 Helem2". by iCombine "Helem1 Helem2" gives %[]. Qed.
  Lemma tkmap_elem_agree k γ tk1 tk2 v1 v2 :
    k ↪[γ]{tk1} v1 -∗ k ↪[γ]{tk2} v2 -∗ ⌜v1 = v2⌝.
-  Proof.
-    iIntros "Helem1 Helem2".
-    iDestruct (tkmap_elem_valid_2 with "Helem1 Helem2") as %[_ ?].
-    done.
-  Qed.
+  Proof. iIntros "Helem1 Helem2". by iCombine "Helem1 Helem2" gives %[_ ?]. Qed.

  Lemma tkmap_elem_tk_ne γ k1 k2 tk1 tk2 v1 v2 :
    ¬ ✓ (to_tgkR tk1 ⋅ to_tgkR tk2) → k1 ↪[γ]{tk1} v1 -∗ k2 ↪[γ]{tk2} v2 -∗ ⌜k1 ≠ k2⌝.
  Proof.
    iIntros (?) "H1 H2"; iIntros (->).
-    by iDestruct (tkmap_elem_valid_2 with "H1 H2") as %[??].
+    by iCombine "H1 H2" gives %[??].
  Qed.
  Lemma tkmap_elem_ne γ k1 k2 tk2 v1 v2 :
    k1 ↪[γ]{tk_unq} v1 -∗ k2 ↪[γ]{tk2} v2 -∗ ⌜k1 ≠ k2⌝.
@@ -699,27 +698,26 @@ Section lemmas.
    iDestruct (own_valid with "Hauth") as %?%tkmap_view_auth_frac_valid.
    done.
  Qed.
-  Lemma tkmap_auth_valid_2 γ q1 q2 m1 m2 :
-    tkmap_auth γ q1 m1 -∗ tkmap_auth γ q2 m2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ m1 = m2⌝.
+  Global Instance tkmap_auth_combine_sep_gives γ q1 q2 m1 m2 :
+    CombineSepGives (tkmap_auth γ q1 m1) (tkmap_auth γ q2 m2)
+      ⌜(q1 + q2 ≤ 1)%Qp ∧ m1 = m2⌝.
  Proof.
-    unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[??]%tkmap_view_auth_frac_op_valid_L.
-    done.
+    rewrite /CombineSepGives. unseal. iIntros "[H1 H2]".
+    iCombine "H1 H2" gives %[??]%tkmap_view_auth_frac_op_valid_L; auto.
  Qed.
+  Lemma tkmap_auth_valid_2 γ q1 q2 m1 m2 :
+    tkmap_auth γ q1 m1 -∗ tkmap_auth γ q2 m2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ m1 = m2⌝.
+  Proof. iIntros "H1 H2". by iCombine "H1 H2" gives %[??]. Qed.
  Lemma tkmap_auth_agree γ q1 q2 m1 m2 :
    tkmap_auth γ q1 m1 -∗ tkmap_auth γ q2 m2 -∗ ⌜m1 = m2⌝.
-  Proof.
-    iIntros "H1 H2".
-    iDestruct (tkmap_auth_valid_2 with "H1 H2") as %[_ ?].
-    done.
-  Qed.
+  Proof. iIntros "H1 H2". by iCombine "H1 H2" gives %[??]. Qed.

  (** * Lemmas about the interaction of [tkmap_auth] with the elements *)
  Lemma tkmap_lookup {γ q m k tk v} :
    tkmap_auth γ q m -∗ k ↪[γ]{tk} v -∗ ⌜m !! k = Some (tk, v)⌝.
  Proof.
    unseal. iIntros "Hauth Hel".
-    iDestruct (own_valid_2 with "Hauth Hel") as %[??]%tkmap_view_both_frac_valid_L.
+    iCombine "Hauth Hel" gives %[??]%tkmap_view_both_frac_valid_L.
    eauto.
  Qed.