From ee751d70e99c9875ba9484f3c9432e6b3f698ddc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2023 15:37:03 +0100
Subject: [PATCH] Bump Iris (beautify code for `iCombine .. gives`).
---
coq-actris.opam | 2 +-
theories/channel/proto.v | 4 ++--
.../logrel/examples/compute_client_list.v | 4 ++--
theories/logrel/examples/par_recv.v | 20 +++++++++----------
theories/utils/contribution.v | 2 +-
5 files changed, 16 insertions(+), 16 deletions(-)
diff --git a/coq-actris.opam b/coq-actris.opam
index 207918c..d72f892 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
depends: [
- "coq-iris-heap-lang" { (= "dev.2023-03-07.1.7e127436") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2023-03-09.0.f91e8eab") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index ff04b17..d001033 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -1032,8 +1032,8 @@ Section proto.
Lemma iProto_own_auth_agree γ s p p' :
iProto_own_auth γ s p -∗ iProto_own_frag γ s p' -∗ ▷ (p ≡ p').
Proof.
- iIntros "H◠H◯". iDestruct (own_valid_2 with "H◠H◯") as "H✓".
- iDestruct (excl_auth_agreeI with "H✓") as "H✓".
+ iIntros "H◠H◯". iCombine "H◠H◯" gives "H✓".
+ iDestruct (excl_auth_agreeI with "H✓") as "{H✓} H✓".
iApply (later_equivI_1 with "H✓").
Qed.
diff --git a/theories/logrel/examples/compute_client_list.v b/theories/logrel/examples/compute_client_list.v
index 97679f3..6f9494b 100644
--- a/theories/logrel/examples/compute_client_list.v
+++ b/theories/logrel/examples/compute_client_list.v
@@ -172,7 +172,7 @@ Section compute_example.
wp_smart_apply (acquire_spec with "Hlk").
iIntros "[Hlocked HI]".
iDestruct "HI" as (n [ | ]) "(Hf' & Hcounter & Hc)"; last first.
- { by iDestruct (own_valid_2 with "Hf Hf'") as %[]. }
+ { by iCombine "Hf Hf'" gives %[]. }
iDestruct (iProto_mapsto_le with "Hc []") as "Hc".
{ iApply iProto_le_trans.
{ iApply iProto_le_app; [ iApply iProto_le_refl | ].
@@ -192,7 +192,7 @@ Section compute_example.
wp_smart_apply (acquire_spec with "Hlk").
iIntros "[Hlocked HI]".
iDestruct "HI" as (n [ | ]) "(Hf' & Hcounter & Hc)"; last first.
- { by iDestruct (own_valid_2 with "Hf Hf'") as %[]. }
+ { by iCombine "Hf Hf'" gives %[]. }
iDestruct (iProto_mapsto_le with "Hc []") as "Hc".
{ iApply iProto_le_trans.
{ iApply iProto_le_app; [ iApply iProto_le_refl | ].
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index 81e56a4..5b72a10 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -77,7 +77,7 @@ Section double.
iIntros "_". wp_pures.
eauto.
+ iDestruct "Hc" as "[Hcredit2 Hc]".
- by iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as %[].
+ by iCombine "Hcredit1 Hcredit2" gives %[].
- (* Acquire lock *)
wp_smart_apply (acquire_spec with "Hlock").
iIntros "[Hlocked Hc]". wp_pures.
@@ -95,7 +95,7 @@ Section double.
iIntros "_". wp_pures.
eauto.
+ iDestruct "Hc" as "[Hcredit1 Hc]".
- by iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as %[].
+ by iCombine "Hcredit1 Hcredit2" gives %[].
- iIntros (?? [[x1 ->] [x2 ->]]) "!>". by iApply "HΦ".
Qed.
@@ -165,7 +165,7 @@ Section double_fc.
{ iRight. iLeft. iExists true, v. iFrame. }
iIntros "_". wp_pures. iLeft. by iFrame.
+ iDestruct "Hc" as ([] v) "[Hγ2 Hc]".
- { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. }
+ { by iCombine "Hγ1 Hγ2" gives %[]. }
wp_recv (v') as "HP". wp_pures.
iMod (own_update _ _ ((1/4 ⋅ 3/4), to_agree (Some v'))%Qp with "Hγ1")
as "[Hγ1a Hγ1b]"; [by apply cmra_update_exclusive|].
@@ -175,7 +175,7 @@ Section double_fc.
{ do 2 iRight. iExists v', v. iFrame. }
iIntros "_". wp_pures. iRight. iExists v. by iFrame.
+ iDestruct "Hc" as (v v') "[Hγ1' _]".
- by iDestruct (own_valid_2 with "Hγ1 Hγ1'") as %[].
+ by iCombine "Hγ1 Hγ1'" gives %[].
- (* Acquire lock *)
wp_smart_apply (acquire_spec with "Hlock").
iIntros "[Hlocked Hc]". wp_pures.
@@ -187,7 +187,7 @@ Section double_fc.
{ iRight. iLeft. iExists false, v. iFrame. }
iIntros "_". wp_pures. iLeft. by iFrame.
+ iDestruct "Hc" as ([] v) "[Hγ1 Hc]"; last first.
- { by iDestruct (own_valid_2 with "Hγ1 Hγ2") as %[]. }
+ { by iCombine "Hγ1 Hγ2" gives %[]. }
wp_recv (v') as "HP". wp_pures.
iMod (own_update _ _ ((1/4 ⋅ 3/4), to_agree (Some v'))%Qp with "Hγ2")
as "[Hγ2a Hγ2b]"; [by apply cmra_update_exclusive|].
@@ -197,17 +197,17 @@ Section double_fc.
{ do 2 iRight. iExists v, v'. iFrame. }
iIntros "_". wp_pures. iRight. iExists v. by iFrame.
+ iDestruct "Hc" as (v v') "(_ & Hγ2' & _)".
- by iDestruct (own_valid_2 with "Hγ2 Hγ2'") as %[].
+ by iCombine "Hγ2 Hγ2'" gives %[].
- iIntros (v1 v2) "[[[H1 Hγ]|H1] [[H2 Hγ']|H2]] !>".
- + by iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
+ + by iCombine "Hγ Hγ'" gives %[].
+ iDestruct "H2" as (v2') "(_&H1'&HP)".
- iDestruct (own_valid_2 with "H1 H1'") as %[_ [=->]%to_agree_op_inv_L].
+ iCombine "H1 H1'" gives %[_ [=->]%to_agree_op_inv_L].
iApply "HΦ"; auto.
+ iDestruct "H1" as (v1') "(_&H2'&HP)".
- iDestruct (own_valid_2 with "H2 H2'") as %[_ [=->]%to_agree_op_inv_L].
+ iCombine "H2 H2'" gives %[_ [=->]%to_agree_op_inv_L].
iApply "HΦ"; auto.
+ iDestruct "H1" as (v1') "[H1 _]"; iDestruct "H2" as (v2') "(_&H2&_)".
- by iDestruct (own_valid_2 with "H1 H2") as %[].
+ by iCombine "H1 H2" gives %[].
Qed.
Lemma prog_typed_fc :
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index cb78e4f..2143b9d 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -87,7 +87,7 @@ Section contribution.
Proof.
rewrite /server /client. iIntros "Hs Hc". case_decide; subst.
- iDestruct "Hs" as "(_ & _ & Hc')".
- by iDestruct (own_valid_2 with "Hc Hc'") as %?%auth_frag_op_valid_1.
+ by iCombine "Hc Hc'" gives %?%auth_frag_op_valid_1.
- iDestruct (own_valid_2 with "Hs Hc")
as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete.
{ setoid_subst. by destruct n. }
--
GitLab