ownership.v 2.71 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
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 σ) ).
Definition ownG {Σ} (m : icmra' Σ) : iProp Σ := uPred_own (Res   m).
Instance: Params (@inv) 2.
Instance: Params (@ownP) 1.
Instance: Params (@ownG) 1.

Section ownership.
Context {Σ : iParam}.
Implicit Types r : res' Σ.
Implicit Types P : iProp Σ.
Implicit Types m : icmra' Σ.

(* 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 inv_duplicate i P : inv i P  (inv i P  inv i P)%I.
Proof.
  by rewrite /inv -uPred.own_op Res_op
    map_op_singleton agree_idempotent !(left_id _ _).
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.

(* 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.

(* 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.

(* 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
66
67
68
69
70
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
71
72
73
74
75
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.