ghost_ownership.v 3.98 KB
Newer Older
1
2
3
4
From iris.prelude Require Export functions.
From iris.algebra Require Export iprod.
From iris.program_logic Require Export pviewshifts global_functor.
From iris.program_logic Require Import ownership.
5
6
Import uPred.

7
Definition own_def `{inG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
8
  ownG (to_globalF γ a).
9
10
11
Definition own_aux : { x | x = @own_def }. by eexists. Qed.
Definition own {Λ Σ A i} := proj1_sig own_aux Λ Σ A i.
Definition own_eq : @own = @own_def := proj2_sig own_aux.
12
Instance: Params (@own) 5.
13
Typeclasses Opaque own.
14

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
(* 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. *)
49
Lemma own_alloc_strong a E (G : gset gname) :
50
   a  True ={E}=>  γ, (γ  G)  own γ a.
51
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  intros Ha.
53
  rewrite -(pvs_mono _ _ ( m,  ( γ, γ  G  m = to_globalF γ a)  ownG m)%I).
54
  - rewrite ownG_empty.
55
    eapply pvs_ownG_updateP, (iprod_singleton_updateP_empty (inG_id i));
56
      first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
57
      naive_solver.
58
59
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
    by rewrite !own_eq /own_def -(exist_intro γ) pure_equiv // left_id.
60
Qed.
61
Lemma own_alloc a E :  a  True ={E}=>  γ, own γ a.
62
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64
  intros Ha. rewrite (own_alloc_strong a E ) //; [].
  apply pvs_mono, exist_mono=>?. eauto with I.
65
Qed.
66

67
Lemma own_updateP P γ a E : a ~~>: P  own γ a ={E}=>  a',  P a'  own γ a'.
68
Proof.
69
  intros Ha. rewrite !own_eq.
70
  rewrite -(pvs_mono _ _ ( m,  ( a', m = to_globalF γ a'  P a')  ownG m)%I).
71
  - eapply pvs_ownG_updateP, iprod_singleton_updateP;
72
      first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
73
    naive_solver.
74
75
  - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
76
77
Qed.

78
Lemma own_update γ a a' E : a ~~> a'  own γ a ={E}=> own γ a'.
79
Proof.
80
  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
81
  by apply pvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
82
Qed.
83
End global.
84

85
86
87
88
Section global_empty.
Context `{i : inG Λ Σ (A:ucmraT)}.
Implicit Types a : A.

89
Lemma own_empty γ E : True ={E}=> own γ (:A).
90
Proof.
91
92
  rewrite ownG_empty !own_eq /own_def.
  apply pvs_ownG_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.
97
End global_empty.