Commit 22d31260 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/access' into 'master'

rename _open rules to _access if they are actually accessors

See merge request !373
parents bc17fc9e 357adad7
...@@ -54,6 +54,15 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -54,6 +54,15 @@ Coq development, but not every API-breaking change is listed. Changes marked
backwards incompatibility. This can usually be fixed by manually clearing some backwards incompatibility. This can usually be fixed by manually clearing some
hypotheses. A more detailed description of the changes can be found in hypotheses. A more detailed description of the changes can be found in
https://gitlab.mpi-sws.org/iris/iris/merge_requests/341. https://gitlab.mpi-sws.org/iris/iris/merge_requests/341.
* Renamed some accessor-style lemmas to consistently use the suffix `_acc`
instead of `_open`:
`inv_open` -> `inv_acc`, `inv_open_strong` -> `inv_acc_strong`,
`inv_open_timeless` -> `inv_acc_timeless`, `na_inv_open` -> `na_inv_acc`,
`cinv_open` -> `cinv_acc`, `cinv_open_strong` -> `cinv_acc_strong`,
`auth_open` -> `auth_acc`, `sts_open` -> `sts_acc`.
To make this work we also had to rename `inv_acc` -> `inv_alter`.
(Most developments should be unaffected as the typical way to invoke these
lemmas is through `iInv`, and that does not change.)
## Iris 3.2.0 (released 2019-08-29) ## Iris 3.2.0 (released 2019-08-29)
......
...@@ -112,7 +112,7 @@ Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ : ...@@ -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 {{ Φ }}. inv N P ( P - WP e @ E N {{ v, P Φ v }}) WP e @ E {{ Φ }}.
Proof. Proof.
iIntros (??) "[#Hinv Hwp]". iIntros (??) "[#Hinv Hwp]".
iMod (inv_open E N P with "Hinv") as "[HP Hclose]"=>//. iMod (inv_acc E N P with "Hinv") as "[HP Hclose]"=>//.
iApply wp_wand_r; iSplitL "HP Hwp"; [by iApply "Hwp"|]. iApply wp_wand_r; iSplitL "HP Hwp"; [by iApply "Hwp"|].
iIntros (v) "[HP $]". by iApply "Hclose". iIntros (v) "[HP $]". by iApply "Hclose".
Qed. Qed.
......
...@@ -132,7 +132,7 @@ Section auth. ...@@ -132,7 +132,7 @@ Section auth.
Lemma auth_empty γ : (|==> auth_own γ ε)%I. Lemma auth_empty γ : (|==> auth_own γ ε)%I.
Proof. by rewrite /auth_own -own_unit. Qed. 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, auth_inv γ f φ auth_own γ a ={E}= t,
a f t φ t u b, a f t φ t u b,
(f t, a) ~l~> (f u, b) φ u ={E}= auth_inv γ f φ auth_own γ b. (f t, a) ~l~> (f u, b) φ u ={E}= auth_inv γ f φ auth_own γ b.
...@@ -147,7 +147,7 @@ Section auth. ...@@ -147,7 +147,7 @@ Section auth.
iModIntro. iFrame. iExists u. iFrame. iModIntro. iFrame. iExists u. iFrame.
Qed. Qed.
Lemma auth_open E N γ a : Lemma auth_acc E N γ a :
N E N E
auth_ctx γ N f φ auth_own γ a ={E,E∖↑N}= t, auth_ctx γ N f φ auth_own γ a ={E,E∖↑N}= t,
a f t φ t u b, a f t φ t u b,
...@@ -155,15 +155,15 @@ Section auth. ...@@ -155,15 +155,15 @@ Section auth.
Proof using Type*. Proof using Type*.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose". iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors (* 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_acc] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having for that currently, this gets more tedious than it should, with us having
to unpack and repack various proofs. to unpack and repack various proofs.
TODO: Make this mostly automatic, by supporting "opening accessors TODO: Make this mostly automatic, by supporting "opening accessors
around 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". iModIntro. iExists t. iFrame. iIntros (u b) "H".
iMod ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv"). iMod ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
Qed. Qed.
End auth. End auth.
Arguments auth_open {_ _ _} [_] {_} [_] _ _ _ _ _ _ _. Arguments auth_acc {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
...@@ -109,13 +109,13 @@ Section proofs. ...@@ -109,13 +109,13 @@ Section proofs.
Qed. Qed.
(*** Accessors *) (*** Accessors *)
Lemma cinv_open_strong E N γ p P : Lemma cinv_acc_strong E N γ p P :
N E N E
cinv N γ P - (cinv_own γ p ={E,E∖↑N}= cinv N γ P - (cinv_own γ p ={E,E∖↑N}=
P cinv_own γ p ( E' : coPset, P cinv_own γ 1 ={E',N E'}= True)). P cinv_own γ p ( E' : coPset, P cinv_own γ 1 ={E',N E'}= True)).
Proof. Proof.
iIntros (?) "Hinv Hown". iIntros (?) "Hinv Hown".
iPoseProof (inv_open ( N) N with "Hinv") as "H"; first done. iPoseProof (inv_acc ( N) N with "Hinv") as "H"; first done.
rewrite difference_diag_L. rewrite difference_diag_L.
iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver. 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]". rewrite left_id_L -union_difference_L //. iMod "H" as "[[$ | >Hown'] H]".
...@@ -126,12 +126,12 @@ Section proofs. ...@@ -126,12 +126,12 @@ Section proofs.
- iDestruct (cinv_own_1_l with "Hown' Hown") as %[]. - iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
Qed. Qed.
Lemma cinv_open E N γ p P : Lemma cinv_acc E N γ p P :
N E N E
cinv N γ P - cinv_own γ p ={E,E∖↑N}= P cinv_own γ p ( P ={E∖↑N,E}= True). cinv N γ P - cinv_own γ p ={E,E∖↑N}= P cinv_own γ p ( P ={E∖↑N,E}= True).
Proof. Proof.
iIntros (?) "#Hinv Hγ". iIntros (?) "#Hinv Hγ".
iMod (cinv_open_strong with "Hinv Hγ") as "($ & $ & H)"; first done. iMod (cinv_acc_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
iIntros "!> HP". iIntros "!> HP".
rewrite {2}(union_difference_L (N) E)=> //. rewrite {2}(union_difference_L (N) E)=> //.
iApply "H". by iLeft. iApply "H". by iLeft.
...@@ -141,7 +141,7 @@ Section proofs. ...@@ -141,7 +141,7 @@ Section proofs.
Lemma cinv_cancel E N γ P : N E cinv N γ P - cinv_own γ 1 ={E}= P. Lemma cinv_cancel E N γ P : N E cinv N γ P - cinv_own γ 1 ={E}= P.
Proof. Proof.
iIntros (?) "#Hinv Hγ". iIntros (?) "#Hinv Hγ".
iMod (cinv_open_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done. iMod (cinv_acc_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
rewrite {2}(union_difference_L (N) E)=> //. rewrite {2}(union_difference_L (N) E)=> //.
iApply "H". by iRight. iApply "H". by iRight.
Qed. Qed.
...@@ -155,7 +155,7 @@ Section proofs. ...@@ -155,7 +155,7 @@ Section proofs.
Proof. Proof.
rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown". rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".
rewrite exist_unit -assoc. rewrite exist_unit -assoc.
iApply (cinv_open with "Hinv"); done. iApply (cinv_acc with "Hinv"); done.
Qed. Qed.
End proofs. End proofs.
......
...@@ -27,7 +27,7 @@ Section inv. ...@@ -27,7 +27,7 @@ Section inv.
Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ := Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i (N:coPset) ownI i P)%I. ( i, i (N:coPset) ownI i P)%I.
Lemma own_inv_open E N P : Lemma own_inv_acc E N P :
N E own_inv N P ={E,E∖↑N}= P ( P ={E∖↑N,E}= True). N E own_inv N P ={E,E∖↑N}= P ( P ={E∖↑N,E}= True).
Proof. Proof.
rewrite uPred_fupd_eq /uPred_fupd_def. iDestruct 1 as (i) "[Hi #HiP]". rewrite uPred_fupd_eq /uPred_fupd_def. iDestruct 1 as (i) "[Hi #HiP]".
...@@ -81,7 +81,7 @@ Section inv. ...@@ -81,7 +81,7 @@ Section inv.
Lemma own_inv_to_inv M P: own_inv M P - inv M P. Lemma own_inv_to_inv M P: own_inv M P - inv M P.
Proof. Proof.
iIntros "#I". rewrite inv_eq. iIntros (E H). iIntros "#I". rewrite inv_eq. iIntros (E H).
iPoseProof (own_inv_open with "I") as "H"; eauto. iPoseProof (own_inv_acc with "I") as "H"; eauto.
Qed. Qed.
(** ** Public API of invariants *) (** ** Public API of invariants *)
...@@ -97,7 +97,7 @@ Section inv. ...@@ -97,7 +97,7 @@ Section inv.
Global Instance inv_persistent N P : Persistent (inv N P). Global Instance inv_persistent N P : Persistent (inv N P).
Proof. rewrite inv_eq. apply _. Qed. Proof. rewrite inv_eq. apply _. Qed.
Lemma inv_acc N P Q: Lemma inv_alter N P Q:
inv N P - (P - Q (Q - P)) - inv N Q. inv N P - (P - Q (Q - P)) - inv N Q.
Proof. Proof.
rewrite inv_eq. iIntros "#HI #Acc !>" (E H). rewrite inv_eq. iIntros "#HI #Acc !>" (E H).
...@@ -108,7 +108,7 @@ Section inv. ...@@ -108,7 +108,7 @@ Section inv.
Lemma inv_iff N P Q : (P Q) - inv N P - inv N Q. Lemma inv_iff N P Q : (P Q) - inv N P - inv N Q.
Proof. Proof.
iIntros "#HPQ #HI". iApply (inv_acc with "HI"). iIntros "#HPQ #HI". iApply (inv_alter with "HI").
iIntros "!> !# HP". iSplitL "HP". iIntros "!> !# HP". iSplitL "HP".
- by iApply "HPQ". - by iApply "HPQ".
- iIntros "HQ". by iApply "HPQ". - iIntros "HQ". by iApply "HPQ".
...@@ -127,7 +127,7 @@ Section inv. ...@@ -127,7 +127,7 @@ Section inv.
iApply own_inv_to_inv. done. iApply own_inv_to_inv. done.
Qed. Qed.
Lemma inv_open E N P : Lemma inv_acc E N P :
N E inv N P ={E,E∖↑N}= P ( P ={E∖↑N,E}= True). N E inv N P ={E,E∖↑N}= P ( P ={E∖↑N,E}= True).
Proof. Proof.
rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI". rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
...@@ -146,11 +146,11 @@ Section inv. ...@@ -146,11 +146,11 @@ Section inv.
Qed. Qed.
(** ** Derived properties *) (** ** Derived properties *)
Lemma inv_open_strong E N P : Lemma inv_acc_strong E N P :
N E inv N P ={E,E∖↑N}= P E', P ={E',N E'}= True. N E inv N P ={E,E∖↑N}= P E', P ={E',N E'}= True.
Proof. Proof.
iIntros (?) "Hinv". iIntros (?) "Hinv".
iPoseProof (inv_open ( N) N with "Hinv") as "H"; first done. iPoseProof (inv_acc ( N) N with "Hinv") as "H"; first done.
rewrite difference_diag_L. rewrite difference_diag_L.
iPoseProof (fupd_mask_frame_r _ _ (E N) with "H") as "H"; first set_solver. 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. rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
...@@ -159,16 +159,16 @@ Section inv. ...@@ -159,16 +159,16 @@ Section inv.
by rewrite left_id_L. by rewrite left_id_L.
Qed. Qed.
Lemma inv_open_timeless E N P `{!Timeless P} : Lemma inv_acc_timeless E N P `{!Timeless P} :
N E inv N P ={E,E∖↑N}= P (P ={E∖↑N,E}= True). N E inv N P ={E,E∖↑N}= P (P ={E∖↑N,E}= True).
Proof. Proof.
iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto. iIntros (?) "Hinv". iMod (inv_acc with "Hinv") as "[>HP Hclose]"; auto.
iIntros "!> {$HP} HP". iApply "Hclose"; auto. iIntros "!> {$HP} HP". iApply "Hclose"; auto.
Qed. Qed.
Lemma inv_sep_l N P Q : inv N (P Q) - inv N P. Lemma inv_sep_l N P Q : inv N (P Q) - inv N P.
Proof. Proof.
iIntros "#HI". iApply inv_acc; eauto. iIntros "#HI". iApply inv_alter; eauto.
iIntros "!> !# [$ $] $". iIntros "!> !# [$ $] $".
Qed. Qed.
......
...@@ -91,7 +91,7 @@ Section proofs. ...@@ -91,7 +91,7 @@ Section proofs.
iNext. iLeft. by iFrame. iNext. iLeft. by iFrame.
Qed. Qed.
Lemma na_inv_open p E F N P : Lemma na_inv_acc p E F N P :
N E N F N E N F
na_inv p N P - na_own p F ={E}= P na_own p (F∖↑N) 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). ( P na_own p (F∖↑N) ={E}= na_own p F).
...@@ -121,6 +121,6 @@ Section proofs. ...@@ -121,6 +121,6 @@ Section proofs.
Proof. Proof.
rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown". rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
rewrite exist_unit -assoc /=. rewrite exist_unit -assoc /=.
iApply (na_inv_open with "Hinv"); done. iApply (na_inv_acc with "Hinv"); done.
Qed. Qed.
End proofs. End proofs.
...@@ -126,7 +126,7 @@ Section sts. ...@@ -126,7 +126,7 @@ Section sts.
rewrite /sts_inv. iNext. iExists s. by iFrame. rewrite /sts_inv. iNext. iExists s. by iFrame.
Qed. Qed.
Lemma sts_accS φ E γ S T : Lemma sts_inv_accS φ E γ S T :
sts_inv γ φ sts_ownS γ S T ={E}= s, sts_inv γ φ sts_ownS γ S T ={E}= s,
s S φ s s' T', s S φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E}= sts_inv γ φ sts_own γ s' T'. sts.steps (s, T) (s', T') φ s' ={E}= sts_inv γ φ sts_own γ s' T'.
...@@ -144,13 +144,13 @@ Section sts. ...@@ -144,13 +144,13 @@ Section sts.
iModIntro. iNext. iExists s'; by iFrame. iModIntro. iNext. iExists s'; by iFrame.
Qed. Qed.
Lemma sts_acc φ E γ s0 T : Lemma sts_inv_acc φ E γ s0 T :
sts_inv γ φ sts_own γ s0 T ={E}= s, sts_inv γ φ sts_own γ s0 T ={E}= s,
sts.frame_steps T s0 s φ s s' T', sts.frame_steps T s0 s φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E}= sts_inv γ φ sts_own γ 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_accS φ E N γ S T :
N E N E
sts_ctx γ N φ sts_ownS γ S T ={E,E∖↑N}= s, sts_ctx γ N φ sts_ownS γ S T ={E,E∖↑N}= s,
s S φ s s' T', s S φ s s' T',
...@@ -158,22 +158,22 @@ Section sts. ...@@ -158,22 +158,22 @@ Section sts.
Proof. Proof.
iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose". iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors (* 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_acc] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having for that currently, this gets more tedious than it should, with us having
to unpack and repack various proofs. to unpack and repack various proofs.
TODO: Make this mostly automatic, by supporting "opening accessors TODO: Make this mostly automatic, by supporting "opening accessors
around 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". iModIntro. iExists s. iFrame. iIntros (s' T') "H".
iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv"). iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
Qed. Qed.
Lemma sts_open φ E N γ s0 T : Lemma sts_acc φ E N γ s0 T :
N E N E
sts_ctx γ N φ sts_own γ s0 T ={E,E∖↑N}= s, sts_ctx γ N φ sts_own γ s0 T ={E,E∖↑N}= s,
sts.frame_steps T s0 s φ s s' T', sts.frame_steps T s0 s φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E∖↑N,E}= sts_own γ 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_accS. Qed.
End sts. End sts.
Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx. Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
...@@ -87,7 +87,7 @@ Module inv. Section inv. ...@@ -87,7 +87,7 @@ Module inv. Section inv.
Arguments inv _ _%I. Arguments inv _ _%I.
Hypothesis inv_persistent : i P, Persistent (inv i P). Hypothesis inv_persistent : i P, Persistent (inv i P).
Hypothesis inv_alloc : P, P fupd M1 ( i, 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). 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]. (* We have tokens for a little "two-state STS": [start] -> [finish].
...@@ -113,9 +113,9 @@ Module inv. Section inv. ...@@ -113,9 +113,9 @@ Module inv. Section inv.
Hypothesis consistency : ¬ (fupd M1 False). Hypothesis consistency : ¬ (fupd M1 False).
(** Some general lemmas and proof mode compatibility. *) (** 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. 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". } { iSplit; first done. iExact "HP". }
iIntros "(HP & HPw)". by iApply "HPw". iIntros "(HP & HPw)". by iApply "HPw".
Qed. Qed.
...@@ -167,7 +167,7 @@ Module inv. Section inv. ...@@ -167,7 +167,7 @@ Module inv. Section inv.
Lemma saved_cast γ P Q : saved γ P saved γ Q P fupd M1 ( Q). Lemma saved_cast γ P Q : saved γ P saved γ Q P fupd M1 ( Q).
Proof. Proof.
iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP". 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". iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf".
{ iDestruct "HaP" as "[Hs | [Hf _]]". { iDestruct "HaP" as "[Hs | [Hf _]]".
- by iApply start_finish. - by iApply start_finish.
...@@ -176,7 +176,7 @@ Module inv. Section inv. ...@@ -176,7 +176,7 @@ Module inv. Section inv.
iApply fupd_intro. iSplitL "Hf'"; first by eauto. iApply fupd_intro. iSplitL "Hf'"; first by eauto.
(* Step 2: Open the Q-invariant. *) (* Step 2: Open the Q-invariant. *)
iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ". 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]]". iIntros "[HaQ | [_ #HQ]]".
{ iExFalso. iApply finished_not_start. by iFrame. } { iExFalso. iApply finished_not_start. by iFrame. }
iApply fupd_intro. iSplitL "Hf". iApply fupd_intro. iSplitL "Hf".
...@@ -308,7 +308,7 @@ Module linear2. Section linear2. ...@@ -308,7 +308,7 @@ Module linear2. Section linear2.
Context (gname : Type) (cinv : gname PROP PROP) (cinv_own : gname PROP). Context (gname : Type) (cinv : gname PROP PROP) (cinv_own : gname PROP).
Hypothesis cinv_alloc : E, Hypothesis cinv_alloc : E,
fupd E E ( γ, P, P - fupd E E (cinv γ P cinv_own γ))%I. fupd E E ( γ, P, P - fupd E E (cinv γ P cinv_own γ))%I.
Hypothesis cinv_access : P γ, Hypothesis cinv_acc : P γ,
cinv γ P - cinv_own γ - fupd M1 M0 ( P cinv_own γ ( P - fupd M0 M1 emp)). cinv γ P - cinv_own γ - fupd M1 M0 ( P cinv_own γ ( P - fupd M0 M1 emp)).
(** Some general lemmas and proof mode compatibility. *) (** Some general lemmas and proof mode compatibility. *)
...@@ -335,7 +335,7 @@ Module linear2. Section linear2. ...@@ -335,7 +335,7 @@ Module linear2. Section linear2.
iIntros "HP". iIntros "HP".
iMod cinv_alloc as (γ) "Hmkinv". iMod cinv_alloc as (γ) "Hmkinv".
iMod ("Hmkinv" $! True%I with "[//]") as "[Hinv Htok]". iMod ("Hmkinv" $! True%I with "[//]") as "[Hinv Htok]".
iMod (cinv_access with "Hinv Htok") as "(Htrue & Htok & Hclose)". iMod (cinv_acc with "Hinv Htok") as "(Htrue & Htok & Hclose)".
iApply "Hclose". done. iApply "Hclose". done.
Qed. Qed.
End linear2. End linear2. End linear2. End linear2.
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