list.v 16.2 KB
Newer Older
1
From fri.algebra Require Export cmra.
2
From stdpp Require Export list.
3
From fri.algebra Require Import upred upred_bi updates local_updates.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
5

Section cofe.
6
Context {A : ofeT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9

Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).

10
11
12
Lemma list_dist_lookup n l1 l2 : l1 {n} l2   i, l1 !! i {n} l2 !! i.
Proof. setoid_rewrite dist_option_Forall2. apply Forall2_lookup. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
Global Instance cons_ne n : Proper (dist n ==> dist n ==> dist n) (@cons A) := _.
Global Instance app_ne n : Proper (dist n ==> dist n ==> dist n) (@app A) := _.
Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.
Global Instance tail_ne n : Proper (dist n ==> dist n) (@tail A) := _.
Global Instance take_ne n : Proper (dist n ==> dist n) (@take A n) := _.
Global Instance drop_ne n : Proper (dist n ==> dist n) (@drop A n) := _.
Global Instance list_lookup_ne n i :
  Proper (dist n ==> dist n) (lookup (M:=list A) i).
Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed.
Global Instance list_alter_ne n f i :
  Proper (dist n ==> dist n) f 
  Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
Global Instance list_insert_ne n i :
  Proper (dist n ==> dist n ==> dist n) (insert (M:=list A) i) := _.
Global Instance list_inserts_ne n i :
  Proper (dist n ==> dist n ==> dist n) (@list_inserts A i) := _.
Global Instance list_delete_ne n i :
  Proper (dist n ==> dist n) (delete (M:=list A) i) := _.
Global Instance option_list_ne n : Proper (dist n ==> dist n) (@option_list A).
Proof. intros ???; by apply Forall2_option_list, dist_option_Forall2. Qed.
Global Instance list_filter_ne n P `{ x, Decision (P x)} :
  Proper (dist n ==> iff) P 
  Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
Global Instance replicate_ne n :
  Proper (dist n ==> dist n) (@replicate A n) := _.
Global Instance reverse_ne n : Proper (dist n ==> dist n) (@reverse A) := _.
Global Instance last_ne n : Proper (dist n ==> dist n) (@last A).
Proof. intros ???; by apply dist_option_Forall2, Forall2_last. Qed.
Global Instance resize_ne n :
  Proper (dist n ==> dist n ==> dist n) (@resize A n) := _.

44
Definition list_cofe_mixin : OfeMixin (list A).
Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
47
48
49
50
51
Proof.
  split.
  - intros l k. rewrite equiv_Forall2 -Forall2_forall.
    split; induction 1; constructor; intros; try apply equiv_dist; auto.
  - apply _.
  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
Qed.
52
53
Canonical Structure listO := OfeT (list A) list_cofe_mixin.
Global Instance list_discrete : OfeDiscrete A  OfeDiscrete listO.
54
Proof. induction 2; constructor; try apply (discrete _); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55

56
Global Instance nil_timeless : Discrete (@nil A).
Robbert Krebbers's avatar
Robbert Krebbers committed
57
Proof. inversion_clear 1; constructor. Qed.
58
59
Global Instance cons_timeless x l : Discrete x  Discrete l  Discrete (x :: l).
Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
End cofe.

62
Arguments listO : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
64

(** Functor *)
65
Instance list_fmap_ne {A B : ofeT} (f : A  B) n:
Robbert Krebbers's avatar
Robbert Krebbers committed
66
67
  Proper (dist n ==> dist n) f  Proper (dist n ==> dist n) (fmap (M:=list) f).
Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed. 
68
69
70
Definition listO_map {A B} (f : A -n> B) : listO A -n> listO B :=
  OfeMor (fmap f : listO A  listO B).
Instance listO_map_ne A B n : Proper (dist n ==> dist n) (@listO_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
Proof. intros f f' ? l; by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.

73
74
75
Program Definition listOF (F : oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := listO (oFunctor_car F A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (oFunctor_map F fg)
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
|}.
Next Obligation.
78
  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
  intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
82
  apply list_fmap_equiv_ext=>y. apply oFunctor_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
84
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
86
  apply list_fmap_equiv_ext=>y; apply oFunctor_compose.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
88
Qed.

89
90
Instance listOF_contractive F :
  oFunctorContractive F  oFunctorContractive (listOF F).
Robbert Krebbers's avatar
Robbert Krebbers committed
91
Proof.
92
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_contractive.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
96

(* CMRA *)
Section cmra.
97
  Context {A : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
99
100
101
102
103
104
105
106
107
  Implicit Types l : list A.
  Local Arguments op _ _ !_ !_ / : simpl nomatch.

  Instance list_op : Op (list A) :=
    fix go l1 l2 := let _ : Op _ := @go in
    match l1, l2 with
    | [], _ => l2
    | _, [] => l1
    | x :: l1, y :: l2 => x  y :: l1  l2
    end.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  Instance list_pcore : PCore (list A) := λ l, Some (core <$> l).
Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111

  Instance list_valid : Valid (list A) := Forall (λ x,  x).
  Instance list_validN : ValidN (list A) := λ n, Forall (λ x, {n} x).
112
113
  (* One can consider many possible step choices *)
  Instance list_stepN : StepN (list A) := λ n x y, True.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132

  Lemma list_lookup_valid l :  l   i,  (l !! i).
  Proof.
    rewrite {1}/valid /list_valid Forall_lookup; split.
    - intros Hl i. by destruct (l !! i) as [x|] eqn:?; [apply (Hl i)|].
    - intros Hl i x Hi. move: (Hl i); by rewrite Hi.
  Qed.
  Lemma list_lookup_validN n l : {n} l   i, {n} (l !! i).
  Proof.
    rewrite {1}/validN /list_validN Forall_lookup; split.
    - intros Hl i. by destruct (l !! i) as [x|] eqn:?; [apply (Hl i)|].
    - intros Hl i x Hi. move: (Hl i); by rewrite Hi.
  Qed.
  Lemma list_lookup_op l1 l2 i : (l1  l2) !! i = l1 !! i  l2 !! i.
  Proof.
    revert i l2. induction l1 as [|x l1]; intros [|i] [|y l2];
      by rewrite /= ?left_id_L ?right_id_L.
  Qed.
  Lemma list_lookup_core l i : core l !! i = core (l !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
135
136
  Proof.
    rewrite /core /= list_lookup_fmap.
    destruct (l !! i); by rewrite /= ?Some_core.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153

  Lemma list_lookup_included l1 l2 : l1  l2   i, l1 !! i  l2 !! i.
  Proof.
    split.
    { intros [l Hl] i. exists (l !! i). by rewrite Hl list_lookup_op. }
    revert l1. induction l2 as [|y l2 IH]=>-[|x l1] Hl.
    - by exists [].
    - destruct (Hl 0) as [[z|] Hz]; inversion Hz.
    - by exists (y :: l2).
    - destruct (IH l1) as [l3 ?]; first (intros i; apply (Hl (S i))).
      destruct (Hl 0) as [[z|] Hz]; inversion_clear Hz; simplify_eq/=.
      + exists (z :: l3); by constructor.
      + exists (core x :: l3); constructor; by rewrite ?cmra_core_r.
  Qed.

  Definition list_cmra_mixin : CMRAMixin (list A).
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
    apply cmra_total_mixin.
    - eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
    - intros n l l1 l2; rewrite !list_dist_lookup=> Hl i.
      by rewrite !list_lookup_op Hl.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
    - intros n l1 l2 Hl; by rewrite /core /= Hl.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
161
162
163
    - intros n l1 l2; rewrite !list_dist_lookup !list_lookup_validN=> Hl ? i.
      by rewrite -Hl.
    - intros l. rewrite list_lookup_valid. setoid_rewrite list_lookup_validN.
      setoid_rewrite cmra_valid_validN. naive_solver.
    - intros n x. rewrite !list_lookup_validN. auto using cmra_validN_S.
164
165
    - by intros.
    - by intros.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
168
169
170
171
172
173
174
    - intros l1 l2 l3; rewrite list_equiv_lookup=> i.
      by rewrite !list_lookup_op assoc.
    - intros l1 l2; rewrite list_equiv_lookup=> i.
      by rewrite !list_lookup_op comm.
    - intros l; rewrite list_equiv_lookup=> i.
      by rewrite list_lookup_op list_lookup_core cmra_core_l.
    - intros l; rewrite list_equiv_lookup=> i.
      by rewrite !list_lookup_core cmra_core_idemp.
    - intros l1 l2; rewrite !list_lookup_included=> Hl i.
175
      rewrite !list_lookup_core. by apply cmra_core_mono.
176
177
178
179
    - intros n l1 l2. 
      rewrite !list_dist_lookup !list_lookup_validN=>Hv i.
      rewrite !list_lookup_core !list_lookup_op !list_lookup_core.
      apply cmra_core_distrib. move:(Hv i). by rewrite list_lookup_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
181
182
183
184
185
186
187
188
189
190
191
    - intros n l1 l2. rewrite !list_lookup_validN.
      setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
    - intros n l. induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Hl';
        try (by exfalso; inversion_clear Hl').
      + by exists ([], []).
      + by exists ([], x :: l).
      + by exists (x :: l, []).
      + destruct (IH l1 l2) as ([l1' l2']&?&?&?),
          (cmra_extend n x y1 y2) as ([y1' y2']&?&?&?);
          [inversion_clear Hl; inversion_clear Hl'; auto ..|]; simplify_eq/=.
        exists (y1' :: l1', y2' :: l2'); repeat constructor; auto.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
  Canonical Structure listR := CMRAT (list A) list_cofe_mixin list_cmra_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194

  Global Instance empty_list : Empty (list A) := [].
195
  Definition list_ucmra_mixin : UCMRAMixin (list A).
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197
198
199
  Proof.
    split.
    - constructor.
    - by intros l.
200
    - by inversion_clear 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
    - by constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
  Qed.
203
204
  Canonical Structure listUR :=
    UCMRAT (list A) list_cofe_mixin list_cmra_mixin list_ucmra_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
207
208
209
210
211

  Global Instance list_cmra_discrete : CMRADiscrete A  CMRADiscrete listR.
  Proof.
    split; [apply _|]=> l; rewrite list_lookup_valid list_lookup_validN=> Hl i.
    by apply cmra_discrete_valid.
  Qed.

212
  Global Instance list_persistent l : ( x : A, cmra.Persistent x)  cmra.Persistent l.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
215
    intros ?; constructor; apply list_equiv_lookup=> i.
    by rewrite list_lookup_core (persistent_core (l !! i)).
Robbert Krebbers's avatar
Robbert Krebbers committed
216
217
218
  Qed.

  (** Internalized properties *)
219
  Lemma list_equivI {M} l1 l2 : l1  l2 ⊣⊢ ( i, l1 !! i  l2 !! i : uPred M).
220
  Proof. uPred.unseal; constructor=> n x y ? ?. apply list_dist_lookup. Qed.
221
  Lemma list_validI {M} l :  l ⊣⊢ ( i,  (l !! i) : uPred M).
222
  Proof. uPred.unseal; constructor=> n x y ? ?. apply list_lookup_validN. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
225
End cmra.

Arguments listR : clear implicits.
226
Arguments listUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
227

228
Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230
231
  replicate n  ++ [x].

Section properties.
232
  Context {A : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
  Implicit Types l : list A.
234
  Implicit Types x y z : A.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
237
  Local Arguments op _ _ !_ !_ / : simpl nomatch.
  Local Arguments cmra_op _ !_ !_ / : simpl nomatch.

Robbert Krebbers's avatar
Robbert Krebbers committed
238
  Lemma list_lookup_opM l mk i : (l ? mk) !! i = l !! i  (mk = (.!! i)).
239
240
  Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
  Lemma list_op_app l1 l2 l3 :
    length l2  length l1  (l1 ++ l3)  l2 = (l1  l2) ++ l3.
  Proof.
    revert l2 l3.
    induction l1 as [|x1 l1]=> -[|x2 l2] [|x3 l3] ?; f_equal/=; auto with lia.
  Qed.

  Lemma list_lookup_validN_Some n l i x : {n} l  l !! i {n} Some x  {n} x.
  Proof. move=> /list_lookup_validN /(_ i)=> Hl Hi; move: Hl. by rewrite Hi. Qed.
  Lemma list_lookup_valid_Some l i x :  l  l !! i  Some x   x.
  Proof. move=> /list_lookup_valid /(_ i)=> Hl Hi; move: Hl. by rewrite Hi. Qed.

  Lemma list_op_length l1 l2 : length (l1  l2) = max (length l1) (length l2).
  Proof. revert l2. induction l1; intros [|??]; f_equal/=; auto. Qed.

  Lemma replicate_valid n (x : A) :  x   replicate n x.
  Proof. apply Forall_replicate. Qed.
258
259
260
261
262
  Global Instance list_singletonM_ne n i :
    Proper (dist n ==> dist n) (@list_singletonM A i).
  Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
  Global Instance list_singletonM_proper i :
    Proper (() ==> ()) (list_singletonM i) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
263

264
  Lemma elem_of_list_singletonM i z x : z  ({[i := x]} : list A)  z =   z = x.
265
266
267
  Proof.
    rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
  Qed.
268
  Lemma list_lookup_singletonM i x : ({[ i := x ]} : list A) !! i = Some x.
269
270
  Proof. induction i; by f_equal/=. Qed.
  Lemma list_lookup_singletonM_ne i j x :
271
272
    i  j 
    ({[ i := x ]} : list A) !! j = None  ({[ i := x ]} : list A) !! j = Some .
Ralf Jung's avatar
Ralf Jung committed
273
  Proof. revert j; induction i; intros [|j]; naive_solver auto with lia. Qed.
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
  Lemma list_singletonM_validN n i x : {n} {[ i := x ]}  {n} x.
  Proof.
    rewrite list_lookup_validN. split.
    { move=> /(_ i). by rewrite list_lookup_singletonM. }
    intros Hx j; destruct (decide (i = j)); subst.
    - by rewrite list_lookup_singletonM.
    - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
        rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
  Qed.
  Lemma list_singleton_valid  i x :  {[ i := x ]}   x.
  Proof.
    rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
  Qed.
  Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
  Proof.
    rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
  Qed.

  Lemma list_core_singletonM i (x : A) : core {[ i := x ]}  {[ i := core x ]}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
294
295
    rewrite /singletonM /list_singletonM.
    by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ).
296
297
298
299
300
301
302
  Qed.
  Lemma list_op_singletonM i (x y : A) :
    {[ i := x ]}  {[ i := y ]}  {[ i := x  y ]}.
  Proof.
    rewrite /singletonM /list_singletonM /=.
    induction i; constructor; rewrite ?left_id; auto.
  Qed.
303
304
  Lemma list_alter_singletonM f i x :
    alter f i ({[i := x]} : list A) = {[i := f x]}.
305
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
    rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
307
308
  Qed.
  Global Instance list_singleton_persistent i (x : A) :
309
    cmra.Persistent x  cmra.Persistent {[ i := x ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
310
  Proof. by rewrite !persistent_total list_core_singletonM=> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
311
312

  (* Update *)
313
  Lemma list_middle_updateP (P : A  Prop) (Q : list A  Prop) l1 x l2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
314
315
    x ~~>: P  ( y, P y  Q (l1 ++ y :: l2))  l1 ++ x :: l2 ~~>: Q.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
316
317
318
    intros Hx%option_updateP' HP.
    apply cmra_total_updateP=> n mf; rewrite list_lookup_validN=> Hm.
    destruct (Hx n (Some (mf !! length l1))) as ([y|]&H1&H2); simpl in *; try done.
Robbert Krebbers's avatar
Robbert Krebbers committed
319
320
321
322
323
324
325
326
327
328
    { move: (Hm (length l1)). by rewrite list_lookup_op list_lookup_middle. }
    exists (l1 ++ y :: l2); split; auto.
    apply list_lookup_validN=> i.
    destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
    - move: (Hm i); by rewrite !list_lookup_op !lookup_app_l.
    - by rewrite list_lookup_op list_lookup_middle.
    - move: (Hm i). rewrite !(cons_middle _ l1 l2) !assoc.
      rewrite !list_lookup_op !lookup_app_r !app_length //=; lia.
  Qed.

329
  Lemma list_middle_update l1 l2 x y : x ~~> y  l1 ++ x :: l2 ~~> l1 ++ y :: l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
330
  Proof.
331
    rewrite !cmra_update_updateP => H; eauto using list_middle_updateP with subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
332
333
  Qed.

334
  Lemma list_middle_local_update l1 l2 x y ml :
Robbert Krebbers's avatar
Robbert Krebbers committed
335
    x ~l~> y @ ml = (.!! length l1) 
336
    l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml.
Robbert Krebbers's avatar
Robbert Krebbers committed
337
  Proof.
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
    intros [Hxy Hxy']; split.
    - intros n; rewrite !list_lookup_validN=> Hl i; move: (Hl i).
      destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
      + by rewrite !list_lookup_opM !lookup_app_l.
      + rewrite !list_lookup_opM !list_lookup_middle // !Some_op_opM; apply (Hxy n).
      + rewrite !(cons_middle _ l1 l2) !assoc.
        rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
    - intros n mk; rewrite !list_lookup_validN !list_dist_lookup => Hl Hl' i.
      move: (Hl i) (Hl' i).
      destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
      + by rewrite !list_lookup_opM !lookup_app_l.
      + rewrite !list_lookup_opM !list_lookup_middle // !Some_op_opM !inj_iff.
        apply (Hxy' n).
      + rewrite !(cons_middle _ l1 l2) !assoc.
        rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
353
  Qed.
354
355

  Lemma list_singleton_local_update i x y ml :
Robbert Krebbers's avatar
Robbert Krebbers committed
356
    x ~l~> y @ ml = (.!! i)  {[ i := x ]} ~l~> {[ i := y ]} @ ml.
357
  Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
359
360
End properties.

(** Functor *)
361
Instance list_fmap_cmra_monotone {A B : ucmraT} (f : A  B)
Robbert Krebbers's avatar
Robbert Krebbers committed
362
363
364
365
366
367
  `{!CMRAMonotone f} : CMRAMonotone (fmap f : list A  list B).
Proof.
  split; try apply _.
  - intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
    by apply (validN_preserving (fmap f : option A  option B)).
  - intros l1 l2. rewrite !list_lookup_included=> Hl i. rewrite !list_lookup_fmap.
368
    by apply (cmra_monotone (fmap f : option A  option B)).
Robbert Krebbers's avatar
Robbert Krebbers committed
369
370
Qed.

371
Program Definition listURF (F : urFunctor) : urFunctor := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
372
  urFunctor_car A _ B _ := listUR (urFunctor_car F A B);
373
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
Robbert Krebbers's avatar
Robbert Krebbers committed
374
375
|}.
Next Obligation.
376
  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
377
378
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
379
  intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
380
  apply list_fmap_equiv_ext=>y. apply urFunctor_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
381
382
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
383
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
384
  apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
Robbert Krebbers's avatar
Robbert Krebbers committed
385
386
Qed.

387
388
Instance listURF_contractive F :
  urFunctorContractive F  urFunctorContractive (listURF F).
Robbert Krebbers's avatar
Robbert Krebbers committed
389
Proof.
390
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_contractive.
Robbert Krebbers's avatar
Robbert Krebbers committed
391
Qed.