From 5f330bab648130356e1f006bcc6668e3bc120d8d Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Fri, 15 Sep 2023 11:13:13 +0200
Subject: [PATCH] Fixes for improved exist instance
---
theories/hocap/concurrent_runners.v | 9 ++--
theories/lecture_notes/lists.v | 9 ++--
.../locks/array_based_queuing_lock/abql.v | 3 +-
theories/logatom/conditional_increment/cinc.v | 7 ++-
.../counter_with_backup/counter_proof.v | 10 ++--
theories/logatom/herlihy_wing_queue/hwq.v | 3 +-
.../binary/examples/stack/refinement.v | 5 +-
theories/spanning_tree/spanning.v | 46 ++++++++-----------
8 files changed, 39 insertions(+), 53 deletions(-)
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index 0b9142ef..476708f3 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -228,7 +228,7 @@ Section contents.
iMod (inv_alloc (N.@"task") _ (task_inv γ γ' status res (Q a))%I with "[-HP HΦ Htask Hinit]") as "#Hinv".
{ iNext. iLeft. iFrame. }
wp_pures. iModIntro. iApply "HΦ".
- iFrame. iSplitL; iExists _,_,_; iFrame "Hinv"; eauto.
+ unfold isTask, task. iFrame "#∗". eauto.
Qed.
Lemma task_Join_spec γb γ γ' (r t a : val) P Q :
@@ -248,14 +248,14 @@ Section contents.
iMod ("Hcl" with "[Hstate Hres]") as "_".
{ iNext; iLeft; iFrame. }
iModIntro. wp_op. wp_if.
- rewrite /task_Join. iApply ("IH" with "[$Htoken] HΦ").
+ rewrite /task_Join. iApply ("IH" with "[Htoken] HΦ").
iExists _,_,_; iFrame "Htask"; eauto.
- iDestruct "Hstatus" as (v) "(>Hstate & >Hres & HQ)".
wp_load.
iMod ("Hcl" with "[Hstate Hres HQ]") as "_".
{ iNext; iRight; iLeft. iExists _; iFrame. }
iModIntro. wp_op. wp_if.
- rewrite /task_Join. iApply ("IH" with "[$Htoken] HΦ").
+ rewrite /task_Join. iApply ("IH" with "[Htoken] HΦ").
iExists _,_,_; iFrame "Htask"; eauto.
- iDestruct "Hstatus" as (v) "(>Hstate & >Hres & #HFIN & HQ)".
wp_load.
@@ -264,8 +264,7 @@ Section contents.
iMod (shoot v γ with "[Htoken Htoken2]") as "#Hshot".
{ iCombine "Htoken Htoken2" as "?". done. }
iMod ("Hcl" with "[Hstate Hres]") as "_".
- { iNext. iRight. iRight. iExists _. iFrame. iFrame "HFIN".
- iRight. eauto. }
+ { iNext. iRight. iRight. iFrame "#∗". }
iModIntro. wp_op. wp_if. wp_bind (!#res)%E.
iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT)|[Hstatus|Hstatus]]" "Hcl".
{ iExFalso. iApply (shot_not_pending with "Hshot Hpending"). }
diff --git a/theories/lecture_notes/lists.v b/theories/lecture_notes/lists.v
index 63ccdae5..6e12ae8b 100644
--- a/theories/lecture_notes/lists.v
+++ b/theories/lecture_notes/lists.v
@@ -76,9 +76,9 @@ Proof.
- eauto.
- by iIntros "(? & _)".
- iDestruct 1 as (l hd') "(? & ? & H & ?)". rewrite IHxs. iDestruct "H" as "(H_isListxs' & ?)".
- iFrame. iExists l, hd'. iFrame.
+ iFrame.
- iDestruct 1 as "(H_isList & ? & H)". iDestruct "H_isList" as (l hd') "(? & ? & ?)".
- iExists l, hd'. rewrite IHxs. iFrame.
+ iFrame. rewrite IHxs. iFrame.
Qed.
(* The predicate
@@ -246,7 +246,7 @@ Proof.
wp_match. do 2 (wp_load; wp_proj; wp_let). wp_op.
wp_store. iApply ("IH" with "Hxs").
iNext. iIntros (w) "H'". iApply "H". iDestruct "H'" as "[Hw Hislist]".
- iFrame. iExists l, hd'. iFrame. done.
+ iFrame. done.
Qed.
@@ -328,8 +328,7 @@ Proof.
iApply ("IH" with "H_isList H_Pxs' H_Iempty [H_l H_Px H_inv]").
iNext. iIntros (r) "(H_isListxs' & H_Ixs')".
iApply ("H_f" with "[$H_Ixs' $H_Px] [H_inv H_isListxs' H_l]").
- iNext. iIntros (r') "H_inv'". iApply "H_inv". iFrame.
- iExists l, hd'. by iFrame.
+ iNext. iIntros (r') "H_inv'". iApply "H_inv". iFrame. done.
Qed.
Lemma foldr_spec_PPI P I (f a hd : val) (xs : list val) :
diff --git a/theories/locks/array_based_queuing_lock/abql.v b/theories/locks/array_based_queuing_lock/abql.v
index d91eff4e..95ddb4be 100644
--- a/theories/locks/array_based_queuing_lock/abql.v
+++ b/theories/locks/array_based_queuing_lock/abql.v
@@ -385,8 +385,7 @@ Section proof.
- iLeft. iFrame. rewrite Nat.Div0.mod_0_l //. }
wp_pures.
iApply "Post".
- rewrite /is_lock. iFrame.
- iExists _, _. auto.
+ rewrite /is_lock. iFrame. auto.
Qed.
Lemma rem_mod_eq (x y : nat) : (0 < y) → (x `rem` y)%Z = x `mod` y.
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index e8d0d507..8d57444d 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -298,11 +298,10 @@ Section conditional_counter.
iSplitL "Hl_ghost_inv Hl_ghost Q Hp' Hl".
(* Update state to Done. *)
{ iNext. iExists _. iFrame "Hp'". iRight. unfold done_state.
- iFrame "#∗". iDestruct "Hl_ghost_inv" as (v) "Hl_ghost_inv".
- iDestruct (pointsto_agree with "Hl_ghost Hl_ghost_inv") as %<-.
- iSplitR "Hl"; iExists _; iFrame. }
+ iDestruct "Hl_ghost_inv" as (v) "Hl_ghost_inv".
+ iDestruct (pointsto_agree with "Hl_ghost Hl_ghost_inv") as %<-. iFrame "#∗". }
iModIntro. iSplitR "HQ".
- { iNext. iDestruct "Hc" as "[Hc1 Hc2]".
+ { iNext. iDestruct "Hc" as "[Hc1 Hc2]".
iExists l_new, _, (Quiescent n). iFrame. }
wp_seq. iApply "HQ".
iApply state_done_extract_Q; done.
diff --git a/theories/logatom/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v
index 7c1ec6cb..7482f654 100644
--- a/theories/logatom/counter_with_backup/counter_proof.v
+++ b/theories/logatom/counter_with_backup/counter_proof.v
@@ -232,8 +232,7 @@ Section counter_proof.
rewrite bool_decide_decide; destruct decide; first lia.
iDestruct "Hget" as (O) "[Hmap Hset]".
iMod (logicall_execute_gets_set with "[$Hc $Hset]") as "[Hc Hset]".
- iModIntro. iFrame. iSplitL "Hset Hmap".
- { iExists O. iFrame. }
+ iModIntro. iFrame.
iApply (big_sepM_impl with "Hgets"). iModIntro.
iIntros (k γ' Hel). iDestruct 1 as (O') "(Hmap & Hset)".
iExists O'. iFrame. iApply (big_sepS_impl with "Hset").
@@ -245,9 +244,9 @@ Section counter_proof.
- eapply delete_notin in Hlook. rewrite -Hlook. iModIntro. iFrame.
iApply (big_sepM_impl with "Hgets"). iModIntro.
iIntros (k γ' Hel). iDestruct 1 as (O') "(Hmap & Hset)".
- iExists O'. iFrame. iApply (big_sepS_impl with "Hset").
+ iFrame. iApply (big_sepS_impl with "Hset").
iModIntro. iIntros ([γ1' γ2'] Hel'). iDestruct 1 as (Ψ) "(I' & Hvar & Hcred)".
- iExists Ψ. iFrame "I'". rewrite !bool_decide_decide.
+ iFrame "I'". rewrite !bool_decide_decide.
destruct decide, decide; [iFrame| | lia | iFrame].
assert (S n = k) as Heq by lia. rewrite Heq lookup_delete in Hel.
naive_solver.
@@ -288,7 +287,6 @@ Section counter_proof.
iSplitR ""; last done.
iSplit; first done. rewrite !big_sepM_insert //.
iFrame. iSplitR; first eauto with iFrame.
- iExists ∅. iFrame.
rewrite big_sepS_empty. done.
Qed.
@@ -483,7 +481,7 @@ Section counter_proof.
awp_apply load_spec.
iInv "I" as (G P n_b n_p) "(>%Hn & >Hb & >Hp & >Hcnt & >Hprim & Hrest)".
iAaccIntro with "Hp".
- { iIntros "?". iModIntro. rewrite /counter_inv /counter_inv_inner. iFrame "Cnt Hone". iFrame. iNext. iExists G, P, n_b, n_p. eauto with iFrame. }
+ { iIntros "?". iModIntro. rewrite /counter_inv /counter_inv_inner. by iFrame. }
iIntros "Hp". iDestruct (mono_nat_auth_own_agree with "Hcnt Cnt") as %[_ ->].
iDestruct (mono_nat_lb_own_get with "Hprim") as "#Hn_p".
iModIntro. iSplitR "Cnt Cnt2 Hone".
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index 23cfae59..ee5dbc4a 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -2160,8 +2160,7 @@ Proof.
intros ->. apply Hpref in Hk as (H1 & H2).
rewrite Hi_free in H1. inversion H1. }
iSplitL "Hbig Hpend_tok_i AU".
- { iApply big_sepM_insert; first done. iFrame. iSplit; first done.
- iExists (Φ #()). iFrame. done. }
+ { iApply big_sepM_insert; first done. iFrame "#∗". }
iPureIntro. subst new_slots. repeat split_and; try done.
- intros k. destruct sz as [|sz]; first by lia.
split; intros Hk.
diff --git a/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v b/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
index 7e300a20..f6ceba91 100644
--- a/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
+++ b/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
@@ -303,9 +303,8 @@ Section Stack_refinement.
iApply ("Hlat" $! istk6 zn2 with "[Hj] [HLK]"); trivial.
rewrite StackLink_unfold; iModIntro; simpl.
iDestruct "HLK" as "[Histk6 [HLK|HLK]]";
- iExists istk6, w'; iSplit; auto; iFrame "#".
- iRight. iDestruct "HLK" as (? ? ? ?) "(?&?&?&?)".
- iExists _, _, _, _; iFrame "#".
+ iExists istk6, w'; iSplit; auto. iFrame "Histk6".
+ iDestruct "HLK" as (? ? ? ?) "(?&?&?&?)". iFrame "#".
Qed.
End Stack_refinement.
diff --git a/theories/spanning_tree/spanning.v b/theories/spanning_tree/spanning.v
index eadae373..64ee1f90 100644
--- a/theories/spanning_tree/spanning.v
+++ b/theories/spanning_tree/spanning.v
@@ -56,7 +56,7 @@ Section Helpers.
wp_load.
iDestruct "Hil1" as %Hil1. iDestruct "Hil2" as %Hil2.
iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3"; eauto.
- { iFrame. iExists _; eauto. iSplitR; eauto. iExists _; by iFrame. }
+ { by iFrame. }
iMod ("Hcl" with "[Hi1 Hi2 Hi3 Hi4]") as "_".
{ iNext. unfold graph_inv at 2. iExists _; iFrame; auto. }
iModIntro. wp_proj. wp_let.
@@ -78,7 +78,7 @@ Section Helpers.
- wp_cmpxchg_fail.
iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3";
eauto.
- { iFrame. iExists _; eauto. iSplitR; eauto. by iExists _; iFrame. }
+ { by iFrame. }
iMod (already_marked with "Hi2") as "[Hi2 Hxm]"; [|iFrame "Hxm"].
{ by eapply in_dom_of_graph. }
iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_".
@@ -93,7 +93,7 @@ Section Helpers.
erewrite delete_marked.
iDestruct (auth_own_graph_valid with "Hi1") as %Hvl'.
iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3".
- { iFrame. iExists (_, _). iSplitR; [| iExists _; iFrame]; trivial.
+ { iFrame "Hi3". iExists (_, _). iFrame.
rewrite mark_update_lookup; eauto. }
iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_".
+ iNext; unfold graph_inv at 2. iExists _; iFrame.
@@ -142,8 +142,7 @@ Section Helpers.
as %Heq; try by iFrame.
pose proof Hil1 as Hil1'. rewrite Heq in Hil1' Hvl.
rewrite mark_update_lookup in Hil1'; trivial.
- iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3"; [iFrame|].
- { iExists _; iSplitR; auto. iExists _; by iFrame. }
+ iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3"; [by iFrame|].
iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_".
{ iNext. unfold graph_inv at 2. iExists _; iFrame; auto. }
iFrame. inversion Hil1'; subst u'; simpl.
@@ -368,14 +367,13 @@ Section Helpers.
iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
destruct u1; destruct u2; inversion Hl1eq; inversion Hl2eq; subst.
iModIntro. iFrame; iLeft. iSplit; [trivial|].
- iExists _; iSplit; [trivial|]. iFrame.
- iDestruct (own_graph_valid with "Hx") as %Hvl.
- iExists ({[l := Excl (Some l1, Some l2)]} â‹… (G1 â‹… G2)).
+ iExists _; iSplit; [trivial|]. iFrame "Hm".
+ iDestruct (own_graph_valid with "Hx") as %Hvl. iFrame "Hx".
iDestruct (front_marked _ _ _ _ (Some l1, Some l2) _ _ G1 G2 with
"[ml1 ml2 Hfml Hfmr]") as (mr)"[Hfr Hfm]"; eauto. iDestruct "Hfr" as %Hfr.
- iExists mr.
+ iFrame "Hfm".
unshelve iExists _; [eapply maximally_marked_tree_both; eauto|].
- iFrame. iSplit; try iPureIntro; eauto.
+ iSplit; try iPureIntro; eauto.
{ rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
split; auto.
{ eapply maximally_marked_tree_both; eauto. }
@@ -393,9 +391,8 @@ Section Helpers.
iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
wp_seq. iModIntro.
iFrame; iLeft. iSplit; [trivial|].
- iExists _; iSplit; [trivial|]. iFrame.
- iDestruct (own_graph_valid with "Hx") as %Hvld.
- iExists ({[l := Excl (u1, None)]} â‹… G1).
+ iExists _; iSplit; [trivial|]. iFrame "Hm".
+ iDestruct (own_graph_valid with "Hx") as %Hvld. iFrame "Hx".
destruct u1; inversion Hl1eq; subst.
iDestruct (front_marked _ _ _ _ (Some l1, None) _ ∅ G1 ∅ with
"[ml1 Hvr Hfml]") as (mr)"[Hfr Hfm]"; eauto.
@@ -405,10 +402,9 @@ Section Helpers.
[iDestruct "Hvr" as %Hvr; inversion Hvr|
iDestruct "Hvr" as (l2) "[Hvreq Hvr]"; iDestruct "Hvreq" as %Hvreq;
by inversion Hvreq]. }
- iDestruct "Hfr" as %Hfr. rewrite right_id_L in Hfr.
- iExists mr.
+ iDestruct "Hfr" as %Hfr. rewrite right_id_L in Hfr. iFrame "Hfm".
unshelve iExists _; [eapply maximally_marked_tree_left; eauto|].
- iFrame. iSplit; try iPureIntro; eauto.
+ iSplit; try iPureIntro; eauto.
{ rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
split; auto.
{ eapply maximally_marked_tree_left; eauto. }
@@ -426,9 +422,8 @@ Section Helpers.
iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
wp_seq. wp_proj. wp_op. wp_if. wp_seq. iModIntro.
iFrame; iLeft. iSplit; [trivial|].
- iExists _; iSplit; [trivial|]. iFrame.
- iDestruct (own_graph_valid with "Hx") as %Hvld.
- iExists ({[l := Excl (None, u2)]} â‹… G2).
+ iExists _; iSplit; [trivial|]. iFrame "Hm".
+ iDestruct (own_graph_valid with "Hx") as %Hvld. iFrame "Hx".
destruct u2; inversion Hl2eq; subst.
iDestruct (front_marked _ _ _ _ (None, Some l2) ∅ _ ∅ G2 with
"[ml2 Hvl Hfmr]") as (mr)"[Hfr Hfm]"; eauto.
@@ -439,9 +434,9 @@ Section Helpers.
iDestruct "Hvl" as (l1) "[Hvleq Hvl]"; iDestruct "Hvleq" as %Hvleq;
by inversion Hvleq]. }
iDestruct "Hfr" as %Hfr. rewrite left_id_L in Hfr.
- iExists mr.
+ iFrame "Hfm".
unshelve iExists _; [eapply maximally_marked_tree_right; eauto|].
- iFrame. iSplit; try iPureIntro; eauto.
+ iSplit; try iPureIntro; eauto.
{ rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
split; auto.
{ eapply maximally_marked_tree_right; eauto. }
@@ -459,9 +454,8 @@ Section Helpers.
iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
wp_seq. iModIntro.
iFrame; iLeft. iSplit; [trivial|].
- iExists _; iSplit; [trivial|]. iFrame.
- iDestruct (own_graph_valid with "Hx") as %Hvld.
- iExists ({[l := Excl (None, None)]} ⋅ ∅).
+ iExists _; iSplit; [trivial|]. iFrame "Hm".
+ iDestruct (own_graph_valid with "Hx") as %Hvld. iFrame "Hx".
iDestruct (front_marked _ _ _ _ (None, None) ∅ ∅ ∅ ∅ with
"[Hvr Hvl]") as (mr)"[Hfr Hfm]"; eauto.
{ rewrite dom_empty_L; apply front_empty. }
@@ -477,10 +471,10 @@ Section Helpers.
iDestruct "Hvreq" as %Hvreq; inversion Hvreq);
iFrame; by repeat iSplit. }
iDestruct "Hfr" as %Hfr. rewrite left_id_L in Hfr.
- iExists mr.
+ iFrame "Hfm".
rewrite right_id_L. rewrite right_id_L in Hvld Hfr.
unshelve iExists _; [eapply maximally_marked_tree_none; eauto|].
- iFrame. iSplit; try iPureIntro; eauto.
+ iSplit; try iPureIntro; eauto.
{ by rewrite dom_singleton elem_of_singleton. }
split; auto.
{ eapply maximally_marked_tree_none; eauto. }
--
GitLab