list.v 20.2 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
Global Instance tail_ne : NonExpansive (@tail A) := _.
Global Instance take_ne : NonExpansive (@take A n) := _.
Global Instance drop_ne : NonExpansive (@drop A n) := _.
22
Global Instance head_ne : NonExpansive (head (A:=A)).
23
Proof. destruct 1; by constructor. Qed.
24 25 26
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
27 28
Global Instance list_alter_ne n f i :
  Proper (dist n ==> dist n) f 
29
  Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
30 31 32 33 34 35 36 37
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
38 39 40
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) := _.
41 42 43 44 45
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
46
Global Instance resize_ne n :
47
  NonExpansive2 (@resize A n) := _.
Robbert Krebbers's avatar
Robbert Krebbers committed
48

49 50 51 52 53 54 55
Lemma list_dist_cons_inv_l n x l k :
  x :: l {n} k   y k', x {n} y  l {n} k'  k = y :: k'.
Proof. apply Forall2_cons_inv_l. Qed.
Lemma list_dist_cons_inv_r n l k y :
  l {n} y :: k   x l', x {n} y  l' {n} k  l = x :: l'.
Proof. apply Forall2_cons_inv_r. Qed.

56 57 58 59 60 61 62 63
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.
64
Canonical Structure listO := OfeT (list A) list_ofe_mixin.
65

66 67 68 69 70 71
(** To define [compl : chain (list A) → list A] we make use of the fact that
given a given chain [c0, c1, c2, ...] of lists, the list [c0] completely
determines the shape (i.e. the length) of all lists in the chain. So, the
[compl] operation is defined by structural recursion on [c0], and takes the
completion of the elements of all lists in the chain point-wise. We use [head]
and [tail] as the inverse of [cons]. *)
72
Fixpoint list_compl_go `{!Cofe A} (c0 : list A) (c : chain listO) : listO :=
73
  match c0 with
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  | [] => []
75
  | x :: c0 => compl (chain_map (default x  head) c) :: list_compl_go c0 (chain_map tail c)
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  end.
77

78
Global Program Instance list_cofe `{!Cofe A} : Cofe listO :=
79
  {| compl c := list_compl_go (c 0) c |}.
80
Next Obligation.
81 82 83 84 85 86 87 88 89
  intros ? n c; rewrite /compl.
  assert (c 0 {0} c n) as Hc0 by (symmetry; apply chain_cauchy; lia).
  revert Hc0. generalize (c 0)=> c0. revert c.
  induction c0 as [|x c0 IH]=> c Hc0 /=.
  { by inversion Hc0. }
  apply list_dist_cons_inv_l in Hc0 as (x' & xs' & Hx & Hc0 & Hcn).
  rewrite Hcn. f_equiv.
  - by rewrite conv_compl /= Hcn /=.
  - rewrite IH /= ?Hcn //.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Qed.
91

92
Global Instance list_ofe_discrete : OfeDiscrete A  OfeDiscrete listO.
93
Proof. induction 2; constructor; try apply (discrete _); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
94

95
Global Instance nil_discrete : Discrete (@nil A).
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Proof. inversion_clear 1; constructor. Qed.
97 98
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
99 100
End cofe.

101
Arguments listO : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103

(** Functor *)
104
Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A  B) (l : list A) n :
105 106
  ( x, f x {n} g x)  f <$> l {n} g <$> l.
Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
107
Instance list_fmap_ne {A B : ofeT} (f : A  B) n:
Robbert Krebbers's avatar
Robbert Krebbers committed
108
  Proper (dist n ==> dist n) f  Proper (dist n ==> dist n) (fmap (M:=list) f).
109
Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
110 111 112
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 : NonExpansive (@listO_map A B).
113
Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
114

115 116 117
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
118 119
|}.
Next Obligation.
120
  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122
Qed.
Next Obligation.
123
  intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
124
  apply list_fmap_equiv_ext=>y. apply oFunctor_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126
Qed.
Next Obligation.
127
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
128
  apply list_fmap_equiv_ext=>y; apply oFunctor_compose.
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130
Qed.

131 132
Instance listOF_contractive F :
  oFunctorContractive F  oFunctorContractive (listOF F).
Robbert Krebbers's avatar
Robbert Krebbers committed
133
Proof.
134
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_contractive.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
136 137 138

(* CMRA *)
Section cmra.
139
  Context {A : ucmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141 142 143 144 145 146 147 148 149
  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
150
  Instance list_pcore : PCore (list A) := λ l, Some (core <$> l).
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153 154

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

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

  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.

201
  Definition list_cmra_mixin : CmraMixin (list A).
Robbert Krebbers's avatar
Robbert Krebbers committed
202
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204
    apply cmra_total_mixin.
    - eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
205 206
    - intros n l l1 l2; rewrite !list_dist_lookup=> Hl i.
      by rewrite !list_lookup_op Hl.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
    - intros n l1 l2 Hl; by rewrite /core /= Hl.
Robbert Krebbers's avatar
Robbert Krebbers committed
208 209 210 211 212 213 214 215 216 217 218 219 220 221
    - 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.
222
      rewrite !list_lookup_core. by apply cmra_core_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
223 224
    - intros n l1 l2. rewrite !list_lookup_validN.
      setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
225
    - intros n l.
226 227
      induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Heq;
        (try by exfalso; inversion Heq).
228
      + by exists [], [].
229 230 231 232 233
      + exists [], (x :: l); inversion Heq; by repeat constructor.
      + exists (x :: l), []; inversion Heq; by repeat constructor.
      + destruct (IH l1 l2) as (l1'&l2'&?&?&?),
          (cmra_extend n x y1 y2) as (y1'&y2'&?&?&?);
          [by inversion_clear Heq; inversion_clear Hl..|].
234
        exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
  Qed.
236
  Canonical Structure listR := CmraT (list A) list_cmra_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
237

Robbert Krebbers's avatar
Robbert Krebbers committed
238
  Global Instance list_unit : Unit (list A) := [].
239
  Definition list_ucmra_mixin : UcmraMixin (list A).
Robbert Krebbers's avatar
Robbert Krebbers committed
240 241 242 243
  Proof.
    split.
    - constructor.
    - by intros l.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
    - by constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
245
  Qed.
246
  Canonical Structure listUR := UcmraT (list A) list_ucmra_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
247

248
  Global Instance list_cmra_discrete : CmraDiscrete A  CmraDiscrete listR.
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250 251 252 253
  Proof.
    split; [apply _|]=> l; rewrite list_lookup_valid list_lookup_validN=> Hl i.
    by apply cmra_discrete_valid.
  Qed.

254
  Global Instance list_core_id l : ( x : A, CoreId x)  CoreId l.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
    intros ?; constructor; apply list_equiv_lookup=> i.
257
    by rewrite list_lookup_core (core_id_core (l !! i)).
Robbert Krebbers's avatar
Robbert Krebbers committed
258 259 260
  Qed.

  (** Internalized properties *)
261
  Lemma list_equivI {M} l1 l2 : l1  l2 @{uPredI M}  i, l1 !! i  l2 !! i.
Robbert Krebbers's avatar
Robbert Krebbers committed
262
  Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
263
  Lemma list_validI {M} l :  l @{uPredI M}  i,  (l !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
264 265 266 267
  Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
End cmra.

Arguments listR : clear implicits.
268
Arguments listUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
269

270
Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
271
  replicate n ε ++ [x].
Robbert Krebbers's avatar
Robbert Krebbers committed
272 273

Section properties.
274
  Context {A : ucmraT}.
275
  Implicit Types l : list A.
276
  Implicit Types x y z : A.
Robbert Krebbers's avatar
Robbert Krebbers committed
277 278
  Local Arguments op _ _ !_ !_ / : simpl nomatch.
  Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
279
  Local Arguments ucmra_op _ !_ !_ / : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
280

281
  Lemma list_lookup_opM l mk i : (l ? mk) !! i = l !! i  (mk = (!! i)).
282 283
  Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.

284 285 286 287 288
  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
289
  Lemma list_op_app l1 l2 l3 :
290
    (l1 ++ l3)  l2 = (l1  take (length l1) l2) ++ (l3  drop (length l1) l2).
Robbert Krebbers's avatar
Robbert Krebbers committed
291 292
  Proof.
    revert l2 l3.
293
    induction l1 as [|x1 l1]=> -[|x2 l2] [|x3 l3]; f_equal/=; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
294
  Qed.
295 296 297
  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
298 299 300 301 302 303 304 305 306 307 308

  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.
309 310 311
  Global Instance list_singletonM_ne i :
    NonExpansive (@list_singletonM A i).
  Proof. intros n l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
312 313
  Global Instance list_singletonM_proper i :
    Proper (() ==> ()) (list_singletonM i) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
314

Robbert Krebbers's avatar
Robbert Krebbers committed
315
  Lemma elem_of_list_singletonM i z x : z  ({[i := x]} : list A)  z = ε  z = x.
316 317 318
  Proof.
    rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
  Qed.
319
  Lemma list_lookup_singletonM i x : ({[ i := x ]} : list A) !! i = Some x.
320
  Proof. induction i; by f_equal/=. Qed.
321
  Lemma list_lookup_singletonM_ne i j x :
322
    i  j 
Robbert Krebbers's avatar
Robbert Krebbers committed
323
    ({[ i := x ]} : list A) !! j = None  ({[ i := x ]} : list A) !! j = Some ε.
Ralf Jung's avatar
Ralf Jung committed
324
  Proof. revert j; induction i; intros [|j]; naive_solver auto with lia. Qed.
325
  Lemma list_singletonM_validN n i x : {n} ({[ i := x ]} : list A)  {n} x.
326 327
  Proof.
    rewrite list_lookup_validN. split.
328
    { move=> /(_ i). by rewrite list_lookup_singletonM. }
329
    intros Hx j; destruct (decide (i = j)); subst.
330 331
    - by rewrite list_lookup_singletonM.
    - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
332 333
        rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
  Qed.
334
  Lemma list_singleton_valid  i x :  ({[ i := x ]} : list A)   x.
335 336 337 338
  Proof.
    rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
  Qed.
  Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
339
  Proof.
340
    rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
341 342
  Qed.

343
  Lemma list_core_singletonM i (x : A) : core {[ i := x ]}  {[ i := core x ]}.
344
  Proof.
345
    rewrite /singletonM /list_singletonM.
346
    by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ).
347
  Qed.
348 349 350 351 352 353
  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.
354 355
  Lemma list_alter_singletonM f i x :
    alter f i ({[i := x]} : list A) = {[i := f x]}.
356 357 358
  Proof.
    rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
  Qed.
359 360 361
  Global Instance list_singleton_core_id i (x : A) :
    CoreId x  CoreId {[ i := x ]}.
  Proof. by rewrite !core_id_total list_core_singletonM=> ->. Qed.
Michael Sammler's avatar
Michael Sammler committed
362 363 364
  Lemma list_singleton_snoc l x:
    {[length l := x]}  l  l ++ [x].
  Proof. elim: l => //= ?? <-. by rewrite left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
365 366

  (* Update *)
367 368
  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
369
  Proof.
370
    rewrite !cmra_total_updateP=> Hup HQ n lf /list_lookup_validN Hv.
371
    destruct (Hup n (default ε (lf !! 0))) as (y&?&Hv').
372 373
    { move: (Hv 0). by destruct lf; rewrite /= ?right_id. }
    exists [y]; split; first by auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
374
    apply list_lookup_validN=> i.
375 376 377 378 379 380 381 382
    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
383 384
  Qed.

385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421
  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.
422
  Lemma list_middle_update l1 l2 x y : x ~~> y  l1 ++ x :: l2 ~~> l1 ++ y :: l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
423
  Proof.
424
    rewrite !cmra_update_updateP=> ?; eauto using list_middle_updateP with subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
425 426
  Qed.

427
(* FIXME
428 429 430
  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
431
  Proof.
432 433 434 435 436 437 438 439 440 441 442 443 444 445 446
    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
447
  Qed.
448
  Lemma list_singleton_local_update i x y ml :
449
    x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
450
  Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
451
*)
Michael Sammler's avatar
Michael Sammler committed
452 453 454 455 456 457 458 459 460 461 462

  Lemma list_alloc_singleton_local_update x l :
     x  (l, ε) ~l~> (l ++ [x], {[length l := x]}).
  Proof.
    move => ?.
    have -> : ({[length l := x]}  {[length l := x]}  ε) by rewrite right_id.
    rewrite -list_singleton_snoc. apply op_local_update => ??.
    rewrite list_singleton_snoc app_validN cons_validN. split_and? => //; [| constructor].
    by apply cmra_valid_validN.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
463 464 465
End properties.

(** Functor *)
466
Instance list_fmap_cmra_morphism {A B : ucmraT} (f : A  B)
467
  `{!CmraMorphism f} : CmraMorphism (fmap f : list A  list B).
Robbert Krebbers's avatar
Robbert Krebbers committed
468 469 470
Proof.
  split; try apply _.
  - intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
471 472 473 474 475
    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
476 477
Qed.

478
Program Definition listURF (F : urFunctor) : urFunctor := {|
479
  urFunctor_car A _ B _ := listUR (urFunctor_car F A B);
480
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
Robbert Krebbers's avatar
Robbert Krebbers committed
481 482
|}.
Next Obligation.
483
  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
484 485
Qed.
Next Obligation.
486
  intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
487
  apply list_fmap_equiv_ext=>y. apply urFunctor_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
488 489
Qed.
Next Obligation.
490
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
491
  apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
Robbert Krebbers's avatar
Robbert Krebbers committed
492 493
Qed.

494 495
Instance listURF_contractive F :
  urFunctorContractive F  urFunctorContractive (listURF F).
Robbert Krebbers's avatar
Robbert Krebbers committed
496
Proof.
497
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_contractive.
Robbert Krebbers's avatar
Robbert Krebbers committed
498
Qed.