Commit 12a6f8fb authored by Robbert Krebbers's avatar Robbert Krebbers

Use notation for `own`.

parent 9d8af00a
......@@ -58,6 +58,8 @@ Definition own {Σ A i} := own_aux.(unseal) Σ A i.
Definition own_eq : @own = @own_def := own_aux.(seal_eq).
Instance: Params (@own) 4 := {}.
Typeclasses Opaque own.
Notation "👻{ γ } x" := (own γ x)
(at level 20, x at next level, format "👻{ γ } x").
(** * Properties about ghost ownership *)
Section global.
......@@ -80,15 +82,15 @@ Proof. rewrite !own_eq. solve_proper. Qed.
Global Instance own_proper γ :
Proper (() ==> ()) (@own Σ A _ γ) := ne_proper _.
Lemma own_op γ a1 a2 : own γ (a1 a2) own γ a1 own γ a2.
Lemma own_op γ a1 a2 : 👻{γ} (a1 a2) 👻{γ} a1 👻{γ} a2.
Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
Lemma own_mono γ a1 a2 : a2 a1 own γ a1 own γ a2.
Lemma own_mono γ a1 a2 : a2 a1 👻{γ} a1 👻{γ} a2.
Proof. move=> [c ->]. by rewrite own_op sep_elim_l. Qed.
Global Instance own_mono' γ : Proper (flip () ==> ()) (@own Σ A _ γ).
Proof. intros a1 a2. apply own_mono. Qed.
Lemma own_valid γ a : own γ a a.
Lemma own_valid γ a : 👻{γ} a a.
Proof.
rewrite !own_eq /own_def ownM_valid /iRes_singleton.
rewrite ofe_fun_validI (forall_elim (inG_id _)) ofe_fun_lookup_singleton.
......@@ -96,21 +98,21 @@ Proof.
(* implicit arguments differ a bit *)
by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
Qed.
Lemma own_valid_2 γ a1 a2 : own γ a1 - own γ a2 - (a1 a2).
Lemma own_valid_2 γ a1 a2 : 👻{γ} a1 - 👻{γ} a2 - (a1 a2).
Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 - own γ a2 - own γ a3 - (a1 a2 a3).
Lemma own_valid_3 γ a1 a2 a3 : 👻{γ} a1 - 👻{γ} a2 - 👻{γ} a3 - (a1 a2 a3).
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
Lemma own_valid_r γ a : own γ a own γ a a.
Lemma own_valid_r γ a : 👻{γ} a 👻{γ} a a.
Proof. apply: bi.persistent_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a a own γ a.
Lemma own_valid_l γ a : 👻{γ} a a 👻{γ} a.
Proof. by rewrite comm -own_valid_r. Qed.
Global Instance own_timeless γ a : Discrete a Timeless (own γ a).
Global Instance own_timeless γ a : Discrete a Timeless (👻{γ} a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Global Instance own_core_persistent γ a : CoreId a Persistent (own γ a).
Global Instance own_core_persistent γ a : CoreId a Persistent (👻{γ} a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Lemma later_own γ a : own γ a - ( b, own γ b (a b)).
Lemma later_own γ a : 👻{γ} a - ( b, 👻{γ} b (a b)).
Proof.
rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
assert (NonExpansive (λ r : iResUR Σ, r (inG_id Hin) !! γ)).
......@@ -145,7 +147,7 @@ Qed.
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc_strong a (P : gname Prop) :
pred_infinite P
a (|==> γ, P γ⌝ own γ a)%I.
a (|==> γ, P γ⌝ 👻{γ} a)%I.
Proof.
intros HP Ha.
rewrite -(bupd_mono ( m, γ, P γ m = iRes_singleton γ a uPred_ownM m)%I).
......@@ -157,7 +159,7 @@ Proof.
by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
Qed.
Lemma own_alloc_cofinite a (G : gset gname) :
a (|==> γ, ⌜γ G own γ a)%I.
a (|==> γ, ⌜γ G 👻{γ} a)%I.
Proof.
intros Ha.
apply (own_alloc_strong a (λ γ, γ G))=> //.
......@@ -165,14 +167,14 @@ Proof.
intros E. set (i := fresh (G E)).
exists i. apply not_elem_of_union, is_fresh.
Qed.
Lemma own_alloc a : a (|==> γ, own γ a)%I.
Lemma own_alloc a : a (|==> γ, 👻{γ} a)%I.
Proof.
intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_cofinite a ) //; [].
apply bupd_mono, exist_mono=>?. eauto using and_elim_r.
Qed.
(** ** Frame preserving updates *)
Lemma own_updateP P γ a : a ~~>: P own γ a == a', P a' own γ a'.
Lemma own_updateP P γ a : a ~~>: P 👻{γ} a == a', P a' 👻{γ} a'.
Proof.
intros Ha. rewrite !own_eq.
rewrite -(bupd_mono ( m, a', m = iRes_singleton γ a' P a' uPred_ownM m)%I).
......@@ -183,16 +185,16 @@ Proof.
rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
Qed.
Lemma own_update γ a a' : a ~~> a' own γ a == own γ a'.
Lemma own_update γ a a' : a ~~> a' 👻{γ} a == 👻{γ} a'.
Proof.
intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
Qed.
Lemma own_update_2 γ a1 a2 a' :
a1 a2 ~~> a' own γ a1 - own γ a2 == own γ a'.
a1 a2 ~~> a' 👻{γ} a1 - 👻{γ} a2 == 👻{γ} a'.
Proof. intros. apply wand_intro_r. rewrite -own_op. by apply own_update. Qed.
Lemma own_update_3 γ a1 a2 a3 a' :
a1 a2 a3 ~~> a' own γ a1 - own γ a2 - own γ a3 == own γ a'.
a1 a2 a3 ~~> a' 👻{γ} a1 - 👻{γ} a2 - 👻{γ} a3 == 👻{γ} a'.
Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. by apply own_update. Qed.
End global.
......@@ -206,7 +208,7 @@ Arguments own_update {_ _} [_] _ _ _ _.
Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
Lemma own_unit A `{!inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
Lemma own_unit A `{!inG Σ (A:ucmraT)} γ : (|==> 👻{γ} ε)%I.
Proof.
rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
apply bupd_ownM_update, ofe_fun_singleton_update_empty.
......@@ -217,7 +219,7 @@ Qed.
(** Big op class instances *)
Instance own_cmra_sep_homomorphism `{!inG Σ (A:ucmraT)} :
WeakMonoidHomomorphism op uPred_sep () (own γ).
WeakMonoidHomomorphism op uPred_sep () (👻{γ}).
Proof. split; try apply _. apply own_op. Qed.
(** Proofmode class instances *)
......@@ -225,19 +227,19 @@ Section proofmode_classes.
Context `{!inG Σ A}.
Implicit Types a b : A.
Global Instance into_sep_own γ a b1 b2 :
IsOp a b1 b2 IntoSep (own γ a) (own γ b1) (own γ b2).
Global Instance into_sep_👻{γ} a b1 b2 :
IsOp a b1 b2 IntoSep (👻{γ} a) (👻{γ} b1) (👻{γ} b2).
Proof. intros. by rewrite /IntoSep (is_op a) own_op. Qed.
Global Instance into_and_own p γ a b1 b2 :
IsOp a b1 b2 IntoAnd p (own γ a) (own γ b1) (own γ b2).
IsOp a b1 b2 IntoAnd p (👻{γ} a) (👻{γ} b1) (👻{γ} b2).
Proof. intros. by rewrite /IntoAnd (is_op a) own_op sep_and. Qed.
Global Instance from_sep_own γ a b1 b2 :
IsOp a b1 b2 FromSep (own γ a) (own γ b1) (own γ b2).
Global Instance from_sep_👻{γ} a b1 b2 :
IsOp a b1 b2 FromSep (👻{γ} a) (👻{γ} b1) (👻{γ} b2).
Proof. intros. by rewrite /FromSep -own_op -is_op. Qed.
Global Instance from_and_own_persistent γ a b1 b2 :
IsOp a b1 b2 TCOr (CoreId b1) (CoreId b2)
FromAnd (own γ a) (own γ b1) (own γ b2).
FromAnd (👻{γ} a) (👻{γ} b1) (👻{γ} b2).
Proof.
intros ? Hb. rewrite /FromAnd (is_op a) own_op.
destruct Hb; by rewrite persistent_and_sep.
......
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