Commit c7bd7639 authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify proofs of lock.

parent 46648f14
......@@ -57,7 +57,7 @@ Proof.
wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
iPvs (inv_alloc N _ (lock_inv γ l R) with "-[HΦ]") as "#?"; first done.
{ iNext. iExists false. by iFrame "Hl HR". }
{ iIntros ">". iExists false. by iFrame "Hl HR". }
iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit.
Qed.
......@@ -78,11 +78,9 @@ Qed.
Lemma release_spec R l (Φ : val iProp) :
(locked l R R Φ #()) WP release #l {{ Φ }}.
Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(%&#?&#?&Hγ)".
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)".
rewrite /release. wp_let.
iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl Hγ']"; destruct b.
- wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
- wp_store. iDestruct "Hγ'" as "[Hγ' _]".
iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%".
iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl _]".
wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
Qed.
End proof.
Markdown is supported
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