updates.v 10.7 KB
Newer Older
1
From fri.algebra Require Export cmra.
2
3

(** * Frame preserving updates *)
4
5
6
7
(* This quantifies over [option A] for the frame.  That is necessary to
   make the following hold:
     x ~~> P  Some c ~~> Some P
*)
8
9
Definition cmra_updateP {A : cmraT} (x : A) (P : A  Prop) :=  n mz,
  {n} (x ? mz)   y, P y  {n} (y ? mz).
10
Instance: Params (@cmra_updateP) 1 := {}.
11
12
13
14
15
Infix "~~>:" := cmra_updateP (at level 70).

Definition cmra_update {A : cmraT} (x y : A) :=  n mz,
  {n} (x ? mz)  {n} (y ? mz).
Infix "~~>" := cmra_update (at level 70).
16
Instance: Params (@cmra_update) 1 := {}.
17

18
19
20
Definition cmra_step_updateP {A : cmraT} (x : A) (xl: A) (P : A  A  Prop) :=  n mz,
  {n} (x  xl ? mz)   y yl, P y yl  {n} (y  yl ? mz)  xl _(n) yl.
Notation "x # y ~~>>: P" := (cmra_step_updateP x y P) (at level 70).
21
Instance: Params (@cmra_step_updateP) 1 := {}.
22
23
24

Definition cmra_step_update {A : cmraT} (x xl y yl : A) :=  n mz,
  {n} (x  xl ? mz)  {n} (y  yl ? mz)  xl _(n) yl.
25
Notation "x # xl ~~>> y #' yl " := (cmra_step_update x xl y yl) (at level 70).
26
Instance: Params (@cmra_step_update) 1 := {}.
27
28


29
Section updates.
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
Context {A : cmraT}.
Implicit Types x y : A.

Global Instance cmra_updateP_proper :
  Proper (() ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
Proof.
  rewrite /pointwise_relation /cmra_updateP=> x x' Hx P P' HP;
    split=> ? n mz; setoid_subst; naive_solver.
Qed.
Global Instance cmra_update_proper :
  Proper (() ==> () ==> iff) (@cmra_update A).
Proof.
  rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
45
Lemma cmra_update_updateP x y : x ~~> y  x ~~>: (y =.).
46
47
48
49
50
51
52
53
54
Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed.
Lemma cmra_updateP_id (P : A  Prop) x : P x  x ~~>: P.
Proof. intros ? n mz ?; eauto. Qed.
Lemma cmra_updateP_compose (P Q : A  Prop) x :
  x ~~>: P  ( y, P y  y ~~>: Q)  x ~~>: Q.
Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed.
Lemma cmra_updateP_compose_l (Q : A  Prop) x y : x ~~> y  y ~~>: Q  x ~~>: Q.
Proof.
  rewrite cmra_update_updateP.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
  intros; apply cmra_updateP_compose with (y =.); naive_solver.
56
57
58
59
60
61
62
63
64
65
66
67
68
Qed.
Lemma cmra_updateP_weaken (P Q : A  Prop) x :
  x ~~>: P  ( y, P y  Q y)  x ~~>: Q.
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Proof.
  split.
  - intros x. by apply cmra_update_updateP, cmra_updateP_id.
  - intros x y z. rewrite !cmra_update_updateP.
    eauto using cmra_updateP_compose with subst.
Qed.
Lemma cmra_update_exclusive `{!Exclusive x} y:
   y  x ~~> y.
69
Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89

Lemma cmra_updateP_op (P1 P2 Q : A  Prop) x1 x2 :
  x1 ~~>: P1  x2 ~~>: P2  ( y1 y2, P1 y1  P2 y2  Q (y1  y2)) 
  x1  x2 ~~>: Q.
Proof.
  intros Hx1 Hx2 Hy n mz ?.
  destruct (Hx1 n (Some (x2 ? mz))) as (y1&?&?).
  { by rewrite /= -cmra_opM_assoc. }
  destruct (Hx2 n (Some (y1 ? mz))) as (y2&?&?).
  { by rewrite /= -cmra_opM_assoc (comm _ x2) cmra_opM_assoc. }
  exists (y1  y2); split; last rewrite (comm _ y1) cmra_opM_assoc; auto.
Qed.
Lemma cmra_updateP_op' (P1 P2 : A  Prop) x1 x2 :
  x1 ~~>: P1  x2 ~~>: P2 
  x1  x2 ~~>: λ y,  y1 y2, y = y1  y2  P1 y1  P2 y2.
Proof. eauto 10 using cmra_updateP_op. Qed.
Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1  x2 ~~> y2  x1  x2 ~~> y1  y2.
Proof.
  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
Qed.
90
91
92
93
94
95
96
Lemma cmra_update_valid0 x y :
  ({0} x  x ~~> y)  x ~~> y.
Proof.
  intros H n mz Hmz. apply H, Hmz.
  apply (cmra_validN_le n); last lia.
  destruct mz. eapply cmra_validN_op_l, Hmz. apply Hmz.
Qed.
97

98
Lemma cmra_step_stepP (x xl y yl: A) : 
99
  x # xl ~~>> y #' yl  (x # xl ~~>>: (λ x xl, y = x  yl = xl)).
100
101
102
103
104
105
106
107
108
109
110
111
112
113
Proof.
  split.
  - by intros Hx n z ?; exists y, yl;  destruct (Hx n z) as (?&?); auto.
  - intros Hx n z ?. destruct (Hx n z) as (?&?&(<-&<-)&?); auto.  
Qed.

Lemma cmra_step_updateP_weaken (P Q : A  A  Prop) x xl: 
  x # xl ~~>>: P  ( y yl, P y yl  Q y yl)  x # xl ~~>>: Q.
Proof.
  intros Hs HPQ n z Hval.
  edestruct (Hs n z Hval) as (y&yl&HP&Hval'&Hs').
  exists y, yl. split_and!; eauto.
Qed.

114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
(** ** Frame preserving updates for total CMRAs *)
Section total_updates.
  Context `{CMRATotal A}.

  Lemma cmra_total_updateP x (P : A  Prop) :
    x ~~>: P   n z, {n} (x  z)   y, P y  {n} (y  z).
  Proof.
    split=> Hup; [intros n z; apply (Hup n (Some z))|].
    intros n [z|] ?; simpl; [by apply Hup|].
    destruct (Hup n (core x)) as (y&?&?); first by rewrite cmra_core_r.
    eauto using cmra_validN_op_l.
  Qed.
  Lemma cmra_total_update x y : x ~~> y   n z, {n} (x  z)  {n} (y  z).
  Proof. rewrite cmra_update_updateP cmra_total_updateP. naive_solver. Qed.

129
130
131
132
133
134
135
136
137
138
139
  Lemma cmra_total_step_updateP (x : A) (xl: A) (P : A  A  Prop) : 
    x # xl ~~>>: P 
     n z, {n} (x  xl   z)   y yl, P y yl  {n} (y  yl  z)  xl _(n) yl.
  Proof.
    split=> Hup; [intros n z; apply (Hup n (Some z))|].
    intros n [z|] ?; simpl; [by apply Hup|].
    destruct (Hup n (core (x  xl))) as (y&yl&?&?&?); first by rewrite cmra_core_r.
    do 2 eexists. split_and!; eauto using cmra_validN_op_l.
  Qed.
  
  Lemma cmra_total_step_update (x xl y yl : A) : 
140
   (x # xl ~~>> y #' yl) 
141
142
143
144
     n z,
      {n} (x  xl  z)  {n} (y  yl  z)  xl _(n) yl.
  Proof. rewrite cmra_step_stepP cmra_total_step_updateP. naive_solver. Qed.

145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
  Context `{CMRADiscrete A}.

  Lemma cmra_discrete_updateP (x : A) (P : A  Prop) :
    x ~~>: P   z,  (x  z)   y, P y   (y  z).
  Proof.
    rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff.
    naive_solver eauto using 0.
  Qed.
  Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
    x ~~> y   z,  (x  z)   (y  z).
  Proof.
    rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff.
    naive_solver eauto using 0.
  Qed.
End total_updates.
160
End updates.
161

162
163
164
165
166
167
Section unit_updates.
  Context {A: ucmraT}.
  Implicit Types x y : A.
  Lemma ucmra_update_unit x : x ~~> .
  Proof. apply cmra_total_update=>n z. rewrite left_id; apply cmra_validN_op_r. Qed.
  Lemma ucmra_update_unit_alt y :  ~~> y   x, x ~~> y.
168
  Proof. split; [intros; trans ( : A)|]; auto using ucmra_update_unit. Qed.
169
170
171
End unit_updates.


172
(** * Transport *)
173
174
175
176
177
178
179
180
181
Section cmra_transport.
  Context {A B : cmraT} (H : A = B).
  Notation T := (cmra_transport H).
  Lemma cmra_transport_updateP (P : A  Prop) (Q : B  Prop) x :
    x ~~>: P  ( y, P y  Q (T y))  T x ~~>: Q.
  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
  Lemma cmra_transport_updateP' (P : A  Prop) x :
    x ~~>: P  T x ~~>: λ y,  y', y = cmra_transport H y'  P y'.
  Proof. eauto using cmra_transport_updateP. Qed.
182
183
184
185
186
187
188
189
190
191
192
193
  Lemma cmra_transport_update x y :
    x ~~> y  T x ~~> T y.
  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
  Lemma cmra_transport_step_updateP (P : A  A  Prop) (Q : B  B  Prop) x xl :
    x # xl ~~>>: P  ( y yl, P y yl  Q (T y) (T yl))  T x # T xl ~~>>: Q.
  Proof. destruct H. eauto using cmra_step_updateP_weaken. Qed.
  Lemma cmra_transport_step_updateP' (P : A  A  Prop) (Q : B  B  Prop) x xl :
    x # xl ~~>>: P  
    T x # T xl ~~>>: (λ y yl,  y' yl', y = cmra_transport H y'
                                         yl = cmra_transport H yl'  P y' yl').
  Proof. intros. eapply cmra_transport_step_updateP; eauto. Qed.
  Lemma cmra_transport_step_update x xl y yl :
194
    x # xl ~~>> y #' yl  T x # T xl ~~>> T y #' T yl.
195
  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
196
197
End cmra_transport.

198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
(** * ucmra Transport *)
Section ucmra_transport.
  Context {A B : ucmraT} (H : A = B).
  Notation T := (ucmra_transport H).
  Lemma ucmra_transport_updateP (P : A  Prop) (Q : B  Prop) x :
    x ~~>: P  ( y, P y  Q (T y))  T x ~~>: Q.
  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
  Lemma ucmra_transport_updateP' (P : A  Prop) x :
    x ~~>: P  T x ~~>: λ y,  y', y = ucmra_transport H y'  P y'.
  Proof. eauto using ucmra_transport_updateP. Qed.
  Lemma ucmra_transport_update x y :
    x ~~> y  T x ~~> T y.
  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
  Lemma ucmra_transport_step_updateP (P : A  A  Prop) (Q : B  B  Prop) x xl :
    x # xl ~~>>: P  ( y yl, P y yl  Q (T y) (T yl))  T x # T xl ~~>>: Q.
  Proof. destruct H. eauto using cmra_step_updateP_weaken. Qed.
  Lemma ucmra_transport_step_updateP' (P : A  A  Prop) (Q : B  B  Prop) x xl :
    x # xl ~~>>: P  
    T x # T xl ~~>>: (λ y yl,  y' yl', y = ucmra_transport H y'
                                         yl = ucmra_transport H yl'  P y' yl').
  Proof. intros. eapply ucmra_transport_step_updateP; eauto. Qed.
  Lemma ucmra_transport_step_update x xl y yl :
220
    x # xl ~~>> y #' yl  T x # T xl ~~>> T y #' T yl.
221
222
223
  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
End ucmra_transport.

224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
(** * Product *)
Section prod.
  Context {A B : cmraT}.
  Implicit Types x : A * B.

  Lemma prod_updateP P1 P2 (Q : A * B  Prop) x :
    x.1 ~~>: P1  x.2 ~~>: P2  ( a b, P1 a  P2 b  Q (a,b))  x ~~>: Q.
  Proof.
    intros Hx1 Hx2 HP n mz [??]; simpl in *.
    destruct (Hx1 n (fst <$> mz)) as (a&?&?); first by destruct mz.
    destruct (Hx2 n (snd <$> mz)) as (b&?&?); first by destruct mz.
    exists (a,b); repeat split; destruct mz; auto.
  Qed.
  Lemma prod_updateP' P1 P2 x :
    x.1 ~~>: P1  x.2 ~~>: P2  x ~~>: λ y, P1 (y.1)  P2 (y.2).
  Proof. eauto using prod_updateP. Qed.
  Lemma prod_update x y : x.1 ~~> y.1  x.2 ~~> y.2  x ~~> y.
  Proof.
    rewrite !cmra_update_updateP.
    destruct x, y; eauto using prod_updateP with subst.
  Qed.
End prod.

(** * Option *)
Section option.
  Context {A : cmraT}.
  Implicit Types x y : A.

  Lemma option_updateP (P : A  Prop) (Q : option A  Prop) x :
    x ~~>: P  ( y, P y  Q (Some y))  Some x ~~>: Q.
  Proof.
    intros Hx Hy; apply cmra_total_updateP=> n [y|] ?.
    { destruct (Hx n (Some y)) as (y'&?&?); auto. exists (Some y'); auto. }
    destruct (Hx n None) as (y'&?&?); rewrite ?cmra_core_r; auto.
    by exists (Some y'); auto.
  Qed.
  Lemma option_updateP' (P : A  Prop) x :
    x ~~>: P  Some x ~~>: from_option P False.
  Proof. eauto using option_updateP. Qed.
  Lemma option_update x y : x ~~> y  Some x ~~> Some y.
264
  Proof. rewrite !cmra_update_updateP; eauto using option_updateP with subst. Qed.
265
End option.