gmap.v 17.7 KB
Newer Older
1
From iris.algebra Require Export cmra.
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 187
Implicit Types i : K.
Implicit Types a : A.
188

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

205
Lemma insert_singleton_opN n m i x :
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  m !! i = None  <[i:=x]> m {n} {[ i := x ]}  m.
207
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
208 209 210
  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.
211
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
Lemma insert_singleton_op m i x : m !! i = None  <[i:=x]> m  {[ i := x ]}  m.
213
Proof. rewrite !equiv_dist; naive_solver eauto using insert_singleton_opN. Qed.
214

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

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

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

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

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

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

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.
Robbert Krebbers's avatar
Robbert Krebbers committed
314 315
  intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
  destruct (Hx n (gf !! i)) as (y&?&Hy).
316
  { move:(Hg i). rewrite !left_id.
317
    case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
Robbert Krebbers's avatar
Robbert Krebbers committed
318
    intros; by apply cmra_valid_validN. }
319 320 321
  exists {[ i := y ]}; split; first by auto.
  intros i'; destruct (decide (i' = i)) as [->|].
  - rewrite lookup_op lookup_singleton.
322
    move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
323 324 325 326 327 328 329 330 331 332 333
  - 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.
334 335
End freshness.

336
(* Allocation is a local update: Just use composition with a singleton map. *)
337

338
Global Instance delete_local_update :
339
  LocalUpdate (λ m,  x, m !! i = Some x  Exclusive x) (delete i).
340 341 342 343 344 345 346 347 348
Proof.
  split; first apply _.
  intros n m1 m2 (x&Hix&Hv) Hm j; destruct (decide (i = j)) as [<-|].
  - rewrite lookup_delete !lookup_op lookup_delete.
    case Hiy: (m2 !! i)=> [y|]; last constructor.
    destruct (Hv y); apply cmra_validN_le with n; last omega.
    move: (Hm i). by rewrite lookup_op Hix Hiy.
  - by rewrite lookup_op !lookup_delete_ne // lookup_op.
Qed.
349 350

(* Applying a local update at a position we own is a local update. *)
351
Global Instance alter_local_update `{!LocalUpdate Lv L} i :
352
  LocalUpdate (λ m,  x, m !! i = Some x  Lv x) (alter L i).
353
Proof.
354 355 356 357
  split; first apply _.
  intros n m1 m2 (x&Hix&?) Hm j; destruct (decide (i = j)) as [->|].
  - rewrite lookup_alter !lookup_op lookup_alter Hix /=.
    move: (Hm j); rewrite lookup_op Hix.
358
    case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN L).
359
  - by rewrite lookup_op !lookup_alter_ne // lookup_op.
360
Qed.
361 362
End properties.

363
(** Functor *)
364
Instance gmap_fmap_ne `{Countable K} {A B : cofeT} (f : A  B) n :
365 366
  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.
367
Instance gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A  B)
368 369
  `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A  gmap K B).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
370
  split; try apply _.
371
  - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
372
  - intros m1 m2; rewrite !lookup_included=> Hm i.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
    by rewrite !lookup_fmap; apply: included_preserving.
374
Qed.
375 376 377 378
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).
379 380 381 382
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
383

384 385 386
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
387
|}.
388
Next Obligation.
389
  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_ne.
390
Qed.
Ralf Jung's avatar
Ralf Jung committed
391
Next Obligation.
392 393
  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
394 395
Qed.
Next Obligation.
396 397 398
  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.
399 400
Instance gmapCF_contractive K `{Countable K} F :
  cFunctorContractive F  cFunctorContractive (gmapCF K F).
401
Proof.
402
  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
403 404
Qed.

405 406 407
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)
408
|}.
409
Next Obligation.
410
  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
411
Qed.
412 413 414 415 416 417 418
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
419
Qed.
420
Instance gmapRF_contractive K `{Countable K} F :
421
  rFunctorContractive F  urFunctorContractive (gmapURF K F).
422
Proof.
423
  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
424
Qed.