gmap.v 23 KB
Newer Older
1
From iris.algebra Require Export cmra.
Ralf Jung's avatar
Ralf Jung committed
2
From stdpp Require Export 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 28 29 30 31 32 33 34 35 36 37 38 39 40 41
Canonical Structure gmapC : ofeT := OfeT (gmap K A) gmap_ofe_mixin.

Program Definition gmap_chain (c : chain gmapC)
  (k : K) : chain (optionC A) := {| chain_car n := c n !! k |}.
Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
Definition gmap_compl `{Cofe A} : Compl gmapC := λ c,
  map_imap (λ i _, compl (gmap_chain c i)) (c 0).
Global Program Instance gmap_cofe `{Cofe A} : Cofe gmapC :=
  {| compl := gmap_compl |}.
Next Obligation.
  intros ? n c k. rewrite /compl /gmap_compl lookup_imap.
  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 gmapC.
43
Proof. intros ? m m' ? i. by apply (discrete _). Qed.
44
(* why doesn't this go automatic? *)
45
Global Instance gmapC_leibniz: LeibnizEquiv A  LeibnizEquiv gmapC.
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 gmapC _ {_ _} _.
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).
153
    by rewrite -lookup_op.
154 155 156 157 158 159 160 161 162 163
  - 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).
    split; [|split]=>i; rewrite ?lookup_op !lookup_imap;
    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  ( i, m1 !! i  m2 !! i : uPred M).
181
Proof. by uPred.unseal. Qed.
182
Lemma gmap_validI {M} m :  m  ( i,  (m !! i) : uPred M).
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 281
Qed.

282 283 284
Global Instance singleton_cancelable i x :
  Cancelable (Some x)  Cancelable {[ i := x ]}.
Proof.
285 286 287 288
  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 _).
289 290
Qed.

291 292 293 294 295 296
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.

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

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

317
Lemma singleton_updateP (P : A  Prop) (Q : gmap K A  Prop) i x :
318
  x ~~>: P  ( y, P y  Q {[ i := y ]})  {[ i := x ]} ~~>: Q.
319 320
Proof. apply insert_updateP. Qed.
Lemma singleton_updateP' (P : A  Prop) i x :
321
  x ~~>: P  {[ i := x ]} ~~>: λ m,  y, m = {[ i := y ]}  P y.
322 323 324
Proof. apply insert_updateP'. Qed.
Lemma singleton_update i (x y : A) : x ~~> y  {[ i := x ]} ~~> {[ i := y ]}.
Proof. apply insert_update. Qed.
325

326
Lemma delete_update m i : m ~~> delete i m.
327
Proof.
328 329 330 331
  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.
332
Qed.
333

334 335 336 337 338 339 340 341 342 343 344
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.

345
Section freshness.
346
  Local Set Default Proof Using "Type*".
347 348 349 350 351 352 353 354 355
  Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
  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.
356 357
    { apply HQ; last done. by eapply not_elem_of_dom. }
    rewrite insert_singleton_op; last by eapply not_elem_of_dom.
358
    rewrite -assoc -insert_singleton_op;
359
      last by eapply (not_elem_of_dom (D:=gset K)); rewrite dom_op not_elem_of_union.
360 361 362 363 364 365 366 367 368 369 370 371 372
    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.
End freshness.

373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398
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.

399 400
Lemma alloc_local_update m1 m2 i x :
  m1 !! i = None   x  (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
401
Proof.
402 403 404 405 406 407 408
  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 //.
409
Qed.
410

411 412 413
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.
414

415 416 417 418
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).
419
Proof.
420 421 422 423 424 425 426 427
  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.
428 429
Qed.

430 431 432 433
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' ]}).
434
Proof.
435
  intros. rewrite /singletonM /map_singleton -(insert_insert  i y' y).
Robbert Krebbers's avatar
Robbert Krebbers committed
436
  by eapply insert_local_update; [|eapply lookup_insert|].
437
Qed.
438

439 440
Lemma delete_local_update m1 m2 i x `{!Exclusive x} :
  m2 !! i = Some x  (m1, m2) ~l~> (delete i m1, delete i m2).
441
Proof.
442 443 444 445 446 447
  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.
448
  - by rewrite lookup_op !lookup_delete_ne // lookup_op.
449 450 451 452 453 454
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
455
  by eapply delete_local_update, lookup_singleton.
456
Qed.
457 458 459 460 461

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.
462 463 464 465 466 467
  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.
468 469 470 471 472 473 474 475 476
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.
477

478
Lemma gmap_fmap_mono {B : cmraT} (f : A  B) m1 m2 :
479 480 481 482 483 484
  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.
485 486
End properties.

487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509
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.

510
(** Functor *)
511
Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A  B) n :
512 513
  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.
514
Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmraT} (f : A  B)
515
  `{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A  gmap K B).
516
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
517
  split; try apply _.
518 519 520 521
  - 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.
522
Qed.
523 524
Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
  gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A  gmapC K B).
525 526
Instance gmapC_map_ne `{Countable K} {A B} :
  NonExpansive (@gmapC_map K _ _ A B).
527
Proof.
528
  intros n f g Hf m k; rewrite /= !lookup_fmap.
529 530
  destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
Qed.
Ralf Jung's avatar
Ralf Jung committed
531

532 533 534
Program Definition gmapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
  cFunctor_car A B := gmapC K (cFunctor_car F A B);
  cFunctor_map A1 A2 B1 B2 fg := gmapC_map (cFunctor_map F fg)
Ralf Jung's avatar
Ralf Jung committed
535
|}.
536
Next Obligation.
537
  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_ne.
538
Qed.
Ralf Jung's avatar
Ralf Jung committed
539
Next Obligation.
540
  intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
541
  apply map_fmap_equiv_ext=>y ??; apply cFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
542 543
Qed.
Next Obligation.
544
  intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
545
  apply map_fmap_equiv_ext=>y ??; apply cFunctor_compose.
546
Qed.
547 548
Instance gmapCF_contractive K `{Countable K} F :
  cFunctorContractive F  cFunctorContractive (gmapCF K F).
549
Proof.
550
  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
551 552
Qed.

553 554 555
Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
  urFunctor_car A B := gmapUR K (rFunctor_car F A B);
  urFunctor_map A1 A2 B1 B2 fg := gmapC_map (rFunctor_map F fg)
556
|}.
557
Next Obligation.
558
  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
559
Qed.
560 561
Next Obligation.
  intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
562
  apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
563 564 565
Qed.
Next Obligation.
  intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
566
  apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
567
Qed.
568
Instance gmapRF_contractive K `{Countable K} F :
569
  rFunctorContractive F  urFunctorContractive (gmapURF K F).
570
Proof.
571
  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
572
Qed.