cmra_maps.v 11.4 KB
 Robbert Krebbers committed Dec 15, 2015 1 ``````Require Export modures.cmra modures.cofe_maps. `````` Robbert Krebbers committed Dec 04, 2015 2 ``````Require Import prelude.pmap prelude.natmap prelude.gmap. `````` Robbert Krebbers committed Nov 16, 2015 3 4 `````` (** option *) `````` Robbert Krebbers committed Nov 20, 2015 5 ``````Instance option_valid `{Valid A} : Valid (option A) := λ mx, `````` Robbert Krebbers committed Nov 23, 2015 6 `````` match mx with Some x => ✓ x | None => True end. `````` Robbert Krebbers committed Nov 20, 2015 7 ``````Instance option_validN `{ValidN A} : ValidN (option A) := λ n mx, `````` Robbert Krebbers committed Nov 23, 2015 8 `````` match mx with Some x => ✓{n} x | None => True end. `````` Robbert Krebbers committed Nov 16, 2015 9 10 11 12 ``````Instance option_unit `{Unit A} : Unit (option A) := fmap unit. Instance option_op `{Op A} : Op (option A) := union_with (λ x y, Some (x ⋅ y)). Instance option_minus `{Minus A} : Minus (option A) := difference_with (λ x y, Some (x ⩪ y)). `````` Robbert Krebbers committed Dec 11, 2015 13 14 15 16 17 18 19 20 21 22 23 ``````Lemma option_included `{CMRA A} mx my : mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y. Proof. split. * intros [mz Hmz]; destruct mx as [x|]; [right|by left]. destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz]. destruct mz as [z|]; inversion_clear Hmz; split_ands; auto; setoid_subst; eauto using ra_included_l. * intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor). by exists (Some z); constructor. Qed. `````` Robbert Krebbers committed Nov 20, 2015 24 25 26 27 28 29 30 ``````Lemma option_includedN `{CMRA A} n mx my : mx ≼{n} my ↔ n = 0 ∨ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y. Proof. split. * intros [mz Hmz]; destruct n as [|n]; [by left|right]. destruct mx as [x|]; [right|by left]. destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz]. `````` Robbert Krebbers committed Dec 11, 2015 31 32 `````` destruct mz as [z|]; inversion_clear Hmz; split_ands; auto; cofe_subst; auto using cmra_included_l. `````` Robbert Krebbers committed Nov 20, 2015 33 34 35 36 `````` * intros [->|[->|(x&y&->&->&z&Hz)]]; try (by exists my; destruct my; constructor). by exists (Some z); constructor. Qed. `````` Robbert Krebbers committed Nov 16, 2015 37 38 39 40 41 42 43 44 45 ``````Instance option_cmra `{CMRA A} : CMRA (option A). Proof. split. * apply _. * by intros n [x|]; destruct 1; constructor; repeat apply (_ : Proper (dist _ ==> _ ==> _) _). * by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _). * destruct 1 as [[?|] [?|]| |]; unfold validN, option_validN; simpl; intros ?; auto using cmra_valid_0; `````` Robbert Krebbers committed Nov 23, 2015 46 `````` eapply (_ : Proper (dist _ ==> impl) (✓{_})); eauto. `````` Robbert Krebbers committed Nov 16, 2015 47 48 49 50 51 52 53 54 55 56 `````` * by destruct 1; inversion_clear 1; constructor; repeat apply (_ : Proper (dist _ ==> _ ==> _) _). * intros [x|]; unfold validN, option_validN; auto using cmra_valid_0. * intros n [x|]; unfold validN, option_validN; auto using cmra_valid_S. * by intros [x|]; unfold valid, validN, option_validN, option_valid; auto using cmra_valid_validN. * intros [x|] [y|] [z|]; constructor; rewrite ?(associative _); auto. * intros [x|] [y|]; constructor; rewrite 1?(commutative _); auto. * by intros [x|]; constructor; rewrite cmra_unit_l. * by intros [x|]; constructor; rewrite cmra_unit_idempotent. `````` Robbert Krebbers committed Nov 20, 2015 57 58 `````` * intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto. do 2 right; exists (unit x), (unit y); eauto using cmra_unit_preserving. `````` Robbert Krebbers committed Nov 16, 2015 59 60 `````` * intros n [x|] [y|]; unfold validN, option_validN; simpl; eauto using cmra_valid_op_l. `````` Robbert Krebbers committed Nov 20, 2015 61 62 63 `````` * intros n mx my; rewrite option_includedN. intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|]. by constructor; apply cmra_op_minus. `````` Robbert Krebbers committed Nov 16, 2015 64 65 66 ``````Qed. Instance option_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (option A). Proof. `````` Robbert Krebbers committed Nov 20, 2015 67 `````` intros n mx my1 my2; destruct (decide (n = 0)) as [->|]. `````` Robbert Krebbers committed Nov 16, 2015 68 69 70 `````` { by exists (mx, None); repeat constructor; destruct mx; constructor. } destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx'; try (by exfalso; inversion Hx'; auto). `````` Robbert Krebbers committed Nov 20, 2015 71 `````` * destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto. `````` Robbert Krebbers committed Nov 16, 2015 72 73 74 75 76 77 `````` { by inversion_clear Hx'. } by exists (Some z1, Some z2); repeat constructor. * by exists (Some x,None); inversion Hx'; repeat constructor. * by exists (None,Some x); inversion Hx'; repeat constructor. * exists (None,None); repeat constructor. Qed. `````` Robbert Krebbers committed Dec 11, 2015 78 79 80 81 82 ``````Instance None_valid_timeless `{Valid A, ValidN A} : ValidTimeless (@None A). Proof. done. Qed. Instance Some_valid_timeless `{Valid A, ValidN A} x : ValidTimeless x → ValidTimeless (Some x). Proof. by intros ? y; apply (valid_timeless x). Qed. `````` Robbert Krebbers committed Nov 22, 2015 83 ``````Instance option_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B) `````` Robbert Krebbers committed Nov 20, 2015 84 `````` `{!CMRAMonotone f} : CMRAMonotone (fmap f : option A → option B). `````` Robbert Krebbers committed Nov 16, 2015 85 86 ``````Proof. split. `````` Robbert Krebbers committed Nov 20, 2015 87 88 `````` * intros n mx my; rewrite !option_includedN. intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving. `````` Robbert Krebbers committed Nov 16, 2015 89 90 91 `````` * by intros n [x|] ?; unfold validN, option_validN; simpl; try apply validN_preserving. Qed. `````` Robbert Krebbers committed Nov 16, 2015 92 93 94 95 96 `````` (** fin maps *) Section map. Context `{FinMap K M}. Existing Instances map_dist map_compl map_cofe. `````` Robbert Krebbers committed Dec 15, 2015 97 98 99 100 101 102 `````` Global Instance map_op `{Op A} : Op (M A) := merge op. Global Instance map_unit `{Unit A} : Unit (M A) := fmap unit. Global Instance map_valid `{Valid A} : Valid (M A) := λ m, ∀ i, ✓ (m !! i). Global Instance map_validN `{ValidN A} : ValidN (M A) := λ n m, ∀ i, ✓{n} (m!!i). Global Instance map_minus `{Minus A} : Minus (M A) := merge minus. `````` Robbert Krebbers committed Nov 16, 2015 103 104 105 106 107 108 `````` Lemma lookup_op `{Op A} m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i. Proof. by apply lookup_merge. Qed. Lemma lookup_minus `{Minus A} m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i. Proof. by apply lookup_merge. Qed. Lemma lookup_unit `{Unit A} m i : unit m !! i = unit (m !! i). Proof. by apply lookup_fmap. Qed. `````` Robbert Krebbers committed Nov 20, 2015 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 `````` Lemma map_included_spec `{CMRA A} (m1 m2 : M A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i. Proof. split. * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm. * intros Hm; exists (m2 ⩪ m1); intros i. by rewrite lookup_op, lookup_minus, ra_op_minus. Qed. Lemma map_includedN_spec `{CMRA A} (m1 m2 : M A) n : m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i. Proof. split. * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm. * intros Hm; exists (m2 ⩪ m1); intros i. by rewrite lookup_op, lookup_minus, cmra_op_minus. Qed. `````` Robbert Krebbers committed Dec 15, 2015 125 `````` Global Instance map_cmra `{CMRA A} : CMRA (M A). `````` Robbert Krebbers committed Nov 16, 2015 126 127 128 129 130 131 132 133 `````` Proof. split. * apply _. * 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). * intros n m1 m1' Hm1 m2 m2' Hm2 i. by rewrite !lookup_minus, (Hm1 i), (Hm2 i). `````` Robbert Krebbers committed Nov 23, 2015 134 `````` * by intros m i. `````` Robbert Krebbers committed Nov 16, 2015 135 136 137 138 139 140 141 `````` * intros n m Hm i; apply cmra_valid_S, Hm. * intros m; split; [by intros Hm n i; apply cmra_valid_validN|]. intros Hm i; apply cmra_valid_validN; intros n; apply 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, ra_unit_l. * by intros m i; rewrite !lookup_unit, ra_unit_idempotent. `````` Robbert Krebbers committed Nov 20, 2015 142 143 `````` * intros n x y; rewrite !map_includedN_spec; intros Hm i. by rewrite !lookup_unit; apply cmra_unit_preserving. `````` Robbert Krebbers committed Nov 16, 2015 144 145 `````` * intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i). by rewrite <-lookup_op. `````` Robbert Krebbers committed Nov 20, 2015 146 147 `````` * intros x y n; rewrite map_includedN_spec; intros ? i. by rewrite lookup_op, lookup_minus, cmra_op_minus by done. `````` Robbert Krebbers committed Nov 16, 2015 148 `````` Qed. `````` Robbert Krebbers committed Dec 15, 2015 149 `````` Global Instance map_ra_empty `{RA A} : RAEmpty (M A). `````` Robbert Krebbers committed Nov 16, 2015 150 151 152 153 154 `````` Proof. split. * by intros ?; rewrite lookup_empty. * by intros m i; simpl; rewrite lookup_op, lookup_empty; destruct (m !! i). Qed. `````` Robbert Krebbers committed Dec 15, 2015 155 `````` Global Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (M A). `````` Robbert Krebbers committed Nov 16, 2015 156 `````` Proof. `````` Robbert Krebbers committed Nov 20, 2015 157 `````` intros n m m1 m2 Hm Hm12. `````` Robbert Krebbers committed Nov 16, 2015 158 159 `````` assert (∀ i, m !! i ={n}= m1 !! i ⋅ m2 !! i) as Hm12' by (by intros i; rewrite <-lookup_op). `````` Robbert Krebbers committed Nov 20, 2015 160 `````` set (f i := cmra_extend_op n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)). `````` Robbert Krebbers committed Nov 16, 2015 161 162 163 164 165 166 167 168 169 170 171 172 `````` 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; simpl; intros i; rewrite ?lookup_op, !lookup_imap. * destruct (m !! i) as [x|] eqn:Hx; simpl; [|constructor]. rewrite <-Hx; apply (proj2_sig (f 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 destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''. * destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|]. pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''. by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''. Qed. `````` Robbert Krebbers committed Dec 11, 2015 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 `````` Global Instance map_empty_valid_timeless `{Valid A, ValidN A} : ValidTimeless (∅ : M A). Proof. by intros ??; rewrite lookup_empty. Qed. Global Instance map_ra_insert_valid_timeless `{Valid A,ValidN A} (m: M A) i x: ValidTimeless x → ValidTimeless m → m !! i = None → ValidTimeless (<[i:=x]>m). Proof. intros ?? Hi Hm j; destruct (decide (i = j)); simplify_map_equality. { specialize (Hm j); simplify_map_equality. by apply (valid_timeless _). } generalize j; clear dependent j; rapply (valid_timeless m). intros j; destruct (decide (i = j)); simplify_map_equality;[by rewrite Hi|]. by specialize (Hm j); simplify_map_equality. Qed. Global Instance map_ra_singleton_timeless `{Valid A, ValidN A} (i : K) x : ValidTimeless x → ValidTimeless ({[ i, x ]} : M A). Proof. intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _); simpl. by rewrite lookup_empty. Qed. `````` Robbert Krebbers committed Dec 15, 2015 192 193 194 195 196 197 `````` Lemma map_insert_valid `{ValidN A} (m : M A) n i x : ✓{n} x → ✓{n} m → ✓{n} (<[i:=x]>m). Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed. Lemma map_insert_op `{Op A} (m1 m2 : M A) i x : m2 !! i = None → <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2. Proof. by intros Hi; apply (insert_merge_l _); rewrite Hi. Qed. `````` Robbert Krebbers committed Nov 16, 2015 198 `````` Definition mapRA (A : cmraT) : cmraT := CMRAT (M A). `````` Robbert Krebbers committed Nov 20, 2015 199 200 `````` Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B) `{!CMRAMonotone f} : CMRAMonotone (fmap f : M A → M B). `````` Robbert Krebbers committed Nov 16, 2015 201 202 `````` Proof. split. `````` Robbert Krebbers committed Nov 20, 2015 203 204 `````` * intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i. by rewrite !lookup_fmap; apply includedN_preserving. `````` Robbert Krebbers committed Nov 16, 2015 205 206 `````` * by intros n m ? i; rewrite lookup_fmap; apply validN_preserving. Qed. `````` Robbert Krebbers committed Nov 19, 2015 207 `````` Hint Resolve (map_fmap_ne (M:=M)) : typeclass_instances. `````` Robbert Krebbers committed Nov 16, 2015 208 209 210 211 `````` Definition mapRA_map {A B : cmraT} (f : A -n> B) : mapRA A -n> mapRA B := CofeMor (fmap f : mapRA A → mapRA B). Global Instance mapRA_map_ne {A B} n : Proper (dist n ==> dist n) (@mapRA_map A B) := mapC_map_ne n. `````` Robbert Krebbers committed Nov 22, 2015 212 `````` Global Instance mapRA_map_monotone {A B : cmraT} (f : A -n> B) `````` Robbert Krebbers committed Nov 20, 2015 213 `````` `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _. `````` Robbert Krebbers committed Nov 16, 2015 214 215 216 ``````End map. Arguments mapRA {_} _ {_ _ _ _ _ _ _ _ _} _. `````` Robbert Krebbers committed Dec 15, 2015 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 ``````Section map_dom. Context `{FinMapDom K M D, Fresh K D, !FreshSpec K D}. Lemma map_dom_op `{Op A} (m1 m2: M A) : dom D (m1 ⋅ m2) ≡ dom D m1 ∪ dom D m2. Proof. apply elem_of_equiv; intros i; rewrite elem_of_union, !elem_of_dom. unfold is_Some; setoid_rewrite lookup_op. destruct (m1 !! i), (m2 !! i); naive_solver. Qed. Lemma map_update_alloc `{CMRA A} (m : M A) x : ✓ x → m ⇝: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None. Proof. intros ? mf n Hm. set (i := fresh (dom D (m ⋅ mf))). assert (i ∉ dom D m ∧ i ∉ dom D mf) as [??]. { rewrite <-not_elem_of_union, <-map_dom_op; apply is_fresh. } exists (<[i:=x]>m); split; [exists i; split; [done|]|]. * by apply not_elem_of_dom. * rewrite <-map_insert_op by (by apply not_elem_of_dom). by apply map_insert_valid; [apply cmra_valid_validN|]. Qed. End map_dom. `````` Robbert Krebbers committed Nov 16, 2015 238 ``````Canonical Structure natmapRA := mapRA natmap. `````` Robbert Krebbers committed Nov 16, 2015 239 240 ``````Definition natmapRA_map {A B : cmraT} (f : A -n> B) : natmapRA A -n> natmapRA B := mapRA_map f. `````` Robbert Krebbers committed Nov 16, 2015 241 ``````Canonical Structure PmapRA := mapRA Pmap. `````` Robbert Krebbers committed Nov 16, 2015 242 243 ``````Definition PmapRA_map {A B : cmraT} (f : A -n> B) : PmapRA A -n> PmapRA B := mapRA_map f. `````` Robbert Krebbers committed Dec 04, 2015 244 245 246 ``````Canonical Structure gmapRA K `{Countable K} := mapRA (gmap K). Definition gmapRA_map `{Countable K} {A B : cmraT} (f : A -n> B) : gmapRA K A -n> gmapRA K B := mapRA_map f.``````