Commit 908a83a4 by Ralf Jung

### simplify atomic triples as suggested by Robbert

parent c0647f6a
 ... @@ -18,6 +18,6 @@ Section atomic. ... @@ -18,6 +18,6 @@ Section atomic. (∀ P Q, (P ={Eo, Ei}=> ∃ x:A, (∀ P Q, (P ={Eo, Ei}=> ∃ x:A, α x ★ α x ★ ((α x ={Ei, Eo}=★ P) ∧ ((α x ={Ei, Eo}=★ P) ∧ (∀ v, β x v ={Ei, Eo}=★ Q x v)) (∀ v, β x v ={Ei, Eo}=★ Q v)) ) -★ {{ P }} e @ ⊤ {{ v, (∃ x: A, Q x v) }})%I. ) -★ {{ P }} e @ ⊤ {{ Q }})%I. End atomic. End atomic.
 ... @@ -46,7 +46,7 @@ Section incr. ... @@ -46,7 +46,7 @@ Section incr. iSpecialize ("Hvs'" \$! #x'). iSpecialize ("Hvs'" \$! #x'). wp_cas_suc. wp_cas_suc. iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame. iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame. iModIntro. wp_if. by iExists x'. iModIntro. wp_if. done. - iDestruct "Hvs'" as "[Hvs' _]". - iDestruct "Hvs'" as "[Hvs' _]". wp_cas_fail. wp_cas_fail. iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame. iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame. ... @@ -80,7 +80,7 @@ Section user. ... @@ -80,7 +80,7 @@ Section user. (* prove worker triple *) (* prove worker triple *) iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//. iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//. rewrite /incr_triple /atomic_triple. rewrite /incr_triple /atomic_triple. iSpecialize ("Hincr" \$! True%I (fun _ _ => True%I) with "[]"). iSpecialize ("Hincr" \$! True%I (fun _ => True%I) with "[]"). - iIntros "!# _". - iIntros "!# _". (* open the invariant *) (* open the invariant *) iInv N as (x') ">Hl'" "Hclose". iInv N as (x') ">Hl'" "Hclose". ... ...
 ... @@ -59,7 +59,7 @@ Section atomic_sync. ... @@ -59,7 +59,7 @@ Section atomic_sync. iAlways. iIntros (α β x) "#Hseq". iAlways. iIntros (α β x) "#Hseq". iIntros (P Q) "#Hvss !# HP". iIntros (P Q) "#Hvss !# HP". (* TODO: Why can't I iApply "Hsynced"? *) (* TODO: Why can't I iApply "Hsynced"? *) iSpecialize ("Hsynced" \$! P (fun v => ∃ x, Q x v)%I x). iSpecialize ("Hsynced" \$! P Q x). iApply wp_wand_r. iSplitL "HP". iApply wp_wand_r. iSplitL "HP". - iApply ("Hsynced" with "[]")=>//. - iApply ("Hsynced" with "[]")=>//. iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]". iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]". ... @@ -81,7 +81,7 @@ Section atomic_sync. ... @@ -81,7 +81,7 @@ Section atomic_sync. apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. } apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. } iMod ("Hvs2" with "[Hg1 Hβ]"). iMod ("Hvs2" with "[Hg1 Hβ]"). { iExists g'. iFrame. } { iExists g'. iFrame. } iModIntro. iSplitL "Hg2 Hϕ'"; last by iExists g''. iModIntro. iSplitL "Hg2 Hϕ'"; last done. iExists g'. by iFrame. iExists g'. by iFrame. - iIntros (?) "?". done. - iIntros (?) "?". done. Qed. Qed. ... ...
 ... @@ -133,7 +133,7 @@ Lemma new_stack_spec' Φ RI: ... @@ -133,7 +133,7 @@ Lemma new_stack_spec' Φ RI: Proof. Proof. iIntros (HN) "(#Hh & HRx & #? & HΦ)". iIntros (HN) "(#Hh & HRx & #? & HΦ)". iDestruct (push_atomic_spec N s x with "Hh") as "Hpush"=>//. iDestruct (push_atomic_spec N s x with "Hh") as "Hpush"=>//. iSpecialize ("Hpush" \$! (R x) (fun _ ret => (∃ hd, evs γ hd x) ★ ret = #())%I with "[]"). iSpecialize ("Hpush" \$! (R x) (fun ret => (∃ hd, evs γ hd x) ★ ret = #())%I with "[]"). - iIntros "!# Rx". - iIntros "!# Rx". (* open the invariant *) (* open the invariant *) iInv N as "[IH1 ?]" "Hclose". iInv N as "[IH1 ?]" "Hclose". ... @@ -180,7 +180,7 @@ Lemma new_stack_spec' Φ RI: ... @@ -180,7 +180,7 @@ Lemma new_stack_spec' Φ RI: iModIntro. iSplitL; last auto. by iExists hd'. iModIntro. iSplitL; last auto. by iExists hd'. - iApply wp_wand_r. iSplitL "HRx Hpush". - iApply wp_wand_r. iSplitL "HRx Hpush". + by iApply "Hpush". + by iApply "Hpush". + iIntros (?) "H". iDestruct "H" as (_) "[? %]". subst. + iIntros (?) "[? %]". subst. by iApply "HΦ". by iApply "HΦ". Qed. Qed. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!