gmap.v 18.9 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 `````` - 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))|]. `````` Robbert Krebbers committed Jun 17, 2016 150 151 `````` move: (Hm12' i). rewrite Hx -!timeless_iff. rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto. `````` Robbert Krebbers committed Feb 24, 2016 152 `````` + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|]. `````` Robbert Krebbers committed Jun 17, 2016 153 154 `````` move: (Hm12' i). rewrite Hx -!timeless_iff. rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto. `````` 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 ``````Implicit Types i : K. `````` Robbert Krebbers committed Jun 16, 2016 187 188 189 190 ``````Implicit Types x y : A. Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i)). Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed. `````` Robbert Krebbers committed Jan 14, 2016 191 `````` `````` Robbert Krebbers committed May 23, 2016 192 ``````Lemma lookup_validN_Some n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x. `````` Robbert Krebbers committed Jan 16, 2016 193 ``````Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed. `````` Robbert Krebbers committed May 23, 2016 194 ``````Lemma lookup_valid_Some m i x : ✓ m → m !! i ≡ Some x → ✓ x. `````` Robbert Krebbers committed Feb 24, 2016 195 ``````Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed. `````` Robbert Krebbers committed Mar 29, 2016 196 ``````Lemma insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m. `````` Robbert Krebbers committed Feb 17, 2016 197 ``````Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed. `````` Robbert Krebbers committed Mar 29, 2016 198 ``````Lemma insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m. `````` Robbert Krebbers committed Feb 24, 2016 199 ``````Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed. `````` Robbert Krebbers committed Mar 29, 2016 200 ``````Lemma singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x. `````` Robbert Krebbers committed Feb 08, 2016 201 ``````Proof. `````` Robbert Krebbers committed May 27, 2016 202 `````` split; [|by intros; apply insert_validN, ucmra_unit_validN]. `````` Robbert Krebbers committed Feb 17, 2016 203 `````` by move=>/(_ i); simplify_map_eq. `````` Robbert Krebbers committed Feb 08, 2016 204 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 205 206 ``````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 207 `````` `````` Robbert Krebbers committed Mar 29, 2016 208 ``````Lemma insert_singleton_opN n m i x : `````` Robbert Krebbers committed May 28, 2016 209 `````` m !! i = None → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m. `````` Robbert Krebbers committed Feb 09, 2016 210 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 211 212 213 `````` 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 214 ``````Qed. `````` Robbert Krebbers committed May 28, 2016 215 ``````Lemma insert_singleton_op m i x : m !! i = None → <[i:=x]> m ≡ {[ i := x ]} ⋅ m. `````` Robbert Krebbers committed Mar 29, 2016 216 ``````Proof. rewrite !equiv_dist; naive_solver eauto using insert_singleton_opN. Qed. `````` Robbert Krebbers committed Feb 09, 2016 217 `````` `````` Robbert Krebbers committed May 28, 2016 218 219 220 221 222 223 224 225 ``````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 226 ``````Lemma op_singleton (i : K) (x y : A) : `````` Robbert Krebbers committed Feb 17, 2016 227 `````` {[ i := x ]} ⋅ {[ i := y ]} = ({[ i := x ⋅ y ]} : gmap K A). `````` Robbert Krebbers committed Jan 14, 2016 228 ``````Proof. by apply (merge_singleton _ _ _ x y). Qed. `````` Ralf Jung committed Feb 08, 2016 229 `````` `````` Robbert Krebbers committed Mar 29, 2016 230 ``````Global Instance gmap_persistent m : (∀ x : A, Persistent x) → Persistent m. `````` Robbert Krebbers committed May 28, 2016 231 232 233 234 ``````Proof. intros; apply persistent_total=> i. rewrite lookup_core. apply (persistent_core _). Qed. `````` Robbert Krebbers committed Mar 29, 2016 235 ``````Global Instance gmap_singleton_persistent i (x : A) : `````` Robbert Krebbers committed Mar 15, 2016 236 `````` Persistent x → Persistent {[ i := x ]}. `````` Robbert Krebbers committed May 28, 2016 237 ``````Proof. intros. by apply persistent_total, core_singleton'. Qed. `````` Robbert Krebbers committed Mar 15, 2016 238 `````` `````` Robbert Krebbers committed Jan 16, 2016 239 ``````Lemma singleton_includedN n m i x : `````` Robbert Krebbers committed May 28, 2016 240 `````` {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ (x ≼{n} y ∨ x ≡{n}≡ y). `````` Robbert Krebbers committed Jan 16, 2016 241 242 ``````Proof. split. `````` Robbert Krebbers committed Mar 11, 2016 243 244 245 `````` - 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 246 247 248 249 250 251 252 253 `````` + 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 254 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 255 ``````Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2. `````` Robbert Krebbers committed Dec 16, 2015 256 ``````Proof. `````` Robbert Krebbers committed Jan 13, 2016 257 `````` apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom. `````` Robbert Krebbers committed Dec 16, 2015 258 259 260 `````` unfold is_Some; setoid_rewrite lookup_op. destruct (m1 !! i), (m2 !! i); naive_solver. Qed. `````` Robbert Krebbers committed Jan 16, 2016 261 `````` `````` Robbert Krebbers committed Mar 29, 2016 262 ``````Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x : `````` Ralf Jung committed Feb 03, 2016 263 `````` x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 264 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 265 266 `````` 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 267 `````` { by generalize (Hm i); rewrite lookup_op; simplify_map_eq. } `````` Robbert Krebbers committed Feb 02, 2016 268 269 `````` exists (<[i:=y]> m); split; first by auto. intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm. `````` Robbert Krebbers committed Feb 17, 2016 270 `````` destruct (decide (i = j)); simplify_map_eq/=; auto. `````` Robbert Krebbers committed Feb 02, 2016 271 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 272 ``````Lemma insert_updateP' (P : A → Prop) m i x : `````` Ralf Jung committed Feb 03, 2016 273 `````` x ~~>: P → <[i:=x]>m ~~>: λ m', ∃ y, m' = <[i:=y]>m ∧ P y. `````` Robbert Krebbers committed Mar 29, 2016 274 275 276 ``````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 277 `````` `````` Robbert Krebbers committed Mar 29, 2016 278 ``````Lemma singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x : `````` Robbert Krebbers committed Feb 17, 2016 279 `````` x ~~>: P → (∀ y, P y → Q {[ i := y ]}) → {[ i := x ]} ~~>: Q. `````` Robbert Krebbers committed Mar 29, 2016 280 281 ``````Proof. apply insert_updateP. Qed. Lemma singleton_updateP' (P : A → Prop) i x : `````` Robbert Krebbers committed Feb 17, 2016 282 `````` x ~~>: P → {[ i := x ]} ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y. `````` Robbert Krebbers committed Mar 29, 2016 283 284 285 ``````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 286 `````` `````` Robbert Krebbers committed Jun 16, 2016 287 ``````Lemma delete_update m i : m ~~> delete i m. `````` Robbert Krebbers committed Dec 16, 2015 288 ``````Proof. `````` Robbert Krebbers committed Jun 16, 2016 289 290 291 292 `````` apply cmra_total_update=> n mf Hm j; destruct (decide (i = j)); subst. - move: (Hm j). rewrite !lookup_op lookup_delete left_id. apply cmra_validN_op_r. - move: (Hm j). by rewrite !lookup_op lookup_delete_ne. `````` Robbert Krebbers committed Dec 16, 2015 293 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 294 `````` `````` Robbert Krebbers committed Jun 16, 2016 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 ``````Section freshness. Context `{Fresh K (gset K), !FreshSpec K (gset K)}. Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x : ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q. Proof. intros ? HQ. apply cmra_total_updateP. intros n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))). assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]]. { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. } exists (<[i:=x]>m); split. { by apply HQ; last done; apply not_elem_of_dom. } rewrite insert_singleton_opN; last by apply not_elem_of_dom. rewrite -assoc -insert_singleton_opN; last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union. by apply insert_validN; [apply cmra_valid_validN|]. Qed. Lemma alloc_updateP (Q : gmap K A → Prop) m x : ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q. Proof. move=>??. eapply alloc_updateP_strong with (I:=∅); by eauto. Qed. Lemma alloc_updateP_strong' m x (I : gset K) : ✓ x → m ~~>: λ m', ∃ i, i ∉ I ∧ m' = <[i:=x]>m ∧ m !! i = None. Proof. eauto using alloc_updateP_strong. Qed. Lemma alloc_updateP' m x : ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None. Proof. eauto using alloc_updateP. Qed. `````` Robbert Krebbers committed Jun 17, 2016 321 `````` Lemma alloc_unit_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) u i : `````` Robbert Krebbers committed Jun 16, 2016 322 323 324 325 326 327 328 329 330 331 332 333 334 335 `````` ✓ u → LeftId (≡) u (⋅) → u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q. Proof. intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg. destruct (Hx n (gf !! i)) as (y&?&Hy). { move:(Hg i). rewrite !left_id. case: (gf !! i)=>[x|]; rewrite /= ?left_id //. intros; by apply cmra_valid_validN. } exists {[ i := y ]}; split; first by auto. intros i'; destruct (decide (i' = i)) as [->|]. - rewrite lookup_op lookup_singleton. move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //. - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id. Qed. `````` Robbert Krebbers committed Jun 17, 2016 336 `````` Lemma alloc_unit_singleton_updateP' (P: A → Prop) u i : `````` Robbert Krebbers committed Jun 16, 2016 337 338 `````` ✓ u → LeftId (≡) u (⋅) → u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y. `````` Robbert Krebbers committed Jun 17, 2016 339 340 `````` Proof. eauto using alloc_unit_singleton_updateP. Qed. Lemma alloc_unit_singleton_update u i (y : A) : `````` Robbert Krebbers committed Jun 16, 2016 341 342 `````` ✓ u → LeftId (≡) u (⋅) → u ~~> y → ∅ ~~> {[ i := y ]}. Proof. `````` Robbert Krebbers committed Jun 17, 2016 343 344 `````` rewrite !cmra_update_updateP; eauto using alloc_unit_singleton_updateP with subst. `````` Robbert Krebbers committed Jun 16, 2016 345 346 347 348 349 `````` Qed. End freshness. Lemma insert_local_update m i x y mf : x ~l~> y @ mf ≫= (!! i) → <[i:=x]>m ~l~> <[i:=y]>m @ mf. `````` Robbert Krebbers committed May 27, 2016 350 ``````Proof. `````` Robbert Krebbers committed Jun 16, 2016 351 352 353 354 355 356 357 358 `````` intros [Hxy Hxy']; split. - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst. + rewrite !lookup_opM !lookup_insert !Some_op_opM. apply Hxy. + by rewrite !lookup_opM !lookup_insert_ne. - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j). destruct (decide (i = j)); subst. + rewrite !lookup_opM !lookup_insert !Some_op_opM !inj_iff. apply Hxy'. + by rewrite !lookup_opM !lookup_insert_ne. `````` Robbert Krebbers committed May 27, 2016 359 ``````Qed. `````` 360 `````` `````` Robbert Krebbers committed Jun 16, 2016 361 362 363 ``````Lemma singleton_local_update i x y mf : x ~l~> y @ mf ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ mf. Proof. apply insert_local_update. Qed. `````` Robbert Krebbers committed May 28, 2016 364 `````` `````` Robbert Krebbers committed Jun 17, 2016 365 366 367 368 369 370 371 372 373 374 375 376 ``````Lemma alloc_singleton_local_update m i x mf : (m ⋅? mf) !! i = None → ✓ x → m ~l~> <[i:=x]> m @ mf. Proof. rewrite lookup_opM op_None=> -[Hi Hif] ?. rewrite insert_singleton_op // comm. apply alloc_local_update. intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst. - intros _; rewrite !lookup_opM lookup_op !lookup_singleton Hif Hi. by apply cmra_valid_validN. - by rewrite !lookup_opM lookup_op !lookup_singleton_ne // right_id. Qed. Lemma alloc_unit_singleton_local_update i x mf : `````` Robbert Krebbers committed Jun 16, 2016 377 `````` mf ≫= (!! i) = None → ✓ x → ∅ ~l~> {[ i := x ]} @ mf. `````` Robbert Krebbers committed May 28, 2016 378 ``````Proof. `````` Robbert Krebbers committed Jun 17, 2016 379 `````` intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi. `````` Robbert Krebbers committed May 28, 2016 380 ``````Qed. `````` Ralf Jung committed Feb 11, 2016 381 `````` `````` Robbert Krebbers committed Jun 16, 2016 382 383 ``````Lemma delete_local_update m i x `{!Exclusive x} mf : m !! i = Some x → m ~l~> delete i m @ mf. `````` 384 ``````Proof. `````` Robbert Krebbers committed Jun 16, 2016 385 386 387 388 389 390 391 `````` intros Hx; split; [intros n; apply delete_update|]. intros n mf' Hm Hm' j. move: (Hm j) (Hm' j). destruct (decide (i = j)); subst. + rewrite !lookup_opM !lookup_delete Hx=> ? Hj. rewrite (exclusiveN_Some_l n x (mf ≫= lookup j)) //. by rewrite (exclusiveN_Some_l n x (mf' ≫= lookup j)) -?Hj. + by rewrite !lookup_opM !lookup_delete_ne. `````` 392 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 393 394 ``````End properties. `````` Robbert Krebbers committed Feb 04, 2016 395 ``````(** Functor *) `````` Robbert Krebbers committed Mar 29, 2016 396 ``````Instance gmap_fmap_ne `{Countable K} {A B : cofeT} (f : A → B) n : `````` Robbert Krebbers committed Jan 14, 2016 397 398 `````` 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 399 ``````Instance gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B) `````` Robbert Krebbers committed Jan 14, 2016 400 401 `````` `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B). Proof. `````` Robbert Krebbers committed Feb 26, 2016 402 `````` split; try apply _. `````` Robbert Krebbers committed Feb 26, 2016 403 `````` - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _). `````` Robbert Krebbers committed May 23, 2016 404 `````` - intros m1 m2; rewrite !lookup_included=> Hm i. `````` Robbert Krebbers committed Feb 26, 2016 405 `````` by rewrite !lookup_fmap; apply: included_preserving. `````` Robbert Krebbers committed Jan 14, 2016 406 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 407 408 409 410 ``````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 411 412 413 414 ``````Proof. intros f g Hf m k; rewrite /= !lookup_fmap. destruct (_ !! k) eqn:?; simpl; constructor; apply Hf. Qed. `````` Ralf Jung committed Feb 05, 2016 415 `````` `````` Robbert Krebbers committed Mar 29, 2016 416 417 418 ``````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 419 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 420 ``````Next Obligation. `````` Robbert Krebbers committed Mar 29, 2016 421 `````` by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_ne. `````` Robbert Krebbers committed Mar 07, 2016 422 ``````Qed. `````` Ralf Jung committed Feb 05, 2016 423 ``````Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 424 425 `````` 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 426 427 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Mar 02, 2016 428 429 430 `````` 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 431 432 ``````Instance gmapCF_contractive K `{Countable K} F : cFunctorContractive F → cFunctorContractive (gmapCF K F). `````` Ralf Jung committed Mar 07, 2016 433 ``````Proof. `````` Robbert Krebbers committed Mar 29, 2016 434 `````` by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive. `````` Ralf Jung committed Mar 07, 2016 435 436 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 437 438 439 ``````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 440 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 441 ``````Next Obligation. `````` Robbert Krebbers committed Mar 29, 2016 442 `````` by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne. `````` Robbert Krebbers committed Mar 07, 2016 443 ``````Qed. `````` Robbert Krebbers committed Mar 02, 2016 444 445 446 447 448 449 450 ``````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 451 ``````Qed. `````` Robbert Krebbers committed Mar 29, 2016 452 ``````Instance gmapRF_contractive K `{Countable K} F : `````` Robbert Krebbers committed May 27, 2016 453 `````` rFunctorContractive F → urFunctorContractive (gmapURF K F). `````` Ralf Jung committed Mar 07, 2016 454 ``````Proof. `````` Robbert Krebbers committed Mar 29, 2016 455 `````` by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive. `````` Ralf Jung committed Mar 07, 2016 456 ``Qed.``