list.v 19.1 KB
Newer Older
1
From iris.algebra Require Export cmra.
Ralf Jung's avatar
Ralf Jung committed
2
From stdpp Require Export list.
3
4
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import updates local_updates.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7

Section cofe.
8
Context {A : ofeT}.
9
Implicit Types l : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
12

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

13
14
15
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.

16
17
Global Instance cons_ne : NonExpansive2 (@cons A) := _.
Global Instance app_ne : NonExpansive2 (@app A) := _.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.
19
20
21
22
23
24
Global Instance tail_ne : NonExpansive (@tail A) := _.
Global Instance take_ne : NonExpansive (@take A n) := _.
Global Instance drop_ne : NonExpansive (@drop A n) := _.
Global Instance list_lookup_ne i :
  NonExpansive (lookup (M:=list A) i).
Proof. intros ????. by apply dist_option_Forall2, Forall2_lookup. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
Global Instance list_alter_ne n f i :
  Proper (dist n ==> dist n) f 
27
  Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
28
29
30
31
32
33
34
35
Global Instance list_insert_ne i :
  NonExpansive2 (insert (M:=list A) i) := _.
Global Instance list_inserts_ne i :
  NonExpansive2 (@list_inserts A i) := _.
Global Instance list_delete_ne i :
  NonExpansive (delete (M:=list A) i) := _.
Global Instance option_list_ne : NonExpansive (@option_list A).
Proof. intros ????; by apply Forall2_option_list, dist_option_Forall2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
38
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) := _.
39
40
41
42
43
Global Instance replicate_ne :
  NonExpansive (@replicate A n) := _.
Global Instance reverse_ne : NonExpansive (@reverse A) := _.
Global Instance last_ne : NonExpansive (@last A).
Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Global Instance resize_ne n :
45
  NonExpansive2 (@resize A n) := _.
Robbert Krebbers's avatar
Robbert Krebbers committed
46

47
48
49
50
51
52
53
54
55
56
Definition list_ofe_mixin : OfeMixin (list A).
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.
Canonical Structure listC := OfeT (list A) list_ofe_mixin.

Robbert Krebbers's avatar
Robbert Krebbers committed
57
Program Definition list_chain
58
    (c : chain listC) (x : A) (k : nat) : chain A :=
59
  {| chain_car n := from_option id x (c n !! k) |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
61
Definition list_compl `{Cofe A} : Compl listC := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
65
  match c 0 with
  | [] => []
  | x :: _ => compl  list_chain c x <$> seq 0 (length (c 0))
  end.
66
67
68
69
70
71
72
73
74
75
76
77
78
Global Program Instance list_cofe `{Cofe A} : Cofe listC :=
  {| compl := list_compl |}.
Next Obligation.
  intros ? n c; rewrite /compl /list_compl.
  destruct (c 0) as [|x l] eqn:Hc0 at 1.
  { by destruct (chain_cauchy c 0 n); auto with omega. }
  rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last omega.
  apply Forall2_lookup=> i. rewrite -dist_option_Forall2 list_lookup_fmap.
  destruct (decide (i < length (c n))); last first.
  { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. }
  rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
  destruct (lookup_lt_is_Some_2 (c n) i) as [? Hcn]; first done.
  by rewrite Hcn.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Qed.
80

81
Global Instance list_ofe_discrete : OfeDiscrete A  OfeDiscrete listC.
82
Proof. induction 2; constructor; try apply (discrete _); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
83

84
Global Instance nil_discrete : Discrete (@nil A).
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Proof. inversion_clear 1; constructor. Qed.
86
87
Global Instance cons_discrete 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
88
89
90
91
92
End cofe.

Arguments listC : clear implicits.

(** Functor *)
93
Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A  B) (l : list A) n :
94
95
  ( x, f x {n} g x)  f <$> l {n} g <$> l.
Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
96
Instance list_fmap_ne {A B : ofeT} (f : A  B) n:
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  Proper (dist n ==> dist n) f  Proper (dist n ==> dist n) (fmap (M:=list) f).
98
Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
  CofeMor (fmap f : listC A  listC B).
101
102
Instance listC_map_ne A B : NonExpansive (@listC_map A B).
Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
105
106
107
108
109
110
111
112

Program Definition listCF (F : cFunctor) : cFunctor := {|
  cFunctor_car A B := listC (cFunctor_car F A B);
  cFunctor_map A1 A2 B1 B2 fg := listC_map (cFunctor_map F fg)
|}.
Next Obligation.
  by intros F A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
  intros F A B x. rewrite /= -{2}(list_fmap_id x).
113
  apply list_fmap_equiv_ext=>y. apply cFunctor_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
116
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
117
  apply list_fmap_equiv_ext=>y; apply cFunctor_compose.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
120
121
122
123
124
Qed.

Instance listCF_contractive F :
  cFunctorContractive F  cFunctorContractive (listCF F).
Proof.
  by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_contractive.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
126
127

(* CMRA *)
Section cmra.
128
  Context {A : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
131
132
133
134
135
136
137
138
  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
139
  Instance list_pcore : PCore (list A) := λ l, Some (core <$> l).
Robbert Krebbers's avatar
Robbert Krebbers committed
140
141
142
143

  Instance list_valid : Valid (list A) := Forall (λ x,  x).
  Instance list_validN : ValidN (list A) := λ n, Forall (λ x, {n} x).

144
145
146
147
148
149
150
151
152
  Lemma cons_valid l x :  (x :: l)   x   l.
  Proof. apply Forall_cons. Qed.
  Lemma cons_validN n l x : {n} (x :: l)  {n} x  {n} l.
  Proof. apply Forall_cons. Qed.
  Lemma app_valid l1 l2 :  (l1 ++ l2)   l1   l2.
  Proof. apply Forall_app. Qed.
  Lemma app_validN n l1 l2 : {n} (l1 ++ l2)  {n} l1  {n} l2.
  Proof. apply Forall_app. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
  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
171
172
173
174
  Proof.
    rewrite /core /= list_lookup_fmap.
    destruct (l !! i); by rewrite /= ?Some_core.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189

  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.

190
  Definition list_cmra_mixin : CmraMixin (list A).
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
    apply cmra_total_mixin.
    - eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
    - intros n l l1 l2; rewrite !list_dist_lookup=> Hl i.
      by rewrite !list_lookup_op Hl.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
    - intros n l1 l2 Hl; by rewrite /core /= Hl.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
198
199
200
201
202
203
204
205
206
207
208
209
210
    - 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.
    - 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.
211
      rewrite !list_lookup_core. by apply cmra_core_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
    - intros n l1 l2. rewrite !list_lookup_validN.
      setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
214
    - intros n l.
215
      induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl; inversion_clear 1.
216
      + by exists [], [].
217
218
219
220
      + exists [], (x :: l); by repeat constructor.
      + exists (x :: l), []; by repeat constructor.
      + inversion_clear Hl. destruct (IH l1 l2) as (l1'&l2'&?&?&?),
          (cmra_extend n x y1 y2) as (y1'&y2'&?&?&?); simplify_eq/=; auto.
221
        exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
  Qed.
223
  Canonical Structure listR := CmraT (list A) list_cmra_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
224

Robbert Krebbers's avatar
Robbert Krebbers committed
225
  Global Instance list_unit : Unit (list A) := [].
226
  Definition list_ucmra_mixin : UcmraMixin (list A).
Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
229
230
  Proof.
    split.
    - constructor.
    - by intros l.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
    - by constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
  Qed.
233
  Canonical Structure listUR := UcmraT (list A) list_ucmra_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
234

235
  Global Instance list_cmra_discrete : CmraDiscrete A  CmraDiscrete listR.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
238
239
240
  Proof.
    split; [apply _|]=> l; rewrite list_lookup_valid list_lookup_validN=> Hl i.
    by apply cmra_discrete_valid.
  Qed.

241
  Global Instance list_core_id l : ( x : A, CoreId x)  CoreId l.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
    intros ?; constructor; apply list_equiv_lookup=> i.
244
    by rewrite list_lookup_core (core_id_core (l !! i)).
Robbert Krebbers's avatar
Robbert Krebbers committed
245
246
247
  Qed.

  (** Internalized properties *)
248
  Lemma list_equivI {M} l1 l2 : l1  l2  ( i, l1 !! i  l2 !! i : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
249
  Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
250
  Lemma list_validI {M} l :  l  ( i,  (l !! i) : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
251
252
253
254
  Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
End cmra.

Arguments listR : clear implicits.
255
Arguments listUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
256

257
Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
258
  replicate n ε ++ [x].
Robbert Krebbers's avatar
Robbert Krebbers committed
259
260

Section properties.
261
  Context {A : ucmraT}.
262
  Implicit Types l : list A.
263
  Implicit Types x y z : A.
Robbert Krebbers's avatar
Robbert Krebbers committed
264
265
  Local Arguments op _ _ !_ !_ / : simpl nomatch.
  Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
266
  Local Arguments ucmra_op _ !_ !_ / : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
267

268
  Lemma list_lookup_opM l mk i : (l ? mk) !! i = l !! i  (mk = (!! i)).
269
270
  Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.

271
272
273
274
275
  Global Instance list_op_nil_l : LeftId (=) (@nil A) op.
  Proof. done. Qed.
  Global Instance list_op_nil_r : RightId (=) (@nil A) op.
  Proof. by intros []. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
276
  Lemma list_op_app l1 l2 l3 :
277
    (l1 ++ l3)  l2 = (l1  take (length l1) l2) ++ (l3  drop (length l1) l2).
Robbert Krebbers's avatar
Robbert Krebbers committed
278
279
  Proof.
    revert l2 l3.
280
    induction l1 as [|x1 l1]=> -[|x2 l2] [|x3 l3]; f_equal/=; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
  Qed.
282
283
284
  Lemma list_op_app_le l1 l2 l3 :
    length l2  length l1  (l1 ++ l3)  l2 = (l1  l2) ++ l3.
  Proof. intros ?. by rewrite list_op_app take_ge // drop_ge // right_id_L. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
286
287
288
289
290
291
292
293
294
295

  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.
296
297
298
  Global Instance list_singletonM_ne i :
    NonExpansive (@list_singletonM A i).
  Proof. intros n l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
299
300
  Global Instance list_singletonM_proper i :
    Proper (() ==> ()) (list_singletonM i) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
301

Robbert Krebbers's avatar
Robbert Krebbers committed
302
  Lemma elem_of_list_singletonM i z x : z  ({[i := x]} : list A)  z = ε  z = x.
303
304
305
  Proof.
    rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
  Qed.
306
  Lemma list_lookup_singletonM i x : ({[ i := x ]} : list A) !! i = Some x.
307
  Proof. induction i; by f_equal/=. Qed.
308
  Lemma list_lookup_singletonM_ne i j x :
309
    i  j 
Robbert Krebbers's avatar
Robbert Krebbers committed
310
    ({[ i := x ]} : list A) !! j = None  ({[ i := x ]} : list A) !! j = Some ε.
311
  Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
312
  Lemma list_singletonM_validN n i x : {n} ({[ i := x ]} : list A)  {n} x.
313
314
  Proof.
    rewrite list_lookup_validN. split.
315
    { move=> /(_ i). by rewrite list_lookup_singletonM. }
316
    intros Hx j; destruct (decide (i = j)); subst.
317
318
    - by rewrite list_lookup_singletonM.
    - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
319
320
        rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
  Qed.
321
  Lemma list_singleton_valid  i x :  ({[ i := x ]} : list A)   x.
322
323
324
325
  Proof.
    rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
  Qed.
  Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
326
  Proof.
327
    rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
328
329
  Qed.

330
  Lemma list_core_singletonM i (x : A) : core {[ i := x ]}  {[ i := core x ]}.
331
  Proof.
332
    rewrite /singletonM /list_singletonM.
333
    by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ).
334
  Qed.
335
336
337
338
339
340
  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.
341
342
  Lemma list_alter_singletonM f i x :
    alter f i ({[i := x]} : list A) = {[i := f x]}.
343
344
345
  Proof.
    rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
  Qed.
346
347
348
  Global Instance list_singleton_core_id i (x : A) :
    CoreId x  CoreId {[ i := x ]}.
  Proof. by rewrite !core_id_total list_core_singletonM=> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
350

  (* Update *)
351
352
  Lemma list_singleton_updateP (P : A  Prop) (Q : list A  Prop) x :
    x ~~>: P  ( y, P y  Q [y])  [x] ~~>: Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
353
  Proof.
354
    rewrite !cmra_total_updateP=> Hup HQ n lf /list_lookup_validN Hv.
Robbert Krebbers's avatar
Robbert Krebbers committed
355
    destruct (Hup n (from_option id ε (lf !! 0))) as (y&?&Hv').
356
357
    { move: (Hv 0). by destruct lf; rewrite /= ?right_id. }
    exists [y]; split; first by auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
    apply list_lookup_validN=> i.
359
360
361
362
363
364
365
366
    move: (Hv i) Hv'. by destruct i, lf; rewrite /= ?right_id.
  Qed.
  Lemma list_singleton_updateP' (P : A  Prop) x :
    x ~~>: P  [x] ~~>: λ k,  y, k = [y]  P y.
  Proof. eauto using list_singleton_updateP. Qed.
  Lemma list_singleton_update x y : x ~~> y  [x] ~~> [y].
  Proof.
    rewrite !cmra_update_updateP; eauto using list_singleton_updateP with subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
367
368
  Qed.

369
370
371
372
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
399
400
401
402
403
404
405
  Lemma app_updateP (P1 P2 Q : list A  Prop) l1 l2 :
    l1 ~~>: P1  l2 ~~>: P2 
    ( k1 k2, P1 k1  P2 k2  length l1 = length k1  Q (k1 ++ k2)) 
    l1 ++ l2 ~~>: Q.
  Proof.
    rewrite !cmra_total_updateP=> Hup1 Hup2 HQ n lf.
    rewrite list_op_app app_validN=> -[??].
    destruct (Hup1 n (take (length l1) lf)) as (k1&?&?); auto.
    destruct (Hup2 n (drop (length l1) lf)) as (k2&?&?); auto.
    exists (k1 ++ k2). rewrite list_op_app app_validN.
    by destruct (HQ k1 k2) as [<- ?].
  Qed.
  Lemma app_update l1 l2 k1 k2 :
    length l1 = length k1 
    l1 ~~> k1  l2 ~~> k2  l1 ++ l2 ~~> k1 ++ k2.
  Proof. rewrite !cmra_update_updateP; eauto using app_updateP with subst. Qed.

  Lemma cons_updateP (P1 : A  Prop) (P2 Q : list A  Prop) x l :
    x ~~>: P1  l ~~>: P2  ( y k, P1 y  P2 k  Q (y :: k))  x :: l ~~>: Q.
  Proof.
    intros. eapply (app_updateP _ _ _ [x]);
      naive_solver eauto using list_singleton_updateP'.
  Qed.
  Lemma cons_updateP' (P1 : A  Prop) (P2 : list A  Prop) x l :
    x ~~>: P1  l ~~>: P2  x :: l ~~>: λ k,  y k', k = y :: k'  P1 y  P2 k'.
  Proof. eauto 10 using cons_updateP. Qed.
  Lemma cons_update x y l k : x ~~> y  l ~~> k  x :: l ~~> y :: k.
  Proof. rewrite !cmra_update_updateP; eauto using cons_updateP with subst. Qed.

  Lemma list_middle_updateP (P : A  Prop) (Q : list A  Prop) l1 x l2 :
    x ~~>: P  ( y, P y  Q (l1 ++ y :: l2))  l1 ++ x :: l2 ~~>: Q.
  Proof.
    intros. eapply app_updateP.
    - by apply cmra_update_updateP.
    - by eapply cons_updateP', cmra_update_updateP.
    - naive_solver.
  Qed.
406
  Lemma list_middle_update l1 l2 x y : x ~~> y  l1 ++ x :: l2 ~~> l1 ++ y :: l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
407
  Proof.
408
    rewrite !cmra_update_updateP=> ?; eauto using list_middle_updateP with subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
409
410
  Qed.

411
(* FIXME
412
413
414
  Lemma list_middle_local_update l1 l2 x y ml :
    x ~l~> y @ ml ≫= (!! length l1) →
    l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
  Proof.
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
    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
431
  Qed.
432
  Lemma list_singleton_local_update i x y ml :
433
    x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
434
  Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
435
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
436
437
438
End properties.

(** Functor *)
439
Instance list_fmap_cmra_morphism {A B : ucmraT} (f : A  B)
440
  `{!CmraMorphism f} : CmraMorphism (fmap f : list A  list B).
Robbert Krebbers's avatar
Robbert Krebbers committed
441
442
443
Proof.
  split; try apply _.
  - intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
444
445
446
447
448
    by apply (cmra_morphism_validN (fmap f : option A  option B)).
  - intros l. apply Some_proper. rewrite -!list_fmap_compose.
    apply list_fmap_equiv_ext, cmra_morphism_core, _.
  - intros l1 l2. apply list_equiv_lookup=>i.
    by rewrite list_lookup_op !list_lookup_fmap list_lookup_op cmra_morphism_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
449
450
Qed.

451
452
453
Program Definition listURF (F : urFunctor) : urFunctor := {|
  urFunctor_car A B := listUR (urFunctor_car F A B);
  urFunctor_map A1 A2 B1 B2 fg := listC_map (urFunctor_map F fg)
Robbert Krebbers's avatar
Robbert Krebbers committed
454
455
|}.
Next Obligation.
456
  by intros F ???? n f g Hfg; apply listC_map_ne, urFunctor_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
458
459
Qed.
Next Obligation.
  intros F A B x. rewrite /= -{2}(list_fmap_id x).
460
  apply list_fmap_equiv_ext=>y. apply urFunctor_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
461
462
463
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
464
  apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
Robbert Krebbers's avatar
Robbert Krebbers committed
465
466
Qed.

467
468
Instance listURF_contractive F :
  urFunctorContractive F  urFunctorContractive (listURF F).
Robbert Krebbers's avatar
Robbert Krebbers committed
469
Proof.
470
  by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, urFunctor_contractive.
Robbert Krebbers's avatar
Robbert Krebbers committed
471
Qed.