From ac2aeb83a00e18be0f113f3d56b1e6c14d9632bc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 10 Mar 2023 14:21:44 +0100
Subject: [PATCH] Bump Iris: beautify proofs using `iCombine gives`; add
`MaybeCombineSepAs` instances.
---
coq-gpfsl.opam | 2 +-
gpfsl-examples/circ_buff/proof_gps.v | 4 ++--
gpfsl-examples/exchanger/proof_graph_piggyback.v | 2 +-
gpfsl-examples/exchanger/proof_mp_client.v | 4 ++--
gpfsl-examples/graph/ghost.v | 4 ++--
gpfsl-examples/gset_disj.v | 4 ++--
gpfsl-examples/history/ghost.v | 6 ++----
gpfsl-examples/queue/proof_mp2_graph.v | 2 +-
gpfsl-examples/queue/proof_mp_graph.v | 4 ++--
gpfsl-examples/queue/proof_ms_abs_graph.v | 4 ++--
gpfsl-examples/queue/proof_spsc_graph.v | 12 ++++++------
gpfsl-examples/stack/proof_elim_graph.v | 4 ++--
gpfsl-examples/stack/proof_mp_client_graph.v | 4 ++--
gpfsl-examples/stack/proof_mp_client_history.v | 4 ++--
gpfsl-examples/stack/proof_treiber_graph.v | 5 ++---
gpfsl-examples/stack/proof_treiber_history.v | 4 ++--
gpfsl-examples/uniq_token.v | 2 +-
gpfsl/algebra/lat_auth.v | 4 ++--
gpfsl/base_logic/history.v | 4 ++--
gpfsl/base_logic/vprop.v | 8 ++++++++
gpfsl/gps/model_defs.v | 2 +-
gpfsl/logic/na_invariants.v | 12 ++++++------
gpfsl/logic/readonly_ptsto.v | 8 ++++----
gpfsl/logic/relacq.v | 8 ++++++++
gpfsl/logic/view_invariants.v | 11 ++++++-----
25 files changed, 71 insertions(+), 57 deletions(-)
diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index ecbbd060..22855277 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
depends: [
- "coq-iris" { (= "dev.2023-03-07.1.7e127436") | (= "dev") }
+ "coq-iris" { (= "dev.2023-03-10.0.45e5a052") }
"coq-orc11" {= version}
]
diff --git a/gpfsl-examples/circ_buff/proof_gps.v b/gpfsl-examples/circ_buff/proof_gps.v
index 1c4232a4..e225849a 100644
--- a/gpfsl-examples/circ_buff/proof_gps.v
+++ b/gpfsl-examples/circ_buff/proof_gps.v
@@ -91,7 +91,7 @@ Context `{!noprolG Σ, cirbG: !cbG Σ, !atomicG Σ}.
Lemma pTok_exclusive γ i: pTok γ i ∗ pTok γ i ⊢ False.
Proof.
iIntros "[T1 T2]".
- iDestruct (own_valid_2 with "T1 T2") as %[Valid _].
+ iCombine "T1 T2" gives %[Valid _].
exfalso. simpl in Valid.
rewrite -> coPset_disj_valid_op, disjoint_singleton_l in Valid.
by apply Valid, elem_of_singleton.
@@ -100,7 +100,7 @@ Qed.
Lemma cTok_exclusive γ i: cTok γ i ∗ cTok γ i ⊢ False.
Proof.
iIntros "[T1 T2]".
- iDestruct (own_valid_2 with "T1 T2") as %[_ Valid].
+ iCombine "T1 T2" gives %[_ Valid].
exfalso. simpl in Valid.
rewrite ->coPset_disj_valid_op, disjoint_singleton_l in Valid.
by apply Valid, elem_of_singleton.
diff --git a/gpfsl-examples/exchanger/proof_graph_piggyback.v b/gpfsl-examples/exchanger/proof_graph_piggyback.v
index 77c40845..1755d411 100644
--- a/gpfsl-examples/exchanger/proof_graph_piggyback.v
+++ b/gpfsl-examples/exchanger/proof_graph_piggyback.v
@@ -611,7 +611,7 @@ Lemma LTM_master_snap_included γ T T' :
LTM_master γ T -∗ LTM_snap γ T' -∗ ⌜T' ⊆ T⌝.
Proof.
iIntros "o1 o2".
- iDestruct (own_valid_2 with "o1 o2") as %[INCL ?]%auth_both_valid_discrete.
+ iCombine "o1 o2" gives %[INCL ?]%auth_both_valid_discrete.
iPureIntro. by move : INCL => /= /to_agreeM_included.
Qed.
Lemma LTM_master_ssnap_lookup γ M l i :
diff --git a/gpfsl-examples/exchanger/proof_mp_client.v b/gpfsl-examples/exchanger/proof_mp_client.v
index ef0af0e3..58d6c26d 100644
--- a/gpfsl-examples/exchanger/proof_mp_client.v
+++ b/gpfsl-examples/exchanger/proof_mp_client.v
@@ -110,7 +110,7 @@ Section ex.
iMod "Close2" as "_".
(* Update the ghost state *)
iDestruct "Hown" as (b1 b2) "[[>Hown1 Hown2] >[%Hsize _]]".
- iDestruct (own_valid_2 with "Hown1 Tokγ11") as %->%excl_auth_agree_L.
+ iCombine "Hown1 Tokγ11" gives %->%excl_auth_agree_L.
iMod (own_update_2 with "Hown1 Tokγ11") as "[Hown1 Tokγ11]".
{ apply (excl_auth_update _ _ true). }
(* Close the client invariant *)
@@ -146,7 +146,7 @@ Section ex.
(* Close other masks *)
iMod "Close2" as "_".
iDestruct "Hown" as (b1 b2) "[[>Hown1 >Hown2] >[%Hsize %Eqb1]]".
- iDestruct (own_valid_2 with "Hown2 Tokγ21") as %->%excl_auth_agree_L.
+ iCombine "Hown2 Tokγ21" gives %->%excl_auth_agree_L.
iMod (own_update_2 with "Hown2 Tokγ21") as "[Hown2 Tokγ21]".
{ apply (excl_auth_update _ _ true). }
diff --git a/gpfsl-examples/graph/ghost.v b/gpfsl-examples/graph/ghost.v
index 5b72b185..1549da26 100644
--- a/gpfsl-examples/graph/ghost.v
+++ b/gpfsl-examples/graph/ghost.v
@@ -109,7 +109,7 @@ Lemma ghost_graph_master_agree γ q1 G1 q2 G2 :
graph_gmaster γ q1 G1 -∗ graph_gmaster γ q2 G2 -∗ ⌜G1 = G2⌝.
Proof.
iIntros "o1 o2".
- iDestruct (own_valid_2 with "o1 o2") as
+ iCombine "o1 o2" gives
%[[? ?]%mono_list_auth_dfrac_op_valid_L
[? EqCo%leibniz_equiv_iff]%lat_auth_auth_valid].
iPureIntro. simplify_eq.
@@ -120,7 +120,7 @@ Lemma ghost_graph_master_snap_included γg q G G' :
graph_gmaster γg q G -∗ graph_gsnap γg G' -∗ ⌜ G' ⊑ G ⌝.
Proof.
iIntros "oM oS".
- iDestruct (own_valid_2 with "oM oS") as
+ iCombine "oM oS" gives
%[[? ?]%mono_list_both_dfrac_valid_L [? [??]]%lat_auth_both_valid].
iPureIntro. by constructor.
Qed.
diff --git a/gpfsl-examples/gset_disj.v b/gpfsl-examples/gset_disj.v
index 70d9b61d..84e59991 100644
--- a/gpfsl-examples/gset_disj.v
+++ b/gpfsl-examples/gset_disj.v
@@ -56,7 +56,7 @@ Lemma GsetDisjAuth_frag_include γ q X a :
GsetDisjAuth γ q X -∗ GsetDisjFrag γ a -∗ ⌜ a ∈ X ⌝.
Proof.
iIntros "o1 o2".
- iDestruct (own_valid_2 with "o1 o2") as
+ iCombine "o1 o2" gives
%[? [INCL%gset_disj_included%elem_of_subseteq_singleton ?]]%auth_both_dfrac_valid_discrete.
done.
Qed.
@@ -86,7 +86,7 @@ Lemma GsetDisjFrag_disj γ a b :
GsetDisjFrag γ a -∗ GsetDisjFrag γ b -∗ ⌜ a ≠ b ⌝.
Proof.
iIntros "o1 o2".
- iDestruct (own_valid_2 with "o1 o2") as %VALID%auth_frag_valid_1%gset_disj_valid_op.
+ iCombine "o1 o2" gives %VALID%auth_frag_valid_1%gset_disj_valid_op.
iPureIntro. set_solver.
Qed.
End gset_disj.
diff --git a/gpfsl-examples/history/ghost.v b/gpfsl-examples/history/ghost.v
index 9314fe5a..a22d6866 100644
--- a/gpfsl-examples/history/ghost.v
+++ b/gpfsl-examples/history/ghost.v
@@ -81,16 +81,14 @@ Lemma ghost_history_master_agree γ f1 E1 f2 E2 :
history_gmaster γ f1 E1 -∗ history_gmaster γ f2 E2 -∗ ⌜E1 = E2⌝.
Proof.
iIntros "o1 o2".
- by iDestruct (own_valid_2 with "o1 o2")
- as %[_ ?%leibniz_equiv]%mono_list_auth_dfrac_op_valid.
+ by iCombine "o1 o2" gives %[_ ?%leibniz_equiv]%mono_list_auth_dfrac_op_valid.
Qed.
Lemma ghost_history_master_snap_included γg f E E' :
history_gmaster γg f E -∗ history_gsnap γg E' -∗ ⌜E' ⊑ E⌝.
Proof.
iIntros "oM oS".
- by iDestruct (own_valid_2 with "oM oS")
- as %[_ ?]%mono_list_both_dfrac_valid_L.
+ by iCombine "oM oS" gives %[_ ?]%mono_list_both_dfrac_valid_L.
Qed.
(** Graph's Master-Snapshot properties *)
diff --git a/gpfsl-examples/queue/proof_mp2_graph.v b/gpfsl-examples/queue/proof_mp2_graph.v
index 266a234a..5855d4de 100644
--- a/gpfsl-examples/queue/proof_mp2_graph.v
+++ b/gpfsl-examples/queue/proof_mp2_graph.v
@@ -284,7 +284,7 @@ Proof using All.
apply (prefix_lookup _ G.(Es)) in HeV2; [|by destruct SubG0G].
iCombine "◯m ◯m2" as "◯m".
- iDestruct (own_valid_2 with "●m ◯m") as %[LT%nat_included _]%auth_both_valid_discrete.
+ iCombine "●m ◯m" gives %[LT%nat_included _]%auth_both_valid_discrete.
have {}LT : (size (com G) ≤ 1)%nat by lia.
iAaccIntro with "QI".
diff --git a/gpfsl-examples/queue/proof_mp_graph.v b/gpfsl-examples/queue/proof_mp_graph.v
index 0f717502..977f32c2 100644
--- a/gpfsl-examples/queue/proof_mp_graph.v
+++ b/gpfsl-examples/queue/proof_mp_graph.v
@@ -108,7 +108,7 @@ Proof using All.
iDestruct "F" as %(SubG' & SubM' & Sub' & Sub'' & IQ & MAX' &
EsG' & SoG' & ComG' & EqM' & _).
rewrite /is_enqueue in IQ. subst enq.
- iDestruct (own_valid_2 with "nodesA nodes") as %EqL%excl_auth_agree_L.
+ iCombine "nodesA nodes" gives %EqL%excl_auth_agree_L.
inversion EqL as [EQL].
iMod (own_update_2 with "nodesA nodes") as "[nodesA nodes]".
@@ -155,7 +155,7 @@ Proof using All.
iIntros (v V' G' enqId deqId enq1 deq Venq M') "(QI' & sV' & Local & F)".
iDestruct "F" as %(SubG' & SubM' & Sub' & Sub'' & CASE).
- iDestruct (own_valid_2 with "nodes nodes1") as %EqL%excl_auth_agree_L.
+ iCombine "nodes nodes1" gives %EqL%excl_auth_agree_L.
inversion EqL as [He].
have He' := He. apply to_set_singleton in He' as [EqeO EQL]. clear EqL.
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index a0ad4176..28854145 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -1175,7 +1175,7 @@ Lemma LTM_master_snap_included γ T T' :
LTM_master γ T -∗ LTM_snap γ T' -∗ ⌜T' ⊆ T⌝.
Proof.
iIntros "[o1 ?] o2".
- iDestruct (own_valid_2 with "o1 o2") as %[_ [INCL _]%auth_both_valid_discrete].
+ iCombine "o1 o2" gives %[_ [INCL _]%auth_both_valid_discrete].
iPureIntro. by move : INCL => /to_agreeM_included.
Qed.
Lemma LTM_master_ssnap_lookup γ T η eid :
@@ -1416,7 +1416,7 @@ Proof.
iIntros "(_ & GM & %γa & MS & QA) (_ & GM' & %γa' & MS' & QA')".
iDestruct (meta_agree with "MS MS'") as %<-.
iDestruct (graph_master_agree with "GM GM'") as %<-.
- iDestruct (own_valid_2 with "QA QA'") as %[_ <-]%frac_agree_op_valid_L. done.
+ iCombine "QA QA'" gives %[_ <-]%frac_agree_op_valid_L. done.
Qed.
Lemma QueueInv_consistent γg q Q G :
diff --git a/gpfsl-examples/queue/proof_spsc_graph.v b/gpfsl-examples/queue/proof_spsc_graph.v
index 0e953ad5..456e77f0 100644
--- a/gpfsl-examples/queue/proof_spsc_graph.v
+++ b/gpfsl-examples/queue/proof_spsc_graph.v
@@ -113,7 +113,7 @@ Lemma Producer_exclusive N γg γed q G1 G2 M1 M2 es1 es2 :
Producer N γg γed q G1 M1 es1 -∗ Producer N γg γed q G2 M2 es2 -∗ False.
Proof.
iDestruct 1 as "(_ & ◯e1 & _)". iDestruct 1 as "(_ & ◯e2 & _)".
- by iDestruct (own_valid_2 with "◯e1 ◯e2") as %[?%excl_auth_frag_op_valid ?].
+ by iCombine "◯e1 ◯e2" gives %[?%excl_auth_frag_op_valid ?].
Qed.
Lemma Producer_QueueLocal N γg γed q G M es :
Producer N γg γed q G M es ⊢ wq.(QueueLocal) N γg q G M.
@@ -126,14 +126,14 @@ Lemma Producer_agree N γg γed q G G' M es es' ds :
Proof.
iDestruct 1 as "[%xs [QI (●ed & %PERM & %PROD & %CONS & %MATCH & %EMP)]]".
iDestruct 1 as "(_ & ◯e & _ & _)".
- by iDestruct (own_valid_2 with "●ed ◯e") as %[<-%excl_auth_agree_L ?].
+ by iCombine "●ed ◯e" gives %[<-%excl_auth_agree_L ?].
Qed.
Lemma Consumer_exclusive N γg γed q G1 G2 M1 M2 ds1 ds2 :
Consumer N γg γed q G1 M1 ds1 -∗ Consumer N γg γed q G2 M2 ds2 -∗ False.
Proof.
iDestruct 1 as "(_ & ◯d1 & _)". iDestruct 1 as "(_ & ◯d2 & _)".
- by iDestruct (own_valid_2 with "◯d1 ◯d2") as %[? ?%excl_auth_frag_op_valid].
+ by iCombine "◯d1 ◯d2" gives %[? ?%excl_auth_frag_op_valid].
Qed.
Lemma Consumer_QueueLocal N γg γed q G M ds :
Consumer N γg γed q G M ds ⊢ wq.(QueueLocal) N γg q G M.
@@ -146,7 +146,7 @@ Lemma Consumer_agree N γg γed q G G' M es ds ds' :
Proof.
iDestruct 1 as "[%xs [QI (●ed & %PERM & %PROD & %CONS & %MATCH & %EMP)]]".
iDestruct 1 as "(_ & ◯d & _ & _)".
- by iDestruct (own_valid_2 with "●ed ◯d") as %[? <-%excl_auth_agree_L].
+ by iCombine "●ed ◯d" gives %[? <-%excl_auth_agree_L].
Qed.
@@ -173,7 +173,7 @@ Proof.
awp_apply (wq.(enqueue_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (G es ds) "[%xs [QI >(●ed & %PERM & %PROD & %CONS & %MATCH & %EMP)]]".
- iDestruct (own_valid_2 with "●ed ◯e") as %[<-%excl_auth_agree_L _].
+ iCombine "●ed ◯e" gives %[<-%excl_auth_agree_L _].
iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC".
rewrite QueueInv_graph_master_acc. iDestruct "QI" as "[>Gm QI]".
iDestruct (graph_master_consistent with "Gm") as %EGC.
@@ -248,7 +248,7 @@ Proof.
awp_apply (wq.(dequeue_spec) with "⊒V QL"); [done..|].
iApply (aacc_aupd_commit with "AU"); [done|].
iIntros (G es ds) "[%xs [QI >(●ed & %PERM & %PROD & %CONS & %MATCH & %EMP)]]".
- iDestruct (own_valid_2 with "●ed ◯d") as %[_ <-%excl_auth_agree_L].
+ iCombine "●ed ◯d" gives %[_ <-%excl_auth_agree_L].
iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC".
have [NODUPes [NODUPds NODUPxs]] : NoDup es ∧ NoDup ds ∧ NoDup xs.
{ symmetry in PERM. move: PERM => /ord_nodup.
diff --git a/gpfsl-examples/stack/proof_elim_graph.v b/gpfsl-examples/stack/proof_elim_graph.v
index 8ac136d8..3b509384 100644
--- a/gpfsl-examples/stack/proof_elim_graph.v
+++ b/gpfsl-examples/stack/proof_elim_graph.v
@@ -627,14 +627,14 @@ Lemma ge_list_auth_lb_valid γ q T T' :
ge_list_auth γ q T -∗ ge_list_lb γ T' -∗ ⌜ T' ⊑ T ⌝.
Proof.
iIntros "o1 o2".
- by iDestruct (own_valid_2 with "o1 o2") as %[_ ?]%mono_list_both_dfrac_valid_L.
+ by iCombine "o1 o2" gives %[_ ?]%mono_list_both_dfrac_valid_L.
Qed.
Lemma ge_list_auth_agree γ q T q' T' :
ge_list_auth γ q T -∗ ge_list_auth γ q' T' -∗ ⌜ T = T' ⌝.
Proof.
iIntros "o1 o2".
- by iDestruct (own_valid_2 with "o1 o2") as %[_ ?]%mono_list_auth_dfrac_op_valid_L.
+ by iCombine "o1 o2" gives %[_ ?]%mono_list_auth_dfrac_op_valid_L.
Qed.
Lemma ge_list_alloc T :
diff --git a/gpfsl-examples/stack/proof_mp_client_graph.v b/gpfsl-examples/stack/proof_mp_client_graph.v
index c2eeefc2..0d71bf09 100644
--- a/gpfsl-examples/stack/proof_mp_client_graph.v
+++ b/gpfsl-examples/stack/proof_mp_client_graph.v
@@ -99,7 +99,7 @@ Section Stack.
iDestruct "F" as %(SubG' & SubM' & Sub' & Sub'' & IQ & MAX' &
EsG' & SoG' & ComG' & EqM' & _).
rewrite / is_push in IQ. subst push.
- iDestruct (own_valid_2 with "nodesA nodes") as %[= EQL]%excl_auth_agree_L.
+ iCombine "nodesA nodes" gives %[= EQL]%excl_auth_agree_L.
iMod (own_update_2 with "nodesA nodes") as "[nodesA nodes]".
{ apply (excl_auth_update _ _ (GSet {[pushId]})). }
@@ -143,7 +143,7 @@ Section Stack.
iIntros (v V' G' pushId popId push1 pop Vpush M') "(SI' & sV' & Local & F)".
iDestruct "F" as %((SubG' & SubM' & Sub' & Sub'') & CASE).
- iDestruct (own_valid_2 with "nodes nodes1") as %[= He]%excl_auth_agree_L.
+ iCombine "nodes nodes1" gives %[= He]%excl_auth_agree_L.
have He' := He. apply to_set_singleton in He' as [EqeO EQL].
iMod (own_update_2 with "nodes nodes1") as "[nodes nodes1]".
diff --git a/gpfsl-examples/stack/proof_mp_client_history.v b/gpfsl-examples/stack/proof_mp_client_history.v
index 1d52632a..8e42eac2 100644
--- a/gpfsl-examples/stack/proof_mp_client_history.v
+++ b/gpfsl-examples/stack/proof_mp_client_history.v
@@ -98,7 +98,7 @@ Section Stack.
iIntros (V' E' pushId push Vpush M') "(SI' & sV' & Local & F)".
iDestruct "F" as %(? & ? & IP & HpushId & HE' & HM').
rewrite /is_push in IP. subst push.
- iDestruct (own_valid_2 with "nodesA nodes") as %[= EQL]%excl_auth_agree_L.
+ iCombine "nodesA nodes" gives %[= EQL]%excl_auth_agree_L.
iMod (own_update_2 with "nodesA nodes") as "[nodesA nodes]".
{ apply (excl_auth_update _ _ (GSet {[pushId]})). }
iIntros "!>".
@@ -141,7 +141,7 @@ Section Stack.
iIntros (v V' E' pushId popId push1 pop Vpush M') "(SI' & sV' & Local & F)".
iDestruct "F" as %((? & ?) & CASE).
- iDestruct (own_valid_2 with "nodes nodes1") as %[= He]%excl_auth_agree_L.
+ iCombine "nodes nodes1" gives %[= He]%excl_auth_agree_L.
apply to_set_singleton in He as [-> EQL].
assert (E = [eV]) as ->; last clear EQL.
{ eapply prefix_lookup in Eqe; [|done]. destruct E; [done|].
diff --git a/gpfsl-examples/stack/proof_treiber_graph.v b/gpfsl-examples/stack/proof_treiber_graph.v
index 93df076d..4e30ebd8 100644
--- a/gpfsl-examples/stack/proof_treiber_graph.v
+++ b/gpfsl-examples/stack/proof_treiber_graph.v
@@ -397,8 +397,7 @@ Lemma LTM_master_snap_included γ q T T' :
Proof.
rewrite /LTM_master /LTM_auth.
iIntros "[o1 ?] o2".
- iDestruct (own_valid_2 with "o1 o2")
- as %(_ & INCL & _)%auth_both_dfrac_valid_discrete.
+ iCombine "o1 o2" gives %(_ & INCL & _)%auth_both_dfrac_valid_discrete.
iPureIntro. by move : INCL => /to_agreeM_included.
Qed.
Lemma LTM_master_ssnap_lookup γ q T n eid :
@@ -446,7 +445,7 @@ Lemma LTM_master_agree γ q1 q2 T1 T2 :
LTM_master γ q1 T1 -∗ LTM_master γ q2 T2 -∗ ⌜ T1 = T2 ⌝.
Proof.
iIntros "T1 T2". rewrite /LTM_master /LTM_auth.
- iDestruct (own_valid_2 with "T1 T2") as %VAL. iPureIntro.
+ iCombine "T1 T2" gives %VAL. iPureIntro.
move : VAL.
rewrite (comm _ (●{#q2} _)) -!assoc (assoc _ (◯ _)).
rewrite -auth_frag_op (comm _ (◯ _)) assoc.
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index 3c0446df..9a457b21 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -967,8 +967,8 @@ Lemma emo_auth_lb_valid γ esi1 esi2 emo1 emo2 :
emo2.*1.*2 `prefixes_of` emo1.*1.*2 ⌝.
Proof.
iIntros "Hauth Hlb".
- by iDestruct (own_valid_2 with "Hauth Hlb")
- as %[[?%mono_list_both_valid_L ?%mono_list_both_valid_L] ?%mono_list_list_both_valid_L].
+ by iCombine "Hauth Hlb"
+ gives %[[?%mono_list_both_valid_L ?%mono_list_both_valid_L] ?%mono_list_list_both_valid_L].
Qed.
Lemma emo_lb_own_get γ esi emo :
diff --git a/gpfsl-examples/uniq_token.v b/gpfsl-examples/uniq_token.v
index 4adcf5f6..471c806d 100644
--- a/gpfsl-examples/uniq_token.v
+++ b/gpfsl-examples/uniq_token.v
@@ -52,6 +52,6 @@ Qed.
Lemma UTok_unique γ : UTok γ -∗ UTok γ -∗ False.
Proof.
rewrite UTok_eq. iIntros "U1 U2".
- by iDestruct (own_valid_2 with "U1 U2") as %?.
+ by iCombine "U1 U2" gives %?.
Qed.
End Tok.
diff --git a/gpfsl/algebra/lat_auth.v b/gpfsl/algebra/lat_auth.v
index be22c3b4..a8ff1784 100644
--- a/gpfsl/algebra/lat_auth.v
+++ b/gpfsl/algebra/lat_auth.v
@@ -115,13 +115,13 @@ Context {LAT : latticeT} `{!@LatBottom LAT bot} `{!inG Σ (lat_authR LAT)}.
Lemma own_master_max γ q a b :
own γ (●L{q} a) -∗ own γ (◯L b) -∗ ⌜b ⊑ a⌝.
Proof.
- iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %[]%lat_auth_both_valid.
+ iIntros "H1 H2". by iCombine "H1 H2" gives %[]%lat_auth_both_valid.
Qed.
Lemma own_master_eq γ p q a b :
own γ (●L{p} a) -∗ own γ (●L{q} b) -∗ ⌜a ≡ b⌝.
Proof.
- iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %[]%lat_auth_auth_valid.
+ iIntros "H1 H2". by iCombine "H1 H2" gives %[]%lat_auth_auth_valid.
Qed.
Lemma own_master_update γ a b (Ext : a ⊑ b) :
diff --git a/gpfsl/base_logic/history.v b/gpfsl/base_logic/history.v
index 03e79f0c..0a05f233 100644
--- a/gpfsl/base_logic/history.v
+++ b/gpfsl/base_logic/history.v
@@ -588,8 +588,8 @@ Section hist.
iDestruct 1 as (hF V Vc) "(_ & _ & _ & _ & _ & _ & oA & wf)".
iDestruct "wf" as %(_ & ? & ? & ?).
rewrite seen_eq. iIntros "oV".
- iDestruct (own_valid_2 with "oA oV")
- as %[Le%latT_included _]%auth_both_valid_discrete. simpl in Le.
+ iCombine "oA oV"
+ gives %[Le%latT_included _]%auth_both_valid_discrete. simpl in Le.
iPureIntro. apply closed_tview_acq_inv. by rewrite Le.
Qed.
diff --git a/gpfsl/base_logic/vprop.v b/gpfsl/base_logic/vprop.v
index 53bac57a..a01b4052 100644
--- a/gpfsl/base_logic/vprop.v
+++ b/gpfsl/base_logic/vprop.v
@@ -541,6 +541,10 @@ Proof. rewrite /IntoSep -view_join_sep=> -> //. Qed.
#[global] Instance from_sep_view_join P Q1 Q2 V :
FromSep P Q1 Q2 → FromSep (⊔{V} P) (⊔{V} Q1) (⊔{V} Q2).
Proof. by rewrite /FromSep -view_join_sep => <-. Qed.
+#[global] Instance maybe_combine_sep_as_view_join P Q1 Q2 V progress :
+ MaybeCombineSepAs P Q1 Q2 progress →
+ MaybeCombineSepAs (⊔{V} P) (⊔{V} Q1) (⊔{V} Q2) progress.
+Proof. by rewrite /MaybeCombineSepAs -view_join_sep => <-. Qed.
#[global] Instance into_or_view_join P Q1 Q2 V :
IntoOr P Q1 Q2 → IntoOr (⊔{V} P) (⊔{V} Q1) (⊔{V} Q2).
@@ -667,6 +671,10 @@ Proof. rewrite /IntoSep -view_at_sep=> -> //. Qed.
#[global] Instance from_sep_view_at P Q1 Q2 V :
FromSep P Q1 Q2 → FromSep (@{V} P) (@{V} Q1) (@{V} Q2).
Proof. by rewrite /FromSep -view_at_sep => <-. Qed.
+#[global] Instance maybe_combine_sep_as_view_at P Q1 Q2 V progress :
+ MaybeCombineSepAs P Q1 Q2 progress →
+ MaybeCombineSepAs (@{V} P) (@{V} Q1) (@{V} Q2) progress.
+Proof. by rewrite /MaybeCombineSepAs -view_at_sep => <-. Qed.
#[global] Instance into_or_view_at P Q1 Q2 V :
IntoOr P Q1 Q2 → IntoOr (@{V} P) (@{V} Q1) (@{V} Q2).
diff --git a/gpfsl/gps/model_defs.v b/gpfsl/gps/model_defs.v
index 1d7a6af9..d95c4366 100644
--- a/gpfsl/gps/model_defs.v
+++ b/gpfsl/gps/model_defs.v
@@ -287,7 +287,7 @@ Section Properties.
gps_own γ χ' -∗ gps_snap γ χ -∗ ⌜ χ ⊆ χ' ⌝.
Proof.
iIntros "oA R".
- iDestruct (own_valid_2 with "oA R") as %VAL.
+ iCombine "oA R" gives %VAL.
iPureIntro. move : VAL.
rewrite /stateMap_auth /stateMap_frag -assoc auth_both_valid_discrete /=.
intros [? _]. apply stateMap_included. etrans; [apply cmra_included_r|done].
diff --git a/gpfsl/logic/na_invariants.v b/gpfsl/logic/na_invariants.v
index 4b9eebe3..090ebb98 100644
--- a/gpfsl/logic/na_invariants.v
+++ b/gpfsl/logic/na_invariants.v
@@ -72,7 +72,7 @@ Section proofs.
Proof.
rewrite /na_own. iIntros "H1 H2".
iDestruct "H1" as (Vs1) "[H1 _]". iDestruct "H2" as (Vs2) "[H2 _]".
- iDestruct (own_valid_2 with "H1 H2") as %Hv. iIntros "!%" (i Hi1 Hi2).
+ iCombine "H1 H2" gives %Hv. iIntros "!%" (i Hi1 Hi2).
specialize (Hv i).
rewrite /to_ofe_funR /= discrete_fun_lookup_op !decide_True in Hv; auto.
by destruct Hv.
@@ -130,11 +130,11 @@ Section proofs.
iDestruct "Htoki" as (Vs) "[Hown #HinVs]".
iInv N as "[HP|>Htoki]" "Hclose"; last first.
{ iDestruct "Htoki" as (V') "[Hown' _]".
- iDestruct (own_valid_2 with "Hown Hown'") as %Hv. specialize (Hv i).
+ iCombine "Hown Hown'" gives %Hv. specialize (Hv i).
rewrite /= discrete_fun_lookup_op discrete_fun_lookup_singleton /to_ofe_funR
decide_True // in Hv; [by destruct Hv|set_solver-]. }
iDestruct "HP" as (V') "(HP & >#HV' & >Hdis)".
- iDestruct (own_valid_2 with "Hown HV'") as %Hv. specialize (Hv i).
+ iCombine "Hown HV'" gives %Hv. specialize (Hv i).
rewrite /= discrete_fun_lookup_op discrete_fun_lookup_singleton /to_ofe_funR
decide_True in Hv; [|set_solver].
apply auth_both_valid_discrete, proj1, latT_included in Hv. simpl in Hv. rewrite [in P _]Hv.
@@ -151,10 +151,10 @@ Section proofs.
iIntros "!> [HP $]".
iInv N as "[HP'|>Htoki]" "Hclose".
{ iDestruct "HP'" as (?) "(_ & _ & >Hdis1)".
- iDestruct (own_valid_2 with "Hdis1 Hdis2")
- as %[Hv'%option_included _]%auth_both_valid_discrete. exfalso. naive_solver. }
+ iCombine "Hdis1 Hdis2"
+ gives %[Hv'%option_included _]%auth_both_valid_discrete. exfalso. naive_solver. }
iDestruct "Htoki" as (Vi) "[Hown Hdis1]".
- iDestruct (own_valid_2 with "Hdis1 Hdis2") as %EQVi%excl_auth_agree%(inj to_latT).
+ iCombine "Hdis1 Hdis2" gives %EQVi%excl_auth_agree%(inj to_latT).
(* FIXME : rewrite EQVi should work. *)
assert (@discrete_fun_singleton _ _ (λ _, _) i (● to_latT Vi) ≡
discrete_fun_singleton i (● to_latT (Vs i))) as -> by by f_equiv; rewrite EQVi.
diff --git a/gpfsl/logic/readonly_ptsto.v b/gpfsl/logic/readonly_ptsto.v
index e30b3ad8..af767f91 100644
--- a/gpfsl/logic/readonly_ptsto.v
+++ b/gpfsl/logic/readonly_ptsto.v
@@ -73,7 +73,7 @@ Proof.
rewrite ROSeen_eq.
iDestruct 1 as (??) "[_ O1]". iDestruct 1 as (??) "[_ O2]".
rewrite !view_at_objective_iff.
- iDestruct (own_valid_2 with "O1 O2") as %?%to_agree_op_valid_L.
+ iCombine "O1 O2" gives %?%to_agree_op_valid_L.
iPureIntro. by simplify_eq.
Qed.
Lemma ROSeen_agree_l l γ v v' V :
@@ -102,7 +102,7 @@ Proof.
rewrite ROPtsTo_eq ROSeen_eq.
iDestruct 1 as (???????) "(_&_&_&O1)". iDestruct 1 as (??) "[_ O2]".
rewrite !view_at_objective_iff.
- iDestruct (own_valid_2 with "O1 O2") as %?%to_agree_op_valid_L.
+ iCombine "O1 O2" gives %?%to_agree_op_valid_L.
iPureIntro. by simplify_eq.
Qed.
Lemma ROPtsTo_ROSeen_agree_l l γ v v' V :
@@ -167,7 +167,7 @@ Proof.
iDestruct "Pts" as (t m rsa rns ws Va (GH & Eqv' & LeVa))
"((SLV & ARL & AWL & NAL) & HC & (AR & AW & NA) & AR1)".
iDestruct "SR" as (t' V') "[SLV' AR2]".
- iDestruct (own_valid_2 with "AR1 AR2") as %Eq'%to_agree_op_valid_L.
+ iCombine "AR1 AR2" gives %Eq'%to_agree_op_valid_L.
inversion Eq'; clear Eq'; subst t' v' V'.
iDestruct (seen_time_AllocLocal_singleton l t m with "[SLV']") as %AL.
@@ -215,7 +215,7 @@ Proof.
iDestruct "Pts" as (t m rsa rns ws Va (GH & Eqv' & LeVa))
"((SLV & ARL & #AWL & NAL) & HC & (AR & AW & NA) & AR1)".
iDestruct "SR" as (t' V') "[SLV' AR2]".
- iDestruct (own_valid_2 with "AR1 AR2") as %Eq'%to_agree_op_valid_L.
+ iCombine "AR1 AR2" gives %Eq'%to_agree_op_valid_L.
inversion Eq'; clear Eq'; subst t' v' V'.
iDestruct (seen_time_AllocLocal_singleton l t m with "[SLV']") as %AL.
{ by inversion Eqv'. } { iDestruct (seen_view_seen_time with "SLV'") as "[$ ?]". }
diff --git a/gpfsl/logic/relacq.v b/gpfsl/logic/relacq.v
index 2e318323..d7dc2427 100644
--- a/gpfsl/logic/relacq.v
+++ b/gpfsl/logic/relacq.v
@@ -507,6 +507,10 @@ Section proofmode.
Global Instance from_sep_rel_mod P Q1 Q2 tid :
FromSep P Q1 Q2 → FromSep (△{tid} P) (△{tid} Q1) (△{tid} Q2).
Proof. by rewrite /FromSep rel_sep => ->. Qed.
+ Global Instance maybe_combine_sep_as_rel_mod P Q1 Q2 tid progress :
+ MaybeCombineSepAs P Q1 Q2 progress →
+ MaybeCombineSepAs (△{tid} P) (△{tid} Q1) (△{tid} Q2) progress.
+ Proof. by rewrite /MaybeCombineSepAs rel_sep => ->. Qed.
Global Instance into_or_rel_mod P Q1 Q2 tid :
IntoOr P Q1 Q2 → IntoOr (△{tid} P) (△{tid} Q1) (△{tid} Q2).
@@ -574,6 +578,10 @@ Section proofmode.
Global Instance from_sep_acq_mod P Q1 Q2 tid :
FromSep P Q1 Q2 → FromSep (▽{tid} P) (▽{tid} Q1) (▽{tid} Q2).
Proof. by rewrite /FromSep acq_sep => ->. Qed.
+ Global Instance maybe_combine_sep_as_acq_mod P Q1 Q2 tid progress :
+ MaybeCombineSepAs P Q1 Q2 progress →
+ MaybeCombineSepAs (▽{tid} P) (▽{tid} Q1) (▽{tid} Q2) progress.
+ Proof. by rewrite /MaybeCombineSepAs acq_sep => ->. Qed.
Global Instance into_or_acq_mod P Q1 Q2 tid :
IntoOr P Q1 Q2 → IntoOr (▽{tid} P) (▽{tid} Q1) (▽{tid} Q2).
diff --git a/gpfsl/logic/view_invariants.v b/gpfsl/logic/view_invariants.v
index 231b7d84..21b8cbcb 100644
--- a/gpfsl/logic/view_invariants.v
+++ b/gpfsl/logic/view_invariants.v
@@ -162,7 +162,8 @@ Proof.
iMod (inv_acc with "Inv") as "[VI Closed]"; [done|].
iDestruct "VI" as (V') "[>tok'|[>oA P]]".
{ rewrite view_tok_eq. iDestruct "tok'" as (V2) "[_ tok']".
- by iDestruct (own_valid_2 with "tok [$tok']") as %[? _]%frac_auth_frag_valid. }
+ rewrite view_at_embed.
+ by iCombine "tok tok'" gives %[? _]%frac_auth_frag_valid. }
iDestruct (own_valid_2 with "[$oA] tok")
as %->%frac_auth_agree%to_latT_inj%leibniz_equiv_iff.
iMod ("Closed" with "[tok]").
@@ -196,8 +197,8 @@ Proof.
iSplitL "P". { rewrite view_join_later. by iFrame. }
iFrame "oA". iSplitL "".
{ iIntros "!>". iDestruct 1 as (V3) "[In3 tok]". iIntros "oA".
- iDestruct (own_valid_2 with "oA tok")
- as %->%frac_auth_agree%to_latT_inj%leibniz_equiv_iff.
+ iCombine "oA tok"
+ gives %->%frac_auth_agree%to_latT_inj%leibniz_equiv_iff.
by iFrame. }
iIntros "oA". iSplit; last iSplit.
- iDestruct 1 as (V3) "[#In3 tok]". iIntros "P".
@@ -225,8 +226,8 @@ Proof.
iExists (V' ⊔ V3). iRight. rewrite view_at_view_join.
iNext. by iFrame.
- iDestruct 1 as (V3) "[#In3 tok]". iSplit.
- + iDestruct (own_valid_2 with "oA tok")
- as %->%frac_auth_agree%to_latT_inj%leibniz_equiv_iff.
+ + iCombine "oA tok"
+ gives %->%frac_auth_agree%to_latT_inj%leibniz_equiv_iff.
by iFrame.
+ iMod ("Closed" with "[tok]"); [|done].
iExists V3. iLeft. rewrite view_tok_eq. iExists V3. by iFrame "tok".
--
GitLab