gmap.v 17.7 KB
 Robbert Krebbers committed Jun 16, 2016 1 ``````From iris.algebra Require Export cmra updates. `````` Robbert Krebbers committed Mar 10, 2016 2 3 ``````From iris.prelude Require Export gmap. From iris.algebra Require Import upred. `````` Robbert Krebbers committed Dec 15, 2015 4 `````` `````` Robbert Krebbers committed Jan 14, 2016 5 6 ``````Section cofe. Context `{Countable K} {A : cofeT}. `````` Robbert Krebbers committed Feb 08, 2016 7 ``````Implicit Types m : gmap K A. `````` Robbert Krebbers committed Dec 15, 2015 8 `````` `````` Robbert Krebbers committed Mar 29, 2016 9 ``````Instance gmap_dist : Dist (gmap K A) := λ n m1 m2, `````` Ralf Jung committed Feb 10, 2016 10 `````` ∀ i, m1 !! i ≡{n}≡ m2 !! i. `````` Robbert Krebbers committed Mar 29, 2016 11 ``````Program Definition gmap_chain (c : chain (gmap K A)) `````` Robbert Krebbers committed Dec 15, 2015 12 `````` (k : K) : chain (option A) := {| chain_car n := c n !! k |}. `````` Robbert Krebbers committed Jan 14, 2016 13 ``````Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed. `````` Robbert Krebbers committed Mar 29, 2016 14 15 16 ``````Instance gmap_compl : Compl (gmap K A) := λ c, map_imap (λ i _, compl (gmap_chain c i)) (c 0). Definition gmap_cofe_mixin : CofeMixin (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 17 18 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 19 `````` - intros m1 m2; split. `````` Robbert Krebbers committed Dec 15, 2015 20 21 `````` + by intros Hm n k; apply equiv_dist. + intros Hm k; apply equiv_dist; intros n; apply Hm. `````` Robbert Krebbers committed Feb 17, 2016 22 `````` - intros n; split. `````` Robbert Krebbers committed Dec 15, 2015 23 24 `````` + by intros m k. + by intros m1 m2 ? k. `````` Ralf Jung committed Feb 20, 2016 25 `````` + by intros m1 m2 m3 ?? k; trans (m2 !! k). `````` Robbert Krebbers committed Feb 17, 2016 26 `````` - by intros n m1 m2 ? k; apply dist_S. `````` Robbert Krebbers committed Mar 29, 2016 27 `````` - intros n c k; rewrite /compl /gmap_compl lookup_imap. `````` Ralf Jung committed Feb 29, 2016 28 `````` feed inversion (λ H, chain_cauchy c 0 n H k); simpl; auto with lia. `````` Robbert Krebbers committed Feb 10, 2016 29 `````` by rewrite conv_compl /=; apply reflexive_eq. `````` Robbert Krebbers committed Dec 15, 2015 30 ``````Qed. `````` Robbert Krebbers committed May 25, 2016 31 ``````Canonical Structure gmapC : cofeT := CofeT (gmap K A) gmap_cofe_mixin. `````` Robbert Krebbers committed Mar 29, 2016 32 ``````Global Instance gmap_discrete : Discrete A → Discrete gmapC. `````` Robbert Krebbers committed Feb 24, 2016 33 ``````Proof. intros ? m m' ? i. by apply (timeless _). Qed. `````` Robbert Krebbers committed Feb 13, 2016 34 ``````(* why doesn't this go automatic? *) `````` Robbert Krebbers committed Mar 29, 2016 35 ``````Global Instance gmapC_leibniz: LeibnizEquiv A → LeibnizEquiv gmapC. `````` Robbert Krebbers committed Feb 13, 2016 36 37 ``````Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed. `````` Robbert Krebbers committed Jan 14, 2016 38 ``````Global Instance lookup_ne n k : `````` Robbert Krebbers committed Dec 16, 2015 39 `````` Proper (dist n ==> dist n) (lookup k : gmap K A → option A). `````` Robbert Krebbers committed Dec 15, 2015 40 ``````Proof. by intros m1 m2. Qed. `````` Robbert Krebbers committed Jan 16, 2016 41 42 ``````Global Instance lookup_proper k : Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _. `````` Robbert Krebbers committed Feb 11, 2016 43 44 45 46 ``````Global Instance alter_ne f k n : Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter f k). Proof. intros ? m m' Hm k'. `````` Robbert Krebbers committed Feb 17, 2016 47 `````` by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k'). `````` Robbert Krebbers committed Feb 11, 2016 48 ``````Qed. `````` Robbert Krebbers committed Feb 08, 2016 49 ``````Global Instance insert_ne i n : `````` Robbert Krebbers committed Dec 16, 2015 50 `````` Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i). `````` Robbert Krebbers committed Dec 15, 2015 51 ``````Proof. `````` Robbert Krebbers committed Feb 17, 2016 52 `````` intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq; `````` Robbert Krebbers committed Dec 15, 2015 53 54 `````` [by constructor|by apply lookup_ne]. Qed. `````` Robbert Krebbers committed Feb 08, 2016 55 ``````Global Instance singleton_ne i n : `````` Robbert Krebbers committed Dec 21, 2015 56 57 `````` Proper (dist n ==> dist n) (singletonM i : A → gmap K A). Proof. by intros ???; apply insert_ne. Qed. `````` Robbert Krebbers committed Feb 08, 2016 58 ``````Global Instance delete_ne i n : `````` Robbert Krebbers committed Dec 16, 2015 59 `````` Proper (dist n ==> dist n) (delete (M:=gmap K A) i). `````` Robbert Krebbers committed Dec 15, 2015 60 ``````Proof. `````` Robbert Krebbers committed Feb 17, 2016 61 `````` intros m m' ? j; destruct (decide (i = j)); simplify_map_eq; `````` Robbert Krebbers committed Dec 15, 2015 62 63 `````` [by constructor|by apply lookup_ne]. Qed. `````` Robbert Krebbers committed Feb 08, 2016 64 `````` `````` Robbert Krebbers committed Mar 29, 2016 65 ``````Instance gmap_empty_timeless : Timeless (∅ : gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 66 67 68 69 ``````Proof. intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *. inversion_clear Hm; constructor. Qed. `````` Robbert Krebbers committed Mar 29, 2016 70 ``````Global Instance gmap_lookup_timeless m i : Timeless m → Timeless (m !! i). `````` Robbert Krebbers committed Dec 15, 2015 71 ``````Proof. `````` Ralf Jung committed Feb 18, 2016 72 `````` intros ? [x|] Hx; [|by symmetry; apply: timeless]. `````` Robbert Krebbers committed Feb 10, 2016 73 `````` assert (m ≡{0}≡ <[i:=x]> m) `````` Robbert Krebbers committed Jan 13, 2016 74 75 `````` by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id). by rewrite (timeless m (<[i:=x]>m)) // lookup_insert. `````` Robbert Krebbers committed Dec 15, 2015 76 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 77 ``````Global Instance gmap_insert_timeless m i x : `````` Robbert Krebbers committed Dec 15, 2015 78 79 `````` Timeless x → Timeless m → Timeless (<[i:=x]>m). Proof. `````` Robbert Krebbers committed Feb 17, 2016 80 `````` intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq. `````` Ralf Jung committed Feb 18, 2016 81 82 `````` { by apply: timeless; rewrite -Hm lookup_insert. } by apply: timeless; rewrite -Hm lookup_insert_ne. `````` Robbert Krebbers committed Dec 15, 2015 83 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 84 ``````Global Instance gmap_singleton_timeless i x : `````` Robbert Krebbers committed Feb 17, 2016 85 `````` Timeless x → Timeless ({[ i := x ]} : gmap K A) := _. `````` Robbert Krebbers committed Jan 14, 2016 86 ``````End cofe. `````` Robbert Krebbers committed Feb 08, 2016 87 `````` `````` Robbert Krebbers committed Mar 29, 2016 88 ``````Arguments gmapC _ {_ _} _. `````` Robbert Krebbers committed Dec 15, 2015 89 90 `````` (* CMRA *) `````` Robbert Krebbers committed Jan 14, 2016 91 92 ``````Section cmra. Context `{Countable K} {A : cmraT}. `````` Robbert Krebbers committed Feb 13, 2016 93 ``````Implicit Types m : gmap K A. `````` Robbert Krebbers committed Jan 14, 2016 94 `````` `````` Robbert Krebbers committed Mar 29, 2016 95 ``````Instance gmap_op : Op (gmap K A) := merge op. `````` Robbert Krebbers committed May 28, 2016 96 ``````Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m). `````` Robbert Krebbers committed Mar 29, 2016 97 98 ``````Instance gmap_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i). Instance gmap_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i). `````` Robbert Krebbers committed Feb 08, 2016 99 `````` `````` Robbert Krebbers committed Jan 14, 2016 100 ``````Lemma lookup_op m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i. `````` Robbert Krebbers committed Dec 15, 2015 101 ``````Proof. by apply lookup_merge. Qed. `````` Ralf Jung committed Mar 08, 2016 102 ``````Lemma lookup_core m i : core m !! i = core (m !! i). `````` Robbert Krebbers committed May 28, 2016 103 ``````Proof. by apply lookup_omap. Qed. `````` Robbert Krebbers committed Feb 08, 2016 104 `````` `````` Robbert Krebbers committed May 23, 2016 105 ``````Lemma lookup_included (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i. `````` Robbert Krebbers committed Dec 15, 2015 106 ``````Proof. `````` Robbert Krebbers committed Mar 11, 2016 107 108 109 110 111 `````` split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|]. revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm. { exists m2. by rewrite left_id. } destruct (IH (delete i m2)) as [m2' Hm2']. { intros j. move: (Hm j); destruct (decide (i = j)) as [->|]. `````` Robbert Krebbers committed May 27, 2016 112 `````` - intros _. rewrite Hi. apply: ucmra_unit_least. `````` Robbert Krebbers committed Mar 11, 2016 113 114 115 116 117 118 `````` - rewrite lookup_insert_ne // lookup_delete_ne //. } destruct (Hm i) as [my Hi']; simplify_map_eq. exists (partial_alter (λ _, my) i m2')=>j; destruct (decide (i = j)) as [->|]. - by rewrite Hi' lookup_op lookup_insert lookup_partial_alter. - move: (Hm2' j). by rewrite !lookup_op lookup_delete_ne // lookup_insert_ne // lookup_partial_alter_ne. `````` Robbert Krebbers committed Dec 15, 2015 119 ``````Qed. `````` Robbert Krebbers committed Feb 08, 2016 120 `````` `````` Robbert Krebbers committed May 27, 2016 121 ``````Lemma gmap_cmra_mixin : CMRAMixin (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 122 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 123 124 125 126 127 `````` apply cmra_total_mixin. - eauto. - intros n m1 m2 m3 Hm i; by rewrite !lookup_op (Hm i). - intros n m1 m2 Hm i; by rewrite !lookup_core (Hm i). - intros n m1 m2 Hm ? i; by rewrite -(Hm i). `````` Robbert Krebbers committed Feb 24, 2016 128 129 130 `````` - intros m; split. + by intros ? n i; apply cmra_valid_validN. + intros Hm i; apply cmra_valid_validN=> n; apply Hm. `````` Robbert Krebbers committed Feb 17, 2016 131 132 133 `````` - intros n m Hm i; apply cmra_validN_S, Hm. - by intros m1 m2 m3 i; rewrite !lookup_op assoc. - by intros m1 m2 i; rewrite !lookup_op comm. `````` Robbert Krebbers committed May 28, 2016 134 135 136 137 `````` - intros m i. by rewrite lookup_op lookup_core cmra_core_l. - intros m i. by rewrite !lookup_core cmra_core_idemp. - intros m1 m2; rewrite !lookup_included=> Hm i. rewrite !lookup_core. by apply cmra_core_preserving. `````` Robbert Krebbers committed Feb 17, 2016 138 `````` - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i). `````` Robbert Krebbers committed Jan 13, 2016 139 `````` by rewrite -lookup_op. `````` Robbert Krebbers committed Feb 24, 2016 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 `````` - intros n m m1 m2 Hm Hm12. assert (∀ i, m !! i ≡{n}≡ m1 !! i ⋅ m2 !! i) as Hm12' by (by intros i; rewrite -lookup_op). set (f i := cmra_extend n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)). set (f_proj i := proj1_sig (f i)). exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m); repeat split; intros i; rewrite /= ?lookup_op !lookup_imap. + destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor]. rewrite -Hx; apply (proj2_sig (f i)). + destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|]. pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. by symmetry; apply option_op_positive_dist_l with (m2 !! i). + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|]. pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. by symmetry; apply option_op_positive_dist_r with (m1 !! i). `````` Robbert Krebbers committed Dec 15, 2015 155 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 156 ``````Canonical Structure gmapR := `````` Robbert Krebbers committed May 25, 2016 157 `````` CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin. `````` Robbert Krebbers committed May 27, 2016 158 159 160 161 162 `````` Global Instance gmap_cmra_discrete : CMRADiscrete A → CMRADiscrete gmapR. Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed. Lemma gmap_ucmra_mixin : UCMRAMixin (gmap K A). `````` Robbert Krebbers committed Feb 01, 2016 163 164 ``````Proof. split. `````` Robbert Krebbers committed Feb 24, 2016 165 `````` - by intros i; rewrite lookup_empty. `````` Robbert Krebbers committed Feb 17, 2016 166 `````` - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _). `````` Robbert Krebbers committed Mar 29, 2016 167 `````` - apply gmap_empty_timeless. `````` Robbert Krebbers committed May 28, 2016 168 `````` - constructor=> i. by rewrite lookup_omap lookup_empty. `````` Robbert Krebbers committed Feb 01, 2016 169 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 170 171 ``````Canonical Structure gmapUR := UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin. `````` Robbert Krebbers committed Feb 13, 2016 172 173 `````` (** Internalized properties *) `````` Robbert Krebbers committed May 31, 2016 174 ``````Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M). `````` Robbert Krebbers committed Feb 25, 2016 175 ``````Proof. by uPred.unseal. Qed. `````` Robbert Krebbers committed May 31, 2016 176 ``````Lemma gmap_validI {M} m : ✓ m ⊣⊢ (∀ i, ✓ (m !! i) : uPred M). `````` Robbert Krebbers committed Feb 25, 2016 177 ``````Proof. by uPred.unseal. Qed. `````` Robbert Krebbers committed Jan 14, 2016 178 ``````End cmra. `````` Robbert Krebbers committed Feb 08, 2016 179 `````` `````` Robbert Krebbers committed Mar 29, 2016 180 ``````Arguments gmapR _ {_ _} _. `````` Robbert Krebbers committed May 27, 2016 181 ``````Arguments gmapUR _ {_ _} _. `````` Robbert Krebbers committed Jan 14, 2016 182 183 `````` Section properties. `````` Robbert Krebbers committed Feb 08, 2016 184 ``````Context `{Countable K} {A : cmraT}. `````` Robbert Krebbers committed Jan 16, 2016 185 ``````Implicit Types m : gmap K A. `````` Robbert Krebbers committed Feb 08, 2016 186 187 ``````Implicit Types i : K. Implicit Types a : A. `````` Robbert Krebbers committed Jan 14, 2016 188 `````` `````` Robbert Krebbers committed May 23, 2016 189 ``````Lemma lookup_validN_Some n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x. `````` Robbert Krebbers committed Jan 16, 2016 190 ``````Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed. `````` Robbert Krebbers committed May 23, 2016 191 ``````Lemma lookup_valid_Some m i x : ✓ m → m !! i ≡ Some x → ✓ x. `````` Robbert Krebbers committed Feb 24, 2016 192 ``````Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed. `````` Robbert Krebbers committed Mar 29, 2016 193 ``````Lemma insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m. `````` Robbert Krebbers committed Feb 17, 2016 194 ``````Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed. `````` Robbert Krebbers committed Mar 29, 2016 195 ``````Lemma insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m. `````` Robbert Krebbers committed Feb 24, 2016 196 ``````Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed. `````` Robbert Krebbers committed Mar 29, 2016 197 ``````Lemma singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x. `````` Robbert Krebbers committed Feb 08, 2016 198 ``````Proof. `````` Robbert Krebbers committed May 27, 2016 199 `````` split; [|by intros; apply insert_validN, ucmra_unit_validN]. `````` Robbert Krebbers committed Feb 17, 2016 200 `````` by move=>/(_ i); simplify_map_eq. `````` Robbert Krebbers committed Feb 08, 2016 201 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 202 203 ``````Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x. Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed. `````` Ralf Jung committed Feb 13, 2016 204 `````` `````` Robbert Krebbers committed Mar 29, 2016 205 ``````Lemma insert_singleton_opN n m i x : `````` Robbert Krebbers committed May 28, 2016 206 `````` m !! i = None → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m. `````` Robbert Krebbers committed Feb 09, 2016 207 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 208 209 210 `````` intros Hi j; destruct (decide (i = j)) as [->|]. - by rewrite lookup_op lookup_insert lookup_singleton Hi right_id. - by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id. `````` Robbert Krebbers committed Feb 09, 2016 211 ``````Qed. `````` Robbert Krebbers committed May 28, 2016 212 ``````Lemma insert_singleton_op m i x : m !! i = None → <[i:=x]> m ≡ {[ i := x ]} ⋅ m. `````` Robbert Krebbers committed Mar 29, 2016 213 ``````Proof. rewrite !equiv_dist; naive_solver eauto using insert_singleton_opN. Qed. `````` Robbert Krebbers committed Feb 09, 2016 214 `````` `````` Robbert Krebbers committed May 28, 2016 215 216 217 218 219 220 221 222 ``````Lemma core_singleton (i : K) (x : A) cx : pcore x = Some cx → core ({[ i := x ]} : gmap K A) = {[ i := cx ]}. Proof. apply omap_singleton. Qed. Lemma core_singleton' (i : K) (x : A) cx : pcore x ≡ Some cx → core ({[ i := x ]} : gmap K A) ≡ {[ i := cx ]}. Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx'). Qed. `````` Robbert Krebbers committed Mar 29, 2016 223 ``````Lemma op_singleton (i : K) (x y : A) : `````` Robbert Krebbers committed Feb 17, 2016 224 `````` {[ i := x ]} ⋅ {[ i := y ]} = ({[ i := x ⋅ y ]} : gmap K A). `````` Robbert Krebbers committed Jan 14, 2016 225 ``````Proof. by apply (merge_singleton _ _ _ x y). Qed. `````` Ralf Jung committed Feb 08, 2016 226 `````` `````` Robbert Krebbers committed Mar 29, 2016 227 ``````Global Instance gmap_persistent m : (∀ x : A, Persistent x) → Persistent m. `````` Robbert Krebbers committed May 28, 2016 228 229 230 231 ``````Proof. intros; apply persistent_total=> i. rewrite lookup_core. apply (persistent_core _). Qed. `````` Robbert Krebbers committed Mar 29, 2016 232 ``````Global Instance gmap_singleton_persistent i (x : A) : `````` Robbert Krebbers committed Mar 15, 2016 233 `````` Persistent x → Persistent {[ i := x ]}. `````` Robbert Krebbers committed May 28, 2016 234 ``````Proof. intros. by apply persistent_total, core_singleton'. Qed. `````` Robbert Krebbers committed Mar 15, 2016 235 `````` `````` Robbert Krebbers committed Jan 16, 2016 236 ``````Lemma singleton_includedN n m i x : `````` Robbert Krebbers committed May 28, 2016 237 `````` {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ (x ≼{n} y ∨ x ≡{n}≡ y). `````` Robbert Krebbers committed Jan 16, 2016 238 239 ``````Proof. split. `````` Robbert Krebbers committed Mar 11, 2016 240 241 242 `````` - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton. case (m' !! i)=> [y|]=> Hm. + exists (x ⋅ y); eauto using cmra_includedN_l. `````` Robbert Krebbers committed May 28, 2016 243 244 245 246 247 248 249 250 `````` + exists x; eauto. - intros (y&Hi&[[z ?]| ->]). + exists (<[i:=z]>m)=> j; destruct (decide (i = j)) as [->|]. * rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor. * by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id. + exists (delete i m)=> j; destruct (decide (i = j)) as [->|]. * by rewrite Hi lookup_op lookup_singleton lookup_delete. * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id. `````` Robbert Krebbers committed Jan 16, 2016 251 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 252 ``````Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2. `````` Robbert Krebbers committed Dec 16, 2015 253 ``````Proof. `````` Robbert Krebbers committed Jan 13, 2016 254 `````` apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom. `````` Robbert Krebbers committed Dec 16, 2015 255 256 257 `````` unfold is_Some; setoid_rewrite lookup_op. destruct (m1 !! i), (m2 !! i); naive_solver. Qed. `````` Robbert Krebbers committed Jan 16, 2016 258 `````` `````` Robbert Krebbers committed Mar 29, 2016 259 ``````Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x : `````` Ralf Jung committed Feb 03, 2016 260 `````` x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 261 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 262 263 `````` intros Hx%option_updateP' HP; apply cmra_total_updateP=> n mf Hm. destruct (Hx n (Some (mf !! i))) as ([y|]&?&?); try done. `````` Robbert Krebbers committed Feb 17, 2016 264 `````` { by generalize (Hm i); rewrite lookup_op; simplify_map_eq. } `````` Robbert Krebbers committed Feb 02, 2016 265 266 `````` exists (<[i:=y]> m); split; first by auto. intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm. `````` Robbert Krebbers committed Feb 17, 2016 267 `````` destruct (decide (i = j)); simplify_map_eq/=; auto. `````` Robbert Krebbers committed Feb 02, 2016 268 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 269 ``````Lemma insert_updateP' (P : A → Prop) m i x : `````` Ralf Jung committed Feb 03, 2016 270 `````` x ~~>: P → <[i:=x]>m ~~>: λ m', ∃ y, m' = <[i:=y]>m ∧ P y. `````` Robbert Krebbers committed Mar 29, 2016 271 272 273 ``````Proof. eauto using insert_updateP. Qed. Lemma insert_update m i x y : x ~~> y → <[i:=x]>m ~~> <[i:=y]>m. Proof. rewrite !cmra_update_updateP; eauto using insert_updateP with subst. Qed. `````` Robbert Krebbers committed Feb 02, 2016 274 `````` `````` Robbert Krebbers committed Mar 29, 2016 275 ``````Lemma singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x : `````` Robbert Krebbers committed Feb 17, 2016 276 `````` x ~~>: P → (∀ y, P y → Q {[ i := y ]}) → {[ i := x ]} ~~>: Q. `````` Robbert Krebbers committed Mar 29, 2016 277 278 ``````Proof. apply insert_updateP. Qed. Lemma singleton_updateP' (P : A → Prop) i x : `````` Robbert Krebbers committed Feb 17, 2016 279 `````` x ~~>: P → {[ i := x ]} ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y. `````` Robbert Krebbers committed Mar 29, 2016 280 281 282 ``````Proof. apply insert_updateP'. Qed. Lemma singleton_update i (x y : A) : x ~~> y → {[ i := x ]} ~~> {[ i := y ]}. Proof. apply insert_update. Qed. `````` Ralf Jung committed Feb 08, 2016 283 `````` `````` 284 ``````Section freshness. `````` Robbert Krebbers committed Jan 16, 2016 285 ``````Context `{Fresh K (gset K), !FreshSpec K (gset K)}. `````` Robbert Krebbers committed Jun 16, 2016 286 ``````Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x : `````` 287 `````` ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q. `````` Robbert Krebbers committed Dec 16, 2015 288 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 289 290 `````` intros ? HQ. apply cmra_total_updateP. intros n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))). `````` 291 `````` assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]]. `````` Robbert Krebbers committed Mar 29, 2016 292 `````` { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. } `````` Robbert Krebbers committed Feb 14, 2016 293 294 `````` exists (<[i:=x]>m); split. { by apply HQ; last done; apply not_elem_of_dom. } `````` Robbert Krebbers committed May 28, 2016 295 `````` rewrite insert_singleton_opN; last by apply not_elem_of_dom. `````` Robbert Krebbers committed Mar 29, 2016 296 `````` rewrite -assoc -insert_singleton_opN; `````` Robbert Krebbers committed May 28, 2016 297 `````` last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union. `````` Robbert Krebbers committed Mar 29, 2016 298 `````` by apply insert_validN; [apply cmra_valid_validN|]. `````` Robbert Krebbers committed Dec 16, 2015 299 ``````Qed. `````` Robbert Krebbers committed Jun 16, 2016 300 ``````Lemma alloc_updateP (Q : gmap K A → Prop) m x : `````` 301 `````` ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q. `````` Robbert Krebbers committed Jun 16, 2016 302 303 ``````Proof. move=>??. eapply alloc_updateP_strong with (I:=∅); by eauto. Qed. Lemma alloc_updateP_strong' m x (I : gset K) : `````` 304 `````` ✓ x → m ~~>: λ m', ∃ i, i ∉ I ∧ m' = <[i:=x]>m ∧ m !! i = None. `````` Robbert Krebbers committed Jun 16, 2016 305 306 ``````Proof. eauto using alloc_updateP_strong. Qed. Lemma alloc_updateP' m x : `````` Ralf Jung committed Feb 03, 2016 307 `````` ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None. `````` Robbert Krebbers committed Jun 16, 2016 308 ``````Proof. eauto using alloc_updateP. Qed. `````` Robbert Krebbers committed May 27, 2016 309 310 311 312 313 `````` Lemma singleton_updateP_unit (P : A → Prop) (Q : gmap K A → Prop) u i : ✓ u → LeftId (≡) u (⋅) → u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q. Proof. `````` Robbert Krebbers committed May 28, 2016 314 315 `````` intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg. destruct (Hx n (gf !! i)) as (y&?&Hy). `````` Robbert Krebbers committed May 27, 2016 316 `````` { move:(Hg i). rewrite !left_id. `````` Robbert Krebbers committed Jun 06, 2016 317 `````` case: (gf !! i)=>[x|]; rewrite /= ?left_id //. `````` Robbert Krebbers committed May 28, 2016 318 `````` intros; by apply cmra_valid_validN. } `````` Robbert Krebbers committed May 27, 2016 319 320 321 `````` exists {[ i := y ]}; split; first by auto. intros i'; destruct (decide (i' = i)) as [->|]. - rewrite lookup_op lookup_singleton. `````` Robbert Krebbers committed Jun 06, 2016 322 `````` move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //. `````` Robbert Krebbers committed May 27, 2016 323 324 325 326 327 328 329 330 331 332 333 `````` - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id. Qed. Lemma singleton_updateP_unit' (P: A → Prop) u i : ✓ u → LeftId (≡) u (⋅) → u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y. Proof. eauto using singleton_updateP_unit. Qed. Lemma singleton_update_unit u i (y : A) : ✓ u → LeftId (≡) u (⋅) → u ~~> y → ∅ ~~> {[ i := y ]}. Proof. rewrite !cmra_update_updateP; eauto using singleton_updateP_unit with subst. Qed. `````` 334 335 ``````End freshness. `````` Ralf Jung committed Feb 11, 2016 336 ``````(* Allocation is a local update: Just use composition with a singleton map. *) `````` Robbert Krebbers committed May 28, 2016 337 `````` `````` Robbert Krebbers committed Jun 16, 2016 338 ``````Global Instance delete_local_update : `````` Jacques-Henri Jourdan committed May 31, 2016 339 `````` LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ Exclusive x) (delete i). `````` Robbert Krebbers committed May 28, 2016 340 341 342 343 344 345 346 347 348 ``````Proof. split; first apply _. intros n m1 m2 (x&Hix&Hv) Hm j; destruct (decide (i = j)) as [<-|]. - rewrite lookup_delete !lookup_op lookup_delete. case Hiy: (m2 !! i)=> [y|]; last constructor. destruct (Hv y); apply cmra_validN_le with n; last omega. move: (Hm i). by rewrite lookup_op Hix Hiy. - by rewrite lookup_op !lookup_delete_ne // lookup_op. Qed. `````` Ralf Jung committed Feb 11, 2016 349 350 `````` (* Applying a local update at a position we own is a local update. *) `````` Robbert Krebbers committed Jun 16, 2016 351 ``````Global Instance alter_local_update `{!LocalUpdate Lv L} i : `````` Ralf Jung committed Feb 11, 2016 352 `````` LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ Lv x) (alter L i). `````` 353 ``````Proof. `````` Robbert Krebbers committed Feb 11, 2016 354 355 356 357 `````` split; first apply _. intros n m1 m2 (x&Hix&?) Hm j; destruct (decide (i = j)) as [->|]. - rewrite lookup_alter !lookup_op lookup_alter Hix /=. move: (Hm j); rewrite lookup_op Hix. `````` Ralf Jung committed Feb 11, 2016 358 `````` case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN L). `````` Robbert Krebbers committed Feb 11, 2016 359 `````` - by rewrite lookup_op !lookup_alter_ne // lookup_op. `````` 360 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 361 362 ``````End properties. `````` Robbert Krebbers committed Feb 04, 2016 363 ``````(** Functor *) `````` Robbert Krebbers committed Mar 29, 2016 364 ``````Instance gmap_fmap_ne `{Countable K} {A B : cofeT} (f : A → B) n : `````` Robbert Krebbers committed Jan 14, 2016 365 366 `````` Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (M:=gmap K) f). Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed. `````` Robbert Krebbers committed Mar 29, 2016 367 ``````Instance gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B) `````` Robbert Krebbers committed Jan 14, 2016 368 369 `````` `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B). Proof. `````` Robbert Krebbers committed Feb 26, 2016 370 `````` split; try apply _. `````` Robbert Krebbers committed Feb 26, 2016 371 `````` - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _). `````` Robbert Krebbers committed May 23, 2016 372 `````` - intros m1 m2; rewrite !lookup_included=> Hm i. `````` Robbert Krebbers committed Feb 26, 2016 373 `````` by rewrite !lookup_fmap; apply: included_preserving. `````` Robbert Krebbers committed Jan 14, 2016 374 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 375 376 377 378 ``````Definition gmapC_map `{Countable K} {A B} (f: A -n> B) : gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A → gmapC K B). Instance gmapC_map_ne `{Countable K} {A B} n : Proper (dist n ==> dist n) (@gmapC_map K _ _ A B). `````` Robbert Krebbers committed Feb 04, 2016 379 380 381 382 ``````Proof. intros f g Hf m k; rewrite /= !lookup_fmap. destruct (_ !! k) eqn:?; simpl; constructor; apply Hf. Qed. `````` Ralf Jung committed Feb 05, 2016 383 `````` `````` Robbert Krebbers committed Mar 29, 2016 384 385 386 ``````Program Definition gmapCF K `{Countable K} (F : cFunctor) : cFunctor := {| cFunctor_car A B := gmapC K (cFunctor_car F A B); cFunctor_map A1 A2 B1 B2 fg := gmapC_map (cFunctor_map F fg) `````` Ralf Jung committed Feb 05, 2016 387 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 388 ``````Next Obligation. `````` Robbert Krebbers committed Mar 29, 2016 389 `````` by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_ne. `````` Robbert Krebbers committed Mar 07, 2016 390 ``````Qed. `````` Ralf Jung committed Feb 05, 2016 391 ``````Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 392 393 `````` intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x). apply map_fmap_setoid_ext=>y ??; apply cFunctor_id. `````` Ralf Jung committed Feb 05, 2016 394 395 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 396 397 398 `````` intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose. apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose. Qed. `````` Robbert Krebbers committed Mar 29, 2016 399 400 ``````Instance gmapCF_contractive K `{Countable K} F : cFunctorContractive F → cFunctorContractive (gmapCF K F). `````` Ralf Jung committed Mar 07, 2016 401 ``````Proof. `````` Robbert Krebbers committed Mar 29, 2016 402 `````` by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive. `````` Ralf Jung committed Mar 07, 2016 403 404 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 405 406 407 ``````Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {| urFunctor_car A B := gmapUR K (rFunctor_car F A B); urFunctor_map A1 A2 B1 B2 fg := gmapC_map (rFunctor_map F fg) `````` Robbert Krebbers committed Mar 02, 2016 408 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 409 ``````Next Obligation. `````` Robbert Krebbers committed Mar 29, 2016 410 `````` by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne. `````` Robbert Krebbers committed Mar 07, 2016 411 ``````Qed. `````` Robbert Krebbers committed Mar 02, 2016 412 413 414 415 416 417 418 ``````Next Obligation. intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x). apply map_fmap_setoid_ext=>y ??; apply rFunctor_id. Qed. Next Obligation. intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose. apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose. `````` Ralf Jung committed Feb 05, 2016 419 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 420 ``````Instance gmapRF_contractive K `{Countable K} F : `````` Robbert Krebbers committed May 27, 2016 421 `````` rFunctorContractive F → urFunctorContractive (gmapURF K F). `````` Ralf Jung committed Mar 07, 2016 422 ``````Proof. `````` Robbert Krebbers committed Mar 29, 2016 423 `````` by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive. `````` Ralf Jung committed Mar 07, 2016 424 ``Qed.``