From 8a65d1b4f729cd35f20f22f8d106448dd6622f9c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2023 15:36:45 +0100
Subject: [PATCH] Bump Iris (beautify code for `iCombine .. gives`).
---
coq-reloc.opam | 2 +-
theories/examples/folly_queue/refinement.v | 6 +++---
theories/examples/folly_queue/turnSequencer.v | 8 ++++----
theories/examples/namegen.v | 2 +-
theories/examples/red_blue_flag.v | 6 +++---
theories/examples/stack_helping/helping_wrapper.v | 2 +-
theories/examples/stack_helping/offers.v | 4 ++--
theories/examples/stack_helping/stack.v | 2 +-
theories/examples/various.v | 6 +++---
theories/experimental/hocap/counter.v | 2 +-
theories/lib/lock.v | 2 +-
theories/logic/adequacy.v | 2 +-
theories/logic/compatibility.v | 12 ++++++------
theories/logic/model.v | 5 ++---
theories/logic/spec_ra.v | 8 ++++++++
theories/prelude/bijections.v | 4 ++--
theories/typing/interp.v | 4 ++--
17 files changed, 42 insertions(+), 35 deletions(-)
diff --git a/coq-reloc.opam b/coq-reloc.opam
index 656929a..4ad0726 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
depends: [
- "coq-iris-heap-lang" { (= "dev.2022-11-29.1.c44ce4c9") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2023-03-09.0.f91e8eab") | (= "dev") }
"coq-autosubst" { = "dev" }
]
diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index 16e5107..5d5ad0b 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/theories/examples/folly_queue/refinement.v
@@ -134,7 +134,7 @@ Section queue_refinement.
Proof.
rewrite /ghost_list /ghost_list_mapsto /list_idx_to_map.
iIntros "Ha Hb".
- iDestruct (own_valid_2 with "Ha Hb") as %[Hincl _]%auth_both_valid_discrete.
+ iCombine "Ha Hb" gives %[Hincl _]%auth_both_valid_discrete.
apply dom_included in Hincl.
rewrite dom_singleton_L in Hincl.
rewrite dom_make_map in Hincl.
@@ -214,7 +214,7 @@ Section queue_refinement.
⌜popTicket ∈ set_seq (C:=gset nat) 0 pushTicketâŒ.
Proof.
iIntros (Hsub) "Ha Hf".
- iDestruct (own_valid_2 with "Ha Hf") as %[H%dom_included _]%auth_both_valid_discrete.
+ iCombine "Ha Hf" gives %[H%dom_included _]%auth_both_valid_discrete.
rewrite dom_make_map in H.
rewrite Hsub in H.
rewrite dom_singleton_L in H.
@@ -893,7 +893,7 @@ Section queue_refinement.
iDestruct (ghost_list_le with "Hlist Hag") as %popLePush.
rewrite (big_sepS_delete _ _ popTicket). 2: { rewrite elem_of_set_seq. lia. }
iDestruct "Hpush" as "[[>Htok'|Hright] Hpush]".
- { by iDestruct (own_valid_2 with "Htok Htok'") as %Hv%set_singleton_invalid. }
+ { by iCombine "Htok Htok'" gives %Hv%set_singleton_invalid. }
iDestruct "Hright" as (id' v' vâ‚›) "(>#Hdec' & Hright & #Hrel & >#Hag')".
iAssert (push_i A γl γt γm popTicket) with "[Htok]" as "Hi".
{ iLeft. iFrame. }
diff --git a/theories/examples/folly_queue/turnSequencer.v b/theories/examples/folly_queue/turnSequencer.v
index 060ad28..d59d6e3 100644
--- a/theories/examples/folly_queue/turnSequencer.v
+++ b/theories/examples/folly_queue/turnSequencer.v
@@ -87,10 +87,10 @@ Section spec.
iInv N as (m) "(>â„“Pts & Hturns & Hdisj)" "Hcl".
wp_load.
destruct (lt_eq_lt_dec n m) as [[Hle|<-]|Hho].
- - iDestruct (own_valid_2 with "Hturns Ht") as %HI%set_upto_singleton_valid.
+ - iCombine "Hturns Ht" gives %HI%set_upto_singleton_valid.
exfalso. lia.
- iDestruct "Hdisj" as "[[Hr â„“Pts'] | Ht']"; last first.
- { by iDestruct (own_valid_2 with "Ht Ht'") as %?%set_singleton_invalid. }
+ { by iCombine "Ht Ht'" gives %?%set_singleton_invalid. }
iMod ("Hcl" with "[Ht â„“Pts Hturns]") as "_".
{ iNext. iExists _. iFrame. }
iModIntro. wp_pures.
@@ -122,7 +122,7 @@ Section spec.
iDestruct "Hc'" as (â„“1' ?) "Hc'".
simplify_eq/=.
iCombine "â„“Pts Hc'" as "â„“Pts".
- iDestruct (mapsto_valid_2 with "â„“Pts Hc") as %[?%Qp.not_add_le_l _].
+ iCombine "â„“Pts Hc" gives %[?%Qp.not_add_le_l _].
done. }
wp_load.
iDestruct (mapsto_agree with "â„“Pts Hc") as %[= Heq].
@@ -136,7 +136,7 @@ Section spec.
iDestruct "Hc'" as (â„“1' ?) "Hc'".
simplify_eq/=.
iCombine "â„“Pts Hc'" as "â„“Pts".
- iDestruct (mapsto_valid_2 with "â„“Pts Hc") as %[?%Qp.not_add_le_l _].
+ iCombine "â„“Pts Hc" gives %[?%Qp.not_add_le_l _].
done. }
iDestruct (mapsto_combine with "â„“Pts Hc") as "[â„“Pts %Heq]".
simplify_eq/=.
diff --git a/theories/examples/namegen.v b/theories/examples/namegen.v
index 890d79c..2bf4979 100644
--- a/theories/examples/namegen.v
+++ b/theories/examples/namegen.v
@@ -64,7 +64,7 @@ Section namegen_refinement.
{ iIntros (Hy). destruct Hy as [y Hy].
rewrite (big_sepS_elem_of _ L (l',y) Hy).
iDestruct "HL" as "[Hl _]".
- iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %[Hfoo _].
+ iCombine "Hl Hl'" gives %[Hfoo _].
compute in Hfoo. eauto. }
iAssert (⌜(∃ x, (x, S n) ∈ L) → FalseâŒ)%I with "[HL]" as %Hc.
{ iIntros (Hx). destruct Hx as [x Hy].
diff --git a/theories/examples/red_blue_flag.v b/theories/examples/red_blue_flag.v
index 6828260..4e2731f 100644
--- a/theories/examples/red_blue_flag.v
+++ b/theories/examples/red_blue_flag.v
@@ -89,7 +89,7 @@ Section offer_theory.
Qed.
Lemma no_offer_exclusive γ q k : no_offer γ -∗ own_offer γ q k -∗ False.
- Proof. iIntros "O P". by iDestruct (own_valid_2 with "O P") as %?. Qed.
+ Proof. iIntros "O P". by iCombine "O P" gives %?. Qed.
Lemma no_offer_to_offer γ k : no_offer γ ==∗ own_offer γ 1 k.
Proof.
@@ -109,7 +109,7 @@ Section offer_theory.
own_offer γ q k -∗ own_offer γ q' k' -∗ ⌜k = k'âŒ.
Proof.
iIntros "O P".
- iDestruct (own_valid_2 with "O P") as %[_ ?%to_agree_op_inv]%pair_valid.
+ iCombine "O P" gives %[_ ?%to_agree_op_inv]%pair_valid.
by unfold_leibniz.
Qed.
@@ -399,7 +399,7 @@ Section proofs.
iDestruct "Hdisj" as (?) "[[% _] | (% & Hdisj)]"; first by subst.
iDestruct "Hdisj" as "[[Hoff' Hj] | Hoff']".
2: {
- iDestruct (own_valid_2 with "Htok Hoff'") as %Hv.
+ iCombine "Htok Hoff'" gives %Hv.
by apply Qp.not_add_le_l in Hv. }
iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
iDestruct (offer_token_split with "Htok") as "[Htok Htok']".
diff --git a/theories/examples/stack_helping/helping_wrapper.v b/theories/examples/stack_helping/helping_wrapper.v
index 49d12cb..8e68dd4 100644
--- a/theories/examples/stack_helping/helping_wrapper.v
+++ b/theories/examples/stack_helping/helping_wrapper.v
@@ -103,7 +103,7 @@ Section offerReg_rules.
-∗ ⌜N !! o = Some (v, γ, k)âŒ.
Proof.
iIntros "HN Hfrag".
- iDestruct (own_valid_2 with "HN Hfrag") as %Hfoo.
+ iCombine "HN Hfrag" gives %Hfoo.
apply auth_both_valid_discrete in Hfoo.
simpl in Hfoo. destruct Hfoo as [Hfoo _].
iAssert (⌜✓ ((to_offer_reg N) !! o)âŒ)%I as %Hvalid.
diff --git a/theories/examples/stack_helping/offers.v b/theories/examples/stack_helping/offers.v
index a14a9af..b781946 100644
--- a/theories/examples/stack_helping/offers.v
+++ b/theories/examples/stack_helping/offers.v
@@ -24,7 +24,7 @@ Section rules.
Definition offer_token γ := own γ (Excl ()).
Lemma offer_token_exclusive γ : offer_token γ -∗ offer_token γ -∗ False.
- Proof. iIntros "H1 H2". iDestruct (own_valid_2 with "H1 H2") as %[]. Qed.
+ Proof. iIntros "H1 H2". iCombine "H1 H2" gives %[]. Qed.
(** The offer invariant *)
Definition is_offer γ (l : loc) (P Q : iProp Σ) :=
@@ -37,7 +37,7 @@ Section rules.
is_offer γ1 l P1 Q1 -∗ is_offer γ2 l P2 Q2 -∗ False.
Proof.
iDestruct 1 as (?) "[Hl1 _]". iDestruct 1 as (?) "[Hl2 _]".
- iDestruct (gen_heap.mapsto_valid_2 with "Hl1 Hl2") as %[? _]. contradiction.
+ iCombine "Hl1 Hl2" gives %[? _]. contradiction.
Qed.
Lemma make_is_offer γ l P Q : l ↦ #0 -∗ P -∗ is_offer γ l P Q.
diff --git a/theories/examples/stack_helping/stack.v b/theories/examples/stack_helping/stack.v
index a411022..bf2533f 100644
--- a/theories/examples/stack_helping/stack.v
+++ b/theories/examples/stack_helping/stack.v
@@ -129,7 +129,7 @@ Section offerReg_rules.
-∗ ⌜N !! o = Some (v, γ, k)âŒ.
Proof.
iIntros "HN Hfrag".
- iDestruct (own_valid_2 with "HN Hfrag") as %Hfoo.
+ iCombine "HN Hfrag" gives %Hfoo.
apply auth_both_valid_discrete in Hfoo.
simpl in Hfoo. destruct Hfoo as [Hfoo _].
iAssert (⌜✓ ((to_offer_reg N) !! o)âŒ)%I as %Hvalid.
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 9d9899d..2c79266 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -232,7 +232,7 @@ Section proofs.
iDestruct "Hx'" as "[Hx' Hx'1]".
iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | Hbb]".
{ iCombine "Hx Hx1" as "Hx".
- iDestruct (mapsto_valid_2 with "Hx Hx2") as %[Hfoo _]. exfalso.
+ iCombine "Hx Hx2" gives %[Hfoo _]. exfalso.
compute in Hfoo. eauto. }
iMod ("Hcl" with "[Hx Hx' Hbb]") as "_".
{ iNext. iExists (S n).
@@ -244,7 +244,7 @@ Section proofs.
iDestruct (mapsto_agree with "Hx Hx1") as %->.
iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | (Hb & Hb')]".
{ iCombine "Hx Hx1" as "Hx".
- iDestruct (mapsto_valid_2 with "Hx Hx2") as %[Hfoo _]. exfalso.
+ iCombine "Hx Hx2" gives %[Hfoo _]. exfalso.
compute in Hfoo. eauto. }
iModIntro; iExists _; iFrame; iNext. iIntros "Hb".
rel_store_r.
@@ -487,7 +487,7 @@ Section proofs.
Proof.
iIntros "#Hinv #Hg #Hf Hcl Hc1 Hc2 Ht".
iDestruct "Hc2" as "[(Hc2 & Hp) | (Hc2 & Hs & Ht'2 & %)]"; last first.
- { iDestruct (own_valid_2 with "Ht Ht'2") as %Hfoo.
+ { iCombine "Ht Ht'2" gives %Hfoo.
inversion Hfoo. }
iMod (shoot γ with "Hp") as "#Hs".
iMod ("Hcl" with "[-]") as "_".
diff --git a/theories/experimental/hocap/counter.v b/theories/experimental/hocap/counter.v
index 50635d1..27d42bb 100644
--- a/theories/experimental/hocap/counter.v
+++ b/theories/experimental/hocap/counter.v
@@ -66,7 +66,7 @@ Section cnt_model.
cnt γ q1 n -∗ cnt γ q2 m -∗ ⌜n = mâŒ.
Proof.
iIntros "H1 H2".
- iDestruct (own_valid_2 with "H1 H2") as %Hfoo.
+ iCombine "H1 H2" gives %Hfoo.
iPureIntro. revert Hfoo.
rewrite -auth_frag_op -Some_op -pair_op.
rewrite auth_frag_valid Some_valid.
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index 713ff94..43b32f5 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -33,7 +33,7 @@ Section lockG_rules.
Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
- Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
+ Proof. iIntros "H1 H2". by iCombine "H1 H2" gives %?. Qed.
Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
Proof. solve_proper. Qed.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index 0bddd07..41f9db9 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -51,7 +51,7 @@ Proof.
iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
iDestruct "Hj" as "[#Hs Hj]".
rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
- iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
+ iCombine "Hown Hj" gives %Hvalid.
move: Hvalid=> /auth_both_valid_discrete
[/prod_included [/tpool_singleton_included Hv2 _] _].
destruct tp as [|? tp']; simplify_eq/=.
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 2258c62..3942275 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -167,14 +167,14 @@ Section compatibility.
iDestruct "Hv" as (r1' r2' ? ?) "#Hv". simplify_eq/=.
destruct (decide ((l1, l2) = (r1, r2'))); simplify_eq/=.
{ iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(Hr1 & >Hr2 & Hrr)" "Hcl".
- iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hl2") as %[]. }
+ iExFalso. by iCombine "Hr2 Hl2" gives %[]. }
destruct (decide ((l1, l2) = (r1', r2'))); simplify_eq/=.
++ assert (r1' ≠r1) by naive_solver.
iInv (relocN.@"ref".@(r1, r2')) as (? ?) "(Hr1 & >Hr2 & Hrr)" "Hcl".
- iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hl2") as %[].
+ iExFalso. by iCombine "Hr2 Hl2" gives %[].
++ iInv (relocN.@"ref".@(r1, r2')) as (? ?) "(Hr1 & >Hr2 & Hrr)" "Hcl".
iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(Hr1' & >Hr2' & Hrr')" "Hcl'".
- iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hr2'") as %[].
+ iExFalso. by iCombine "Hr2 Hr2'" gives %[].
* rel_cmpxchg_fail_r.
iMod ("Hclose" with "[-]").
{ iNext; iExists _, _; by iFrame. }
@@ -185,13 +185,13 @@ Section compatibility.
iDestruct "Hv" as (r1' r2' ? ?) "#Hv". simplify_eq/=.
destruct (decide ((l1, l2) = (r1', r2'))); simplify_eq/=.
{ iInv (relocN.@"ref".@(r1', r2)) as (? ?) "(>Hr1 & >Hr2 & Hrr)" "Hcl".
- iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hl1") as %[]. }
+ iExFalso. by iCombine "Hr1 Hl1" gives %[]. }
destruct (decide ((l1, l2) = (r1', r2))); simplify_eq/=.
{ iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(>Hr1 & >Hr2 & Hrr)" "Hcl".
- iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hl1") as %[]. }
+ iExFalso. by iCombine "Hr1 Hl1" gives %[]. }
iInv (relocN.@"ref".@(r1', r2)) as (? ?) "(>Hr1 & >Hr2 & Hrr)" "Hcl".
iInv (relocN.@"ref".@(r1', r2')) as (? ?) "(>Hr1' & >Hr2' & Hrr')" "Hcl'".
- iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hr1'") as %[].
+ iExFalso. by iCombine "Hr1 Hr1'" gives %[].
Qed.
End compatibility.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 0dac2d5..6e94adf 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -196,7 +196,7 @@ Section semtypes_properties.
iInv (relocN.@"ref".@(l, l1')) as (? ?) "[>Hl ?]" "Hcl".
iInv (relocN.@"ref".@(l, l2')) as (? ?) "[>Hl' ?]" "Hcl'".
simpl. iExFalso.
- iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %[Hfoo _].
+ iCombine "Hl Hl'" gives %[Hfoo _].
compute in Hfoo. eauto.
Qed.
@@ -212,8 +212,7 @@ Section semtypes_properties.
iInv (relocN.@"ref".@(l1', l)) as (? ?) "(? & >Hl & ?)" "Hcl".
iInv (relocN.@"ref".@(l2', l)) as (? ?) "(? & >Hl' & ?)" "Hcl'".
simpl. iExFalso.
- iDestruct (mapstoS_valid_2 with "Hl Hl'") as %Hfoo.
- compute in Hfoo. eauto.
+ by iCombine "Hl Hl'" gives %[??].
Qed.
End semtypes_properties.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index c0e14c0..d6cb896 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -191,6 +191,14 @@ Section mapsto.
iApply (mapstoS_valid l _ v2). by iFrame.
Qed.
+ Global Instance mapstoS_combine_sep_gives l dq1 dq2 v1 v2 :
+ CombineSepGives (l ↦ₛ{dq1} v1) (l ↦ₛ{dq2} v2) ⌜✓ (dq1 â‹… dq2) ∧ v1 = v2âŒ.
+ Proof.
+ rewrite /CombineSepGives. iIntros "[H1 H2]". iSplit.
+ - iDestruct (mapstoS_valid_2 with "H1 H2") as %?; auto.
+ - iDestruct (mapstoS_agree with "H1 H2") as %?; auto.
+ Qed.
+
Lemma mapstoS_half_combine l v1 v2 :
l ↦ₛ{1/2} v1 -∗ l ↦ₛ{1/2} v2 -∗ ⌜v1 = v2⌠∗ l ↦ₛ v1.
Proof.
diff --git a/theories/prelude/bijections.v b/theories/prelude/bijections.v
index 66d630c..9a11fcf 100644
--- a/theories/prelude/bijections.v
+++ b/theories/prelude/bijections.v
@@ -116,8 +116,8 @@ Section logic.
Proof.
iIntros "HL H1 H2". rewrite BIJ_eq /BIJ_def inBij_eq /inBij_def.
iDestruct "HL" as "[HL HL1]"; iDestruct "HL1" as %HL.
- iDestruct (own_valid_2 with "HL H1") as %Hv1%auth_both_valid_discrete.
- iDestruct (own_valid_2 with "HL H2") as %Hv2%auth_both_valid_discrete.
+ iCombine "HL H1" gives %Hv1%auth_both_valid_discrete.
+ iCombine "HL H2" gives %Hv2%auth_both_valid_discrete.
iPureIntro.
destruct Hv1 as [Hv1 _]; destruct Hv2 as [Hv2 _].
apply gset_included, elem_of_subseteq_singleton in Hv1;
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index c1347cd..6d41cb4 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -94,12 +94,12 @@ Section semtypes.
+ destruct (decide (l2 = r2)); subst; first by eauto.
iInv (relocN.@"ref".@(r1, l2)) as (v1 v2) "(>Hr1 & >Hr2 & Hinv1)".
iInv (relocN.@"ref".@(r1, r2)) as (w1 w2) "(>Hr1' & >Hr2' & Hinv2)".
- iExFalso. by iDestruct (mapsto_valid_2 with "Hr1 Hr1'") as %[].
+ iExFalso. by iCombine "Hr1 Hr1'" gives %[].
+ destruct (decide (l2 = r2)); subst; last first.
{ iModIntro. iPureIntro. naive_solver. }
iInv (relocN.@"ref".@(r1, r2)) as (v1 v2) "(>Hr1 & >Hr2 & Hinv1)".
iInv (relocN.@"ref".@(l1, r2)) as (w1 w2) "(>Hr1' & >Hr2' & Hinv2)".
- iExFalso. by iDestruct (mapstoS_valid_2 with "Hr2 Hr2'") as %[]. }
+ iExFalso. by iCombine "Hr2 Hr2'" gives %[]. }
by apply unboxed_type_ref_or_eqtype.
Qed.
--
GitLab