gmap.v 18.8 KB
Newer Older
1
From iris.algebra Require Export cmra updates.
2 3
From iris.prelude Require Export gmap.
From iris.algebra Require Import upred.
4

5 6
Section cofe.
Context `{Countable K} {A : cofeT}.
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
Program Definition gmap_chain (c : chain (gmap K A))
12
  (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
13
Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
14 15 16
Instance gmap_compl : Compl (gmap K A) := λ c,
  map_imap (λ i _, compl (gmap_chain c i)) (c 0).
Definition gmap_cofe_mixin : CofeMixin (gmap K A).
17 18
Proof.
  split.
19
  - intros m1 m2; split.
20 21
    + by intros Hm n k; apply equiv_dist.
    + intros Hm k; apply equiv_dist; intros n; apply Hm.
22
  - intros n; split.
23 24
    + by intros m k.
    + by intros m1 m2 ? k.
25
    + by intros m1 m2 m3 ?? k; trans (m2 !! k).
26
  - by intros n m1 m2 ? k; apply dist_S.
27
  - intros n c k; rewrite /compl /gmap_compl lookup_imap.
28
    feed inversion (λ H, chain_cauchy c 0 n H k); simpl; auto with lia.
29
    by rewrite conv_compl /=; apply reflexive_eq.
30
Qed.
31
Canonical Structure gmapC : cofeT := CofeT (gmap K A) gmap_cofe_mixin.
32
Global Instance gmap_discrete : Discrete A  Discrete gmapC.
33
Proof. intros ? m m' ? i. by apply (timeless _). Qed.
34
(* why doesn't this go automatic? *)
35
Global Instance gmapC_leibniz: LeibnizEquiv A  LeibnizEquiv gmapC.
36 37
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.

38
Global Instance lookup_ne n k :
39
  Proper (dist n ==> dist n) (lookup k : gmap K A  option A).
40
Proof. by intros m1 m2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42
Global Instance lookup_proper k :
  Proper (() ==> ()) (lookup k : gmap K A  option A) := _.
43 44 45 46
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'.
47
  by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
48
Qed.
49
Global Instance insert_ne i n :
50
  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
51
Proof.
52
  intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
53 54
    [by constructor|by apply lookup_ne].
Qed.
55
Global Instance singleton_ne i n :
56 57
  Proper (dist n ==> dist n) (singletonM i : A  gmap K A).
Proof. by intros ???; apply insert_ne. Qed.
58
Global Instance delete_ne i n :
59
  Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
60
Proof.
61
  intros m m' ? j; destruct (decide (i = j)); simplify_map_eq;
62 63
    [by constructor|by apply lookup_ne].
Qed.
64

65
Instance gmap_empty_timeless : Timeless ( : gmap K A).
66 67 68 69
Proof.
  intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
  inversion_clear Hm; constructor.
Qed.
70
Global Instance gmap_lookup_timeless m i : Timeless m  Timeless (m !! i).
71
Proof.
72
  intros ? [x|] Hx; [|by symmetry; apply: timeless].
73
  assert (m {0} <[i:=x]> m)
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75
    by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
  by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
76
Qed.
77
Global Instance gmap_insert_timeless m i x :
78 79
  Timeless x  Timeless m  Timeless (<[i:=x]>m).
Proof.
80
  intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq.
81 82
  { by apply: timeless; rewrite -Hm lookup_insert. }
  by apply: timeless; rewrite -Hm lookup_insert_ne.
83
Qed.
84
Global Instance gmap_singleton_timeless i x :
85
  Timeless x  Timeless ({[ i := x ]} : gmap K A) := _.
86
End cofe.
87

88
Arguments gmapC _ {_ _} _.
89 90

(* CMRA *)
91 92
Section cmra.
Context `{Countable K} {A : cmraT}.
93
Implicit Types m : gmap K A.
94

95
Instance gmap_op : Op (gmap K A) := merge op.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m).
97 98
Instance gmap_valid : Valid (gmap K A) := λ m,  i,  (m !! i).
Instance gmap_validN : ValidN (gmap K A) := λ n m,  i, {n} (m !! i).
99

100
Lemma lookup_op m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
101
Proof. by apply lookup_merge. Qed.
Ralf Jung's avatar
Ralf Jung committed
102
Lemma lookup_core m i : core m !! i = core (m !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
103
Proof. by apply lookup_omap. Qed.
104

105
Lemma lookup_included (m1 m2 : gmap K A) : m1  m2   i, m1 !! i  m2 !! i.
106
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
107 108 109 110 111
  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 [->|].
112
    - intros _. rewrite Hi. apply: ucmra_unit_least.
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114 115 116 117 118
    - 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.
119
Qed.
120

121
Lemma gmap_cmra_mixin : CMRAMixin (gmap K A).
122
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
123 124 125 126 127
  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).
128 129 130
  - intros m; split.
    + by intros ? n i; apply cmra_valid_validN.
    + intros Hm i; apply cmra_valid_validN=> n; apply Hm.
131 132 133
  - 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
134 135 136 137
  - 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.
    rewrite !lookup_core. by apply cmra_core_preserving.
138
  - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
139
    by rewrite -lookup_op.
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
  - 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);
      repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
    + 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))|].
      pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
      by symmetry; apply option_op_positive_dist_l with (m2 !! i).
    + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
      pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
      by symmetry; apply option_op_positive_dist_r with (m1 !! i).
155
Qed.
156
Canonical Structure gmapR :=
157
  CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
158 159 160 161 162

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

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

180
Arguments gmapR _ {_ _} _.
181
Arguments gmapUR _ {_ _} _.
182 183

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

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

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

208
Lemma insert_singleton_opN n m i x :
Robbert Krebbers's avatar
Robbert Krebbers committed
209
  m !! i = None  <[i:=x]> m {n} {[ i := x ]}  m.
210
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
211 212 213
  intros Hi j; destruct (decide (i = j)) as [->|].
  - by rewrite lookup_op lookup_insert lookup_singleton Hi right_id.
  - by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id.
214
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
Lemma insert_singleton_op m i x : m !! i = None  <[i:=x]> m  {[ i := x ]}  m.
216
Proof. rewrite !equiv_dist; naive_solver eauto using insert_singleton_opN. Qed.
217

Robbert Krebbers's avatar
Robbert Krebbers committed
218 219 220 221 222 223 224 225
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.
226
Lemma op_singleton (i : K) (x y : A) :
227
  {[ i := x ]}  {[ i := y ]} = ({[ i := x  y ]} : gmap K A).
228
Proof. by apply (merge_singleton _ _ _ x y). Qed.
229

230
Global Instance gmap_persistent m : ( x : A, Persistent x)  Persistent m.
Robbert Krebbers's avatar
Robbert Krebbers committed
231 232 233 234
Proof.
  intros; apply persistent_total=> i.
  rewrite lookup_core. apply (persistent_core _).
Qed.
235
Global Instance gmap_singleton_persistent i (x : A) :
236
  Persistent x  Persistent {[ i := x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
Proof. intros. by apply persistent_total, core_singleton'. Qed.
238

Robbert Krebbers's avatar
Robbert Krebbers committed
239
Lemma singleton_includedN n m i x :
Robbert Krebbers's avatar
Robbert Krebbers committed
240
  {[ i := x ]} {n} m   y, m !! i {n} Some y  (x {n} y  x {n} y).
Robbert Krebbers's avatar
Robbert Krebbers committed
241 242
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
243 244 245
  - 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
246 247 248 249 250 251 252 253
    + 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
254
Qed.
255
Lemma dom_op m1 m2 : dom (gset K) (m1  m2)  dom _ m1  dom _ m2.
256
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
  apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
258 259 260
  unfold is_Some; setoid_rewrite lookup_op.
  destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
261

262
Lemma insert_updateP (P : A  Prop) (Q : gmap K A  Prop) m i x :
263
  x ~~>: P  ( y, P y  Q (<[i:=y]>m))  <[i:=x]>m ~~>: Q.
264
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
265 266
  intros Hx%option_updateP' HP; apply cmra_total_updateP=> n mf Hm.
  destruct (Hx n (Some (mf !! i))) as ([y|]&?&?); try done.
267
  { by generalize (Hm i); rewrite lookup_op; simplify_map_eq. }
268 269
  exists (<[i:=y]> m); split; first by auto.
  intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
270
  destruct (decide (i = j)); simplify_map_eq/=; auto.
271
Qed.
272
Lemma insert_updateP' (P : A  Prop) m i x :
273
  x ~~>: P  <[i:=x]>m ~~>: λ m',  y, m' = <[i:=y]>m  P y.
274 275 276
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.
277

278
Lemma singleton_updateP (P : A  Prop) (Q : gmap K A  Prop) i x :
279
  x ~~>: P  ( y, P y  Q {[ i := y ]})  {[ i := x ]} ~~>: Q.
280 281
Proof. apply insert_updateP. Qed.
Lemma singleton_updateP' (P : A  Prop) i x :
282
  x ~~>: P  {[ i := x ]} ~~>: λ m,  y, m = {[ i := y ]}  P y.
283 284 285
Proof. apply insert_updateP'. Qed.
Lemma singleton_update i (x y : A) : x ~~> y  {[ i := x ]} ~~> {[ i := y ]}.
Proof. apply insert_update. Qed.
286

287
Lemma delete_update m i : m ~~> delete i m.
288
Proof.
289 290 291 292
  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.
293
Qed.
294

295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348
Section freshness.
  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.
    { by apply HQ; last done; apply not_elem_of_dom. }
    rewrite insert_singleton_opN; last by apply not_elem_of_dom.
    rewrite -assoc -insert_singleton_opN;
      last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
    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.

  Lemma singleton_updateP_unit (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 singleton_updateP_unit' (P: A  Prop) u i :
     u  LeftId () u () 
    u ~~>: P   ~~>: λ m,  y, m = {[ i := y ]}  P y.
  Proof. eauto using singleton_updateP_unit. Qed.
  Lemma singleton_update_unit u i (y : A) :
     u  LeftId () u ()  u ~~> y   ~~> {[ i := y ]}.
  Proof.
    rewrite !cmra_update_updateP; eauto using singleton_updateP_unit with subst.
  Qed.
End freshness.

Lemma insert_local_update m i x y mf :
  x ~l~> y @ mf = (!! i)  <[i:=x]>m ~l~> <[i:=y]>m @ mf.
349
Proof.
350 351 352 353 354 355 356 357
  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.
358
Qed.
359

360 361 362
Lemma singleton_local_update i x y mf :
  x ~l~> y @ mf = (!! i)  {[ i := x ]} ~l~> {[ i := y ]} @ mf.
Proof. apply insert_local_update. Qed.
363

364 365
Lemma alloc_singleton_local_update i x mf :
  mf = (!! i) = None   x   ~l~> {[ i := x ]} @ mf.
366
Proof.
367 368 369 370 371 372 373 374 375 376
  intros Hi. split.
  - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
    + intros _; rewrite !lookup_opM !lookup_insert !Some_op_opM Hi /=.
      by apply cmra_valid_validN.
    + by rewrite !lookup_opM !lookup_insert_ne.
  - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
    destruct (decide (i = j)); subst.
    + intros _. rewrite !lookup_opM !lookup_insert !Hi !lookup_empty !left_id_L.
      by intros <-.
    + by rewrite !lookup_opM !lookup_insert_ne.
377
Qed.
378

379 380
Lemma delete_local_update m i x `{!Exclusive x} mf :
  m !! i = Some x  m ~l~> delete i m @ mf.
381
Proof.
382 383 384 385 386 387 388
  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.
389
Qed.
390 391
End properties.

392
(** Functor *)
393
Instance gmap_fmap_ne `{Countable K} {A B : cofeT} (f : A  B) n :
394 395
  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.
396
Instance gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A  B)
397 398
  `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A  gmap K B).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
399
  split; try apply _.
400
  - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
401
  - intros m1 m2; rewrite !lookup_included=> Hm i.
Robbert Krebbers's avatar
Robbert Krebbers committed
402
    by rewrite !lookup_fmap; apply: included_preserving.
403
Qed.
404 405 406 407
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).
Instance gmapC_map_ne `{Countable K} {A B} n :
  Proper (dist n ==> dist n) (@gmapC_map K _ _ A B).
408 409 410 411
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
412

413 414 415
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
416
|}.
417
Next Obligation.
418
  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_ne.
419
Qed.
Ralf Jung's avatar
Ralf Jung committed
420
Next Obligation.
421 422
  intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
  apply map_fmap_setoid_ext=>y ??; apply cFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
423 424
Qed.
Next Obligation.
425 426 427
  intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
  apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose.
Qed.
428 429
Instance gmapCF_contractive K `{Countable K} F :
  cFunctorContractive F  cFunctorContractive (gmapCF K F).
430
Proof.
431
  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
432 433
Qed.

434 435 436
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)
437
|}.
438
Next Obligation.
439
  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
440
Qed.
441 442 443 444 445 446 447
Next Obligation.
  intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
  apply map_fmap_setoid_ext=>y ??; apply rFunctor_id.
Qed.
Next Obligation.
  intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
  apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
448
Qed.
449
Instance gmapRF_contractive K `{Countable K} F :
450
  rFunctorContractive F  urFunctorContractive (gmapURF K F).
451
Proof.
452
  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
453
Qed.