ghost_ownership.v 4.65 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
Require Export algebra.iprod program_logic.pviewshifts.
Require Import program_logic.ownership.
3
4
5
Import uPred.

Definition gid := positive.
Ralf Jung's avatar
Ralf Jung committed
6
7
Definition globalC (Σ : gid  iFunctor) : iFunctor :=
  iprodF (λ i, mapF gid (Σ i)).
8

9
Class InG (Λ : language) (Σ : gid  iFunctor) (i : gid) (A : cmraT) :=
Ralf Jung's avatar
Ralf Jung committed
10
  inG : A = Σ i (laterC (iPreProp Λ (globalC Σ))).
11

Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
14
15
16
17
18
19
20
21
Definition to_globalC {Λ Σ A}
    (i : gid) `{!InG Λ Σ i A} (γ : gid) (a : A) : iGst Λ (globalC Σ) :=
  iprod_singleton i {[ γ  cmra_transport inG a ]}.
Definition own {Λ Σ A}
    (i : gid) `{!InG Λ Σ i A} (γ : gid) (a : A) : iProp Λ (globalC Σ) :=
  ownG (to_globalC i γ a).
Instance: Params (@to_globalC) 6.
Instance: Params (@own) 6.
Typeclasses Opaque to_globalC own.

22
Section global.
Ralf Jung's avatar
Ralf Jung committed
23
Context {Λ : language} {Σ : gid  iFunctor} (i : gid) `{!InG Λ Σ i A}.
24
25
Implicit Types a : A.

26
(* Properties of to_globalC *)
Robbert Krebbers's avatar
Robbert Krebbers committed
27
28
29
Instance to_globalC_ne γ n : Proper (dist n ==> dist n) (to_globalC i γ).
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma to_globalC_validN n γ a : {n} (to_globalC i γ a)  {n} a.
30
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
  by rewrite /to_globalC
    iprod_singleton_validN map_singleton_validN cmra_transport_validN.
33
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
Lemma to_globalC_op γ a1 a2 :
  to_globalC i γ (a1  a2)  to_globalC i γ a1  to_globalC i γ a2.
36
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  by rewrite /to_globalC iprod_op_singleton map_op_singleton cmra_transport_op.
38
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
Lemma to_globalC_unit γ a : unit (to_globalC i γ a)  to_globalC i γ (unit a).
40
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
  by rewrite /to_globalC
    iprod_unit_singleton map_unit_singleton cmra_transport_unit.
43
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
Instance to_globalC_timeless γ m : Timeless m  Timeless (to_globalC i γ m).
Proof. rewrite /to_globalC; apply _. Qed.
46

47
(* Properties of own *)
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
50
51
52
53
54
55
56
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
Proof. by intros m m' Hm; rewrite /own Hm. Qed.
Global Instance own_proper γ : Proper (() ==> ()) (own i γ) := ne_proper _.

Lemma own_op γ a1 a2 : own i γ (a1  a2)  (own i γ a1  own i γ a2)%I.
Proof. by rewrite /own -ownG_op to_globalC_op. Qed.
Lemma always_own_unit γ a : ( own i γ (unit a))%I  own i γ (unit a).
Proof. by rewrite /own -to_globalC_unit always_ownG_unit. Qed.
Lemma own_valid γ a : own i γ a   a.
57
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
  rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalC_validN.
59
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Lemma own_valid_r' γ a : own i γ a  (own i γ a   a).
61
Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
Global Instance own_timeless γ a : Timeless a  TimelessP (own i γ a).
Proof. unfold own; apply _. Qed.
64

Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
(* 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. *)
Lemma own_alloc E a :  a  True  pvs E E ( γ, own i γ a).
68
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
70
71
72
73
74
  intros Ha.
  rewrite -(pvs_mono _ _ ( m,  ( γ, m = to_globalC i γ a)  ownG m)%I).
  * eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty i);
      first (eapply map_updateP_alloc', cmra_transport_valid, Ha); naive_solver.
  * apply exist_elim=>m; apply const_elim_l=>-[γ ->].
    by rewrite -(exist_intro γ).
75
Qed.
76

77
Lemma own_updateP E γ a P :
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  a ~~>: P  own i γ a  pvs E E ( a',  P a'  own i γ a').
79
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  intros Ha.
81
  rewrite -(pvs_mono _ _ ( m,  ( a', m = to_globalC i γ a'  P a')  ownG m)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  * eapply pvs_ownG_updateP, iprod_singleton_updateP;
83
      first by (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
86
    naive_solver.
  * apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
87
88
Qed.

89
90
Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} E γ a P :
   ~~>: P  True  pvs E E ( a,  P a  own i γ a).
91
Proof.
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
  intros Hemp.
  rewrite -(pvs_mono _ _ ( m,  ( a', m = to_globalC i γ a'  P a')  ownG m)%I).
  * eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty with (x:=i);
      first by (eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp).
    naive_solver.
  * apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
Unshelve.
(* We have to prove that we actually follow the identity laws on the "other side". *)
split.
- apply cmra_transport_valid, cmra_empty_valid.
- move=>b. by rewrite -cmra_transport_back_op_r left_id cmra_transport_back_and.
- apply _. 
Qed.

Lemma own_update E γ a a' : a ~~> a'  own i γ a  pvs E E (own i γ a').
Proof.
  intros; rewrite (own_updateP E _ _ (a' =)); last by apply cmra_update_updateP.
110
111
  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
Qed.
112
End global.