gmap.v 23.8 KB
Newer Older
1
From iris.algebra Require Export cmra.
Dan Frumin's avatar
Dan Frumin committed
2
From stdpp Require Export list gmap.
3 4
From iris.algebra Require Import updates local_updates.
From iris.base_logic Require Import base_logic.
5
From iris.algebra Require Import proofmode_classes.
6
Set Default Proof Using "Type".
7

8
Section cofe.
9
Context `{Countable K} {A : ofeT}.
10
Implicit Types m : gmap K A.
11
Implicit Types i : K.
12

13
Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
14
   i, m1 !! i {n} m2 !! i.
15
Definition gmap_ofe_mixin : OfeMixin (gmap K A).
16 17
Proof.
  split.
18
  - intros m1 m2; split.
19 20
    + by intros Hm n k; apply equiv_dist.
    + intros Hm k; apply equiv_dist; intros n; apply Hm.
21
  - intros n; split.
22 23
    + by intros m k.
    + by intros m1 m2 ? k.
24
    + by intros m1 m2 m3 ?? k; trans (m2 !! k).
25
  - by intros n m1 m2 ? k; apply dist_S.
26
Qed.
27
Canonical Structure gmapO : ofeT := OfeT (gmap K A) gmap_ofe_mixin.
28

29 30
Program Definition gmap_chain (c : chain gmapO)
  (k : K) : chain (optionO A) := {| chain_car n := c n !! k |}.
31
Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
32
Definition gmap_compl `{Cofe A} : Compl gmapO := λ c,
33
  map_imap (λ i _, compl (gmap_chain c i)) (c 0).
34
Global Program Instance gmap_cofe `{Cofe A} : Cofe gmapO :=
35 36
  {| compl := gmap_compl |}.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  intros ? n c k. rewrite /compl /gmap_compl map_lookup_imap.
38 39 40 41
  feed inversion (λ H, chain_cauchy c 0 n H k);simplify_option_eq;auto with lia.
  by rewrite conv_compl /=; apply reflexive_eq.
Qed.

42
Global Instance gmap_ofe_discrete : OfeDiscrete A  OfeDiscrete gmapO.
43
Proof. intros ? m m' ? i. by apply (discrete _). Qed.
44
(* why doesn't this go automatic? *)
45
Global Instance gmapO_leibniz: LeibnizEquiv A  LeibnizEquiv gmapO.
46 47
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.

48 49
Global Instance lookup_ne k :
  NonExpansive (lookup k : gmap K A  option A).
50
Proof. by intros m1 m2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52
Global Instance lookup_proper k :
  Proper (() ==> ()) (lookup k : gmap K A  option A) := _.
53 54 55 56
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'.
57
  by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
58
Qed.
59 60
Global Instance insert_ne i :
  NonExpansive2 (insert (M:=gmap K A) i).
61
Proof.
62
  intros n x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
63 64
    [by constructor|by apply lookup_ne].
Qed.
65 66 67 68 69
Global Instance singleton_ne i :
  NonExpansive (singletonM i : A  gmap K A).
Proof. by intros ????; apply insert_ne. Qed.
Global Instance delete_ne i :
  NonExpansive (delete (M:=gmap K A) i).
70
Proof.
71
  intros n m m' ? j; destruct (decide (i = j)); simplify_map_eq;
72 73
    [by constructor|by apply lookup_ne].
Qed.
74

75
Global Instance gmap_empty_discrete : Discrete ( : gmap K A).
76 77 78 79
Proof.
  intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
  inversion_clear Hm; constructor.
Qed.
80
Global Instance gmap_lookup_discrete m i : Discrete m  Discrete (m !! i).
81
Proof.
82
  intros ? [x|] Hx; [|by symmetry; apply: discrete].
83
  assert (m {0} <[i:=x]> m)
84
    by (by symmetry in Hx; inversion Hx; ofe_subst; rewrite insert_id).
85
  by rewrite (discrete m (<[i:=x]>m)) // lookup_insert.
86
Qed.
87 88
Global Instance gmap_insert_discrete m i x :
  Discrete x  Discrete m  Discrete (<[i:=x]>m).
89
Proof.
90
  intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq.
91 92
  { by apply: discrete; rewrite -Hm lookup_insert. }
  by apply: discrete; rewrite -Hm lookup_insert_ne.
93
Qed.
94 95
Global Instance gmap_singleton_discrete i x :
  Discrete x  Discrete ({[ i := x ]} : gmap K A) := _.
96 97 98
Lemma insert_idN n m i x :
  m !! i {n} Some x  <[i:=x]>m {n} m.
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
99
End cofe.
100

101
Arguments gmapO _ {_ _} _.
102 103

(* CMRA *)
104 105
Section cmra.
Context `{Countable K} {A : cmraT}.
106
Implicit Types m : gmap K A.
107

Robbert Krebbers's avatar
Robbert Krebbers committed
108
Instance gmap_unit : Unit (gmap K A) := ( : gmap K A).
109
Instance gmap_op : Op (gmap K A) := merge op.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m).
111 112
Instance gmap_valid : Valid (gmap K A) := λ m,  i,  (m !! i).
Instance gmap_validN : ValidN (gmap K A) := λ n m,  i, {n} (m !! i).
113

114
Lemma lookup_op m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
115
Proof. by apply lookup_merge. Qed.
Ralf Jung's avatar
Ralf Jung committed
116
Lemma lookup_core m i : core m !! i = core (m !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Proof. by apply lookup_omap. Qed.
118

119
Lemma lookup_included (m1 m2 : gmap K A) : m1  m2   i, m1 !! i  m2 !! i.
120
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122 123 124 125
  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 [->|].
126
    - intros _. rewrite Hi. apply: ucmra_unit_least.
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128 129 130 131 132
    - 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.
133
Qed.
134

135
Lemma gmap_cmra_mixin : CmraMixin (gmap K A).
136
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138 139 140 141
  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).
142 143 144
  - intros m; split.
    + by intros ? n i; apply cmra_valid_validN.
    + intros Hm i; apply cmra_valid_validN=> n; apply Hm.
145 146 147
  - intros n m Hm i; apply cmra_validN_S, Hm.
  - 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
148 149 150
  - 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.
151
    rewrite !lookup_core. by apply cmra_core_mono.
152
  - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
153
    by rewrite -lookup_op.
154 155 156 157 158
  - intros n m y1 y2 Hm Heq.
    refine ((λ FUN, _) (λ i, cmra_extend n (m !! i) (y1 !! i) (y2 !! i) (Hm i) _));
      last by rewrite -lookup_op.
    exists (map_imap (λ i _, projT1 (FUN i)) y1).
    exists (map_imap (λ i _, proj1_sig (projT2 (FUN i))) y2).
Robbert Krebbers's avatar
Robbert Krebbers committed
159
    split; [|split]=>i; rewrite ?lookup_op !map_lookup_imap;
160 161 162 163
    destruct (FUN i) as (z1i&z2i&Hmi&Hz1i&Hz2i)=>/=.
    + destruct (y1 !! i), (y2 !! i); inversion Hz1i; inversion Hz2i; subst=>//.
    + revert Hz1i. case: (y1!!i)=>[?|] //.
    + revert Hz2i. case: (y2!!i)=>[?|] //.
164
Qed.
165
Canonical Structure gmapR := CmraT (gmap K A) gmap_cmra_mixin.
166

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

170
Lemma gmap_ucmra_mixin : UcmraMixin (gmap K A).
171 172
Proof.
  split.
173
  - by intros i; rewrite lookup_empty.
174
  - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  - constructor=> i. by rewrite lookup_omap lookup_empty.
176
Qed.
177
Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin.
178 179

(** Internalized properties *)
180
Lemma gmap_equivI {M} m1 m2 : m1  m2 @{uPredI M}  i, m1 !! i  m2 !! i.
181
Proof. by uPred.unseal. Qed.
182
Lemma gmap_validI {M} m :  m @{uPredI M}  i,  (m !! i).
183
Proof. by uPred.unseal. Qed.
184
End cmra.
185

186
Arguments gmapR _ {_ _} _.
187
Arguments gmapUR _ {_ _} _.
188 189

Section properties.
190
Context `{Countable K} {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Implicit Types m : gmap K A.
192
Implicit Types i : K.
193 194
Implicit Types x y : A.

195
Global Instance lookup_op_homomorphism :
196 197
  MonoidHomomorphism op op () (lookup i : gmap K A  option A).
Proof. split; [split|]; try apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
198

199
Lemma lookup_opM m1 mm2 i : (m1 ? mm2) !! i = m1 !! i  (mm2 = (!! i)).
200
Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
201

202
Lemma lookup_validN_Some n m i x : {n} m  m !! i {n} Some x  {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
204
Lemma lookup_valid_Some m i x :  m  m !! i  Some x   x.
205
Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed.
206

207
Lemma insert_validN n m i x : {n} x  {n} m  {n} <[i:=x]>m.
208
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
209
Lemma insert_valid m i x :  x   m   <[i:=x]>m.
210
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
211
Lemma singleton_validN n i x : {n} ({[ i := x ]} : gmap K A)  {n} x.
212
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
213 214 215
  split.
  - move=>/(_ i); by simplify_map_eq.
  - intros. apply insert_validN. done. apply: ucmra_unit_validN.
216
Qed.
217 218
Lemma singleton_valid i x :  ({[ i := x ]} : gmap K A)   x.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
219

220 221 222 223 224
Lemma delete_validN n m i : {n} m  {n} (delete i m).
Proof. intros Hm j; destruct (decide (i = j)); by simplify_map_eq. Qed.
Lemma delete_valid m i :  m   (delete i m).
Proof. intros Hm j; destruct (decide (i = j)); by simplify_map_eq. Qed.

225
Lemma insert_singleton_op m i x : m !! i = None  <[i:=x]> m = {[ i := x ]}  m.
226
Proof.
227 228 229
  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.
230 231
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
232 233 234 235 236 237 238 239
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 ]}.
Proof.
  intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx').
Qed.
240
Lemma op_singleton (i : K) (x y : A) :
241
  {[ i := x ]}  {[ i := y ]} = ({[ i := x  y ]} : gmap K A).
242
Proof. by apply (merge_singleton _ _ _ x y). Qed.
243 244 245
Global Instance is_op_singleton i a a1 a2 :
  IsOp a a1 a2  IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -op_singleton. Qed.
246

247
Global Instance gmap_core_id m : ( x : A, CoreId x)  CoreId m.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
Proof.
249 250
  intros; apply core_id_total=> i.
  rewrite lookup_core. apply (core_id_core _).
Robbert Krebbers's avatar
Robbert Krebbers committed
251
Qed.
252 253 254
Global Instance gmap_singleton_core_id i (x : A) :
  CoreId x  CoreId {[ i := x ]}.
Proof. intros. by apply core_id_total, core_singleton'. Qed.
255

Robbert Krebbers's avatar
Robbert Krebbers committed
256
Lemma singleton_includedN n m i x :
257
  {[ i := x ]} {n} m   y, m !! i {n} Some y  Some x {n} Some y.
Robbert Krebbers's avatar
Robbert Krebbers committed
258 259
Proof.
  split.
260 261 262 263 264 265 266
  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hi.
    exists (x ? m' !! i). rewrite -Some_op_opM.
    split. done. apply cmra_includedN_l.
  - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
    intros j; destruct (decide (i = j)) as [->|].
    + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
    + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
267 268 269
Qed.
(* We do not have [x ≼ y ↔ ∀ n, x ≼{n} y], so we cannot use the previous lemma *)
Lemma singleton_included m i x :
270
  {[ i := x ]}  m   y, m !! i  Some y  Some x  Some y.
271 272 273
Proof.
  split.
  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
274 275 276 277 278 279
    exists (x ? m' !! i). rewrite -Some_op_opM.
    split. done. apply cmra_included_l.
  - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
    intros j; destruct (decide (i = j)) as [->|].
    + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
    + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
Qed.
281 282 283 284 285 286 287
Lemma singleton_included_exclusive m i x :
  Exclusive x   m 
  {[ i := x ]}  m  m !! i  Some x.
Proof.
  intros ? Hm. rewrite singleton_included. split; last by eauto.
  intros (y&?&->%(Some_included_exclusive _)); eauto using lookup_valid_Some.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
288

289 290 291
Global Instance singleton_cancelable i x :
  Cancelable (Some x)  Cancelable {[ i := x ]}.
Proof.
292 293 294 295
  intros ? n m1 m2 Hv EQ j. move: (Hv j) (EQ j). rewrite !lookup_op.
  destruct (decide (i = j)) as [->|].
  - rewrite lookup_singleton. by apply cancelableN.
  - by rewrite lookup_singleton_ne // !(left_id None _).
296 297
Qed.

298 299 300 301 302 303
Global Instance gmap_cancelable (m : gmap K A) :
  ( x : A, IdFree x)  ( x : A, Cancelable x)  Cancelable m.
Proof.
  intros ?? n m1 m2 ?? i. apply (cancelableN (m !! i)); by rewrite -!lookup_op.
Qed.

304 305 306 307
Lemma insert_op m1 m2 i x y :
  <[i:=x  y]>(m1  m2) =  <[i:=x]>m1  <[i:=y]>m2.
Proof. by rewrite (insert_merge () m1 m2 i (x  y) x y). Qed.

308
Lemma insert_updateP (P : A  Prop) (Q : gmap K A  Prop) m i x :
Ralf Jung's avatar
Ralf Jung committed
309 310 311
  x ~~>: P 
  ( y, P y  Q (<[i:=y]>m)) 
  <[i:=x]>m ~~>: Q.
312
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
313 314
  intros Hx%option_updateP' HP; apply cmra_total_updateP=> n mf Hm.
  destruct (Hx n (Some (mf !! i))) as ([y|]&?&?); try done.
315
  { by generalize (Hm i); rewrite lookup_op; simplify_map_eq. }
316 317
  exists (<[i:=y]> m); split; first by auto.
  intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
318
  destruct (decide (i = j)); simplify_map_eq/=; auto.
319
Qed.
320
Lemma insert_updateP' (P : A  Prop) m i x :
321
  x ~~>: P  <[i:=x]>m ~~>: λ m',  y, m' = <[i:=y]>m  P y.
322 323 324
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.
325

326
Lemma singleton_updateP (P : A  Prop) (Q : gmap K A  Prop) i x :
327
  x ~~>: P  ( y, P y  Q {[ i := y ]})  {[ i := x ]} ~~>: Q.
328 329
Proof. apply insert_updateP. Qed.
Lemma singleton_updateP' (P : A  Prop) i x :
330
  x ~~>: P  {[ i := x ]} ~~>: λ m,  y, m = {[ i := y ]}  P y.
331 332 333
Proof. apply insert_updateP'. Qed.
Lemma singleton_update i (x y : A) : x ~~> y  {[ i := x ]} ~~> {[ i := y ]}.
Proof. apply insert_update. Qed.
334

335
Lemma delete_update m i : m ~~> delete i m.
336
Proof.
337 338 339 340
  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.
341
Qed.
342

343 344 345 346 347 348 349 350 351 352 353
Lemma dom_op m1 m2 : dom (gset K) (m1  m2) = dom _ m1  dom _ m2.
Proof.
  apply elem_of_equiv_L=> i; rewrite elem_of_union !elem_of_dom.
  unfold is_Some; setoid_rewrite lookup_op.
  destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Lemma dom_included m1 m2 : m1  m2  dom (gset K) m1  dom _ m2.
Proof.
  rewrite lookup_included=>? i; rewrite !elem_of_dom. by apply is_Some_included.
Qed.

354
Section freshness.
355
  Local Set Default Proof Using "Type*".
356
  Context `{!Infinite K}.
Dan Frumin's avatar
Dan Frumin committed
357 358 359
  Lemma alloc_updateP_strong (Q : gmap K A  Prop) (I : K  Prop) m x :
    pred_infinite I 
     x  ( i, m !! i = None  I i  Q (<[i:=x]>m))  m ~~>: Q.
360
  Proof.
Dan Frumin's avatar
Dan Frumin committed
361 362 363 364 365 366
    move=> /(pred_infinite_set I (C:=gset K)) HP ? HQ.
    apply cmra_total_updateP. intros n mf Hm.
    destruct (HP (dom (gset K) (m  mf))) as [i [Hi1 Hi2]].
    assert (m !! i = None).
    { eapply (not_elem_of_dom (D:=gset K)). revert Hi2.
      rewrite dom_op not_elem_of_union. naive_solver. }
367
    exists (<[i:=x]>m); split.
Dan Frumin's avatar
Dan Frumin committed
368 369 370 371
    - by apply HQ.
    - rewrite insert_singleton_op //.
      rewrite -assoc -insert_singleton_op;
        last by eapply (not_elem_of_dom (D:=gset K)).
372 373 374 375
    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.
Dan Frumin's avatar
Dan Frumin committed
376 377 378 379 380 381 382 383
  Proof.
    move=>??.
    eapply alloc_updateP_strong with (I:=λ _, True);
    eauto using pred_infinite_True.
  Qed.
  Lemma alloc_updateP_strong' m x (I : K  Prop) :
    pred_infinite I 
     x  m ~~>: λ m',  i, I i  m' = <[i:=x]>m  m !! i = None.
384 385 386 387
  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.
Dan Frumin's avatar
Dan Frumin committed
388 389 390 391 392 393 394 395 396 397 398
  Lemma alloc_updateP_cofinite (Q : gmap K A  Prop) (J : gset K) m x :
     x  ( i, m !! i = None  i  J  Q (<[i:=x]>m))  m ~~>: Q.
  Proof.
    eapply alloc_updateP_strong.
    apply (pred_infinite_set (C:=gset K)).
    intros E. exists (fresh (J  E)).
    apply not_elem_of_union, is_fresh.
  Qed.
  Lemma alloc_updateP_cofinite' m x (J : gset K) :
     x  m ~~>: λ m',  i, i  J  m' = <[i:=x]>m  m !! i = None.
  Proof. eauto using alloc_updateP_cofinite. Qed.
399 400
End freshness.

401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426
Lemma alloc_unit_singleton_updateP (P : A  Prop) (Q : gmap K A  Prop) u i :
   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.
Lemma alloc_unit_singleton_updateP' (P: A  Prop) u i :
   u  LeftId () u () 
  u ~~>: P   ~~>: λ m,  y, m = {[ i := y ]}  P y.
Proof. eauto using alloc_unit_singleton_updateP. Qed.
Lemma alloc_unit_singleton_update (u : A) i (y : A) :
   u  LeftId () u ()  u ~~> y  (:gmap K A) ~~> {[ i := y ]}.
Proof.
  rewrite !cmra_update_updateP;
    eauto using alloc_unit_singleton_updateP with subst.
Qed.

427 428
Lemma alloc_local_update m1 m2 i x :
  m1 !! i = None   x  (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
429
Proof.
430 431 432 433 434 435 436
  rewrite cmra_valid_validN=> Hi ?.
  apply local_update_unital=> n mf Hmv Hm; simpl in *.
  split; auto using insert_validN.
  intros j; destruct (decide (i = j)) as [->|].
  - move: (Hm j); rewrite Hi symmetry_iff dist_None lookup_op op_None=>-[_ Hj].
    by rewrite lookup_op !lookup_insert Hj.
  - rewrite Hm lookup_insert_ne // !lookup_op lookup_insert_ne //.
437
Qed.
438

439 440 441
Lemma alloc_singleton_local_update m i x :
  m !! i = None   x  (m,) ~l~> (<[i:=x]>m, {[ i:=x ]}).
Proof. apply alloc_local_update. Qed.
442

443 444 445 446
Lemma insert_local_update m1 m2 i x y x' y' :
  m1 !! i = Some x  m2 !! i = Some y 
  (x, y) ~l~> (x', y') 
  (m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
447
Proof.
448 449 450 451 452 453 454 455
  intros Hi1 Hi2 Hup; apply local_update_unital=> n mf Hmv Hm; simpl in *.
  destruct (Hup n (mf !! i)) as [? Hx']; simpl in *.
  { move: (Hmv i). by rewrite Hi1. }
  { move: (Hm i). by rewrite lookup_op Hi1 Hi2 Some_op_opM (inj_iff Some). }
  split; auto using insert_validN.
  rewrite Hm Hx'=> j; destruct (decide (i = j)) as [->|].
  - by rewrite lookup_insert lookup_op lookup_insert Some_op_opM.
  - by rewrite lookup_insert_ne // !lookup_op lookup_insert_ne.
456 457
Qed.

458 459 460 461
Lemma singleton_local_update m i x y x' y' :
  m !! i = Some x 
  (x, y) ~l~> (x', y') 
  (m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}).
462
Proof.
463
  intros. rewrite /singletonM /map_singleton -(insert_insert  i y' y).
Robbert Krebbers's avatar
Robbert Krebbers committed
464
  by eapply insert_local_update; [|eapply lookup_insert|].
465
Qed.
466

467 468
Lemma delete_local_update m1 m2 i x `{!Exclusive x} :
  m2 !! i = Some x  (m1, m2) ~l~> (delete i m1, delete i m2).
469
Proof.
470 471 472 473 474 475
  intros Hi. apply local_update_unital=> n mf Hmv Hm; simpl in *.
  split; auto using delete_validN.
  rewrite Hm=> j; destruct (decide (i = j)) as [<-|].
  - rewrite lookup_op !lookup_delete left_id symmetry_iff dist_None.
    apply eq_None_not_Some=> -[y Hi'].
    move: (Hmv i). rewrite Hm lookup_op Hi Hi' -Some_op. by apply exclusiveN_l.
476
  - by rewrite lookup_op !lookup_delete_ne // lookup_op.
477 478 479 480 481 482
Qed.

Lemma delete_singleton_local_update m i x `{!Exclusive x} :
  (m, {[ i := x ]}) ~l~> (delete i m, ).
Proof.
  rewrite -(delete_singleton i x).
Robbert Krebbers's avatar
Robbert Krebbers committed
483
  by eapply delete_local_update, lookup_singleton.
484
Qed.
485 486 487 488 489

Lemma delete_local_update_cancelable m1 m2 i mx `{!Cancelable mx} :
  m1 !! i  mx  m2 !! i  mx 
  (m1, m2) ~l~> (delete i m1, delete i m2).
Proof.
490 491 492 493 494 495
  intros Hm1i Hm2i. apply local_update_unital=> n mf Hmv Hm; simpl in *.
  split; [eauto using delete_validN|].
  intros j. destruct (decide (i = j)) as [->|].
  - move: (Hm j). rewrite !lookup_op Hm1i Hm2i !lookup_delete. intros Hmx.
    rewrite (cancelableN mx n (mf !! j) None) ?right_id // -Hmx -Hm1i. apply Hmv.
  - by rewrite lookup_op !lookup_delete_ne // Hm lookup_op.
496 497 498 499 500 501 502 503 504
Qed.

Lemma delete_singleton_local_update_cancelable m i x `{!Cancelable (Some x)} :
  m !! i  Some x  (m, {[ i := x ]}) ~l~> (delete i m, ).
Proof.
  intros. rewrite -(delete_singleton i x).
  apply (delete_local_update_cancelable m _ i (Some x));
    [done|by rewrite lookup_singleton].
Qed.
505

506
Lemma gmap_fmap_mono {B : cmraT} (f : A  B) m1 m2 :
507 508 509 510 511 512
  Proper (() ==> ()) f 
  ( x y, x  y  f x  f y)  m1  m2  fmap f m1  fmap f m2.
Proof.
  intros ??. rewrite !lookup_included=> Hm i.
  rewrite !lookup_fmap. by apply option_fmap_mono.
Qed.
513 514
End properties.

515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537
Section unital_properties.
Context `{Countable K} {A : ucmraT}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.

Lemma insert_alloc_local_update m1 m2 i x x' y' :
  m1 !! i = Some x  m2 !! i = None 
  (x, ε) ~l~> (x', y') 
  (m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
Proof.
  intros Hi1 Hi2 Hup. apply local_update_unital=> n mf Hm1v Hm.
  assert (mf !! i {n} Some x) as Hif.
  { move: (Hm i). by rewrite lookup_op Hi1 Hi2 left_id. }
  destruct (Hup n (mf !! i)) as [Hx'v Hx'eq].
  { move: (Hm1v i). by rewrite Hi1. }
  { by rewrite Hif -(inj_iff Some) -Some_op_opM -Some_op left_id. }
  split.
  - by apply insert_validN.
  - simpl in Hx'eq. by rewrite -(insert_idN n mf i x) // -insert_op -Hm Hx'eq Hif.
Qed.
End unital_properties.

538
(** Functor *)
539
Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A  B) n :
540 541
  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.
542
Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmraT} (f : A  B)
543
  `{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A  gmap K B).
544
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
  split; try apply _.
546 547 548 549
  - by intros n m ? i; rewrite lookup_fmap; apply (cmra_morphism_validN _).
  - intros m. apply Some_proper=>i. rewrite lookup_fmap !lookup_omap lookup_fmap.
    case: (m!!i)=>//= ?. apply cmra_morphism_pcore, _.
  - intros m1 m2 i. by rewrite lookup_op !lookup_fmap lookup_op cmra_morphism_op.
550
Qed.
551 552 553 554
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} :
  NonExpansive (@gmapO_map K _ _ A B).
555
Proof.
556
  intros n f g Hf m k; rewrite /= !lookup_fmap.
557 558
  destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
Ralf Jung's avatar
Ralf Jung committed
559

560 561 562
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
563
|}.
564
Next Obligation.
565
  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_ne.
566
Qed.
Ralf Jung's avatar
Ralf Jung committed
567
Next Obligation.
568
  intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
569
  apply map_fmap_equiv_ext=>y ??; apply oFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
570 571
Qed.
Next Obligation.
572
  intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
573
  apply map_fmap_equiv_ext=>y ??; apply oFunctor_compose.
574
Qed.
575 576
Instance gmapOF_contractive K `{Countable K} F :
  oFunctorContractive F  oFunctorContractive (gmapOF K F).
577
Proof.
578
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_contractive.
579 580
Qed.

581
Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
582
  urFunctor_car A _ B _ := gmapUR K (rFunctor_car F A B);
583
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
584
|}.
585
Next Obligation.
586
  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_ne.
587
Qed.
588
Next Obligation.
589
  intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
590
  apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
591 592
Qed.
Next Obligation.
593
  intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
594
  apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
595
Qed.
596
Instance gmapRF_contractive K `{Countable K} F :
597
  rFunctorContractive F  urFunctorContractive (gmapURF K F).
598
Proof.
599
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_contractive.
600
Qed.