list.v 16.7 KB
 Robbert Krebbers committed Jul 25, 2016 1 ``````From iris.algebra Require Export cmra. `````` Robbert Krebbers committed May 25, 2016 2 ``````From iris.prelude Require Export list. `````` Robbert Krebbers committed Jul 25, 2016 3 ``````From iris.algebra Require Import upred updates local_updates. `````` Robbert Krebbers committed Mar 21, 2016 4 5 6 7 8 9 `````` Section cofe. Context {A : cofeT}. Instance list_dist : Dist (list A) := λ n, Forall2 (dist n). `````` Robbert Krebbers committed May 23, 2016 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 committed Mar 21, 2016 13 14 15 16 17 18 19 ``````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 : `````` Robbert Krebbers committed Jul 27, 2016 20 `````` Proper (dist n ==> dist n) (lookup (M:=list A) i). `````` Robbert Krebbers committed Mar 21, 2016 21 22 23 ``````Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed. Global Instance list_alter_ne n f i : Proper (dist n ==> dist n) f → `````` Robbert Krebbers committed Jul 27, 2016 24 `````` Proper (dist n ==> dist n) (alter (M:=list A) f i) := _. `````` Robbert Krebbers committed Mar 21, 2016 25 ``````Global Instance list_insert_ne n i : `````` Robbert Krebbers committed Jul 27, 2016 26 `````` Proper (dist n ==> dist n ==> dist n) (insert (M:=list A) i) := _. `````` Robbert Krebbers committed Mar 21, 2016 27 28 29 ``````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 : `````` Robbert Krebbers committed Jul 27, 2016 30 `````` Proper (dist n ==> dist n) (delete (M:=list A) i) := _. `````` Robbert Krebbers committed Mar 21, 2016 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 ``````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) := _. Program Definition list_chain (c : chain (list A)) (x : A) (k : nat) : chain A := `````` Robbert Krebbers committed May 27, 2016 46 `````` {| chain_car n := from_option id x (c n !! k) |}. `````` Robbert Krebbers committed Mar 21, 2016 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 ``````Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed. Instance list_compl : Compl (list A) := λ c, match c 0 with | [] => [] | x :: _ => compl ∘ list_chain c x <\$> seq 0 (length (c 0)) end. Definition list_cofe_mixin : CofeMixin (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. - 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. `````` Robbert Krebbers committed May 27, 2016 65 66 `````` apply Forall2_lookup=> i. rewrite -dist_option_Forall2 list_lookup_fmap. destruct (decide (i < length (c n))); last first. `````` Robbert Krebbers committed Mar 21, 2016 67 68 69 70 `````` { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. } rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=. by destruct (lookup_lt_is_Some_2 (c n) i) as [? ->]. Qed. `````` Robbert Krebbers committed May 25, 2016 71 ``````Canonical Structure listC := CofeT (list A) list_cofe_mixin. `````` Robbert Krebbers committed Mar 21, 2016 72 73 74 75 76 77 78 79 80 81 82 83 ``````Global Instance list_discrete : Discrete A → Discrete listC. Proof. induction 2; constructor; try apply (timeless _); auto. Qed. Global Instance nil_timeless : Timeless (@nil A). Proof. inversion_clear 1; constructor. Qed. Global Instance cons_timeless x l : Timeless x → Timeless l → Timeless (x :: l). Proof. intros ??; inversion_clear 1; constructor; by apply timeless. Qed. End cofe. Arguments listC : clear implicits. (** Functor *) `````` Robbert Krebbers committed Aug 08, 2016 84 85 86 ``````Lemma list_fmap_ext_ne {A} {B : cofeT} (f g : A → B) (l : list A) n : (∀ x, f x ≡{n}≡ g x) → f <\$> l ≡{n}≡ g <\$> l. Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed. `````` Robbert Krebbers committed Mar 21, 2016 87 88 ``````Instance list_fmap_ne {A B : cofeT} (f : A → B) n: Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=list) f). `````` Robbert Krebbers committed Aug 08, 2016 89 ``````Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed. `````` Robbert Krebbers committed Mar 21, 2016 90 91 92 ``````Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B := CofeMor (fmap f : listC A → listC B). Instance listC_map_ne A B n : Proper (dist n ==> dist n) (@listC_map A B). `````` Robbert Krebbers committed Aug 08, 2016 93 ``````Proof. intros f g ? l. by apply list_fmap_ext_ne. Qed. `````` Robbert Krebbers committed Mar 21, 2016 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 `````` 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). apply list_fmap_setoid_ext=>y. apply cFunctor_id. Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose. apply list_fmap_setoid_ext=>y; apply cFunctor_compose. 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 committed May 23, 2016 116 117 118 `````` (* CMRA *) Section cmra. `````` Robbert Krebbers committed May 27, 2016 119 `````` Context {A : ucmraT}. `````` Robbert Krebbers committed May 23, 2016 120 121 122 123 124 125 126 127 128 129 `````` 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 committed May 28, 2016 130 `````` Instance list_pcore : PCore (list A) := λ l, Some (core <\$> l). `````` Robbert Krebbers committed May 23, 2016 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 `````` Instance list_valid : Valid (list A) := Forall (λ x, ✓ x). Instance list_validN : ValidN (list A) := λ n, Forall (λ x, ✓{n} x). 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 committed May 28, 2016 153 154 155 156 `````` Proof. rewrite /core /= list_lookup_fmap. destruct (l !! i); by rewrite /= ?Some_core. Qed. `````` Robbert Krebbers committed May 23, 2016 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 `````` 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 committed May 28, 2016 174 175 `````` apply cmra_total_mixin. - eauto. `````` Robbert Krebbers committed May 23, 2016 176 177 `````` - intros n l l1 l2; rewrite !list_dist_lookup=> Hl i. by rewrite !list_lookup_op Hl. `````` Robbert Krebbers committed May 28, 2016 178 `````` - intros n l1 l2 Hl; by rewrite /core /= Hl. `````` Robbert Krebbers committed May 23, 2016 179 180 181 182 183 184 185 186 187 188 189 190 191 192 `````` - 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. `````` Ralf Jung committed Jul 25, 2016 193 `````` rewrite !list_lookup_core. by apply cmra_core_mono. `````` Robbert Krebbers committed May 23, 2016 194 195 196 197 198 199 200 201 202 203 204 205 `````` - 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 committed May 28, 2016 206 `````` Canonical Structure listR := CMRAT (list A) list_cofe_mixin list_cmra_mixin. `````` Robbert Krebbers committed May 23, 2016 207 208 `````` Global Instance empty_list : Empty (list A) := []. `````` Robbert Krebbers committed May 27, 2016 209 `````` Definition list_ucmra_mixin : UCMRAMixin (list A). `````` Robbert Krebbers committed May 23, 2016 210 211 212 213 214 `````` Proof. split. - constructor. - by intros l. - by inversion_clear 1. `````` Robbert Krebbers committed May 28, 2016 215 `````` - by constructor. `````` Robbert Krebbers committed May 23, 2016 216 `````` Qed. `````` Robbert Krebbers committed May 27, 2016 217 218 `````` Canonical Structure listUR := UCMRAT (list A) list_cofe_mixin list_cmra_mixin list_ucmra_mixin. `````` Robbert Krebbers committed May 23, 2016 219 220 221 222 223 224 225 226 227 `````` 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. Global Instance list_persistent l : (∀ x : A, Persistent x) → Persistent l. Proof. `````` Robbert Krebbers committed May 28, 2016 228 229 `````` intros ?; constructor; apply list_equiv_lookup=> i. by rewrite list_lookup_core (persistent_core (l !! i)). `````` Robbert Krebbers committed May 23, 2016 230 231 232 `````` Qed. (** Internalized properties *) `````` Robbert Krebbers committed May 31, 2016 233 `````` Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M). `````` Robbert Krebbers committed May 23, 2016 234 `````` Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed. `````` Robbert Krebbers committed May 31, 2016 235 `````` Lemma list_validI {M} l : ✓ l ⊣⊢ (∀ i, ✓ (l !! i) : uPred M). `````` Robbert Krebbers committed May 23, 2016 236 237 238 239 `````` Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed. End cmra. Arguments listR : clear implicits. `````` Robbert Krebbers committed May 27, 2016 240 ``````Arguments listUR : clear implicits. `````` Robbert Krebbers committed May 23, 2016 241 `````` `````` Robbert Krebbers committed Jul 27, 2016 242 ``````Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x, `````` Robbert Krebbers committed May 23, 2016 243 244 245 `````` replicate n ∅ ++ [x]. Section properties. `````` Robbert Krebbers committed May 27, 2016 246 `````` Context {A : ucmraT}. `````` Robbert Krebbers committed Jul 27, 2016 247 `````` Implicit Types l : list A. `````` Robbert Krebbers committed May 27, 2016 248 `````` Implicit Types x y z : A. `````` Robbert Krebbers committed May 23, 2016 249 250 251 `````` Local Arguments op _ _ !_ !_ / : simpl nomatch. Local Arguments cmra_op _ !_ !_ / : simpl nomatch. `````` Robbert Krebbers committed Jul 27, 2016 252 `````` Lemma list_lookup_opM l mk i : (l ⋅? mk) !! i = l !! i ⋅ (mk ≫= (!! i)). `````` Robbert Krebbers committed Jun 16, 2016 253 254 `````` Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed. `````` Robbert Krebbers committed May 23, 2016 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 `````` 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. `````` Robbert Krebbers committed Jul 27, 2016 272 273 `````` Global Instance list_singletonM_ne n i : Proper (dist n ==> dist n) (@list_singletonM A i). `````` Robbert Krebbers committed May 27, 2016 274 `````` Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed. `````` Robbert Krebbers committed Jul 27, 2016 275 276 `````` Global Instance list_singletonM_proper i : Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _. `````` Robbert Krebbers committed May 23, 2016 277 `````` `````` Robbert Krebbers committed Jul 27, 2016 278 `````` Lemma elem_of_list_singletonM i z x : z ∈ {[i := x]} → z = ∅ ∨ z = x. `````` Robbert Krebbers committed May 27, 2016 279 280 281 `````` Proof. rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver. Qed. `````` Robbert Krebbers committed Jul 27, 2016 282 `````` Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x. `````` Robbert Krebbers committed May 27, 2016 283 `````` Proof. induction i; by f_equal/=. Qed. `````` Robbert Krebbers committed Jul 27, 2016 284 285 `````` Lemma list_lookup_singletonM_ne i j x : i ≠ j → {[ i := x ]} !! j = None ∨ {[ i := x ]} !! j = Some ∅. `````` Robbert Krebbers committed May 27, 2016 286 `````` Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed. `````` Robbert Krebbers committed Jul 27, 2016 287 `````` Lemma list_singletonM_validN n i x : ✓{n} {[ i := x ]} ↔ ✓{n} x. `````` Robbert Krebbers committed May 27, 2016 288 289 `````` Proof. rewrite list_lookup_validN. split. `````` Robbert Krebbers committed Jul 27, 2016 290 `````` { move=> /(_ i). by rewrite list_lookup_singletonM. } `````` Robbert Krebbers committed May 27, 2016 291 `````` intros Hx j; destruct (decide (i = j)); subst. `````` Robbert Krebbers committed Jul 27, 2016 292 293 `````` - by rewrite list_lookup_singletonM. - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done; `````` Robbert Krebbers committed May 27, 2016 294 295 `````` rewrite Hi; by try apply (ucmra_unit_validN (A:=A)). Qed. `````` Robbert Krebbers committed Jul 27, 2016 296 297 298 299 300 `````` 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. `````` Robbert Krebbers committed May 27, 2016 301 `````` Proof. `````` Robbert Krebbers committed Jul 27, 2016 302 `````` rewrite /singletonM /list_singletonM app_length replicate_length /=; lia. `````` Robbert Krebbers committed May 27, 2016 303 304 `````` Qed. `````` Robbert Krebbers committed Jul 27, 2016 305 `````` Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}. `````` Robbert Krebbers committed May 27, 2016 306 `````` Proof. `````` Robbert Krebbers committed Jul 27, 2016 307 `````` rewrite /singletonM /list_singletonM. `````` Robbert Krebbers committed May 28, 2016 308 `````` by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ∅). `````` Robbert Krebbers committed May 27, 2016 309 `````` Qed. `````` Robbert Krebbers committed Jul 27, 2016 310 311 312 313 314 315 316 317 318 319 320 321 322 `````` 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. Lemma list_alter_singletonM f i x : alter f i {[i := x]} = {[i := f x]}. Proof. rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto. Qed. Global Instance list_singleton_persistent i (x : A) : Persistent x → Persistent {[ i := x ]}. Proof. by rewrite !persistent_total list_core_singletonM=> ->. Qed. `````` Robbert Krebbers committed May 23, 2016 323 324 `````` (* Update *) `````` Robbert Krebbers committed Jun 16, 2016 325 `````` Lemma list_middle_updateP (P : A → Prop) (Q : list A → Prop) l1 x l2 : `````` Robbert Krebbers committed May 23, 2016 326 327 `````` x ~~>: P → (∀ y, P y → Q (l1 ++ y :: l2)) → l1 ++ x :: l2 ~~>: Q. Proof. `````` Robbert Krebbers committed May 28, 2016 328 329 330 `````` 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 committed May 23, 2016 331 332 333 334 335 336 337 338 339 340 `````` { 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. `````` Robbert Krebbers committed Jun 16, 2016 341 `````` Lemma list_middle_update l1 l2 x y : x ~~> y → l1 ++ x :: l2 ~~> l1 ++ y :: l2. `````` Robbert Krebbers committed May 23, 2016 342 `````` Proof. `````` Robbert Krebbers committed Jun 16, 2016 343 `````` rewrite !cmra_update_updateP => H; eauto using list_middle_updateP with subst. `````` Robbert Krebbers committed May 23, 2016 344 345 `````` Qed. `````` Robbert Krebbers committed Jun 16, 2016 346 347 348 `````` 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 committed May 23, 2016 349 `````` Proof. `````` Robbert Krebbers committed Jun 16, 2016 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 `````` 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 committed May 23, 2016 365 `````` Qed. `````` Robbert Krebbers committed Jun 17, 2016 366 367 `````` Lemma list_singleton_local_update i x y ml : `````` Robbert Krebbers committed Jul 27, 2016 368 `````` x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml. `````` Robbert Krebbers committed Jun 17, 2016 369 `````` Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed. `````` Robbert Krebbers committed May 23, 2016 370 371 372 ``````End properties. (** Functor *) `````` Robbert Krebbers committed May 27, 2016 373 ``````Instance list_fmap_cmra_monotone {A B : ucmraT} (f : A → B) `````` Robbert Krebbers committed May 23, 2016 374 375 376 377 378 379 `````` `{!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. `````` Ralf Jung committed Jul 25, 2016 380 `````` by apply (cmra_monotone (fmap f : option A → option B)). `````` Robbert Krebbers committed May 23, 2016 381 382 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 383 384 385 ``````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 committed May 23, 2016 386 387 ``````|}. Next Obligation. `````` Robbert Krebbers committed May 27, 2016 388 `````` by intros F ???? n f g Hfg; apply listC_map_ne, urFunctor_ne. `````` Robbert Krebbers committed May 23, 2016 389 390 391 ``````Qed. Next Obligation. intros F A B x. rewrite /= -{2}(list_fmap_id x). `````` Robbert Krebbers committed May 27, 2016 392 `````` apply list_fmap_setoid_ext=>y. apply urFunctor_id. `````` Robbert Krebbers committed May 23, 2016 393 394 395 ``````Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose. `````` Robbert Krebbers committed May 27, 2016 396 `````` apply list_fmap_setoid_ext=>y; apply urFunctor_compose. `````` Robbert Krebbers committed May 23, 2016 397 398 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 399 400 ``````Instance listURF_contractive F : urFunctorContractive F → urFunctorContractive (listURF F). `````` Robbert Krebbers committed May 23, 2016 401 ``````Proof. `````` Robbert Krebbers committed May 27, 2016 402 `````` by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, urFunctor_contractive. `````` Robbert Krebbers committed May 23, 2016 403 ``Qed.``