Commit c728bfdf authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup

parent 7aed15f2
......@@ -1556,11 +1556,10 @@ Lemma find_tail_repeat_spec γ γh γl γg q tid :
SeenEnqueuedLink_val G.(Es) T L η' (l >> link) }}}.
Proof.
iIntros (Φ) "#T Post".
iLöb as "IH" forall "#".
wp_rec.
iLöb as "IH". wp_rec.
wp_apply (find_tail_spec with "T").
iIntros (n) "[%|P]".
- subst n. wp_let. wp_op. wp_if. by iApply ("IH" with "Post T").
- subst n. wp_let. wp_op. wp_if. by iApply ("IH" with "Post").
- iClear "#". iDestruct "P" as (l ?) "P".
subst n. wp_let. wp_op. wp_if. by iApply "Post".
Qed.
......@@ -2367,9 +2366,7 @@ Lemma atom_enqueue :
Proof.
intros q tid γg G1 M V v Posx.
iIntros "#sV #Gs" (Φ) "AU".
iLöb as "IH" forall "#".
wp_rec.
iLöb as "IH". wp_rec.
awp_apply (atom_try_enq _ _ γg with "sV Gs"); [eauto..|].
iApply (aacc_aupd with "AU"); [done|].
iIntros (G) "QI".
......@@ -2381,7 +2378,7 @@ Proof.
- iLeft. iDestruct "QI" as "(QI & sV' & Local & Le)".
iDestruct "Le" as %(?&?&?&?&?).
subst G'. iFrame "QI". iIntros "AU !> _".
wp_if. by iApply ("IH" with "AU sV Gs").
wp_if. by iApply ("IH" with "AU").
Qed.
#[local] Transparent QueueLocal.
......@@ -3460,9 +3457,7 @@ Lemma atom_dequeue :
dequeue_spec' dequeue ( msqueueRootN) QueueLocal QueueInv.
Proof.
intros q tid γg G1 M V. iIntros "#sV #Gs" (Φ) "AU".
iLöb as "IH" forall "#".
wp_rec.
iLöb as "IH". wp_rec.
awp_apply (atom_try_deq with "sV Gs").
iApply (aacc_aupd with "AU"); [done|].
iIntros (G) "QI".
......@@ -3473,7 +3468,7 @@ Proof.
- destruct CASE as (?&?). subst G'. iLeft.
iFrame "QI". iIntros "AU !> _".
wp_let. wp_op. rewrite bool_decide_false; last lia.
wp_if. by iApply ("IH" with "AU sV Gs").
wp_if. by iApply ("IH" with "AU").
- iRight.
iExists x, V', G'. iExists enqId, deqId, enq, deq, Vdeq, M'.
iFrame "QI sV' Local". iSplit; [done|]. iIntros "H !> _".
......
......@@ -1274,9 +1274,7 @@ Lemma push_spec N (SUB: ↑N ⊆ Eo) (DISJ: N ## histN) :
Proof.
intros s tid γg G0 M V v Posv.
iIntros "#sV #SL" (Φ) "AU".
iLöb as "IH".
wp_rec.
iLöb as "IH". wp_rec.
awp_apply (try_push_spec with "sV SL"); [done..|].
iApply (aacc_aupd with "AU"); [done|].
iIntros (G) "QI".
......@@ -1285,8 +1283,7 @@ Proof.
iDestruct "CASE" as %[(-> & -> & ->)|[-> F]].
- iLeft. iFrame "QI". iIntros "AU !> _".
wp_if. by iApply ("IH" with "AU").
- iRight.
iExists V', G', psId, ps, Vps, M'.
- iRight. iExists V', G', psId, ps, Vps, M'.
iFrame "QI sV' SL'". iSplit; [done|].
iIntros "HΦ !> _". wp_if. by iApply "HΦ".
Qed.
......@@ -2436,9 +2433,7 @@ Lemma pop_spec N (SUB: ↑N ⊆ Eo) (DISJ: N ## histN) :
Proof.
intros s tid γg G0 M V.
iIntros "#sV #SL" (Φ) "AU".
iLöb as "IH".
wp_rec.
iLöb as "IH". wp_rec.
awp_apply (try_pop_spec with "sV SL"); [done..|].
iApply (aacc_aupd with "AU"); [done|].
iIntros (G) "QI".
......@@ -2461,5 +2456,4 @@ Proof.
+ iIntros "H !> _". wp_let. wp_op. rewrite bool_decide_false; [|lia].
wp_if. by iApply "H".
Qed.
End proof.
......@@ -2079,7 +2079,7 @@ Lemma atom_pop :
Proof.
intros s tid γg G1 M V.
iIntros "#sV #Gs" (Φ) "AU".
iLöb as "IH" forall "#".
iLöb as "IH".
wp_rec.
awp_apply (atom_try_pop with "sV Gs"); [eauto..|].
......@@ -2090,7 +2090,7 @@ Proof.
iDestruct "CASE" as "[CASE|[CASE|CASE]]".
- iLeft. iDestruct "CASE" as %(-> & -> & ->).
iFrame "QI". iIntros "AU !> _".
wp_let. wp_op. wp_if. by iApply ("IH" with "AU sV Gs").
wp_let. wp_op. wp_if. by iApply ("IH" with "AU").
- iRight. iClear "IH". iDestruct "CASE" as %[? ?].
iExists v, V', G', psId, ppId, ps, pp. iExists Vpp, M'.
iFrame "QI sV' Local F". iSplitL.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment