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

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

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

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

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

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

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

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

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

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

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

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

134
Lemma gmap_cmra_mixin : CmraMixin (gmap K A).
135
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
136 137 138 139 140
  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).
141 142 143
  - intros m; split.
    + by intros ? n i; apply cmra_valid_validN.
    + intros Hm i; apply cmra_valid_validN=> n; apply Hm.
144 145 146
  - 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
147 148 149
  - 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.
150
    rewrite !lookup_core. by apply cmra_core_mono.
151
  - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
152
    by rewrite -lookup_op.
153 154 155 156 157
  - 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
158
    split; [|split]=>i; rewrite ?lookup_op !map_lookup_imap;
159 160 161 162
    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)=>[?|] //.
163
Qed.
164
Canonical Structure gmapR := CmraT (gmap K A) gmap_cmra_mixin.
165

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

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

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

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

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

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

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

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

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

219 220 221 222 223
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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
231 232 233 234 235 236 237 238
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.
239
Lemma op_singleton (i : K) (x y : A) :
240
  {[ i := x ]}  {[ i := y ]} = ({[ i := x  y ]} : gmap K A).
241
Proof. by apply (merge_singleton _ _ _ x y). Qed.
242 243 244
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.
245

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

Robbert Krebbers's avatar
Robbert Krebbers committed
255
Lemma singleton_includedN n m i x :
256
  {[ i := x ]} {n} m   y, m !! i {n} Some y  Some x {n} Some y.
Robbert Krebbers's avatar
Robbert Krebbers committed
257 258
Proof.
  split.
259 260 261 262 263 264 265
  - 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.
266 267 268
Qed.
(* We do not have [x ≼ y ↔ ∀ n, x ≼{n} y], so we cannot use the previous lemma *)
Lemma singleton_included m i x :
269
  {[ i := x ]}  m   y, m !! i  Some y  Some x  Some y.
270 271 272
Proof.
  split.
  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
273 274 275 276 277 278
    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
279
Qed.
280 281 282 283 284 285 286
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
287

288 289 290
Global Instance singleton_cancelable i x :
  Cancelable (Some x)  Cancelable {[ i := x ]}.
Proof.
291 292 293 294
  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 _).
295 296
Qed.

297 298 299 300 301 302
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.

303 304 305 306
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.

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

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

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

342 343 344 345 346 347 348 349 350 351 352
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.

353
Section freshness.
354
  Local Set Default Proof Using "Type*".
355
  Context `{!Infinite K}.
Dan Frumin's avatar
Dan Frumin committed
356 357 358
  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.
359
  Proof.
Dan Frumin's avatar
Dan Frumin committed
360 361 362 363 364 365
    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. }
366
    exists (<[i:=x]>m); split.
Dan Frumin's avatar
Dan Frumin committed
367 368 369 370
    - by apply HQ.
    - rewrite insert_singleton_op //.
      rewrite -assoc -insert_singleton_op;
        last by eapply (not_elem_of_dom (D:=gset K)).
371 372 373 374
    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
375 376 377 378 379 380 381 382
  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.
383 384 385 386
  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
387 388 389 390 391 392 393 394 395 396 397
  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.
398 399
End freshness.

400 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
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.

426 427
Lemma alloc_local_update m1 m2 i x :
  m1 !! i = None   x  (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
428
Proof.
429 430 431 432 433 434 435
  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 //.
436
Qed.
437

438 439 440
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.
441

442 443 444 445
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).
446
Proof.
447 448 449 450 451 452 453 454
  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.
455 456
Qed.

457 458 459 460
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' ]}).
461
Proof.
462
  intros. rewrite /singletonM /map_singleton -(insert_insert  i y' y).
Robbert Krebbers's avatar
Robbert Krebbers committed
463
  by eapply insert_local_update; [|eapply lookup_insert|].
464
Qed.
465

466 467
Lemma delete_local_update m1 m2 i x `{!Exclusive x} :
  m2 !! i = Some x  (m1, m2) ~l~> (delete i m1, delete i m2).
468
Proof.
469 470 471 472 473 474
  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.
475
  - by rewrite lookup_op !lookup_delete_ne // lookup_op.
476 477 478 479 480 481
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
482
  by eapply delete_local_update, lookup_singleton.
483
Qed.
484 485 486 487 488

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.
489 490 491 492 493 494
  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.
495 496 497 498 499 500 501 502 503
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.
504

505
Lemma gmap_fmap_mono {B : cmraT} (f : A  B) m1 m2 :
506 507 508 509 510 511
  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.
512 513
End properties.

514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536
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.

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

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

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