ownership.v 3.01 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6
Require Export iris.model.

Definition inv {Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
  uPred_own (Res {[ i  to_agree (Later (iProp_unfold P)) ]}  ).
Arguments inv {_} _ _%I.
Definition ownP {Σ} (σ : istate Σ) : iProp Σ := uPred_own (Res  (Excl σ) ).
7
Definition ownG {Σ} (m : iGst Σ) : iProp Σ := uPred_own (Res   m).
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10 11
Instance: Params (@inv) 2.
Instance: Params (@ownP) 1.
Instance: Params (@ownG) 1.

Robbert Krebbers's avatar
Robbert Krebbers committed
12 13
Typeclasses Opaque inv ownG ownP.

Robbert Krebbers's avatar
Robbert Krebbers committed
14 15
Section ownership.
Context {Σ : iParam}.
16
Implicit Types r : iRes Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
Implicit Types σ : istate Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Implicit Types P : iProp Σ.
19
Implicit Types m : iGst Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21 22 23 24 25 26 27 28 29 30 31

(* Invariants *)
Global Instance inv_contractive i : Contractive (@inv Σ i).
Proof.
  intros n P Q HPQ.
  apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
  by unfold inv; rewrite HPQ.
Qed.
Lemma always_inv i P : ( inv i P)%I  inv i P.
Proof.
  by apply uPred.always_own; rewrite Res_unit !ra_unit_empty map_unit_singleton.
Qed.
32 33 34 35
Global Instance inv_always_stable i P : AlwaysStable (inv i P).
Proof. by rewrite /AlwaysStable always_inv. Qed.
Lemma inv_sep_dup i P : inv i P  (inv i P  inv i P)%I.
Proof. apply (uPred.always_sep_dup' _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38 39 40 41 42

(* physical state *)
Lemma ownP_twice σ1 σ2 : (ownP σ1  ownP σ2 : iProp Σ)  False.
Proof.
  rewrite /ownP -uPred.own_op Res_op.
  by apply uPred.own_invalid; intros (_&?&_).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44
Global Instance ownP_timeless σ : TimelessP (ownP σ).
Proof. rewrite /ownP; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46 47 48 49 50 51 52 53 54 55 56 57

(* ghost state *)
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Σ).
Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
Global Instance ownG_proper : Proper (() ==> ()) (@ownG Σ) := ne_proper _.
Lemma ownG_op m1 m2 : ownG (m1  m2)  (ownG m1  ownG m2)%I.
Proof. by rewrite /ownG -uPred.own_op Res_op !(left_id _ _). Qed.
Lemma always_ownG_unit m : ( ownG (unit m))%I  ownG (unit m).
Proof.
  by apply uPred.always_own; rewrite Res_unit !ra_unit_empty ra_unit_idempotent.
Qed.
Lemma ownG_valid m : (ownG m)  ( m).
Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
Global Instance ownG_timeless m : Timeless m  TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61 62 63 64 65 66 67 68 69 70 71

(* inversion lemmas *)
Lemma inv_spec r n i P :
  {n} r 
  (inv i P) n r  wld r !! i ={n}= Some (to_agree (Later (iProp_unfold P))).
Proof.
  intros [??]; rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
  * intros [(P'&Hi&HP) _]; rewrite Hi.
    by apply Some_dist, symmetry, agree_valid_includedN,
      (cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
  * intros ?; split_ands; try apply cmra_empty_least; eauto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74 75 76
Lemma ownP_spec r n σ : {n} r  (ownP σ) n r  pst r ={n}= Excl σ.
Proof.
  intros (?&?&?); rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
  naive_solver (apply cmra_empty_least).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78 79 80 81
Lemma ownG_spec r n m : (ownG m) n r  m {n} gst r.
Proof.
  rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_least).
Qed.
End ownership.