list.v 19 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 `````` 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 135 136 137 138 139 140 141 142 143 `````` 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 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 `````` 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 162 163 164 165 `````` Proof. rewrite /core /= list_lookup_fmap. destruct (l !! i); by rewrite /= ?Some_core. Qed. `````` Robbert Krebbers committed May 23, 2016 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 `````` 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 183 184 `````` apply cmra_total_mixin. - eauto. `````` Robbert Krebbers committed May 23, 2016 185 186 `````` - intros n l l1 l2; rewrite !list_dist_lookup=> Hl i. by rewrite !list_lookup_op Hl. `````` Robbert Krebbers committed May 28, 2016 187 `````` - intros n l1 l2 Hl; by rewrite /core /= Hl. `````` Robbert Krebbers committed May 23, 2016 188 189 190 191 192 193 194 195 196 197 198 199 200 201 `````` - 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 202 `````` rewrite !list_lookup_core. by apply cmra_core_mono. `````` Robbert Krebbers committed May 23, 2016 203 204 `````` - 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 205 206 207 208 209 210 211 212 `````` - 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 213 `````` Qed. `````` Robbert Krebbers committed May 28, 2016 214 `````` Canonical Structure listR := CMRAT (list A) list_cofe_mixin list_cmra_mixin. `````` Robbert Krebbers committed May 23, 2016 215 216 `````` Global Instance empty_list : Empty (list A) := []. `````` Robbert Krebbers committed May 27, 2016 217 `````` Definition list_ucmra_mixin : UCMRAMixin (list A). `````` Robbert Krebbers committed May 23, 2016 218 219 220 221 `````` Proof. split. - constructor. - by intros l. `````` Robbert Krebbers committed May 28, 2016 222 `````` - by constructor. `````` Robbert Krebbers committed May 23, 2016 223 `````` Qed. `````` Robbert Krebbers committed May 27, 2016 224 225 `````` Canonical Structure listUR := UCMRAT (list A) list_cofe_mixin list_cmra_mixin list_ucmra_mixin. `````` Robbert Krebbers committed May 23, 2016 226 227 228 229 230 231 232 233 234 `````` 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 235 236 `````` intros ?; constructor; apply list_equiv_lookup=> i. by rewrite list_lookup_core (persistent_core (l !! i)). `````` Robbert Krebbers committed May 23, 2016 237 238 239 `````` Qed. (** Internalized properties *) `````` Robbert Krebbers committed May 31, 2016 240 `````` Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M). `````` Robbert Krebbers committed May 23, 2016 241 `````` Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed. `````` Robbert Krebbers committed May 31, 2016 242 `````` Lemma list_validI {M} l : ✓ l ⊣⊢ (∀ i, ✓ (l !! i) : uPred M). `````` Robbert Krebbers committed May 23, 2016 243 244 245 246 `````` Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed. End cmra. Arguments listR : clear implicits. `````` Robbert Krebbers committed May 27, 2016 247 ``````Arguments listUR : clear implicits. `````` Robbert Krebbers committed May 23, 2016 248 `````` `````` Robbert Krebbers committed Jul 27, 2016 249 ``````Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x, `````` Robbert Krebbers committed May 23, 2016 250 251 252 `````` replicate n ∅ ++ [x]. Section properties. `````` Robbert Krebbers committed May 27, 2016 253 `````` Context {A : ucmraT}. `````` Robbert Krebbers committed Jul 27, 2016 254 `````` Implicit Types l : list A. `````` Robbert Krebbers committed May 27, 2016 255 `````` Implicit Types x y z : A. `````` Robbert Krebbers committed May 23, 2016 256 257 `````` Local Arguments op _ _ !_ !_ / : simpl nomatch. Local Arguments cmra_op _ !_ !_ / : simpl nomatch. `````` Robbert Krebbers committed Sep 21, 2016 258 `````` Local Arguments ucmra_op _ !_ !_ / : simpl nomatch. `````` Robbert Krebbers committed May 23, 2016 259 `````` `````` Robbert Krebbers committed Jul 27, 2016 260 `````` Lemma list_lookup_opM l mk i : (l ⋅? mk) !! i = l !! i ⋅ (mk ≫= (!! i)). `````` Robbert Krebbers committed Jun 16, 2016 261 262 `````` Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed. `````` Robbert Krebbers committed Sep 21, 2016 263 264 265 266 267 `````` 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 268 `````` Lemma list_op_app l1 l2 l3 : `````` Robbert Krebbers committed Sep 21, 2016 269 `````` (l1 ++ l3) ⋅ l2 = (l1 ⋅ take (length l1) l2) ++ (l3 ⋅ drop (length l1) l2). `````` Robbert Krebbers committed May 23, 2016 270 271 `````` Proof. revert l2 l3. `````` Robbert Krebbers committed Sep 21, 2016 272 `````` induction l1 as [|x1 l1]=> -[|x2 l2] [|x3 l3]; f_equal/=; auto. `````` Robbert Krebbers committed May 23, 2016 273 `````` Qed. `````` Robbert Krebbers committed Sep 21, 2016 274 275 276 `````` 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 277 278 279 280 281 282 283 284 285 286 287 `````` 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 288 289 `````` Global Instance list_singletonM_ne n i : Proper (dist n ==> dist n) (@list_singletonM A i). `````` Robbert Krebbers committed May 27, 2016 290 `````` Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed. `````` Robbert Krebbers committed Jul 27, 2016 291 292 `````` Global Instance list_singletonM_proper i : Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _. `````` Robbert Krebbers committed May 23, 2016 293 `````` `````` Robbert Krebbers committed Jul 27, 2016 294 `````` Lemma elem_of_list_singletonM i z x : z ∈ {[i := x]} → z = ∅ ∨ z = x. `````` Robbert Krebbers committed May 27, 2016 295 296 297 `````` Proof. rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver. Qed. `````` Robbert Krebbers committed Jul 27, 2016 298 `````` Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x. `````` Robbert Krebbers committed May 27, 2016 299 `````` Proof. induction i; by f_equal/=. Qed. `````` Robbert Krebbers committed Jul 27, 2016 300 301 `````` Lemma list_lookup_singletonM_ne i j x : i ≠ j → {[ i := x ]} !! j = None ∨ {[ i := x ]} !! j = Some ∅. `````` Robbert Krebbers committed May 27, 2016 302 `````` Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed. `````` Robbert Krebbers committed Jul 27, 2016 303 `````` Lemma list_singletonM_validN n i x : ✓{n} {[ i := x ]} ↔ ✓{n} x. `````` Robbert Krebbers committed May 27, 2016 304 305 `````` Proof. rewrite list_lookup_validN. split. `````` Robbert Krebbers committed Jul 27, 2016 306 `````` { move=> /(_ i). by rewrite list_lookup_singletonM. } `````` Robbert Krebbers committed May 27, 2016 307 `````` intros Hx j; destruct (decide (i = j)); subst. `````` Robbert Krebbers committed Jul 27, 2016 308 309 `````` - by rewrite list_lookup_singletonM. - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done; `````` Robbert Krebbers committed May 27, 2016 310 311 `````` rewrite Hi; by try apply (ucmra_unit_validN (A:=A)). Qed. `````` Robbert Krebbers committed Jul 27, 2016 312 313 314 315 316 `````` 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 317 `````` Proof. `````` Robbert Krebbers committed Jul 27, 2016 318 `````` rewrite /singletonM /list_singletonM app_length replicate_length /=; lia. `````` Robbert Krebbers committed May 27, 2016 319 320 `````` Qed. `````` Robbert Krebbers committed Jul 27, 2016 321 `````` Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}. `````` Robbert Krebbers committed May 27, 2016 322 `````` Proof. `````` Robbert Krebbers committed Jul 27, 2016 323 `````` rewrite /singletonM /list_singletonM. `````` Robbert Krebbers committed May 28, 2016 324 `````` by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ∅). `````` Robbert Krebbers committed May 27, 2016 325 `````` Qed. `````` Robbert Krebbers committed Jul 27, 2016 326 327 328 329 330 331 332 333 334 335 336 337 338 `````` 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 339 340 `````` (* Update *) `````` Robbert Krebbers committed Sep 21, 2016 341 342 `````` 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 343 `````` Proof. `````` Robbert Krebbers committed Sep 21, 2016 344 345 346 347 `````` 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 348 `````` apply list_lookup_validN=> i. `````` Robbert Krebbers committed Sep 21, 2016 349 350 351 352 353 354 355 356 `````` 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 357 358 `````` Qed. `````` Robbert Krebbers committed Sep 21, 2016 359 360 361 362 363 364 365 366 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 `````` 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 396 `````` Lemma list_middle_update l1 l2 x y : x ~~> y → l1 ++ x :: l2 ~~> l1 ++ y :: l2. `````` Robbert Krebbers committed May 23, 2016 397 `````` Proof. `````` Robbert Krebbers committed Sep 21, 2016 398 `````` rewrite !cmra_update_updateP=> ?; eauto using list_middle_updateP with subst. `````` Robbert Krebbers committed May 23, 2016 399 400 `````` Qed. `````` Robbert Krebbers committed Jun 16, 2016 401 402 403 `````` 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 404 `````` Proof. `````` Robbert Krebbers committed Jun 16, 2016 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 `````` 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 420 `````` Qed. `````` Robbert Krebbers committed Jun 17, 2016 421 `````` Lemma list_singleton_local_update i x y ml : `````` Robbert Krebbers committed Jul 27, 2016 422 `````` x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml. `````` Robbert Krebbers committed Jun 17, 2016 423 `````` Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed. `````` Robbert Krebbers committed May 23, 2016 424 425 426 ``````End properties. (** Functor *) `````` Robbert Krebbers committed May 27, 2016 427 ``````Instance list_fmap_cmra_monotone {A B : ucmraT} (f : A → B) `````` Robbert Krebbers committed May 23, 2016 428 429 430 431 `````` `{!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 432 `````` by apply (cmra_monotone_validN (fmap f : option A → option B)). `````` Robbert Krebbers committed May 23, 2016 433 `````` - intros l1 l2. rewrite !list_lookup_included=> Hl i. rewrite !list_lookup_fmap. `````` Ralf Jung committed Jul 25, 2016 434 `````` by apply (cmra_monotone (fmap f : option A → option B)). `````` Robbert Krebbers committed May 23, 2016 435 436 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 437 438 439 ``````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 440 441 ``````|}. Next Obligation. `````` Robbert Krebbers committed May 27, 2016 442 `````` by intros F ???? n f g Hfg; apply listC_map_ne, urFunctor_ne. `````` Robbert Krebbers committed May 23, 2016 443 444 445 ``````Qed. Next Obligation. intros F A B x. rewrite /= -{2}(list_fmap_id x). `````` Robbert Krebbers committed May 27, 2016 446 `````` apply list_fmap_setoid_ext=>y. apply urFunctor_id. `````` Robbert Krebbers committed May 23, 2016 447 448 449 ``````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 450 `````` apply list_fmap_setoid_ext=>y; apply urFunctor_compose. `````` Robbert Krebbers committed May 23, 2016 451 452 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 453 454 ``````Instance listURF_contractive F : urFunctorContractive F → urFunctorContractive (listURF F). `````` Robbert Krebbers committed May 23, 2016 455 ``````Proof. `````` Robbert Krebbers committed May 27, 2016 456 `````` by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, urFunctor_contractive. `````` Robbert Krebbers committed May 23, 2016 457 ``Qed.``