fin_maps.v 13.7 KB
 Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export algebra.cmra prelude.gmap algebra.option. `````` Ralf Jung committed Feb 05, 2016 2 ``````Require Import algebra.functor. `````` Robbert Krebbers committed Dec 15, 2015 3 `````` `````` Robbert Krebbers committed Jan 14, 2016 4 5 ``````Section cofe. Context `{Countable K} {A : cofeT}. `````` Robbert Krebbers committed Feb 08, 2016 6 ``````Implicit Types m : gmap K A. `````` Robbert Krebbers committed Dec 15, 2015 7 `````` `````` Robbert Krebbers committed Jan 14, 2016 8 ``````Instance map_dist : Dist (gmap K A) := λ n m1 m2, `````` Ralf Jung committed Feb 10, 2016 9 `````` ∀ i, m1 !! i ≡{n}≡ m2 !! i. `````` Robbert Krebbers committed Jan 14, 2016 10 ``````Program Definition map_chain (c : chain (gmap K A)) `````` Robbert Krebbers committed Dec 15, 2015 11 `````` (k : K) : chain (option A) := {| chain_car n := c n !! k |}. `````` Robbert Krebbers committed Jan 14, 2016 12 13 ``````Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed. Instance map_compl : Compl (gmap K A) := λ c, `````` Robbert Krebbers committed Dec 15, 2015 14 `````` map_imap (λ i _, compl (map_chain c i)) (c 1). `````` Robbert Krebbers committed Jan 14, 2016 15 ``````Definition map_cofe_mixin : CofeMixin (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 16 17 18 19 20 21 22 23 24 25 ``````Proof. split. * intros m1 m2; split. + by intros Hm n k; apply equiv_dist. + intros Hm k; apply equiv_dist; intros n; apply Hm. * intros n; split. + by intros m k. + by intros m1 m2 ? k. + by intros m1 m2 m3 ?? k; transitivity (m2 !! k). * by intros n m1 m2 ? k; apply dist_S. `````` Robbert Krebbers committed Feb 10, 2016 26 27 28 `````` * intros c n k; rewrite /compl /map_compl lookup_imap. feed inversion (λ H, chain_cauchy c 0 (S n) H k); simpl; auto with lia. by rewrite conv_compl /=; apply reflexive_eq. `````` Robbert Krebbers committed Dec 15, 2015 29 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 30 31 32 ``````Canonical Structure mapC : cofeT := CofeT map_cofe_mixin. Global Instance lookup_ne n k : `````` Robbert Krebbers committed Dec 16, 2015 33 `````` Proper (dist n ==> dist n) (lookup k : gmap K A → option A). `````` Robbert Krebbers committed Dec 15, 2015 34 ``````Proof. by intros m1 m2. Qed. `````` Robbert Krebbers committed Jan 16, 2016 35 36 ``````Global Instance lookup_proper k : Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _. `````` Robbert Krebbers committed Feb 11, 2016 37 38 39 40 41 42 ``````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'. by destruct (decide (k = k')); simplify_map_equality; rewrite (Hm k'). Qed. `````` Robbert Krebbers committed Feb 08, 2016 43 ``````Global Instance insert_ne i n : `````` Robbert Krebbers committed Dec 16, 2015 44 `````` Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i). `````` Robbert Krebbers committed Dec 15, 2015 45 46 47 48 ``````Proof. intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality; [by constructor|by apply lookup_ne]. Qed. `````` Robbert Krebbers committed Feb 08, 2016 49 ``````Global Instance singleton_ne i n : `````` Robbert Krebbers committed Dec 21, 2015 50 51 `````` Proper (dist n ==> dist n) (singletonM i : A → gmap K A). Proof. by intros ???; apply insert_ne. Qed. `````` Robbert Krebbers committed Feb 08, 2016 52 ``````Global Instance delete_ne i n : `````` Robbert Krebbers committed Dec 16, 2015 53 `````` Proper (dist n ==> dist n) (delete (M:=gmap K A) i). `````` Robbert Krebbers committed Dec 15, 2015 54 55 56 57 ``````Proof. intros m m' ? j; destruct (decide (i = j)); simplify_map_equality; [by constructor|by apply lookup_ne]. Qed. `````` Robbert Krebbers committed Feb 08, 2016 58 `````` `````` Robbert Krebbers committed Feb 01, 2016 59 ``````Instance map_empty_timeless : Timeless (∅ : gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 60 61 62 63 ``````Proof. intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *. inversion_clear Hm; constructor. Qed. `````` Robbert Krebbers committed Feb 08, 2016 64 ``````Global Instance map_lookup_timeless m i : Timeless m → Timeless (m !! i). `````` Robbert Krebbers committed Dec 15, 2015 65 66 ``````Proof. intros ? [x|] Hx; [|by symmetry; apply (timeless _)]. `````` Robbert Krebbers committed Feb 10, 2016 67 `````` assert (m ≡{0}≡ <[i:=x]> m) `````` Robbert Krebbers committed Jan 13, 2016 68 69 `````` 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 70 ``````Qed. `````` Robbert Krebbers committed Feb 08, 2016 71 ``````Global Instance map_insert_timeless m i x : `````` Robbert Krebbers committed Dec 15, 2015 72 73 74 `````` Timeless x → Timeless m → Timeless (<[i:=x]>m). Proof. intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality. `````` Robbert Krebbers committed Jan 13, 2016 75 76 `````` { by apply (timeless _); rewrite -Hm lookup_insert. } by apply (timeless _); rewrite -Hm lookup_insert_ne. `````` Robbert Krebbers committed Dec 15, 2015 77 ``````Qed. `````` Robbert Krebbers committed Feb 08, 2016 78 ``````Global Instance map_singleton_timeless i x : `````` Robbert Krebbers committed Dec 21, 2015 79 `````` Timeless x → Timeless ({[ i ↦ x ]} : gmap K A) := _. `````` Robbert Krebbers committed Jan 14, 2016 80 ``````End cofe. `````` Robbert Krebbers committed Feb 08, 2016 81 `````` `````` Robbert Krebbers committed Jan 14, 2016 82 ``````Arguments mapC _ {_ _} _. `````` Robbert Krebbers committed Dec 15, 2015 83 84 `````` (* CMRA *) `````` Robbert Krebbers committed Jan 14, 2016 85 86 87 88 89 ``````Section cmra. Context `{Countable K} {A : cmraT}. Instance map_op : Op (gmap K A) := merge op. Instance map_unit : Unit (gmap K A) := fmap unit. `````` Robbert Krebbers committed Feb 11, 2016 90 ``````Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i). `````` Robbert Krebbers committed Jan 14, 2016 91 ``````Instance map_minus : Minus (gmap K A) := merge minus. `````` Robbert Krebbers committed Feb 08, 2016 92 `````` `````` Robbert Krebbers committed Jan 14, 2016 93 ``````Lemma lookup_op m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i. `````` Robbert Krebbers committed Dec 15, 2015 94 ``````Proof. by apply lookup_merge. Qed. `````` Robbert Krebbers committed Jan 14, 2016 95 ``````Lemma lookup_minus m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i. `````` Robbert Krebbers committed Dec 15, 2015 96 ``````Proof. by apply lookup_merge. Qed. `````` Robbert Krebbers committed Jan 14, 2016 97 ``````Lemma lookup_unit m i : unit m !! i = unit (m !! i). `````` Robbert Krebbers committed Dec 15, 2015 98 ``````Proof. by apply lookup_fmap. Qed. `````` Robbert Krebbers committed Feb 08, 2016 99 `````` `````` Robbert Krebbers committed Jan 14, 2016 100 ``````Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i. `````` Robbert Krebbers committed Dec 15, 2015 101 102 ``````Proof. split. `````` Robbert Krebbers committed Jan 13, 2016 103 `````` * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm. `````` Robbert Krebbers committed Dec 15, 2015 104 `````` * intros Hm; exists (m2 ⩪ m1); intros i. `````` Robbert Krebbers committed Feb 01, 2016 105 `````` by rewrite lookup_op lookup_minus cmra_op_minus'. `````` Robbert Krebbers committed Dec 15, 2015 106 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 107 ``````Lemma map_includedN_spec (m1 m2 : gmap K A) n : `````` Robbert Krebbers committed Dec 15, 2015 108 109 110 `````` m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i. Proof. split. `````` Robbert Krebbers committed Jan 13, 2016 111 `````` * by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm. `````` Robbert Krebbers committed Dec 15, 2015 112 `````` * intros Hm; exists (m2 ⩪ m1); intros i. `````` Robbert Krebbers committed Jan 13, 2016 113 `````` by rewrite lookup_op lookup_minus cmra_op_minus. `````` Robbert Krebbers committed Dec 15, 2015 114 ``````Qed. `````` Robbert Krebbers committed Feb 08, 2016 115 `````` `````` Robbert Krebbers committed Jan 14, 2016 116 ``````Definition map_cmra_mixin : CMRAMixin (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 117 118 ``````Proof. split. `````` Robbert Krebbers committed Jan 13, 2016 119 120 121 122 `````` * by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i). * by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i). * by intros n m1 m2 Hm ? i; rewrite -(Hm i). * by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i). `````` Robbert Krebbers committed Feb 01, 2016 123 124 125 126 127 `````` * intros n m Hm i; apply cmra_validN_S, Hm. * by intros m1 m2 m3 i; rewrite !lookup_op associative. * by intros m1 m2 i; rewrite !lookup_op commutative. * by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l. * by intros m i; rewrite !lookup_unit cmra_unit_idempotent. `````` Robbert Krebbers committed Dec 15, 2015 128 `````` * intros n x y; rewrite !map_includedN_spec; intros Hm i. `````` Robbert Krebbers committed Feb 01, 2016 129 130 `````` by rewrite !lookup_unit; apply cmra_unit_preservingN. * intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i). `````` Robbert Krebbers committed Jan 13, 2016 131 `````` by rewrite -lookup_op. `````` Robbert Krebbers committed Feb 01, 2016 132 `````` * intros x y n; rewrite map_includedN_spec=> ? i. `````` Robbert Krebbers committed Jan 13, 2016 133 `````` by rewrite lookup_op lookup_minus cmra_op_minus. `````` Robbert Krebbers committed Dec 15, 2015 134 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 135 ``````Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 136 137 ``````Proof. intros n m m1 m2 Hm Hm12. `````` Ralf Jung committed Feb 10, 2016 138 `````` assert (∀ i, m !! i ≡{n}≡ m1 !! i ⋅ m2 !! i) as Hm12' `````` Robbert Krebbers committed Jan 13, 2016 139 `````` by (by intros i; rewrite -lookup_op). `````` Robbert Krebbers committed Dec 15, 2015 140 141 142 `````` set (f i := cmra_extend_op 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); `````` Robbert Krebbers committed Jan 13, 2016 143 `````` repeat split; intros i; rewrite /= ?lookup_op !lookup_imap. `````` Robbert Krebbers committed Jan 14, 2016 144 `````` * destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor]. `````` Robbert Krebbers committed Jan 13, 2016 145 `````` rewrite -Hx; apply (proj2_sig (f i)). `````` Robbert Krebbers committed Jan 14, 2016 146 `````` * destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|]. `````` Robbert Krebbers committed Dec 15, 2015 147 `````` pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. `````` Robbert Krebbers committed Jan 14, 2016 148 `````` by symmetry; apply option_op_positive_dist_l with (m2 !! i). `````` Robbert Krebbers committed Dec 15, 2015 149 150 `````` * destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|]. pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. `````` Robbert Krebbers committed Jan 14, 2016 151 `````` by symmetry; apply option_op_positive_dist_r with (m1 !! i). `````` Robbert Krebbers committed Dec 15, 2015 152 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 153 154 ``````Canonical Structure mapRA : cmraT := CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin. `````` Robbert Krebbers committed Feb 01, 2016 155 156 157 158 159 160 161 ``````Global Instance map_cmra_identity : CMRAIdentity mapRA. Proof. split. * by intros ? n; rewrite lookup_empty. * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _). * apply map_empty_timeless. Qed. `````` Robbert Krebbers committed Jan 14, 2016 162 ``````End cmra. `````` Robbert Krebbers committed Feb 08, 2016 163 `````` `````` Robbert Krebbers committed Jan 14, 2016 164 165 166 ``````Arguments mapRA _ {_ _} _. Section properties. `````` Robbert Krebbers committed Feb 08, 2016 167 ``````Context `{Countable K} {A : cmraT}. `````` Robbert Krebbers committed Jan 16, 2016 168 ``````Implicit Types m : gmap K A. `````` Robbert Krebbers committed Feb 08, 2016 169 170 ``````Implicit Types i : K. Implicit Types a : A. `````` Robbert Krebbers committed Jan 14, 2016 171 `````` `````` Ralf Jung committed Feb 10, 2016 172 ``````Lemma map_lookup_validN n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x. `````` Robbert Krebbers committed Jan 16, 2016 173 ``````Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed. `````` Robbert Krebbers committed Feb 11, 2016 174 ``````Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m. `````` Robbert Krebbers committed Dec 15, 2015 175 ``````Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed. `````` Robbert Krebbers committed Feb 08, 2016 176 177 178 179 180 ``````Lemma map_singleton_validN n i x : ✓{n} ({[ i ↦ x ]} : gmap K A) ↔ ✓{n} x. Proof. split; [|by intros; apply map_insert_validN, cmra_empty_valid]. by move=>/(_ i); simplify_map_equality. Qed. `````` Ralf Jung committed Feb 08, 2016 181 `````` `````` Robbert Krebbers committed Feb 09, 2016 182 ``````Lemma map_insert_op_None m1 m2 i x : `````` Robbert Krebbers committed Feb 02, 2016 183 `````` m2 !! i = None → <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2. `````` Robbert Krebbers committed Jan 14, 2016 184 ``````Proof. by intros Hi; apply (insert_merge_l _ m1 m2); rewrite Hi. Qed. `````` Robbert Krebbers committed Feb 09, 2016 185 186 187 188 189 190 191 192 193 194 195 196 197 198 ``````Lemma map_insert_op_unit m1 m2 i x : m2 !! i ≡ Some (unit x) → <[i:=x]>(m1 ⋅ m2) ≡ <[i:=x]>m1 ⋅ m2. Proof. intros Hu j; destruct (decide (i = j)) as [->|]. * by rewrite lookup_insert lookup_op lookup_insert Hu cmra_unit_r. * by rewrite lookup_insert_ne // !lookup_op lookup_insert_ne. Qed. Lemma map_insert_op m1 m2 i x : m2 !! i = None ∨ m2 !! i ≡ Some (unit x) → <[i:=x]>(m1 ⋅ m2) ≡ <[i:=x]>m1 ⋅ m2. Proof. by intros [?|?]; [rewrite map_insert_op_None|rewrite map_insert_op_unit]. Qed. `````` Robbert Krebbers committed Jan 14, 2016 199 200 201 202 203 204 ``````Lemma map_unit_singleton (i : K) (x : A) : unit ({[ i ↦ x ]} : gmap K A) = {[ i ↦ unit x ]}. Proof. apply map_fmap_singleton. Qed. Lemma map_op_singleton (i : K) (x y : A) : {[ i ↦ x ]} ⋅ {[ i ↦ y ]} = ({[ i ↦ x ⋅ y ]} : gmap K A). Proof. by apply (merge_singleton _ _ _ x y). Qed. `````` Ralf Jung committed Feb 08, 2016 205 `````` `````` Robbert Krebbers committed Jan 16, 2016 206 ``````Lemma singleton_includedN n m i x : `````` Ralf Jung committed Feb 10, 2016 207 `````` {[ i ↦ x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ x ≼ y. `````` Robbert Krebbers committed Jan 16, 2016 208 209 210 211 212 `````` (* not m !! i = Some y ∧ x ≼{n} y to deal with n = 0 *) Proof. split. * move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hm. destruct (m' !! i) as [y|]; `````` Robbert Krebbers committed Feb 01, 2016 213 `````` [exists (x ⋅ y)|exists x]; eauto using cmra_included_l. `````` Robbert Krebbers committed Jan 16, 2016 214 215 216 217 218 `````` * intros (y&Hi&?); rewrite map_includedN_spec=>j. destruct (decide (i = j)); simplify_map_equality. + by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN. + apply None_includedN. Qed. `````` Robbert Krebbers committed Feb 02, 2016 219 ``````Lemma map_dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2. `````` Robbert Krebbers committed Dec 16, 2015 220 ``````Proof. `````` Robbert Krebbers committed Jan 13, 2016 221 `````` apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom. `````` Robbert Krebbers committed Dec 16, 2015 222 223 224 `````` unfold is_Some; setoid_rewrite lookup_op. destruct (m1 !! i), (m2 !! i); naive_solver. Qed. `````` Robbert Krebbers committed Jan 16, 2016 225 `````` `````` Robbert Krebbers committed Feb 02, 2016 226 ``````Lemma map_insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x : `````` Ralf Jung committed Feb 03, 2016 227 `````` x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q. `````` Robbert Krebbers committed Feb 02, 2016 228 229 230 231 232 233 234 235 ``````Proof. intros Hx%option_updateP' HP mf n Hm. destruct (Hx (mf !! i) n) as ([y|]&?&?); try done. { by generalize (Hm i); rewrite lookup_op; simplify_map_equality. } exists (<[i:=y]> m); split; first by auto. intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm. destruct (decide (i = j)); simplify_map_equality'; auto. Qed. `````` Robbert Krebbers committed Feb 04, 2016 236 ``````Lemma map_insert_updateP' (P : A → Prop) m i x : `````` Ralf Jung committed Feb 03, 2016 237 `````` x ~~>: P → <[i:=x]>m ~~>: λ m', ∃ y, m' = <[i:=y]>m ∧ P y. `````` Robbert Krebbers committed Feb 02, 2016 238 ``````Proof. eauto using map_insert_updateP. Qed. `````` Ralf Jung committed Feb 03, 2016 239 ``````Lemma map_insert_update m i x y : x ~~> y → <[i:=x]>m ~~> <[i:=y]>m. `````` Robbert Krebbers committed Feb 02, 2016 240 ``````Proof. `````` Robbert Krebbers committed Feb 08, 2016 241 `````` rewrite !cmra_update_updateP; eauto using map_insert_updateP with subst. `````` Robbert Krebbers committed Feb 02, 2016 242 243 ``````Qed. `````` Ralf Jung committed Feb 08, 2016 244 245 246 247 ``````Lemma map_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x : x ~~>: P → (∀ y, P y → Q {[ i ↦ y ]}) → {[ i ↦ x ]} ~~>: Q. Proof. apply map_insert_updateP. Qed. Lemma map_singleton_updateP' (P : A → Prop) i x : `````` Ralf Jung committed Feb 09, 2016 248 `````` x ~~>: P → {[ i ↦ x ]} ~~>: λ m, ∃ y, m = {[ i ↦ y ]} ∧ P y. `````` Robbert Krebbers committed Feb 08, 2016 249 ``````Proof. apply map_insert_updateP'. Qed. `````` Ralf Jung committed Feb 08, 2016 250 ``````Lemma map_singleton_update i (x y : A) : x ~~> y → {[ i ↦ x ]} ~~> {[ i ↦ y ]}. `````` Robbert Krebbers committed Feb 08, 2016 251 ``````Proof. apply map_insert_update. Qed. `````` Ralf Jung committed Feb 08, 2016 252 `````` `````` Ralf Jung committed Feb 09, 2016 253 ``````Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A} `````` Robbert Krebbers committed Feb 10, 2016 254 `````` (P : A → Prop) (Q : gmap K A → Prop) i : `````` Ralf Jung committed Feb 09, 2016 255 `````` ∅ ~~>: P → (∀ y, P y → Q {[ i ↦ y ]}) → ∅ ~~>: Q. `````` Robbert Krebbers committed Feb 10, 2016 256 257 258 259 260 261 262 263 264 265 266 ``````Proof. intros Hx HQ gf n Hg. destruct (Hx (from_option ∅ (gf !! i)) n) as (y&?&Hy). { move:(Hg i). rewrite !left_id. case _: (gf !! i); simpl; auto using cmra_empty_valid. } exists {[ i ↦ y ]}; split; first by auto. intros i'; destruct (decide (i' = i)) as [->|]. - rewrite lookup_op lookup_singleton. move:Hy; case _: (gf !! i); first done. by rewrite right_id. - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id. `````` Ralf Jung committed Feb 09, 2016 267 ``````Qed. `````` Robbert Krebbers committed Feb 10, 2016 268 ``````Lemma map_singleton_updateP_empty' `{Empty A, !CMRAIdentity A} (P: A → Prop) i : `````` Ralf Jung committed Feb 09, 2016 269 270 271 `````` ∅ ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i ↦ y ]} ∧ P y. Proof. eauto using map_singleton_updateP_empty. Qed. `````` 272 ``````Section freshness. `````` Robbert Krebbers committed Jan 16, 2016 273 ``````Context `{Fresh K (gset K), !FreshSpec K (gset K)}. `````` Robbert Krebbers committed Feb 02, 2016 274 ``````Lemma map_updateP_alloc (Q : gmap K A → Prop) m x : `````` Ralf Jung committed Feb 03, 2016 275 `````` ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q. `````` Robbert Krebbers committed Dec 16, 2015 276 ``````Proof. `````` Robbert Krebbers committed Feb 02, 2016 277 `````` intros ? HQ mf n Hm. set (i := fresh (dom (gset K) (m ⋅ mf))). `````` Robbert Krebbers committed Dec 16, 2015 278 `````` assert (i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [??]. `````` Robbert Krebbers committed Jan 13, 2016 279 `````` { rewrite -not_elem_of_union -map_dom_op; apply is_fresh. } `````` Robbert Krebbers committed Feb 02, 2016 280 `````` exists (<[i:=x]>m); split; first by apply HQ, not_elem_of_dom. `````` Robbert Krebbers committed Feb 09, 2016 281 `````` rewrite -map_insert_op_None; last by apply not_elem_of_dom. `````` Robbert Krebbers committed Feb 02, 2016 282 `````` by apply map_insert_validN; [apply cmra_valid_validN|]. `````` Robbert Krebbers committed Dec 16, 2015 283 ``````Qed. `````` Robbert Krebbers committed Feb 02, 2016 284 ``````Lemma map_updateP_alloc' m x : `````` Ralf Jung committed Feb 03, 2016 285 `````` ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None. `````` Robbert Krebbers committed Feb 02, 2016 286 ``````Proof. eauto using map_updateP_alloc. Qed. `````` 287 288 ``````End freshness. `````` Ralf Jung committed Feb 11, 2016 289 290 291 292 293 294 ``````(* Allocation is a local update: Just use composition with a singleton map. *) (* Deallocation is *not* a local update. The trouble is that if we own {[ i ↦ x ]}, then the frame could always own "unit x", and prevent deallocation. *) (* Applying a local update at a position we own is a local update. *) `````` Ralf Jung committed Feb 11, 2016 295 296 ``````Global Instance map_alter_update `{!LocalUpdate Lv L} i : LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ Lv x) (alter L i). `````` 297 ``````Proof. `````` Robbert Krebbers committed Feb 11, 2016 298 299 300 301 `````` 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 302 `````` case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN L). `````` Robbert Krebbers committed Feb 11, 2016 303 `````` - by rewrite lookup_op !lookup_alter_ne // lookup_op. `````` 304 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 305 306 ``````End properties. `````` Robbert Krebbers committed Feb 04, 2016 307 ``````(** Functor *) `````` Robbert Krebbers committed Jan 14, 2016 308 309 310 311 312 313 314 315 316 317 318 ``````Instance map_fmap_ne `{Countable K} {A B : cofeT} (f : A → B) n : 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. Instance map_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B) `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B). Proof. split. * intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i. by rewrite !lookup_fmap; apply: includedN_preserving. * by intros n m ? i; rewrite lookup_fmap; apply validN_preserving. Qed. `````` Robbert Krebbers committed Feb 04, 2016 319 320 321 322 323 324 325 326 ``````Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B := CofeMor (fmap f : mapC K A → mapC K B). Instance mapC_map_ne `{Countable K} {A B} n : Proper (dist n ==> dist n) (@mapC_map K _ _ A B). Proof. intros f g Hf m k; rewrite /= !lookup_fmap. destruct (_ !! k) eqn:?; simpl; constructor; apply Hf. Qed. `````` Ralf Jung committed Feb 05, 2016 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 `````` Program Definition mapF K `{Countable K} (Σ : iFunctor) : iFunctor := {| ifunctor_car := mapRA K ∘ Σ; ifunctor_map A B := mapC_map ∘ ifunctor_map Σ |}. Next Obligation. by intros K ?? Σ A B n f g Hfg; apply mapC_map_ne, ifunctor_map_ne. Qed. Next Obligation. intros K ?? Σ A x. rewrite /= -{2}(map_fmap_id x). apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_id. Qed. Next Obligation. intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose. apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose. Qed.``````