fin_maps.v 16.2 KB
Newer Older
1
2
From algebra Require Export cmra option.
From prelude Require Export gmap.
3
From algebra Require Import functor upred.
4

5
6
Section cofe.
Context `{Countable K} {A : cofeT}.
7
Implicit Types m : gmap K A.
8

9
Instance map_dist : Dist (gmap K A) := λ n m1 m2,
10
   i, m1 !! i {n} m2 !! i.
11
Program Definition map_chain (c : chain (gmap K A))
12
  (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
13
14
Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
Instance map_compl : Compl (gmap K A) := λ c,
15
  map_imap (λ i _, compl (map_chain c i)) (c 1).
16
Definition map_cofe_mixin : CofeMixin (gmap K A).
17
18
Proof.
  split.
19
  - intros m1 m2; split.
20
    + by intros Hm n k; apply equiv_dist.
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
    + intros Hm k.

(**
Goal is

  @equiv (option (cofe_car A)) (@option_equiv (cofe_car A) (cofe_equiv A))
    (@lookup K (cofe_car A) (@gmap K H H0 (cofe_car A)) (@gmap_lookup K H H0 (cofe_car A)) k m1)
    (@lookup K (cofe_car A) (@gmap K H H0 (cofe_car A)) (@gmap_lookup K H H0 (cofe_car A)) k m2)
*)

(** LHS of equiv_dist is:

  @equiv (cofe_car B) (cofe_equiv B) x y

for some [B : cofeT].
*)

Fail apply equiv_dist.

(* Works: apply @equiv_dist.  *)


(* Note that equiv_dist is an iff, so [apply:] needs some help. But it works.

apply: (fun {A} x y => proj2 (@equiv_dist A x y)).
*)

(* I do not think it is just about the type of the projection of the [equiv]
operational typeclass being in the way. The following also fails. *)

change (option (cofe_car A)) with (cofe_car (optionC A)).

Fail apply equiv_dist.

change (@option_equiv (cofe_car A) (cofe_equiv A)) with
  (@cofe_equiv (optionC A)).

(* Only now it works *)
apply equiv_dist.



intros n; apply Hm.
64
  - intros n; split.
65
66
    + by intros m k.
    + by intros m1 m2 ? k.
67
    + by intros m1 m2 m3 ?? k; trans (m2 !! k).
68
  - by intros n m1 m2 ? k; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  - intros n c k; rewrite /compl /map_compl lookup_imap.
70
71
    feed inversion (λ H, chain_cauchy c 0 (S n) H k); simpl; auto with lia.
    by rewrite conv_compl /=; apply reflexive_eq.
72
Qed.
73
74
Canonical Structure mapC : cofeT := CofeT map_cofe_mixin.

75
76
77
78
(* why doesn't this go automatic? *)
Global Instance mapC_leibniz: LeibnizEquiv A  LeibnizEquiv mapC.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.

79
Global Instance lookup_ne n k :
80
  Proper (dist n ==> dist n) (lookup k : gmap K A  option A).
81
Proof. by intros m1 m2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
83
Global Instance lookup_proper k :
  Proper (() ==> ()) (lookup k : gmap K A  option A) := _.
84
85
86
87
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'.
88
  by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
89
Qed.
90
Global Instance insert_ne i n :
91
  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
92
Proof.
93
  intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
94
95
    [by constructor|by apply lookup_ne].
Qed.
96
Global Instance singleton_ne i n :
97
98
  Proper (dist n ==> dist n) (singletonM i : A  gmap K A).
Proof. by intros ???; apply insert_ne. Qed.
99
Global Instance delete_ne i n :
100
  Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
101
Proof.
102
  intros m m' ? j; destruct (decide (i = j)); simplify_map_eq;
103
104
    [by constructor|by apply lookup_ne].
Qed.
105

Robbert Krebbers's avatar
Robbert Krebbers committed
106
Global Instance map_timeless `{ a : A, Timeless a} m : Timeless m.
107
Proof. by intros m' ? i; apply: timeless. Qed.
108

109
Instance map_empty_timeless : Timeless ( : gmap K A).
110
111
112
113
Proof.
  intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
  inversion_clear Hm; constructor.
Qed.
114
Global Instance map_lookup_timeless m i : Timeless m  Timeless (m !! i).
115
Proof.
116
  intros ? [x|] Hx; [|by symmetry; apply: timeless].
117
  assert (m {0} <[i:=x]> m)
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
    by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
  by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
120
Qed.
121
Global Instance map_insert_timeless m i x :
122
123
  Timeless x  Timeless m  Timeless (<[i:=x]>m).
Proof.
124
  intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq.
125
126
  { by apply: timeless; rewrite -Hm lookup_insert. }
  by apply: timeless; rewrite -Hm lookup_insert_ne.
127
Qed.
128
Global Instance map_singleton_timeless i x :
129
  Timeless x  Timeless ({[ i := x ]} : gmap K A) := _.
130
End cofe.
131

132
Arguments mapC _ {_ _} _.
133
134

(* CMRA *)
135
136
Section cmra.
Context `{Countable K} {A : cmraT}.
137
Implicit Types m : gmap K A.
138
139
140

Instance map_op : Op (gmap K A) := merge op.
Instance map_unit : Unit (gmap K A) := fmap unit.
141
Instance map_validN : ValidN (gmap K A) := λ n m,  i, {n} (m !! i).
142
Instance map_minus : Minus (gmap K A) := merge minus.
143

144
Lemma lookup_op m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
145
Proof. by apply lookup_merge. Qed.
146
Lemma lookup_minus m1 m2 i : (m1  m2) !! i = m1 !! i  m2 !! i.
147
Proof. by apply lookup_merge. Qed.
148
Lemma lookup_unit m i : unit m !! i = unit (m !! i).
149
Proof. by apply lookup_fmap. Qed.
150

151
152
Lemma map_valid_spec m :  m   i,  (m !! i).
Proof. split; intros Hm ??; apply Hm. Qed.
153
Lemma map_included_spec (m1 m2 : gmap K A) : m1  m2   i, m1 !! i  m2 !! i.
154
155
Proof.
  split.
156
157
  - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
  - intros Hm; exists (m2  m1); intros i.
158
    by rewrite lookup_op lookup_minus cmra_op_minus'.
159
Qed.
160
Lemma map_includedN_spec (m1 m2 : gmap K A) n :
161
162
163
  m1 {n} m2   i, m1 !! i {n} m2 !! i.
Proof.
  split.
164
165
  - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
  - intros Hm; exists (m2  m1); intros i.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
    by rewrite lookup_op lookup_minus cmra_op_minus.
167
Qed.
168

169
Definition map_cmra_mixin : CMRAMixin (gmap K A).
170
171
Proof.
  split.
172
173
174
175
176
177
178
179
180
181
  - by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
  - by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
  - by intros n m1 m2 Hm ? i; rewrite -(Hm i).
  - by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i).
  - 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.
  - by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l.
  - by intros m i; rewrite !lookup_unit cmra_unit_idemp.
  - intros n x y; rewrite !map_includedN_spec; intros Hm i.
182
    by rewrite !lookup_unit; apply cmra_unit_preservingN.
183
  - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
184
    by rewrite -lookup_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
  - intros n x y; rewrite map_includedN_spec=> ? i.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
    by rewrite lookup_op lookup_minus cmra_op_minus.
187
Qed.
188
Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
189
190
Proof.
  intros n m m1 m2 Hm Hm12.
191
  assert ( i, m !! i {n} m1 !! i  m2 !! i) as Hm12'
Robbert Krebbers's avatar
Robbert Krebbers committed
192
    by (by intros i; rewrite -lookup_op).
193
194
195
  set (f i := cmra_extend_op 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);
Robbert Krebbers's avatar
Robbert Krebbers committed
196
    repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
197
  - destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
Robbert Krebbers's avatar
Robbert Krebbers committed
198
    rewrite -Hx; apply (proj2_sig (f i)).
199
  - destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
200
    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
201
    by symmetry; apply option_op_positive_dist_l with (m2 !! i).
202
  - destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
203
    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
204
    by symmetry; apply option_op_positive_dist_r with (m1 !! i).
205
Qed.
206
207
Canonical Structure mapRA : cmraT :=
  CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin.
208
209
210
Global Instance map_cmra_identity : CMRAIdentity mapRA.
Proof.
  split.
211
212
213
  - by intros ? n; rewrite lookup_empty.
  - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
  - apply map_empty_timeless.
214
Qed.
215
216
Global Instance mapRA_leibniz : LeibnizEquiv A  LeibnizEquiv mapRA.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
217
218
219
220
221
222

(** Internalized properties *)
Lemma map_equivI {M} m1 m2 : (m1  m2)%I  ( i, m1 !! i  m2 !! i : uPred M)%I.
Proof. done. Qed.
Lemma map_validI {M} m : ( m)%I  ( i,  (m !! i) : uPred M)%I.
Proof. done. Qed.
223
End cmra.
224

225
226
227
Arguments mapRA _ {_ _} _.

Section properties.
228
Context `{Countable K} {A : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
Implicit Types m : gmap K A.
230
231
Implicit Types i : K.
Implicit Types a : A.
232

233
Lemma map_lookup_validN n m i x : {n} m  m !! i {n} Some x  {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
234
Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
235
236
Lemma map_lookup_valid m i x :  m  m !! i  Some x   x.
Proof. move=>Hm Hi n. move:(Hm n i). by rewrite Hi. Qed.
237
Lemma map_insert_validN n m i x : {n} x  {n} m  {n} <[i:=x]>m.
238
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
239
240
Lemma map_insert_valid m i x :  x   m   <[i:=x]>m.
Proof. intros ?? n j; apply map_insert_validN; auto. Qed.
241
Lemma map_singleton_validN n i x : {n} ({[ i := x ]} : gmap K A)  {n} x.
242
243
Proof.
  split; [|by intros; apply map_insert_validN, cmra_empty_valid].
244
  by move=>/(_ i); simplify_map_eq.
245
Qed.
246
Lemma map_singleton_valid i x :  ({[ i := x ]} : gmap K A)   x.
247
248
Proof. split; intros ? n; eapply map_singleton_validN; eauto. Qed.

249
Lemma map_insert_singleton_opN n m i x :
250
  m !! i = None  m !! i {n} Some (unit x)  <[i:=x]> m {n} {[ i := x ]}  m.
251
Proof.
252
253
254
255
  intros Hi j; destruct (decide (i = j)) as [->|];
    [|by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id].
  rewrite lookup_op lookup_insert lookup_singleton.
  by destruct Hi as [->| ->]; constructor; rewrite ?cmra_unit_r.
256
Qed.
257
Lemma map_insert_singleton_op m i x :
258
  m !! i = None  m !! i  Some (unit x)  <[i:=x]> m  {[ i := x ]}  m.
259
Proof.
260
  rewrite !equiv_dist; naive_solver eauto using map_insert_singleton_opN.
261
262
Qed.

263
Lemma map_unit_singleton (i : K) (x : A) :
264
  unit ({[ i := x ]} : gmap K A) = {[ i := unit x ]}.
265
266
Proof. apply map_fmap_singleton. Qed.
Lemma map_op_singleton (i : K) (x y : A) :
267
  {[ i := x ]}  {[ i := y ]} = ({[ i := x  y ]} : gmap K A).
268
Proof. by apply (merge_singleton _ _ _ x y). Qed.
269

Robbert Krebbers's avatar
Robbert Krebbers committed
270
Lemma singleton_includedN n m i x :
271
  {[ i := x ]} {n} m   y, m !! i {n} Some y  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
272
273
274
  (* not m !! i = Some y ∧ x ≼{n} y to deal with n = 0 *)
Proof.
  split.
275
  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hm.
Robbert Krebbers's avatar
Robbert Krebbers committed
276
    destruct (m' !! i) as [y|];
277
      [exists (x  y)|exists x]; eauto using cmra_included_l.
278
  - intros (y&Hi&?); rewrite map_includedN_spec=>j.
279
    destruct (decide (i = j)); simplify_map_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
281
282
    + by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN.
    + apply None_includedN.
Qed.
283
Lemma map_dom_op m1 m2 : dom (gset K) (m1  m2)  dom _ m1  dom _ m2.
284
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
  apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
286
287
288
  unfold is_Some; setoid_rewrite lookup_op.
  destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
289

290
Lemma map_insert_updateP (P : A  Prop) (Q : gmap K A  Prop) m i x :
291
  x ~~>: P  ( y, P y  Q (<[i:=y]>m))  <[i:=x]>m ~~>: Q.
292
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
293
294
  intros Hx%option_updateP' HP n mf Hm.
  destruct (Hx n (mf !! i)) as ([y|]&?&?); try done.
295
  { by generalize (Hm i); rewrite lookup_op; simplify_map_eq. }
296
297
  exists (<[i:=y]> m); split; first by auto.
  intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
298
  destruct (decide (i = j)); simplify_map_eq/=; auto.
299
Qed.
300
Lemma map_insert_updateP' (P : A  Prop) m i x :
301
  x ~~>: P  <[i:=x]>m ~~>: λ m',  y, m' = <[i:=y]>m  P y.
302
Proof. eauto using map_insert_updateP. Qed.
303
Lemma map_insert_update m i x y : x ~~> y  <[i:=x]>m ~~> <[i:=y]>m.
304
Proof.
305
  rewrite !cmra_update_updateP; eauto using map_insert_updateP with subst.
306
307
Qed.

308
Lemma map_singleton_updateP (P : A  Prop) (Q : gmap K A  Prop) i x :
309
  x ~~>: P  ( y, P y  Q {[ i := y ]})  {[ i := x ]} ~~>: Q.
310
311
Proof. apply map_insert_updateP. Qed.
Lemma map_singleton_updateP' (P : A  Prop) i x :
312
  x ~~>: P  {[ i := x ]} ~~>: λ m,  y, m = {[ i := y ]}  P y.
313
Proof. apply map_insert_updateP'. Qed.
314
Lemma map_singleton_update i (x y : A) : x ~~> y  {[ i := x ]} ~~> {[ i := y ]}.
315
Proof. apply map_insert_update. Qed.
316

317
Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A}
Robbert Krebbers's avatar
Robbert Krebbers committed
318
    (P : A  Prop) (Q : gmap K A  Prop) i :
319
   ~~>: P  ( y, P y  Q {[ i := y ]})   ~~>: Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
320
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
322
  intros Hx HQ n gf Hg.
  destruct (Hx n (from_option  (gf !! i))) as (y&?&Hy).
Robbert Krebbers's avatar
Robbert Krebbers committed
323
324
  { move:(Hg i). rewrite !left_id.
    case _: (gf !! i); simpl; auto using cmra_empty_valid. }
325
  exists {[ i := y ]}; split; first by auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
327
328
329
330
  intros i'; destruct (decide (i' = i)) as [->|].
  - rewrite lookup_op lookup_singleton.
    move:Hy; case _: (gf !! i); first done.
    by rewrite right_id.
  - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
331
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
332
Lemma map_singleton_updateP_empty' `{Empty A, !CMRAIdentity A} (P: A  Prop) i :
333
   ~~>: P   ~~>: λ m,  y, m = {[ i := y ]}  P y.
334
335
Proof. eauto using map_singleton_updateP_empty. Qed.

336
Section freshness.
Robbert Krebbers's avatar
Robbert Krebbers committed
337
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
338
339
Lemma map_updateP_alloc_strong (Q : gmap K A  Prop) (I : gset K) m x :
   x  ( i, m !! i = None  i  I  Q (<[i:=x]>m))  m ~~>: Q.
340
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
  intros ? HQ n mf Hm. set (i := fresh (I  dom (gset K) (m  mf))).
342
343
  assert (i  I  i  dom (gset K) m  i  dom (gset K) mf) as [?[??]].
  { rewrite -not_elem_of_union -map_dom_op -not_elem_of_union; apply is_fresh. }
344
345
346
347
348
  exists (<[i:=x]>m); split.
  { by apply HQ; last done; apply not_elem_of_dom. }
  rewrite map_insert_singleton_opN; last by left; apply not_elem_of_dom.
  rewrite -assoc -map_insert_singleton_opN;
    last by left; apply not_elem_of_dom; rewrite map_dom_op not_elem_of_union.
349
  by apply map_insert_validN; [apply cmra_valid_validN|].
350
Qed.
351
352
353
354
355
356
Lemma map_updateP_alloc (Q : gmap K A  Prop) m x :
   x  ( i, m !! i = None  Q (<[i:=x]>m))  m ~~>: Q.
Proof. move=>??. eapply map_updateP_alloc_strong with (I:=); by eauto. Qed.
Lemma map_updateP_alloc_strong' m x (I : gset K) :
   x  m ~~>: λ m',  i, i  I  m' = <[i:=x]>m  m !! i = None.
Proof. eauto using map_updateP_alloc_strong. Qed.
357
Lemma map_updateP_alloc' m x :
358
   x  m ~~>: λ m',  i, m' = <[i:=x]>m  m !! i = None.
359
Proof. eauto using map_updateP_alloc. Qed.
360
361
End freshness.

362
363
364
365
366
367
(* Allocation is a local update: Just use composition with a singleton map. *)
(* Deallocation is *not* a local update. The trouble is that if we
   own {[ i ↦ x ]}, then the frame could always own "unit x", and prevent
   deallocation. *)

(* Applying a local update at a position we own is a local update. *)
368
369
Global Instance map_alter_update `{!LocalUpdate Lv L} i :
  LocalUpdate (λ m,  x, m !! i = Some x  Lv x) (alter L i).
370
Proof.
371
372
373
374
  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.
375
    case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN L).
376
  - by rewrite lookup_op !lookup_alter_ne // lookup_op.
377
Qed.
378
379
End properties.

380
(** Functor *)
381
382
383
384
385
386
387
Instance map_fmap_ne `{Countable K} {A B : cofeT} (f : A  B) n :
  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.
Instance map_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A  B)
  `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A  gmap K B).
Proof.
  split.
388
  - intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
389
    by rewrite !lookup_fmap; apply: includedN_preserving.
390
  - by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
391
Qed.
392
393
394
395
396
397
398
399
Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B :=
  CofeMor (fmap f : mapC K A  mapC K B).
Instance mapC_map_ne `{Countable K} {A B} n :
  Proper (dist n ==> dist n) (@mapC_map K _ _ A B).
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
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414

Program Definition mapF K `{Countable K} (Σ : iFunctor) : iFunctor := {|
  ifunctor_car := mapRA K  Σ; ifunctor_map A B := mapC_map  ifunctor_map Σ
|}.
Next Obligation.
  by intros K ?? Σ A B n f g Hfg; apply mapC_map_ne, ifunctor_map_ne.
Qed.
Next Obligation.
  intros K ?? Σ A x. rewrite /= -{2}(map_fmap_id x).
  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_id.
Qed.
Next Obligation.
  intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
Qed.