ownership.v 2.96 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
14
15
16
Section ownership.
Context {Σ : iParam}.
Implicit Types r : res' Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
Implicit Types σ : istate Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
Global Instance ownP_timeless σ : TimelessP (ownP σ).
Proof. rewrite /ownP; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
48
49
50
51
52
53
54
55
56
57
58

(* 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
59
60
Global Instance ownG_timeless m : Timeless m  TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
62
63
64
65
66
67
68
69
70
71
72

(* 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
73
74
75
76
77
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
78
79
80
81
82
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.