Commit 964f1cfe authored by Ralf Jung's avatar Ralf Jung

add a tactic for the final introduction of an atomic accessor

parent bb978c7d
......@@ -450,6 +450,13 @@ Tactic Notation "iAuIntro" :=
| iSolveTC || fail "iAuIntro: not all spatial assumptions are laterable"
| (* P = ...: make the P pretty *) pm_reflexivity
| (* the new proof mode goal *) ].
Tactic Notation "iAaccIntro" "with" constr(sel) :=
iStartProof; lazymatch goal with
| |- environments.envs_entails _ (@atomic_acc ?PROP ?H ?TA ?TB ?Eo ?Ei ?α ?P ?β ?Φ) =>
iApply (@aacc_intro PROP H TA TB Eo Ei α P β Φ with sel);
first try solve_ndisj; last iSplit
| _ => fail "iAAccIntro: Goal is not an atomic accessor"
end.
(* From here on, prevent TC search from implicitly unfolding these. *)
Typeclasses Opaque atomic_acc atomic_update.
......@@ -27,22 +27,14 @@ Section increment.
wp_apply (load_spec with "[HQ]"); first by iAccu.
(* Prove the atomic update for load *)
iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
iIntros (x) "H↦".
(* FIXME: Oh wow this is bad. *)
iApply (aacc_intro $! ([tele_arg _; _] : [tele (_:val) (_:Qp)]) with "[H↦]"); [solve_ndisj|done|iSplit].
{ iIntros "$ !> $ !> //". }
iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "$ !> AU !> HQ".
(* Now go on *)
wp_let. wp_op. wp_bind (CAS _ _ _)%I.
wp_apply (cas_spec with "[HQ]"); [done|iAccu|].
(* Prove the atomic update for CAS *)
iAuIntro. iApply (aacc_aupd with "AU"); first done.
iIntros (x') "H↦".
(* FIXME: Oh wow this is bad. *)
iApply (aacc_intro $! ([tele_arg _] : [tele (_:val)]) with "[H↦]"); [solve_ndisj|simpl; by auto with iFrame|iSplit].
{ eauto 10 with iFrame. }
(* FIXME: Manual reduction should not be needed. *)
reduction.pm_reduce.
iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
iIntros "H↦ !>".
destruct (decide (#x' = #x)) as [[= ->]|Hx].
- iRight. iFrame. iIntros "HΦ !> HQ".
......@@ -73,10 +65,8 @@ Section increment.
iAuIntro. iApply (aacc_aupd_commit with "AU"); first done.
iIntros (x) "H↦".
iDestruct (mapsto_agree with "Hl H↦") as %[= <-].
iCombine "Hl" "H↦" as "Hl".
(* FIXME: Oh wow this is bad. *)
iApply (aacc_intro $! ([tele_arg _] : [tele (_:val)]) with "[Hl]"); [solve_ndisj|done|simpl; iSplit].
{ simpl. iIntros "[$ $] !> $ !> //". }
iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl".
{ iIntros "[$ $]"; eauto. }
iIntros "$ !>". iSplit; first done.
iIntros "HΦ !> HQ". wp_seq. iApply "HΦ". done.
Qed.
......@@ -101,11 +91,8 @@ Section increment_client.
(* FIXME: I am only using persistent stuff, so I should be allowed
to move this to the persisten context even without the additional □. *)
iAssert ( WP incr #l {{ _, True }})%I as "#Aupd".
{ iAlways. wp_apply (incr_spec with "[]"); first by iAccu. clear x.
iAuIntro. iInv nroot as (x) ">H↦".
(* FIXME: Oh wow this is bad. *)
iApply (aacc_intro $! ([tele_arg _] : [tele (_:Z)]) with "[H↦]"); [solve_ndisj|done|iSplit].
{ by eauto 10. }
{ iAlways. wp_apply incr_spec; first by iAccu. clear x.
iAuIntro. iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10.
(* The continuation: From after the atomic triple to the postcondition of the WP *)
done.
......
......@@ -104,8 +104,7 @@ Section lemmas.
Proof.
rewrite ->tforall_forall in HL.
iIntros "Hwp" (Φ x) "Hα HΦ". iApply ("Hwp" with "[HΦ]"); first iAccu.
iAuIntro. iApply (aacc_intro with "Hα"); first solve_ndisj.
iSplit; first by eauto. iIntros (y) "Hβ !>".
iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
(* FIXME: Using ssreflect rewrite does not work? *)
rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
Qed.
......
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