list.v 18.9 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 Oct 25, 2016 3 4 ``````From iris.base_logic Require Import base_logic. From iris.algebra Require Import updates local_updates. `````` Ralf Jung committed Jan 05, 2017 5 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Mar 21, 2016 6 7 `````` Section cofe. `````` Ralf Jung committed Nov 22, 2016 8 ``````Context {A : ofeT}. `````` Robbert Krebbers committed Mar 21, 2016 9 10 11 `````` Instance list_dist : Dist (list A) := λ n, Forall2 (dist n). `````` Robbert Krebbers committed May 23, 2016 12 13 14 ``````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. `````` Ralf Jung committed Jan 27, 2017 15 16 ``````Global Instance cons_ne : NonExpansive2 (@cons A) := _. Global Instance app_ne : NonExpansive2 (@app A) := _. `````` Robbert Krebbers committed Mar 21, 2016 17 ``````Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _. `````` Ralf Jung committed Jan 27, 2017 18 19 20 21 22 23 ``````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 committed Mar 21, 2016 24 25 ``````Global Instance list_alter_ne n f i : Proper (dist n ==> dist n) f → `````` Robbert Krebbers committed Jul 27, 2016 26 `````` Proper (dist n ==> dist n) (alter (M:=list A) f i) := _. `````` Ralf Jung committed Jan 27, 2017 27 28 29 30 31 32 33 34 ``````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 committed Mar 21, 2016 35 36 37 ``````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) := _. `````` Ralf Jung committed Jan 27, 2017 38 39 40 41 42 ``````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 committed Mar 21, 2016 43 ``````Global Instance resize_ne n : `````` Ralf Jung committed Jan 27, 2017 44 `````` NonExpansive2 (@resize A n) := _. `````` Robbert Krebbers committed Mar 21, 2016 45 `````` `````` Ralf Jung committed Nov 22, 2016 46 47 48 49 50 51 52 53 54 55 ``````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 committed Mar 21, 2016 56 ``````Program Definition list_chain `````` Ralf Jung committed Nov 22, 2016 57 `````` (c : chain listC) (x : A) (k : nat) : chain A := `````` Robbert Krebbers committed May 27, 2016 58 `````` {| chain_car n := from_option id x (c n !! k) |}. `````` Robbert Krebbers committed Mar 21, 2016 59 ``````Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed. `````` Ralf Jung committed Nov 22, 2016 60 ``````Definition list_compl `{Cofe A} : Compl listC := λ c, `````` Robbert Krebbers committed Mar 21, 2016 61 62 63 64 `````` match c 0 with | [] => [] | x :: _ => compl ∘ list_chain c x <\$> seq 0 (length (c 0)) end. `````` Ralf Jung committed Nov 22, 2016 65 66 67 68 69 70 71 72 73 74 75 76 77 ``````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 committed Mar 21, 2016 78 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 79 `````` `````` Robbert Krebbers committed Mar 21, 2016 80 81 82 83 84 85 86 87 88 89 90 91 ``````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 *) `````` Ralf Jung committed Nov 22, 2016 92 ``````Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A → B) (l : list A) n : `````` Robbert Krebbers committed Aug 08, 2016 93 94 `````` (∀ x, f x ≡{n}≡ g x) → f <\$> l ≡{n}≡ g <\$> l. Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed. `````` Ralf Jung committed Nov 22, 2016 95 ``````Instance list_fmap_ne {A B : ofeT} (f : A → B) n: `````` Robbert Krebbers committed Mar 21, 2016 96 `````` Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=list) f). `````` Robbert Krebbers committed Aug 08, 2016 97 ``````Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed. `````` Robbert Krebbers committed Mar 21, 2016 98 99 ``````Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B := CofeMor (fmap f : listC A → listC B). `````` Ralf Jung committed Jan 27, 2017 100 101 ``````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 committed Mar 21, 2016 102 103 104 105 106 107 108 109 110 111 `````` 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). `````` 112 `````` apply list_fmap_equiv_ext=>y. apply cFunctor_id. `````` Robbert Krebbers committed Mar 21, 2016 113 114 115 ``````Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose. `````` 116 `````` apply list_fmap_equiv_ext=>y; apply cFunctor_compose. `````` Robbert Krebbers committed Mar 21, 2016 117 118 119 120 121 122 123 ``````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 124 125 126 `````` (* CMRA *) Section cmra. `````` Robbert Krebbers committed May 27, 2016 127 `````` Context {A : ucmraT}. `````` Robbert Krebbers committed May 23, 2016 128 129 130 131 132 133 134 135 136 137 `````` 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 138 `````` Instance list_pcore : PCore (list A) := λ l, Some (core <\$> l). `````` Robbert Krebbers committed May 23, 2016 139 140 141 142 `````` Instance list_valid : Valid (list A) := Forall (λ x, ✓ x). Instance list_validN : ValidN (list A) := λ n, Forall (λ x, ✓{n} x). `````` Robbert Krebbers committed Sep 21, 2016 143 144 145 146 147 148 149 150 151 `````` 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 committed May 23, 2016 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 `````` 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 170 171 172 173 `````` Proof. rewrite /core /= list_lookup_fmap. destruct (l !! i); by rewrite /= ?Some_core. Qed. `````` Robbert Krebbers committed May 23, 2016 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 `````` 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 191 192 `````` apply cmra_total_mixin. - eauto. `````` Robbert Krebbers committed May 23, 2016 193 194 `````` - intros n l l1 l2; rewrite !list_dist_lookup=> Hl i. by rewrite !list_lookup_op Hl. `````` Robbert Krebbers committed May 28, 2016 195 `````` - intros n l1 l2 Hl; by rewrite /core /= Hl. `````` Robbert Krebbers committed May 23, 2016 196 197 198 199 200 201 202 203 204 205 206 207 208 209 `````` - 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 210 `````` rewrite !list_lookup_core. by apply cmra_core_mono. `````` Robbert Krebbers committed May 23, 2016 211 212 `````` - intros n l1 l2. rewrite !list_lookup_validN. setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l. `````` Robbert Krebbers committed Aug 14, 2016 213 214 215 216 217 218 219 220 `````` - intros n l. induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl; inversion_clear 1. + by exists [], []. + 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. exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto. `````` Robbert Krebbers committed May 23, 2016 221 `````` Qed. `````` Ralf Jung committed Nov 22, 2016 222 `````` Canonical Structure listR := CMRAT (list A) list_ofe_mixin list_cmra_mixin. `````` Robbert Krebbers committed May 23, 2016 223 224 `````` Global Instance empty_list : Empty (list A) := []. `````` Robbert Krebbers committed May 27, 2016 225 `````` Definition list_ucmra_mixin : UCMRAMixin (list A). `````` Robbert Krebbers committed May 23, 2016 226 227 228 229 `````` Proof. split. - constructor. - by intros l. `````` Robbert Krebbers committed May 28, 2016 230 `````` - by constructor. `````` Robbert Krebbers committed May 23, 2016 231 `````` Qed. `````` Robbert Krebbers committed May 27, 2016 232 `````` Canonical Structure listUR := `````` Ralf Jung committed Nov 22, 2016 233 `````` UCMRAT (list A) list_ofe_mixin list_cmra_mixin list_ucmra_mixin. `````` Robbert Krebbers committed May 23, 2016 234 235 236 237 238 239 240 241 242 `````` 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 243 244 `````` intros ?; constructor; apply list_equiv_lookup=> i. by rewrite list_lookup_core (persistent_core (l !! i)). `````` Robbert Krebbers committed May 23, 2016 245 246 247 `````` Qed. (** Internalized properties *) `````` Robbert Krebbers committed May 31, 2016 248 `````` Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M). `````` Robbert Krebbers committed May 23, 2016 249 `````` Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed. `````` Robbert Krebbers committed May 31, 2016 250 `````` Lemma list_validI {M} l : ✓ l ⊣⊢ (∀ i, ✓ (l !! i) : uPred M). `````` Robbert Krebbers committed May 23, 2016 251 252 253 254 `````` Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed. End cmra. Arguments listR : clear implicits. `````` Robbert Krebbers committed May 27, 2016 255 ``````Arguments listUR : clear implicits. `````` Robbert Krebbers committed May 23, 2016 256 `````` `````` Robbert Krebbers committed Jul 27, 2016 257 ``````Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x, `````` Robbert Krebbers committed May 23, 2016 258 259 260 `````` replicate n ∅ ++ [x]. Section properties. `````` Robbert Krebbers committed May 27, 2016 261 `````` Context {A : ucmraT}. `````` Robbert Krebbers committed Jul 27, 2016 262 `````` Implicit Types l : list A. `````` Robbert Krebbers committed May 27, 2016 263 `````` Implicit Types x y z : A. `````` Robbert Krebbers committed May 23, 2016 264 265 `````` Local Arguments op _ _ !_ !_ / : simpl nomatch. Local Arguments cmra_op _ !_ !_ / : simpl nomatch. `````` Robbert Krebbers committed Sep 21, 2016 266 `````` Local Arguments ucmra_op _ !_ !_ / : simpl nomatch. `````` Robbert Krebbers committed May 23, 2016 267 `````` `````` Robbert Krebbers committed Jul 27, 2016 268 `````` Lemma list_lookup_opM l mk i : (l ⋅? mk) !! i = l !! i ⋅ (mk ≫= (!! i)). `````` Robbert Krebbers committed Jun 16, 2016 269 270 `````` Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed. `````` Robbert Krebbers committed Sep 21, 2016 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 committed May 23, 2016 276 `````` Lemma list_op_app l1 l2 l3 : `````` Robbert Krebbers committed Sep 21, 2016 277 `````` (l1 ++ l3) ⋅ l2 = (l1 ⋅ take (length l1) l2) ++ (l3 ⋅ drop (length l1) l2). `````` Robbert Krebbers committed May 23, 2016 278 279 `````` Proof. revert l2 l3. `````` Robbert Krebbers committed Sep 21, 2016 280 `````` induction l1 as [|x1 l1]=> -[|x2 l2] [|x3 l3]; f_equal/=; auto. `````` Robbert Krebbers committed May 23, 2016 281 `````` Qed. `````` Robbert Krebbers committed Sep 21, 2016 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 committed May 23, 2016 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. `````` Ralf Jung committed Jan 27, 2017 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. `````` Robbert Krebbers committed Jul 27, 2016 299 300 `````` Global Instance list_singletonM_proper i : Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _. `````` Robbert Krebbers committed May 23, 2016 301 `````` `````` Robbert Krebbers committed Jul 27, 2016 302 `````` Lemma elem_of_list_singletonM i z x : z ∈ {[i := x]} → z = ∅ ∨ z = x. `````` Robbert Krebbers committed May 27, 2016 303 304 305 `````` Proof. rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver. Qed. `````` Robbert Krebbers committed Jul 27, 2016 306 `````` Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x. `````` Robbert Krebbers committed May 27, 2016 307 `````` Proof. induction i; by f_equal/=. Qed. `````` Robbert Krebbers committed Jul 27, 2016 308 309 `````` Lemma list_lookup_singletonM_ne i j x : i ≠ j → {[ i := x ]} !! j = None ∨ {[ i := x ]} !! j = Some ∅. `````` Robbert Krebbers committed May 27, 2016 310 `````` Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed. `````` Robbert Krebbers committed Jul 27, 2016 311 `````` Lemma list_singletonM_validN n i x : ✓{n} {[ i := x ]} ↔ ✓{n} x. `````` Robbert Krebbers committed May 27, 2016 312 313 `````` Proof. rewrite list_lookup_validN. split. `````` Robbert Krebbers committed Jul 27, 2016 314 `````` { move=> /(_ i). by rewrite list_lookup_singletonM. } `````` Robbert Krebbers committed May 27, 2016 315 `````` intros Hx j; destruct (decide (i = j)); subst. `````` Robbert Krebbers committed Jul 27, 2016 316 317 `````` - by rewrite list_lookup_singletonM. - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done; `````` Robbert Krebbers committed May 27, 2016 318 319 `````` rewrite Hi; by try apply (ucmra_unit_validN (A:=A)). Qed. `````` Robbert Krebbers committed Jul 27, 2016 320 321 322 323 324 `````` 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 325 `````` Proof. `````` Robbert Krebbers committed Jul 27, 2016 326 `````` rewrite /singletonM /list_singletonM app_length replicate_length /=; lia. `````` Robbert Krebbers committed May 27, 2016 327 328 `````` Qed. `````` Robbert Krebbers committed Jul 27, 2016 329 `````` Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}. `````` Robbert Krebbers committed May 27, 2016 330 `````` Proof. `````` Robbert Krebbers committed Jul 27, 2016 331 `````` rewrite /singletonM /list_singletonM. `````` Robbert Krebbers committed May 28, 2016 332 `````` by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ∅). `````` Robbert Krebbers committed May 27, 2016 333 `````` Qed. `````` Robbert Krebbers committed Jul 27, 2016 334 335 336 337 338 339 340 341 342 343 344 345 346 `````` 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 347 348 `````` (* Update *) `````` Robbert Krebbers committed Sep 21, 2016 349 350 `````` Lemma list_singleton_updateP (P : A → Prop) (Q : list A → Prop) x : x ~~>: P → (∀ y, P y → Q [y]) → [x] ~~>: Q. `````` Robbert Krebbers committed May 23, 2016 351 `````` Proof. `````` Robbert Krebbers committed Sep 21, 2016 352 353 354 355 `````` rewrite !cmra_total_updateP=> Hup HQ n lf /list_lookup_validN Hv. destruct (Hup n (from_option id ∅ (lf !! 0))) as (y&?&Hv'). { move: (Hv 0). by destruct lf; rewrite /= ?right_id. } exists [y]; split; first by auto. `````` Robbert Krebbers committed May 23, 2016 356 `````` apply list_lookup_validN=> i. `````` Robbert Krebbers committed Sep 21, 2016 357 358 359 360 361 362 363 364 `````` 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 committed May 23, 2016 365 366 `````` Qed. `````` Robbert Krebbers committed Sep 21, 2016 367 368 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 `````` 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. `````` Robbert Krebbers committed Jun 16, 2016 404 `````` Lemma list_middle_update l1 l2 x y : x ~~> y → l1 ++ x :: l2 ~~> l1 ++ y :: l2. `````` Robbert Krebbers committed May 23, 2016 405 `````` Proof. `````` Robbert Krebbers committed Sep 21, 2016 406 `````` rewrite !cmra_update_updateP=> ?; eauto using list_middle_updateP with subst. `````` Robbert Krebbers committed May 23, 2016 407 408 `````` Qed. `````` Robbert Krebbers committed Oct 06, 2016 409 ``````(* FIXME `````` Robbert Krebbers committed Jun 16, 2016 410 411 412 `````` 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 413 `````` Proof. `````` Robbert Krebbers committed Jun 16, 2016 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 `````` 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 429 `````` Qed. `````` Robbert Krebbers committed Jun 17, 2016 430 `````` Lemma list_singleton_local_update i x y ml : `````` Robbert Krebbers committed Jul 27, 2016 431 `````` x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml. `````` Robbert Krebbers committed Jun 17, 2016 432 `````` Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed. `````` Robbert Krebbers committed Oct 06, 2016 433 ``````*) `````` Robbert Krebbers committed May 23, 2016 434 435 436 ``````End properties. (** Functor *) `````` Robbert Krebbers committed May 27, 2016 437 ``````Instance list_fmap_cmra_monotone {A B : ucmraT} (f : A → B) `````` Robbert Krebbers committed May 23, 2016 438 439 440 441 `````` `{!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. `````` Robbert Krebbers committed Sep 28, 2016 442 `````` by apply (cmra_monotone_validN (fmap f : option A → option B)). `````` Robbert Krebbers committed May 23, 2016 443 `````` - intros l1 l2. rewrite !list_lookup_included=> Hl i. rewrite !list_lookup_fmap. `````` Ralf Jung committed Jul 25, 2016 444 `````` by apply (cmra_monotone (fmap f : option A → option B)). `````` Robbert Krebbers committed May 23, 2016 445 446 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 447 448 449 ``````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 450 451 ``````|}. Next Obligation. `````` Robbert Krebbers committed May 27, 2016 452 `````` by intros F ???? n f g Hfg; apply listC_map_ne, urFunctor_ne. `````` Robbert Krebbers committed May 23, 2016 453 454 455 ``````Qed. Next Obligation. intros F A B x. rewrite /= -{2}(list_fmap_id x). `````` 456 `````` apply list_fmap_equiv_ext=>y. apply urFunctor_id. `````` Robbert Krebbers committed May 23, 2016 457 458 459 ``````Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose. `````` 460 `````` apply list_fmap_equiv_ext=>y; apply urFunctor_compose. `````` Robbert Krebbers committed May 23, 2016 461 462 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 463 464 ``````Instance listURF_contractive F : urFunctorContractive F → urFunctorContractive (listURF F). `````` Robbert Krebbers committed May 23, 2016 465 ``````Proof. `````` Robbert Krebbers committed May 27, 2016 466 `````` by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, urFunctor_contractive. `````` Robbert Krebbers committed May 23, 2016 467 ``Qed.``