gmap.v 18.8 KB
Newer Older
1
From fri.algebra Require Export cmra.
2
From stdpp Require Export gmap.
3
From fri.algebra Require Import upred upred_bi updates local_updates.
4

5
Section cofe.
6
Context `{Countable K} {A : ofeT}.
7
Implicit Types m : gmap K A.
8

9
Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
10
   i, m1 !! i {n} m2 !! i.
11
Definition gmap_cofe_mixin : OfeMixin (gmap K A).
12
13
Proof.
  split.
14
  - intros m1 m2; split.
15
16
    + by intros Hm n k; apply equiv_dist.
    + intros Hm k; apply equiv_dist; intros n; apply Hm.
17
  - intros n; split.
18
19
    + by intros m k.
    + by intros m1 m2 ? k.
20
    + by intros m1 m2 m3 ?? k; trans (m2 !! k).
21
  - by intros n m1 m2 ? k; apply dist_S.
22
Qed.
23
24
Canonical Structure gmapO : ofeT := OfeT (gmap K A) gmap_cofe_mixin.
Global Instance gmap_discrete : OfeDiscrete A  OfeDiscrete gmapO.
25
Proof. intros ? m m' ? i. by apply (discrete _). Qed.
26
(* why doesn't this go automatic? *)
27
Global Instance gmapO_leibniz: LeibnizEquiv A  LeibnizEquiv gmapO.
28
29
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.

30
Global Instance lookup_ne n k :
31
  Proper (dist n ==> dist n) (lookup k : gmap K A  option A).
32
Proof. by intros m1 m2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
Global Instance lookup_proper k :
  Proper (() ==> ()) (lookup k : gmap K A  option A) := _.
35
36
37
38
Global Instance alter_ne f k n :
  Proper (dist n ==> dist n) f  Proper (dist n ==> dist n) (alter f k).
Proof.
  intros ? m m' Hm k'.
39
  by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
40
Qed.
41
Global Instance insert_ne i n :
42
  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
43
Proof.
44
  intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
45
46
    [by constructor|by apply lookup_ne].
Qed.
47
Global Instance singleton_ne i n :
48
49
  Proper (dist n ==> dist n) (singletonM i : A  gmap K A).
Proof. by intros ???; apply insert_ne. Qed.
50
Global Instance delete_ne i n :
51
  Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
52
Proof.
53
  intros m m' ? j; destruct (decide (i = j)); simplify_map_eq;
54
55
    [by constructor|by apply lookup_ne].
Qed.
56

57
Global Instance gmap_empty_timeless : Discrete ( : gmap K A).
58
59
60
61
Proof.
  intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
  inversion_clear Hm; constructor.
Qed.
62
Global Instance gmap_lookup_timeless m i : Discrete m  Discrete (m !! i).
63
Proof.
64
  intros ? [x|] Hx; [|by symmetry; apply: discrete].
65
  assert (m {0} <[i:=x]> m)
66
67
    by (by symmetry in Hx; inversion Hx; ofe_subst; rewrite insert_id).
  by rewrite (discrete m (<[i:=x]>m)) // lookup_insert.
68
Qed.
69
Global Instance gmap_insert_timeless m i x :
70
  Discrete x  Discrete m  Discrete (<[i:=x]>m).
71
Proof.
72
  intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq.
73
74
  { by apply: discrete; rewrite -Hm lookup_insert. }
  by apply: discrete; rewrite -Hm lookup_insert_ne.
75
Qed.
76
Global Instance gmap_singleton_timeless i x :
77
  Discrete x  Discrete ({[ i := x ]} : gmap K A) := _.
78
End cofe.
79

80
Arguments gmapO _ {_ _} _.
81
82

(* CMRA *)
83
84
Section cmra.
Context `{Countable K} {A : cmraT}.
85
Implicit Types m : gmap K A.
86

87
Instance gmap_op : Op (gmap K A) := merge op.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m).
89
90
Instance gmap_valid : Valid (gmap K A) := λ m,  i,  (m !! i).
Instance gmap_validN : ValidN (gmap K A) := λ n m,  i, {n} (m !! i).
91
Instance gmap_stepN : StepN (gmap K A) :=  λ n m1 m2,  i, (m1 !! i) _(n) (m2 !! i).
92

93
Lemma lookup_op m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
94
Proof. by apply lookup_merge. Qed.
Ralf Jung's avatar
Ralf Jung committed
95
Lemma lookup_core m i : core m !! i = core (m !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Proof. by apply lookup_omap. Qed.
97

98
Lemma lookup_included (m1 m2 : gmap K A) : m1  m2   i, m1 !! i  m2 !! i.
99
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
102
103
104
  split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|].
  revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm.
  { exists m2. by rewrite left_id. }
  destruct (IH (delete i m2)) as [m2' Hm2'].
  { intros j. move: (Hm j); destruct (decide (i = j)) as [->|].
105
    - intros _. rewrite Hi. apply: ucmra_unit_least.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
109
110
111
    - rewrite lookup_insert_ne // lookup_delete_ne //. }
  destruct (Hm i) as [my Hi']; simplify_map_eq.
  exists (partial_alter (λ _, my) i m2')=>j; destruct (decide (i = j)) as [->|].
  - by rewrite Hi' lookup_op lookup_insert lookup_partial_alter.
  - move: (Hm2' j). by rewrite !lookup_op lookup_delete_ne //
      lookup_insert_ne // lookup_partial_alter_ne.
112
Qed.
113

114
Lemma gmap_cmra_mixin : CMRAMixin (gmap K A).
115
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
118
119
120
  apply cmra_total_mixin.
  - eauto.
  - intros n m1 m2 m3 Hm i; by rewrite !lookup_op (Hm i).
  - intros n m1 m2 Hm i; by rewrite !lookup_core (Hm i).
  - intros n m1 m2 Hm ? i; by rewrite -(Hm i).
121
122
123
  - intros m; split.
    + by intros ? n i; apply cmra_valid_validN.
    + intros Hm i; apply cmra_valid_validN=> n; apply Hm.
124
  - intros n m Hm i; apply cmra_validN_S, Hm.
125
126
127
  - intros n m1 m1' Hm1 m2 m2' Hm2 Hs i. 
    specialize (Hs i); rewrite -Hm1 -Hm2 in Hs *; eauto.
  - intros n m1 m1' Hs i. specialize (Hs i); eapply cmra_stepN_S; eauto.
128
129
  - by intros m1 m2 m3 i; rewrite !lookup_op assoc.
  - by intros m1 m2 i; rewrite !lookup_op comm.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
132
  - intros m i. by rewrite lookup_op lookup_core cmra_core_l.
  - intros m i. by rewrite !lookup_core cmra_core_idemp.
  - intros m1 m2; rewrite !lookup_included=> Hm i.
133
    rewrite !lookup_core. by apply cmra_core_mono.
134
135
  - intros n x y Hval i. rewrite !lookup_core ?lookup_op !lookup_core cmra_core_distrib //=.
    specialize (Hval i). rewrite !lookup_op in Hval; auto.
136
  - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
137
    by rewrite -lookup_op.
138
139
140
141
142
143
  - intros n m m1 m2 Hm Hm12.
    assert ( i, m !! i {n} m1 !! i  m2 !! i) as Hm12'
      by (by intros i; rewrite -lookup_op).
    set (f i := cmra_extend n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
    set (f_proj i := proj1_sig (f i)).
    exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
Robbert Krebbers's avatar
Robbert Krebbers committed
144
      repeat split; intros i; rewrite /= ?lookup_op !map_lookup_imap.
145
146
147
    + destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
      rewrite -Hx; apply (proj2_sig (f i)).
    + destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
148
      move: (Hm12' i). rewrite Hx -!discrete_iff.
149
      rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
150
    + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
151
      move: (Hm12' i). rewrite Hx -!discrete_iff.
152
      rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
153
Qed.
154
Canonical Structure gmapR :=
155
  CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
156
157
158
159
160

Global Instance gmap_cmra_discrete : CMRADiscrete A  CMRADiscrete gmapR.
Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.

Lemma gmap_ucmra_mixin : UCMRAMixin (gmap K A).
161
162
Proof.
  split.
163
  - by intros i; rewrite lookup_empty.
164
  - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
165
  - apply gmap_empty_timeless.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  - constructor=> i. by rewrite lookup_omap lookup_empty.
167
Qed.
168
169
Canonical Structure gmapUR :=
  UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
170
171

(** Internalized properties *)
172
Lemma gmap_equivI {M} m1 m2 : m1  m2 ⊣⊢ ( i, m1 !! i  m2 !! i : uPred M).
173
Proof. by uPred.unseal. Qed.
174
Lemma gmap_validI {M} m :  m ⊣⊢ ( i,  (m !! i) : uPred M).
175
Proof. by uPred.unseal. Qed.
176
End cmra.
177

178
Arguments gmapR _ {_ _} _.
179
Arguments gmapUR _ {_ _} _.
180
181

Section properties.
182
Context `{Countable K} {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
Implicit Types m : gmap K A.
184
Implicit Types i : K.
185
186
Implicit Types x y : A.

Robbert Krebbers's avatar
Robbert Krebbers committed
187
Lemma lookup_opM m1 mm2 i : (m1 ? mm2) !! i = m1 !! i  (mm2 = (.!! i)).
188
Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
189

190
Lemma lookup_validN_Some n m i x : {n} m  m !! i {n} Some x  {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
192
Lemma lookup_valid_Some m i x :  m  m !! i  Some x   x.
193
Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed.
194
Lemma insert_validN n m i x : {n} x  {n} m  {n} <[i:=x]>m.
195
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
196
Lemma insert_valid m i x :  x   m   <[i:=x]>m.
197
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
198
Lemma singleton_validN n i x : {n} ({[ i := x ]} : gmap K A)  {n} x.
199
Proof.
200
  split; [|by intros; apply insert_validN, ucmra_unit_validN].
201
  by move=>/(_ i); simplify_map_eq.
202
Qed.
203
204
Lemma singleton_valid i x :  ({[ i := x ]} : gmap K A)   x.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
205

206
Lemma insert_singleton_op m i x : m !! i = None  <[i:=x]> m = {[ i := x ]}  m.
207
Proof.
208
209
210
  intros Hi; apply map_eq=> j; destruct (decide (i = j)) as [->|].
  - by rewrite lookup_op lookup_insert lookup_singleton Hi right_id_L.
  - by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id_L.
211
212
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
213
214
215
216
217
Lemma core_singleton (i : K) (x : A) cx :
  pcore x = Some cx  core ({[ i := x ]} : gmap K A) = {[ i := cx ]}.
Proof. apply omap_singleton. Qed.
Lemma core_singleton' (i : K) (x : A) cx :
  pcore x  Some cx  core ({[ i := x ]} : gmap K A)  {[ i := cx ]}.
218
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
219
220
  intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx').
Qed.
221
Lemma op_singleton (i : K) (x y : A) :
222
  {[ i := x ]}  {[ i := y ]} = ({[ i := x  y ]} : gmap K A).
223
Proof. by apply (merge_singleton _ _ _ x y). Qed.
224

225
Global Instance gmap_persistent m : ( x : A, cmra.Persistent x)  cmra.Persistent m.
Robbert Krebbers's avatar
Robbert Krebbers committed
226
227
228
229
Proof.
  intros; apply persistent_total=> i.
  rewrite lookup_core. apply (persistent_core _).
Qed.
230
Global Instance gmap_singleton_persistent i (x : A) :
231
  cmra.Persistent x  cmra.Persistent {[ i := x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
Proof. intros. by apply persistent_total, core_singleton'. Qed.
233

Robbert Krebbers's avatar
Robbert Krebbers committed
234
Lemma singleton_includedN n m i x :
Robbert Krebbers's avatar
Robbert Krebbers committed
235
  {[ i := x ]} {n} m   y, m !! i {n} Some y  (x {n} y  x {n} y).
Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
238
239
240
  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
    case (m' !! i)=> [y|]=> Hm.
    + exists (x  y); eauto using cmra_includedN_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
241
242
243
244
245
246
247
248
    + exists x; eauto.
  - intros (y&Hi&[[z ?]| ->]).
    + exists (<[i:=z]>m)=> j; destruct (decide (i = j)) as [->|].
      * rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor.
      * by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id.
    + exists (delete i m)=> j; destruct (decide (i = j)) as [->|].
      * by rewrite Hi lookup_op lookup_singleton lookup_delete.
      * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
249
Qed.
250
Lemma dom_op m1 m2 : dom (gset K) (m1  m2) = dom _ m1  dom _ m2.
251
Proof.
252
  apply elem_of_equiv_L=> i; rewrite elem_of_union !elem_of_dom.
253
254
255
  unfold is_Some; setoid_rewrite lookup_op.
  destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
256

257
Lemma insert_updateP (P : A  Prop) (Q : gmap K A  Prop) m i x :
258
  x ~~>: P  ( y, P y  Q (<[i:=y]>m))  <[i:=x]>m ~~>: Q.
259
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
260
261
  intros Hx%option_updateP' HP; apply cmra_total_updateP=> n mf Hm.
  destruct (Hx n (Some (mf !! i))) as ([y|]&?&?); try done.
262
  { by generalize (Hm i); rewrite lookup_op; simplify_map_eq. }
263
264
  exists (<[i:=y]> m); split; first by auto.
  intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
265
  destruct (decide (i = j)); simplify_map_eq/=; auto.
266
Qed.
267
Lemma insert_updateP' (P : A  Prop) m i x :
268
  x ~~>: P  <[i:=x]>m ~~>: λ m',  y, m' = <[i:=y]>m  P y.
269
270
271
Proof. eauto using insert_updateP. Qed.
Lemma insert_update m i x y : x ~~> y  <[i:=x]>m ~~> <[i:=y]>m.
Proof. rewrite !cmra_update_updateP; eauto using insert_updateP with subst. Qed.
272

273
Lemma singleton_updateP (P : A  Prop) (Q : gmap K A  Prop) i x :
274
  x ~~>: P  ( y, P y  Q {[ i := y ]})  {[ i := x ]} ~~>: Q.
275
276
Proof. apply insert_updateP. Qed.
Lemma singleton_updateP' (P : A  Prop) i x :
277
  x ~~>: P  {[ i := x ]} ~~>: λ m,  y, m = {[ i := y ]}  P y.
278
279
280
Proof. apply insert_updateP'. Qed.
Lemma singleton_update i (x y : A) : x ~~> y  {[ i := x ]} ~~> {[ i := y ]}.
Proof. apply insert_update. Qed.
281

282
Lemma delete_update m i : m ~~> delete i m.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
Proof.
284
285
286
287
  apply cmra_total_update=> n mf Hm j; destruct (decide (i = j)); subst.
  - move: (Hm j). rewrite !lookup_op lookup_delete left_id.
    apply cmra_validN_op_r.
  - move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
288
Qed.
289

290
Section freshness.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  Context `{Infinite K}.
292
293
294
295
296
297
298
299
  Lemma alloc_updateP_strong (Q : gmap K A  Prop) (I : gset K) m x :
     x  ( i, m !! i = None  i  I  Q (<[i:=x]>m))  m ~~>: Q.
  Proof.
    intros ? HQ. apply cmra_total_updateP.
    intros n mf Hm. set (i := fresh (I  dom (gset K) (m  mf))).
    assert (i  I  i  dom (gset K) m  i  dom (gset K) mf) as [?[??]].
    { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
    exists (<[i:=x]>m); split.
300
301
    { apply HQ; last done. by eapply not_elem_of_dom. }
    rewrite insert_singleton_op; first by eapply not_elem_of_dom.
302
    rewrite -assoc -insert_singleton_op;
303
      first by eapply (not_elem_of_dom (D:=gset K)); rewrite dom_op not_elem_of_union.
304
305
306
307
308
309
310
311
312
313
314
315
    by apply insert_validN; [apply cmra_valid_validN|].
  Qed.
  Lemma alloc_updateP (Q : gmap K A  Prop) m x :
     x  ( i, m !! i = None  Q (<[i:=x]>m))  m ~~>: Q.
  Proof. move=>??. eapply alloc_updateP_strong with (I:=); by eauto. Qed.
  Lemma alloc_updateP_strong' m x (I : gset K) :
     x  m ~~>: λ m',  i, i  I  m' = <[i:=x]>m  m !! i = None.
  Proof. eauto using alloc_updateP_strong. Qed.
  Lemma alloc_updateP' m x :
     x  m ~~>: λ m',  i, m' = <[i:=x]>m  m !! i = None.
  Proof. eauto using alloc_updateP. Qed.

316
  Lemma alloc_unit_singleton_updateP (P : A  Prop) (Q : gmap K A  Prop) u i :
317
318
319
320
321
322
323
324
325
326
327
328
329
330
     u  LeftId () u () 
    u ~~>: P  ( y, P y  Q {[ i := y ]})   ~~>: Q.
  Proof.
    intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
    destruct (Hx n (gf !! i)) as (y&?&Hy).
    { move:(Hg i). rewrite !left_id.
      case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
      intros; by apply cmra_valid_validN. }
    exists {[ i := y ]}; split; first by auto.
    intros i'; destruct (decide (i' = i)) as [->|].
    - rewrite lookup_op lookup_singleton.
      move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
    - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
  Qed.
331
  Lemma alloc_unit_singleton_updateP' (P: A  Prop) u i :
332
333
     u  LeftId () u () 
    u ~~>: P   ~~>: λ m,  y, m = {[ i := y ]}  P y.
334
335
  Proof. eauto using alloc_unit_singleton_updateP. Qed.
  Lemma alloc_unit_singleton_update u i (y : A) :
336
337
     u  LeftId () u ()  u ~~> y   ~~> {[ i := y ]}.
  Proof.
338
339
    rewrite !cmra_update_updateP;
      eauto using alloc_unit_singleton_updateP with subst.
340
  Qed.
341
342
End freshness.

343
Lemma insert_local_update m i x y mf :
Robbert Krebbers's avatar
Robbert Krebbers committed
344
  x ~l~> y @ mf = (.!! i)  <[i:=x]>m ~l~> <[i:=y]>m @ mf.
345
Proof.
346
347
348
349
350
351
352
353
  intros [Hxy Hxy']; split.
  - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
    + rewrite !lookup_opM !lookup_insert !Some_op_opM. apply Hxy.
    + by rewrite !lookup_opM !lookup_insert_ne.
  - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
    destruct (decide (i = j)); subst.
    + rewrite !lookup_opM !lookup_insert !Some_op_opM !inj_iff. apply Hxy'.
    + by rewrite !lookup_opM !lookup_insert_ne.
354
Qed.
355

356
Lemma singleton_local_update i x y mf :
Robbert Krebbers's avatar
Robbert Krebbers committed
357
  x ~l~> y @ mf = (.!! i)  {[ i := x ]} ~l~> {[ i := y ]} @ mf.
358
Proof. apply insert_local_update. Qed.
359

360
361
362
363
364
365
366
367
368
369
370
371
Lemma alloc_singleton_local_update m i x mf :
  (m ? mf) !! i = None   x  m ~l~> <[i:=x]> m @ mf.
Proof.
  rewrite lookup_opM op_None=> -[Hi Hif] ?.
  rewrite insert_singleton_op // comm. apply alloc_local_update.
  intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
  - intros _; rewrite !lookup_opM lookup_op !lookup_singleton Hif Hi.
    by apply cmra_valid_validN.
  - by rewrite !lookup_opM lookup_op !lookup_singleton_ne // right_id.
Qed.

Lemma alloc_unit_singleton_local_update i x mf :
Robbert Krebbers's avatar
Robbert Krebbers committed
372
  mf = (.!! i) = None   x   ~l~> {[ i := x ]} @ mf.
373
Proof.
374
  intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
375
Qed.
376

377
378
Lemma delete_local_update m i x `{!Exclusive x} mf :
  m !! i = Some x  m ~l~> delete i m @ mf.
379
Proof.
380
381
382
383
384
385
386
  intros Hx; split; [intros n; apply delete_update|].
  intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
  destruct (decide (i = j)); subst.
  + rewrite !lookup_opM !lookup_delete Hx=> ? Hj.
    rewrite (exclusiveN_Some_l n x (mf = lookup j)) //.
    by rewrite (exclusiveN_Some_l n x (mf' = lookup j)) -?Hj.
  + by rewrite !lookup_opM !lookup_delete_ne.
387
Qed.
388
389
End properties.

390
(** Functor *)
391
Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A  B) n :
392
393
  Proper (dist n ==> dist n) f  Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
394
Instance gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A  B)
395
396
  `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A  gmap K B).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
397
  split; try apply _.
398
  - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
399
  - intros m1 m2; rewrite !lookup_included=> Hm i.
400
    by rewrite !lookup_fmap; apply: cmra_monotone.
401
Qed.
402
403
404
405
Definition gmapO_map `{Countable K} {A B} (f: A -n> B) :
  gmapO K A -n> gmapO K B := OfeMor (fmap f : gmapO K A  gmapO K B).
Instance gmapO_map_ne `{Countable K} {A B} n :
  Proper (dist n ==> dist n) (@gmapO_map K _ _ A B).
406
407
408
409
Proof.
  intros f g Hf m k; rewrite /= !lookup_fmap.
  destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
Ralf Jung's avatar
Ralf Jung committed
410

411
412
413
Program Definition gmapOF K `{Countable K} (F : oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := gmapO K (oFunctor_car F A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (oFunctor_map F fg)
Ralf Jung's avatar
Ralf Jung committed
414
415
|}.
Next Obligation.
416
  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_ne.
Ralf Jung's avatar
Ralf Jung committed
417
418
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
419
  intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
420
  apply map_fmap_equiv_ext=>y ??; apply oFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
421
422
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
423
  intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
424
  apply map_fmap_equiv_ext=>y ??; apply oFunctor_compose.
425
Qed.
426
427
Instance gmapOF_contractive K `{Countable K} F :
  oFunctorContractive F  oFunctorContractive (gmapOF K F).
428
Proof.
429
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_contractive.
430
Qed.
431

432
Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
433
  urFunctor_car A _ B _ := gmapUR K (rFunctor_car F A B);
434
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
435
436
|}.
Next Obligation.
437
  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_ne.
438
439
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
440
  intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
441
  apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
442
443
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
444
  intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
445
  apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
446
Qed.
447
Instance gmapRF_contractive K `{Countable K} F :
448
  rFunctorContractive F  urFunctorContractive (gmapURF K F).
449
Proof.
450
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_contractive.
451
Qed.