fin_maps.v 9.97 KB
 Robbert Krebbers committed Dec 16, 2015 1 2 ``````Require Export modures.cmra prelude.gmap. Require Import modures.option. `````` Robbert Krebbers committed Dec 15, 2015 3 4 `````` Section map. `````` Robbert Krebbers committed Dec 16, 2015 5 ``````Context `{Countable K}. `````` Robbert Krebbers committed Dec 15, 2015 6 7 `````` (* COFE *) `````` Robbert Krebbers committed Dec 16, 2015 8 ``````Global Instance map_dist `{Dist A} : Dist (gmap K A) := λ n m1 m2, `````` Robbert Krebbers committed Dec 15, 2015 9 `````` ∀ i, m1 !! i ={n}= m2 !! i. `````` Robbert Krebbers committed Dec 16, 2015 10 ``````Program Definition map_chain `{Dist A} (c : chain (gmap K A)) `````` Robbert Krebbers committed Dec 15, 2015 11 12 `````` (k : K) : chain (option A) := {| chain_car n := c n !! k |}. Next Obligation. by intros A ? c k n i ?; apply (chain_cauchy c). Qed. `````` Robbert Krebbers committed Dec 16, 2015 13 ``````Global Instance map_compl `{Cofe A} : 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 Dec 16, 2015 15 ``````Global Instance map_cofe `{Cofe A} : Cofe (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 ``````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. * by intros m1 m2 k. * intros c n k; unfold compl, map_compl; rewrite lookup_imap. destruct (decide (n = 0)) as [->|]; [constructor|]. feed inversion (λ H, chain_cauchy c 1 n H k); simpl; auto with lia. by rewrite conv_compl; simpl; apply reflexive_eq. Qed. Global Instance lookup_ne `{Dist A} 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 35 ``````Proof. by intros m1 m2. Qed. Global Instance insert_ne `{Dist A} (i : K) n : `````` Robbert Krebbers committed Dec 16, 2015 36 `````` Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i). `````` Robbert Krebbers committed Dec 15, 2015 37 38 39 40 ``````Proof. intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality; [by constructor|by apply lookup_ne]. Qed. `````` Robbert Krebbers committed Dec 21, 2015 41 42 43 ``````Global Instance singleton_ne `{Cofe A} (i : K) n : Proper (dist n ==> dist n) (singletonM i : A → gmap K A). Proof. by intros ???; apply insert_ne. Qed. `````` Robbert Krebbers committed Dec 15, 2015 44 ``````Global Instance delete_ne `{Dist A} (i : K) n : `````` Robbert Krebbers committed Dec 16, 2015 45 `````` Proper (dist n ==> dist n) (delete (M:=gmap K A) i). `````` Robbert Krebbers committed Dec 15, 2015 46 47 48 49 ``````Proof. intros m m' ? j; destruct (decide (i = j)); simplify_map_equality; [by constructor|by apply lookup_ne]. Qed. `````` Robbert Krebbers committed Dec 16, 2015 50 ``````Global Instance map_empty_timeless `{Dist A, Equiv A} : Timeless (∅ : gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 51 52 53 54 ``````Proof. intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *. inversion_clear Hm; constructor. Qed. `````` Robbert Krebbers committed Dec 16, 2015 55 ``````Global Instance map_lookup_timeless `{Cofe A} (m : gmap K A) i : `````` Robbert Krebbers committed Dec 15, 2015 56 57 58 59 60 61 `````` Timeless m → Timeless (m !! i). Proof. intros ? [x|] Hx; [|by symmetry; apply (timeless _)]. rewrite (timeless m (<[i:=x]>m)), lookup_insert; auto. by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id. Qed. `````` Robbert Krebbers committed Dec 16, 2015 62 ``````Global Instance map_ra_insert_timeless `{Cofe A} (m : gmap K A) i x : `````` Robbert Krebbers committed Dec 15, 2015 63 64 65 66 67 68 69 `````` Timeless x → Timeless m → Timeless (<[i:=x]>m). Proof. intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality. { by apply (timeless _); rewrite <-Hm, lookup_insert. } by apply (timeless _); rewrite <-Hm, lookup_insert_ne by done. Qed. Global Instance map_ra_singleton_timeless `{Cofe A} (i : K) (x : A) : `````` Robbert Krebbers committed Dec 21, 2015 70 `````` Timeless x → Timeless ({[ i ↦ x ]} : gmap K A) := _. `````` Robbert Krebbers committed Dec 21, 2015 71 ``````Global Instance map_fmap_ne `{Dist A, Dist B} (f : A → B) n : `````` Robbert Krebbers committed Dec 16, 2015 72 73 `````` Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=gmap K) f). `````` Robbert Krebbers committed Dec 15, 2015 74 ``````Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed. `````` Robbert Krebbers committed Dec 16, 2015 75 ``````Canonical Structure mapC (A : cofeT) : cofeT := CofeT (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 76 77 78 79 80 81 82 83 84 85 ``````Definition mapC_map {A B} (f: A -n> B) : mapC A -n> mapC B := CofeMor (fmap f : mapC A → mapC B). Global Instance mapC_map_ne {A B} n : Proper (dist n ==> dist n) (@mapC_map A B). Proof. intros f g Hf m k; simpl; rewrite !lookup_fmap. destruct (_ !! k) eqn:?; simpl; constructor; apply Hf. Qed. (* CMRA *) `````` Robbert Krebbers committed Dec 16, 2015 86 87 88 89 ``````Global Instance map_op `{Op A} : Op (gmap K A) := merge op. Global Instance map_unit `{Unit A} : Unit (gmap K A) := fmap unit. Global Instance map_valid `{Valid A} : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i). Global Instance map_validN `{ValidN A} : ValidN (gmap K A) := λ n m, `````` Robbert Krebbers committed Dec 15, 2015 90 `````` ∀ i, ✓{n} (m!!i). `````` Robbert Krebbers committed Dec 16, 2015 91 ``````Global Instance map_minus `{Minus A} : Minus (gmap K A) := merge minus. `````` Robbert Krebbers committed Dec 15, 2015 92 93 94 95 96 97 ``````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 Dec 16, 2015 98 ``````Lemma map_included_spec `{CMRA A} (m1 m2 : gmap K A) : `````` Robbert Krebbers committed Dec 15, 2015 99 100 101 102 103 104 105 `````` 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. `````` Robbert Krebbers committed Dec 16, 2015 106 ``````Lemma map_includedN_spec `{CMRA A} (m1 m2 : gmap K A) n : `````` Robbert Krebbers committed Dec 15, 2015 107 108 109 110 111 112 113 `````` 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 16, 2015 114 ``````Global Instance map_cmra `{CMRA A} : CMRA (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 ``````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). * by intros m i. * 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. * intros n x y; rewrite !map_includedN_spec; intros Hm i. by rewrite !lookup_unit; apply cmra_unit_preserving. * intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i). by rewrite <-lookup_op. * intros x y n; rewrite map_includedN_spec; intros ? i. by rewrite lookup_op, lookup_minus, cmra_op_minus by done. Qed. `````` Robbert Krebbers committed Dec 16, 2015 138 ``````Global Instance map_ra_empty `{RA A} : RAIdentity (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 139 140 141 142 143 ``````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 16, 2015 144 ``````Global Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 ``````Proof. 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_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); 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. Global Instance map_empty_valid_timeless `{Valid A, ValidN A} : `````` Robbert Krebbers committed Dec 16, 2015 163 `````` ValidTimeless (∅ : gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 164 ``````Proof. by intros ??; rewrite lookup_empty. Qed. `````` Robbert Krebbers committed Dec 16, 2015 165 166 ``````Global Instance map_ra_insert_valid_timeless `{Valid A, ValidN A} (m : gmap K A) i x: `````` Robbert Krebbers committed Dec 15, 2015 167 168 169 170 171 172 173 174 175 176 `````` 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_valid_timeless `{Valid A, ValidN A} (i : K) x : `````` Robbert Krebbers committed Dec 21, 2015 177 `````` ValidTimeless x → ValidTimeless ({[ i ↦ x ]} : gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 178 179 180 181 ``````Proof. intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _); simpl. by rewrite lookup_empty. Qed. `````` Robbert Krebbers committed Dec 16, 2015 182 ``````Lemma map_insert_valid `{ValidN A} (m : gmap K A) n i x : `````` Robbert Krebbers committed Dec 15, 2015 183 184 `````` ✓{n} x → ✓{n} m → ✓{n} (<[i:=x]>m). Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed. `````` Robbert Krebbers committed Dec 16, 2015 185 ``````Lemma map_insert_op `{Op A} (m1 m2 : gmap K A) i x : `````` Robbert Krebbers committed Dec 15, 2015 186 187 `````` 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 Dec 21, 2015 188 189 190 191 ``````Lemma map_singleton_op `{Op A} (i : K) (x y : A) : ({[ i ↦ x ⋅ y ]} : gmap K A) = {[ i ↦ x ]} ⋅ {[ i ↦ y ]}. Proof. by apply symmetry, merge_singleton. Qed. `````` Robbert Krebbers committed Dec 16, 2015 192 ``````Canonical Structure mapRA (A : cmraT) : cmraT := CMRAT (gmap K A). `````` Robbert Krebbers committed Dec 15, 2015 193 ``````Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B) `````` Robbert Krebbers committed Dec 16, 2015 194 `````` `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B). `````` Robbert Krebbers committed Dec 15, 2015 195 196 197 198 199 200 201 202 203 204 205 206 207 ``````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. 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. Global Instance mapRA_map_monotone {A B : cmraT} (f : A -n> B) `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _. `````` Robbert Krebbers committed Dec 16, 2015 208 ``````Context `{Fresh K (gset K), !FreshSpec K (gset K)}. `````` Robbert Krebbers committed Dec 15, 2015 209 `````` `````` Robbert Krebbers committed Dec 16, 2015 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 ``````Lemma map_dom_op `{Op A} (m1 m2 : gmap K A) : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ 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 : gmap K A) x : ✓ x → m ⇝: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None. Proof. intros ? mf n Hm. set (i := fresh (dom (gset K) (m ⋅ mf))). assert (i ∉ dom (gset K) m ∧ i ∉ dom (gset K) 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. Arguments mapC _ {_ _} _. Arguments mapRA _ {_ _} _.``````