ghost_ownership.v 3.94 KB
Newer Older
1
2
From iris.program_logic Require Export global_functor.
From iris.algebra Require Import iprod gmap.
3
4
Import uPred.

5
6
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
  uPred_ownM (to_iRes γ a).
7
Definition own_aux : { x | x = @own_def }. by eexists. Qed.
8
Definition own {Σ A i} := proj1_sig own_aux Σ A i.
9
Definition own_eq : @own = @own_def := proj2_sig own_aux.
10
Instance: Params (@own) 4.
11
Typeclasses Opaque own.
12

13
(** Properties about ghost ownership *)
14
Section global.
15
Context `{i : inG Σ A}.
16
17
Implicit Types a : A.

18
(** * Properties of own *)
19
Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Σ A _ γ).
20
Proof. rewrite !own_eq. solve_proper. Qed.
21
Global Instance own_proper γ :
22
  Proper (() ==> ()) (@own Σ A _ γ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
23

24
Lemma own_op γ a1 a2 : own γ (a1  a2)  own γ a1  own γ a2.
25
26
Proof. by rewrite !own_eq /own_def -ownM_op to_iRes_op. Qed.
Global Instance own_mono γ : Proper (flip () ==> ()) (@own Σ A _ γ).
27
Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
28
Lemma own_valid γ a : own γ a   a.
29
Proof.
30
  rewrite !own_eq /own_def ownM_valid /to_iRes.
31
  rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
32
  rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
33
  (* implicit arguments differ a bit *)
34
  by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
35
Qed.
36
Lemma own_valid_r γ a : own γ a  own γ a   a.
37
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
38
Lemma own_valid_l γ a : own γ a   a  own γ a.
39
Proof. by rewrite comm -own_valid_r. Qed.
40
Global Instance own_timeless γ a : Timeless a  TimelessP (own γ a).
41
Proof. rewrite !own_eq /own_def; apply _. Qed.
42
Global Instance own_core_persistent γ a : Persistent a  PersistentP (own γ a).
43
Proof. rewrite !own_eq /own_def; apply _. Qed.
44

Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
   assertion. However, the map_updateP_alloc does not suffice to show this. *)
47
48
Lemma own_alloc_strong a (G : gset gname) :
   a  True =r=>  γ,  (γ  G)  own γ a.
49
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  intros Ha.
51
52
53
  rewrite -(rvs_mono ( m,  ( γ, γ  G  m = to_iRes γ a)  uPred_ownM m)%I).
  - rewrite ownM_empty.
    eapply rvs_ownM_updateP, (iprod_singleton_updateP_empty (inG_id i));
54
      first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
55
      naive_solver.
56
57
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
    by rewrite !own_eq /own_def -(exist_intro γ) pure_equiv // left_id.
58
Qed.
59
Lemma own_alloc a :  a  True =r=>  γ, own γ a.
60
Proof.
61
62
  intros Ha. rewrite (own_alloc_strong a ) //; [].
  apply rvs_mono, exist_mono=>?. eauto with I.
63
Qed.
64

65
Lemma own_updateP P γ a : a ~~>: P  own γ a =r=>  a',  P a'  own γ a'.
66
Proof.
67
  intros Ha. rewrite !own_eq.
68
69
  rewrite -(rvs_mono ( m,  ( a', m = to_iRes γ a'  P a')  uPred_ownM m)%I).
  - eapply rvs_ownM_updateP, iprod_singleton_updateP;
70
      first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
71
    naive_solver.
72
73
  - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
74
75
Qed.

76
Lemma own_update γ a a' : a ~~> a'  own γ a =r=> own γ a'.
77
Proof.
78
  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
79
  by apply rvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
80
Qed.
81
End global.
82

83
84
85
86
87
Arguments own_valid {_ _} [_] _ _.
Arguments own_valid_l {_ _} [_] _ _.
Arguments own_valid_r {_ _} [_] _ _.
Arguments own_updateP {_ _} [_] _ _ _ _.
Arguments own_update {_ _} [_] _ _ _ _.
88

89
Lemma own_empty `{inG Σ (A:ucmraT)} γ : True =r=> own γ .
90
Proof.
91
92
  rewrite ownM_empty !own_eq /own_def.
  apply rvs_ownM_update, iprod_singleton_update_empty.
93
  apply (alloc_unit_singleton_update (cmra_transport inG_prf )); last done.
94
95
  - apply cmra_transport_valid, ucmra_unit_valid.
  - intros x; destruct inG_prf. by rewrite left_id.
96
Qed.