Commit 8d1b743e authored by Robbert Krebbers's avatar Robbert Krebbers

Rename box_inv into box_slice_inv.

parent 5d66333c
...@@ -19,22 +19,22 @@ Section box_defs. ...@@ -19,22 +19,22 @@ Section box_defs.
Definition box_own_prop (γ : gname) (P : iProp) : iProp := Definition box_own_prop (γ : gname) (P : iProp) : iProp :=
own γ (:auth _, Some (to_agree (Next (iProp_unfold P)))). own γ (:auth _, Some (to_agree (Next (iProp_unfold P)))).
Definition box_inv (γ : gname) (P : iProp) : iProp := Definition box_slice_inv (γ : gname) (P : iProp) : iProp :=
( b, box_own_auth γ ( Excl' b) box_own_prop γ P if b then P else True)%I. ( b, box_own_auth γ ( Excl' b) box_own_prop γ P if b then P else True)%I.
Definition box_slice (γ : gname) (P : iProp) : iProp := Definition box_slice (γ : gname) (P : iProp) : iProp :=
inv N (box_inv γ P). inv N (box_slice_inv γ P).
Definition box (f : gmap gname bool) (P : iProp) : iProp := Definition box (f : gmap gname bool) (P : iProp) : iProp :=
( Φ : gname iProp, ( Φ : gname iProp,
(P [ map] γ b f, Φ γ) (P [ map] γ b f, Φ γ)
[ map] γ b f, box_own_auth γ ( Excl' b) box_own_prop γ (Φ γ) [ map] γ b f, box_own_auth γ ( Excl' b) box_own_prop γ (Φ γ)
inv N (box_inv γ (Φ γ)))%I. inv N (box_slice_inv γ (Φ γ)))%I.
End box_defs. End box_defs.
Instance: Params (@box_own_auth) 4. Instance: Params (@box_own_auth) 4.
Instance: Params (@box_own_prop) 4. Instance: Params (@box_own_prop) 4.
Instance: Params (@box_inv) 4. Instance: Params (@box_slice_inv) 4.
Instance: Params (@box_slice) 5. Instance: Params (@box_slice) 5.
Instance: Params (@box) 5. Instance: Params (@box) 5.
...@@ -46,7 +46,7 @@ Implicit Types P Q : iProp. ...@@ -46,7 +46,7 @@ Implicit Types P Q : iProp.
(* FIXME: solve_proper picks the eq ==> instance for Next. *) (* FIXME: solve_proper picks the eq ==> instance for Next. *)
Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ). Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (box_inv γ). Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (box_slice_inv γ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance box_slice_ne n γ : Proper (dist n ==> dist n) (box_slice N γ). Global Instance box_slice_ne n γ : Proper (dist n ==> dist n) (box_slice N γ).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
...@@ -103,7 +103,7 @@ Proof. ...@@ -103,7 +103,7 @@ Proof.
as {γ} "[Hdom Hγ]"; first done. as {γ} "[Hdom Hγ]"; first done.
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]". rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom. iDestruct "Hdom" as % ?%not_elem_of_dom.
iPvs (inv_alloc N _ (box_inv γ Q) with "[Hγ]") as "#Hinv"; first done. iPvs (inv_alloc N _ (box_slice_inv γ Q) with "[Hγ]") as "#Hinv"; first done.
{ iNext. iExists false. by repeat iSplit. } { iNext. iExists false. by repeat iSplit. }
iPvsIntro; iExists γ; repeat iSplit; auto. iPvsIntro; iExists γ; repeat iSplit; auto.
iNext. iExists (<[γ:=Q]> Φ); iSplit. iNext. iExists (<[γ:=Q]> Φ); iSplit.
......
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