Commit 1ff665fc authored by Ralf Jung's avatar Ralf Jung

rename _open rules to _access if they are actually accessors

parent 740affc3
......@@ -112,7 +112,7 @@ Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ :
inv N P ( P - WP e @ E N {{ v, P Φ v }}) WP e @ E {{ Φ }}.
Proof.
iIntros (??) "[#Hinv Hwp]".
iMod (inv_open E N P with "Hinv") as "[HP Hclose]"=>//.
iMod (inv_access E N P with "Hinv") as "[HP Hclose]"=>//.
iApply wp_wand_r; iSplitL "HP Hwp"; [by iApply "Hwp"|].
iIntros (v) "[HP $]". by iApply "Hclose".
Qed.
......
......@@ -132,7 +132,7 @@ Section auth.
Lemma auth_empty γ : (|==> auth_own γ ε)%I.
Proof. by rewrite /auth_own -own_unit. Qed.
Lemma auth_acc E γ a :
Lemma auth_inv_acc E γ a :
auth_inv γ f φ auth_own γ a ={E}= t,
a f t φ t u b,
(f t, a) ~l~> (f u, b) φ u ={E}= auth_inv γ f φ auth_own γ b.
......@@ -147,7 +147,7 @@ Section auth.
iModIntro. iFrame. iExists u. iFrame.
Qed.
Lemma auth_open E N γ a :
Lemma auth_access E N γ a :
N E
auth_ctx γ N f φ auth_own γ a ={E,E∖↑N}= t,
a f t φ t u b,
......@@ -155,15 +155,15 @@ Section auth.
Proof using Type*.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
[auth_acc] and [inv_open] -- but since we don't have any good support
[auth_inv_acc] and [inv_access] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having
to unpack and repack various proofs.
TODO: Make this mostly automatic, by supporting "opening accessors
around accessors". *)
iMod (auth_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
iMod (auth_inv_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
iModIntro. iExists t. iFrame. iIntros (u b) "H".
iMod ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
Qed.
End auth.
Arguments auth_open {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
Arguments auth_access {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
......@@ -109,13 +109,13 @@ Section proofs.
Qed.
(*** Accessors *)
Lemma cinv_open_strong E N γ p P :
Lemma cinv_access_strong E N γ p P :
N E
cinv N γ P - (cinv_own γ p ={E,E∖↑N}=
P cinv_own γ p ( E' : coPset, P cinv_own γ 1 ={E',N E'}= True)).
Proof.
iIntros (?) "Hinv Hown".
iPoseProof (inv_open ( N) N with "Hinv") as "H"; first done.
iPoseProof (inv_access ( N) N with "Hinv") as "H"; first done.
rewrite difference_diag_L.
iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver.
rewrite left_id_L -union_difference_L //. iMod "H" as "[[$ | >Hown'] H]".
......@@ -126,12 +126,12 @@ Section proofs.
- iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
Qed.
Lemma cinv_open E N γ p P :
Lemma cinv_access E N γ p P :
N E
cinv N γ P - cinv_own γ p ={E,E∖↑N}= P cinv_own γ p ( P ={E∖↑N,E}= True).
Proof.
iIntros (?) "#Hinv Hγ".
iMod (cinv_open_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
iMod (cinv_access_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
iIntros "!> HP".
rewrite {2}(union_difference_L (N) E)=> //.
iApply "H". by iLeft.
......@@ -141,7 +141,7 @@ Section proofs.
Lemma cinv_cancel E N γ P : N E cinv N γ P - cinv_own γ 1 ={E}= P.
Proof.
iIntros (?) "#Hinv Hγ".
iMod (cinv_open_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
iMod (cinv_access_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
rewrite {2}(union_difference_L (N) E)=> //.
iApply "H". by iRight.
Qed.
......@@ -155,7 +155,7 @@ Section proofs.
Proof.
rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".
rewrite exist_unit -assoc.
iApply (cinv_open with "Hinv"); done.
iApply (cinv_access with "Hinv"); done.
Qed.
End proofs.
......
......@@ -27,7 +27,7 @@ Section inv.
Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i (N:coPset) ownI i P)%I.
Lemma own_inv_open E N P :
Lemma own_inv_access E N P :
N E own_inv N P ={E,E∖↑N}= P ( P ={E∖↑N,E}= True).
Proof.
rewrite uPred_fupd_eq /uPred_fupd_def. iDestruct 1 as (i) "[Hi #HiP]".
......@@ -81,7 +81,7 @@ Section inv.
Lemma own_inv_to_inv M P: own_inv M P - inv M P.
Proof.
iIntros "#I". rewrite inv_eq. iIntros (E H).
iPoseProof (own_inv_open with "I") as "H"; eauto.
iPoseProof (own_inv_access with "I") as "H"; eauto.
Qed.
(** ** Public API of invariants *)
......@@ -127,7 +127,7 @@ Section inv.
iApply own_inv_to_inv. done.
Qed.
Lemma inv_open E N P :
Lemma inv_access E N P :
N E inv N P ={E,E∖↑N}= P ( P ={E∖↑N,E}= True).
Proof.
rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
......@@ -146,11 +146,11 @@ Section inv.
Qed.
(** ** Derived properties *)
Lemma inv_open_strong E N P :
Lemma inv_access_strong E N P :
N E inv N P ={E,E∖↑N}= P E', P ={E',N E'}= True.
Proof.
iIntros (?) "Hinv".
iPoseProof (inv_open ( N) N with "Hinv") as "H"; first done.
iPoseProof (inv_access ( N) N with "Hinv") as "H"; first done.
rewrite difference_diag_L.
iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver.
rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
......@@ -159,10 +159,10 @@ Section inv.
by rewrite left_id_L.
Qed.
Lemma inv_open_timeless E N P `{!Timeless P} :
Lemma inv_access_timeless E N P `{!Timeless P} :
N E inv N P ={E,E∖↑N}= P (P ={E∖↑N,E}= True).
Proof.
iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
iIntros (?) "Hinv". iMod (inv_access with "Hinv") as "[>HP Hclose]"; auto.
iIntros "!> {$HP} HP". iApply "Hclose"; auto.
Qed.
......
......@@ -91,7 +91,7 @@ Section proofs.
iNext. iLeft. by iFrame.
Qed.
Lemma na_inv_open p E F N P :
Lemma na_inv_access p E F N P :
N E N F
na_inv p N P - na_own p F ={E}= P na_own p (F∖↑N)
( P na_own p (F∖↑N) ={E}= na_own p F).
......@@ -121,6 +121,6 @@ Section proofs.
Proof.
rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
rewrite exist_unit -assoc /=.
iApply (na_inv_open with "Hinv"); done.
iApply (na_inv_access with "Hinv"); done.
Qed.
End proofs.
......@@ -126,7 +126,7 @@ Section sts.
rewrite /sts_inv. iNext. iExists s. by iFrame.
Qed.
Lemma sts_accS φ E γ S T :
Lemma sts_inv_accS φ E γ S T :
sts_inv γ φ sts_ownS γ S T ={E}= s,
s S φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E}= sts_inv γ φ sts_own γ s' T'.
......@@ -144,13 +144,13 @@ Section sts.
iModIntro. iNext. iExists s'; by iFrame.
Qed.
Lemma sts_acc φ E γ s0 T :
Lemma sts_inv_acc φ E γ s0 T :
sts_inv γ φ sts_own γ s0 T ={E}= s,
sts.frame_steps T s0 s φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E}= sts_inv γ φ sts_own γ s' T'.
Proof. by apply sts_accS. Qed.
Proof. by apply sts_inv_accS. Qed.
Lemma sts_openS φ E N γ S T :
Lemma sts_accessS φ E N γ S T :
N E
sts_ctx γ N φ sts_ownS γ S T ={E,E∖↑N}= s,
s S φ s s' T',
......@@ -158,22 +158,22 @@ Section sts.
Proof.
iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
[sts_acc] and [inv_open] -- but since we don't have any good support
[sts_inv_acc] and [inv_access] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having
to unpack and repack various proofs.
TODO: Make this mostly automatic, by supporting "opening accessors
around accessors". *)
iMod (sts_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
iMod (sts_inv_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
iModIntro. iExists s. iFrame. iIntros (s' T') "H".
iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
Qed.
Lemma sts_open φ E N γ s0 T :
Lemma sts_access φ E N γ s0 T :
N E
sts_ctx γ N φ sts_own γ s0 T ={E,E∖↑N}= s,
sts.frame_steps T s0 s φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E∖↑N,E}= sts_own γ s' T'.
Proof. by apply sts_openS. Qed.
Proof. by apply sts_accessS. Qed.
End sts.
Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
......@@ -87,7 +87,7 @@ Module inv. Section inv.
Arguments inv _ _%I.
Hypothesis inv_persistent : i P, Persistent (inv i P).
Hypothesis inv_alloc : P, P fupd M1 ( i, inv i P).
Hypothesis inv_open :
Hypothesis inv_fupd :
i P Q R, (P Q fupd M0 (P R)) (inv i P Q fupd M1 R).
(* We have tokens for a little "two-state STS": [start] -> [finish].
......@@ -113,9 +113,9 @@ Module inv. Section inv.
Hypothesis consistency : ¬ (fupd M1 False).
(** Some general lemmas and proof mode compatibility. *)
Lemma inv_open' i P R : inv i P (P - fupd M0 (P fupd M1 R)) fupd M1 R.
Lemma inv_fupd' i P R : inv i P (P - fupd M0 (P fupd M1 R)) fupd M1 R.
Proof.
iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first.
iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_fupd; last first.
{ iSplit; first done. iExact "HP". }
iIntros "(HP & HPw)". by iApply "HPw".
Qed.
......@@ -167,7 +167,7 @@ Module inv. Section inv.
Lemma saved_cast γ P Q : saved γ P saved γ Q P fupd M1 ( Q).
Proof.
iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
iApply (inv_open' i). iSplit; first done.
iApply (inv_fupd' i). iSplit; first done.
iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf".
{ iDestruct "HaP" as "[Hs | [Hf _]]".
- by iApply start_finish.
......@@ -176,7 +176,7 @@ Module inv. Section inv.
iApply fupd_intro. iSplitL "Hf'"; first by eauto.
(* Step 2: Open the Q-invariant. *)
iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ".
iApply (inv_open' i). iSplit; first done.
iApply (inv_fupd' i). iSplit; first done.
iIntros "[HaQ | [_ #HQ]]".
{ iExFalso. iApply finished_not_start. by iFrame. }
iApply fupd_intro. iSplitL "Hf".
......
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