global_cmra.v 5.15 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
12

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

16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
Definition to_Σ (a : A) : Σ i (laterC (iPreProp Λ (globalC Σ))) :=
  eq_rect A id a _ inG.
Definition to_globalC (γ : gid) `{!InG Λ Σ i A} (a : A) : iGst Λ (globalC Σ) :=
  iprod_singleton i {[ γ  to_Σ a ]}.
Definition own (γ : gid) (a : A) : iProp Λ (globalC Σ) :=
  ownG (to_globalC γ a).

Definition from_Σ (b : Σ i (laterC (iPreProp Λ (globalC Σ)))) : A  :=
  eq_rect (Σ i _) id b _ (Logic.eq_sym inG).
Definition P_to_Σ (P : A  Prop) (b : Σ i (laterC (iPreProp Λ (globalC Σ)))) : Prop
  := P (from_Σ b).

(* Properties of the transport. *)
Lemma to_from_Σ b :
  to_Σ (from_Σ b) = b.
Proof.
  rewrite /to_Σ /from_Σ. by destruct inG.
Qed.

(* Properties of to_globalC *)
36
Lemma globalC_op γ a1 a2 :
37
  to_globalC γ (a1  a2)  to_globalC γ a1  to_globalC γ a2.
38
39
40
Proof.
  rewrite /to_globalC iprod_op_singleton map_op_singleton.
  apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
Ralf Jung's avatar
Ralf Jung committed
41
  by rewrite /to_Σ; destruct inG.
42
43
Qed.

44
Lemma globalC_validN n γ a : {n} (to_globalC γ a)  {n} a.
45
Proof.
46
  rewrite /to_globalC iprod_singleton_validN map_singleton_validN.
Ralf Jung's avatar
Ralf Jung committed
47
  by rewrite /to_Σ; destruct inG.
48
49
Qed.

50
Lemma globalC_unit γ a :
51
  unit (to_globalC γ a)  to_globalC γ (unit a).
52
53
54
55
56
57
58
Proof.
  rewrite /to_globalC.
  rewrite iprod_unit_singleton map_unit_singleton.
  apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
  by rewrite /to_Σ; destruct inG.
Qed.

59
Global Instance globalC_timeless γ m : Timeless m  Timeless (to_globalC γ m).
60
61
Proof.
  rewrite /to_globalC => ?.
62
  apply (iprod_singleton_timeless _ _ _), map_singleton_timeless.
63
64
65
  by rewrite /to_Σ; destruct inG.
Qed.

66
67
68
69
70
71
72
73
74
75
(* Properties of the lifted frame-preserving updates *)
Lemma update_to_Σ a P :
  a ~~>: P  to_Σ a ~~>: P_to_Σ P.
Proof.
  move=>Hu gf n Hf. destruct (Hu (from_Σ gf) n) as [a' Ha'].
  { move: Hf. rewrite /to_Σ /from_Σ. by destruct inG. }
  exists (to_Σ a'). move:Hf Ha'.
  rewrite /P_to_Σ /to_Σ /from_Σ. destruct inG. done.
Qed. 

76
77
(* Properties of own *)

78
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
79
80
Proof.
  intros m m' Hm; apply ownG_ne, iprod_singleton_ne, singleton_ne.
Ralf Jung's avatar
Ralf Jung committed
81
  by rewrite /to_globalC /to_Σ; destruct inG.
82
83
Qed.

84
Global Instance own_proper γ : Proper (() ==> ()) (own γ) := ne_proper _.
85

86
Lemma own_op γ a1 a2 : own γ (a1  a2)  (own γ a1  own γ a2)%I.
87
Proof. rewrite /own -ownG_op. apply ownG_proper, globalC_op. Qed.
88
89
90
91

(* 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 :
92
  a  True  pvs E E ( γ, own γ a).
93
Proof.
94
  intros Ha. set (P m :=  γ, m = to_globalC γ a).
95
  rewrite -(pvs_mono _ _ ( m, P m  ownG m)%I).
96
  - rewrite -pvs_ownG_updateP_empty //; [].
97
    subst P. eapply (iprod_singleton_updateP_empty i).
98
    + apply map_updateP_alloc' with (x:=to_Σ a).
Ralf Jung's avatar
Ralf Jung committed
99
      by rewrite /to_Σ; destruct inG.
100
    + simpl. move=>? [γ [-> ?]]. exists γ. done.
101
102
  - apply exist_elim=>m. apply const_elim_l=>-[p ->] {P}.
    by rewrite -(exist_intro p).
103
Qed.
104

105
Lemma always_own_unit γ a : ( own γ (unit a))%I  own γ (unit a).
106
Proof. rewrite /own -globalC_unit. by apply always_ownG_unit. Qed.
107

108
Lemma own_valid γ a : (own γ a)  ( a).
109
Proof.
110
111
112
  rewrite /own ownG_valid. apply uPred.valid_mono=>n.
  by apply globalC_validN.
Qed.
113

114
Lemma own_valid_r' γ a : (own γ a)  (own γ a   a).
115
116
Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.

117
Global Instance ownG_timeless γ a : Timeless a  TimelessP (own γ a).
118
Proof.
119
120
  intros. apply ownG_timeless. apply _.
Qed.
121

122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
Lemma pvs_updateP E γ a P :
  a ~~>: P  own γ a  pvs E E ( a',  P a'  own γ a').
Proof.
  intros Ha. set (P' m :=  a', P a'  m = to_globalC γ a').
  rewrite -(pvs_mono _ _ ( m, P' m  ownG m)%I).
  - rewrite -pvs_ownG_updateP; first by rewrite /own.
    rewrite /to_globalC. eapply iprod_singleton_updateP.
    + (* FIXME RJ: I tried apply... with instead of instantiate, that
         does not work. *)
      apply map_singleton_updateP'. instantiate (1:=P_to_Σ P).
      by apply update_to_Σ.
    + simpl. move=>? [y [-> HP]]. exists (from_Σ y). split.
      * move: HP. rewrite /P_to_Σ /from_Σ. by destruct inG.
      * clear HP. rewrite /to_globalC to_from_Σ; done.
  - apply exist_elim=>m. apply const_elim_l=>-[a' [HP ->]].
    rewrite -(exist_intro a'). apply and_intro; last done.
    by apply const_intro.
Qed.

Lemma pvs_update E γ a a' : a ~~> a'  own γ a  pvs E E (own γ a').
Proof.
  intros; rewrite (pvs_updateP E _ _ (a' =)); last by apply cmra_update_updateP.
  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
Qed.

147
End global.