fin_maps.v 19 KB
 Robbert Krebbers committed Aug 29, 2012 1 2 3 4 5 6 ``````(* Copyright (c) 2012, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** Finite maps associate data to keys. This file defines an interface for finite maps and collects some theory on it. Most importantly, it proves useful induction principles for finite maps and implements the tactic [simplify_map] to simplify goals involving finite maps. *) `````` Robbert Krebbers committed Jun 11, 2012 7 8 ``````Require Export prelude. `````` Robbert Krebbers committed Aug 29, 2012 9 10 ``````(** * Axiomatization of finite maps *) (** We require Leibniz equality to be extensional on finite maps. This of `````` 11 12 13 14 15 ``````course limits the space of finite map implementations, but since we are mainly interested in finite maps with numbers as indexes, we do not consider this to be a serious limitation. The main application of finite maps is to implement the memory, where extensionality of Leibniz equality is very important for a convenient use in the assertions of our axiomatic semantics. *) `````` Robbert Krebbers committed Aug 29, 2012 16 17 18 19 20 21 ``````(** Finiteness is axiomatized by requiring each map to have a finite domain. Since we may have multiple implementations of finite sets, the [dom] function is parametrized by an implementation of finite sets over the map's key type. *) (** Finite map implementations are required to implement the [merge] function which enables us to give a generic implementation of [union_with], [intersection_with], and [difference_with]. *) `````` Robbert Krebbers committed Oct 19, 2012 22 23 24 ``````Class FinMap K M `{Lookup K M} `{∀ A, Empty (M A)} `{∀ `(f : A → B), FMap M f} `{PartialAlter K M} `{Dom K M} `{Merge M} `{∀ i j : K, Decision (i = j)} := { `````` Robbert Krebbers committed Aug 21, 2012 25 26 27 28 29 30 31 32 33 34 35 36 `````` finmap_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2; lookup_empty {A} i : (∅ : M A) !! i = None; lookup_partial_alter {A} f (m : M A) i : partial_alter f i m !! i = f (m !! i); lookup_partial_alter_ne {A} f (m : M A) i j : i ≠ j → partial_alter f i m !! j = m !! j; lookup_fmap {A B} (f : A → B) (m : M A) i : (f <\$> m) !! i = f <\$> m !! i; elem_of_dom C {A} `{Collection K C} (m : M A) i : i ∈ dom C m ↔ is_Some (m !! i); `````` Robbert Krebbers committed Aug 29, 2012 37 `````` merge_spec {A} f `{!PropHolds (f None None = None)} `````` Robbert Krebbers committed Jun 11, 2012 38 39 40 `````` (m1 m2 : M A) i : merge f m1 m2 !! i = f (m1 !! i) (m2 !! i) }. `````` Robbert Krebbers committed Aug 29, 2012 41 42 43 44 45 ``````(** * Derived operations *) (** All of the following functions are defined in a generic way for arbitrary finite map implementations. These generic implementations do not cause a significant enough performance loss to make including them in the finite map axiomatization worthwhile. *) `````` Robbert Krebbers committed Aug 21, 2012 46 47 48 49 ``````Instance finmap_alter `{PartialAlter K M} : Alter K M := λ A f, partial_alter (fmap f). Instance finmap_insert `{PartialAlter K M} : Insert K M := λ A k x, partial_alter (λ _, Some x) k. `````` 50 ``````Instance finmap_delete `{PartialAlter K M} : Delete K M := λ A, `````` Robbert Krebbers committed Aug 21, 2012 51 `````` partial_alter (λ _, None). `````` Robbert Krebbers committed Aug 29, 2012 52 ``````Instance finmap_singleton `{PartialAlter K M} {A} `````` Robbert Krebbers committed Aug 21, 2012 53 `````` `{Empty (M A)} : Singleton (K * A) (M A) := λ p, <[fst p:=snd p]>∅. `````` Robbert Krebbers committed Jun 11, 2012 54 `````` `````` Robbert Krebbers committed Aug 29, 2012 55 56 ``````Definition list_to_map `{Insert K M} {A} `{Empty (M A)} (l : list (K * A)) : M A := insert_list l ∅. `````` Robbert Krebbers committed Jun 11, 2012 57 `````` `````` Robbert Krebbers committed Oct 10, 2012 58 ``````Instance finmap_union_with `{Merge M} : UnionWith M := λ A f, `````` Robbert Krebbers committed Aug 21, 2012 59 `````` merge (union_with f). `````` Robbert Krebbers committed Oct 10, 2012 60 ``````Instance finmap_intersection_with `{Merge M} : IntersectionWith M := λ A f, `````` Robbert Krebbers committed Aug 21, 2012 61 `````` merge (intersection_with f). `````` Robbert Krebbers committed Oct 10, 2012 62 ``````Instance finmap_difference_with `{Merge M} : DifferenceWith M := λ A f, `````` Robbert Krebbers committed Aug 21, 2012 63 `````` merge (difference_with f). `````` Robbert Krebbers committed Jun 11, 2012 64 `````` `````` Robbert Krebbers committed Oct 10, 2012 65 66 67 68 69 70 71 72 73 74 ``````(** Two finite maps are disjoint if they do not have overlapping cells. *) Instance finmap_disjoint `{Lookup K M} {A} : Disjoint (M A) := λ m1 m2, ∀ i, m1 !! i = None ∨ m2 !! i = None. (** The union of two finite maps only has a meaningful definition for maps that are disjoint. However, as working with partial functions is inconvenient in Coq, we define the union as a total function. In case both finite maps have a value at the same index, we take the value of the first map. *) Instance finmap_union `{Merge M} {A} : Union (M A) := union_with (λ x _ , x). `````` Robbert Krebbers committed Aug 29, 2012 75 ``````(** * General theorems *) `````` Robbert Krebbers committed Jun 11, 2012 76 ``````Section finmap. `````` Robbert Krebbers committed Oct 19, 2012 77 ``````Context `{FinMap K M} {A : Type}. `````` Robbert Krebbers committed Aug 21, 2012 78 79 80 81 `````` Global Instance finmap_subseteq: SubsetEq (M A) := λ m n, ∀ i x, m !! i = Some x → n !! i = Some x. Global Instance: BoundedPreOrder (M A). `````` Robbert Krebbers committed Oct 19, 2012 82 ``````Proof. split; [firstorder |]. intros m i x. by rewrite lookup_empty. Qed. `````` Robbert Krebbers committed Aug 21, 2012 83 `````` `````` Robbert Krebbers committed Oct 19, 2012 84 85 ``````Lemma lookup_weaken (m1 m2 : M A) i x : m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x. `````` Robbert Krebbers committed Aug 21, 2012 86 ``````Proof. auto. Qed. `````` Robbert Krebbers committed Oct 19, 2012 87 88 ``````Lemma lookup_weaken_None (m1 m2 : M A) i : m2 !! i = None → m1 ⊆ m2 → m1 !! i = None. `````` Robbert Krebbers committed Aug 21, 2012 89 90 91 92 93 94 ``````Proof. rewrite !eq_None_not_Some. firstorder. Qed. Lemma lookup_ne (m : M A) i j : m !! i ≠ m !! j → i ≠ j. Proof. congruence. Qed. Lemma not_elem_of_dom C `{Collection K C} (m : M A) i : i ∉ dom C m ↔ m !! i = None. `````` Robbert Krebbers committed Oct 19, 2012 95 ``````Proof. by rewrite (elem_of_dom C), eq_None_not_Some. Qed. `````` Robbert Krebbers committed Aug 21, 2012 96 97 `````` Lemma finmap_empty (m : M A) : (∀ i, m !! i = None) → m = ∅. `````` Robbert Krebbers committed Oct 19, 2012 98 ``````Proof. intros Hm. apply finmap_eq. intros. by rewrite Hm, lookup_empty. Qed. `````` Robbert Krebbers committed Aug 21, 2012 99 100 101 ``````Lemma dom_empty C `{Collection K C} : dom C (∅ : M A) ≡ ∅. Proof. split; intro. `````` Robbert Krebbers committed Oct 19, 2012 102 `````` * rewrite (elem_of_dom C), lookup_empty. by destruct 1. `````` Robbert Krebbers committed Aug 29, 2012 103 `````` * solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 104 105 106 107 ``````Qed. Lemma dom_empty_inv C `{Collection K C} (m : M A) : dom C m ≡ ∅ → m = ∅. Proof. intros E. apply finmap_empty. intros. apply (not_elem_of_dom C). `````` Robbert Krebbers committed Aug 29, 2012 108 `````` rewrite E. solve_elem_of. `````` Robbert Krebbers committed Aug 21, 2012 109 110 111 ``````Qed. Lemma lookup_empty_not i : ¬is_Some ((∅ : M A) !! i). `````` Robbert Krebbers committed Oct 19, 2012 112 ``````Proof. rewrite lookup_empty. by destruct 1. Qed. `````` Robbert Krebbers committed Aug 21, 2012 113 ``````Lemma lookup_empty_Some i (x : A) : ¬∅ !! i = Some x. `````` Robbert Krebbers committed Oct 19, 2012 114 ``````Proof. by rewrite lookup_empty. Qed. `````` Robbert Krebbers committed Aug 21, 2012 115 116 117 118 119 `````` Lemma partial_alter_compose (m : M A) i f g : partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m). Proof. intros. apply finmap_eq. intros ii. case (decide (i = ii)). `````` Robbert Krebbers committed Oct 19, 2012 120 121 `````` * intros. subst. by rewrite !lookup_partial_alter. * intros. by rewrite !lookup_partial_alter_ne. `````` Robbert Krebbers committed Aug 21, 2012 122 123 124 125 126 127 128 ``````Qed. Lemma partial_alter_comm (m : M A) i j f g : i ≠ j → partial_alter f i (partial_alter g j m) = partial_alter g j (partial_alter f i m). Proof. intros. apply finmap_eq. intros jj. destruct (decide (jj = j)). `````` Robbert Krebbers committed Oct 19, 2012 129 `````` * subst. by rewrite lookup_partial_alter_ne, `````` Robbert Krebbers committed Aug 21, 2012 130 131 `````` !lookup_partial_alter, lookup_partial_alter_ne. * destruct (decide (jj = i)). `````` Robbert Krebbers committed Oct 19, 2012 132 `````` + subst. by rewrite lookup_partial_alter, `````` Robbert Krebbers committed Aug 21, 2012 133 `````` !lookup_partial_alter_ne, lookup_partial_alter by congruence. `````` Robbert Krebbers committed Oct 19, 2012 134 `````` + by rewrite !lookup_partial_alter_ne by congruence. `````` Robbert Krebbers committed Aug 21, 2012 135 136 137 138 139 140 ``````Qed. Lemma partial_alter_self_alt (m : M A) i x : x = m !! i → partial_alter (λ _, x) i m = m. Proof. intros. apply finmap_eq. intros ii. destruct (decide (i = ii)). `````` Robbert Krebbers committed Oct 19, 2012 141 142 `````` * subst. by rewrite lookup_partial_alter. * by rewrite lookup_partial_alter_ne. `````` Robbert Krebbers committed Aug 21, 2012 143 144 ``````Qed. Lemma partial_alter_self (m : M A) i : partial_alter (λ _, m !! i) i m = m. `````` Robbert Krebbers committed Oct 19, 2012 145 ``````Proof. by apply partial_alter_self_alt. Qed. `````` Robbert Krebbers committed Aug 21, 2012 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 `````` Lemma lookup_insert (m : M A) i x : <[i:=x]>m !! i = Some x. Proof. unfold insert. apply lookup_partial_alter. Qed. Lemma lookup_insert_rev (m : M A) i x y : <[i:= x ]>m !! i = Some y → x = y. Proof. rewrite lookup_insert. congruence. Qed. Lemma lookup_insert_ne (m : M A) i j x : i ≠ j → <[i:=x]>m !! j = m !! j. Proof. unfold insert. apply lookup_partial_alter_ne. Qed. Lemma insert_comm (m : M A) i j x y : i ≠ j → <[i:=x]>(<[j:=y]>m) = <[j:=y]>(<[i:=x]>m). Proof. apply partial_alter_comm. Qed. Lemma lookup_insert_Some (m : M A) i j x y : <[i:=x]>m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠ j ∧ m !! j = Some y). Proof. split. * destruct (decide (i = j)); subst; rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence. * intros [[??]|[??]]. + subst. apply lookup_insert. `````` Robbert Krebbers committed Oct 19, 2012 165 `````` + by rewrite lookup_insert_ne. `````` Robbert Krebbers committed Aug 21, 2012 166 167 168 169 170 171 172 ``````Qed. Lemma lookup_insert_None (m : M A) i j x : <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠ j. Proof. split. * destruct (decide (i = j)); subst; rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence. `````` Robbert Krebbers committed Oct 19, 2012 173 `````` * intros [??]. by rewrite lookup_insert_ne. `````` Robbert Krebbers committed Aug 21, 2012 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 ``````Qed. Lemma lookup_singleton_Some i j (x y : A) : {[(i, x)]} !! j = Some y ↔ i = j ∧ x = y. Proof. unfold singleton, finmap_singleton. rewrite lookup_insert_Some, lookup_empty. simpl. intuition congruence. Qed. Lemma lookup_singleton_None i j (x : A) : {[(i, x)]} !! j = None ↔ i ≠ j. Proof. unfold singleton, finmap_singleton. rewrite lookup_insert_None, lookup_empty. simpl. tauto. Qed. `````` Robbert Krebbers committed Oct 19, 2012 189 190 191 192 193 ``````Lemma insert_singleton i (x y : A) : <[i:=y]>{[(i, x)]} = {[(i, y)]}. Proof. unfold singleton, finmap_singleton, insert, finmap_insert. by rewrite <-partial_alter_compose. Qed. `````` Robbert Krebbers committed Aug 21, 2012 194 195 `````` Lemma lookup_singleton i (x : A) : {[(i, x)]} !! i = Some x. `````` Robbert Krebbers committed Oct 19, 2012 196 ``````Proof. by rewrite lookup_singleton_Some. Qed. `````` Robbert Krebbers committed Aug 21, 2012 197 ``````Lemma lookup_singleton_ne i j (x : A) : i ≠ j → {[(i, x)]} !! j = None. `````` Robbert Krebbers committed Oct 19, 2012 198 ``````Proof. by rewrite lookup_singleton_None. Qed. `````` Robbert Krebbers committed Aug 21, 2012 199 200 201 202 203 204 205 206 207 208 209 210 `````` Lemma lookup_delete (m : M A) i : delete i m !! i = None. Proof. apply lookup_partial_alter. Qed. Lemma lookup_delete_ne (m : M A) i j : i ≠ j → delete i m !! j = m !! j. Proof. apply lookup_partial_alter_ne. Qed. Lemma lookup_delete_Some (m : M A) i j y : delete i m !! j = Some y ↔ i ≠ j ∧ m !! j = Some y. Proof. split. * destruct (decide (i = j)); subst; rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence. `````` Robbert Krebbers committed Oct 19, 2012 211 `````` * intros [??]. by rewrite lookup_delete_ne. `````` Robbert Krebbers committed Aug 21, 2012 212 213 214 215 216 217 218 219 220 221 ``````Qed. Lemma lookup_delete_None (m : M A) i j : delete i m !! j = None ↔ i = j ∨ m !! j = None. Proof. destruct (decide (i = j)). * subst. rewrite lookup_delete. tauto. * rewrite lookup_delete_ne; tauto. Qed. Lemma delete_empty i : delete i (∅ : M A) = ∅. `````` Robbert Krebbers committed Oct 19, 2012 222 ``````Proof. rewrite <-(partial_alter_self ∅) at 2. by rewrite lookup_empty. Qed. `````` Robbert Krebbers committed Aug 21, 2012 223 224 225 ``````Lemma delete_singleton i (x : A) : delete i {[(i, x)]} = ∅. Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed. Lemma delete_comm (m : M A) i j : delete i (delete j m) = delete j (delete i m). `````` Robbert Krebbers committed Oct 19, 2012 226 ``````Proof. destruct (decide (i = j)). by subst. by apply partial_alter_comm. Qed. `````` Robbert Krebbers committed Aug 21, 2012 227 228 ``````Lemma delete_insert_comm (m : M A) i j x : i ≠ j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m). `````` Robbert Krebbers committed Oct 19, 2012 229 ``````Proof. intro. by apply partial_alter_comm. Qed. `````` Robbert Krebbers committed Aug 21, 2012 230 231 232 233 234 `````` Lemma delete_notin (m : M A) i : m !! i = None → delete i m = m. Proof. intros. apply finmap_eq. intros j. destruct (decide (i = j)). `````` Robbert Krebbers committed Oct 19, 2012 235 236 `````` * subst. by rewrite lookup_delete. * by apply lookup_delete_ne. `````` Robbert Krebbers committed Aug 21, 2012 237 238 239 240 241 ``````Qed. Lemma delete_partial_alter (m : M A) i f : m !! i = None → delete i (partial_alter f i m) = m. Proof. `````` Robbert Krebbers committed Aug 29, 2012 242 `````` intros. unfold delete, finmap_delete. rewrite <-partial_alter_compose. `````` Robbert Krebbers committed Aug 21, 2012 243 244 `````` rapply partial_alter_self_alt. congruence. Qed. `````` Robbert Krebbers committed Aug 29, 2012 245 ``````Lemma delete_partial_alter_dom C `{Collection K C} (m : M A) i f : `````` Robbert Krebbers committed Aug 21, 2012 246 247 248 249 250 251 252 253 254 255 256 `````` i ∉ dom C m → delete i (partial_alter f i m) = m. Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed. Lemma delete_insert (m : M A) i x : m !! i = None → delete i (<[i:=x]>m) = m. Proof. apply delete_partial_alter. Qed. Lemma delete_insert_dom C `{Collection K C} (m : M A) i x : i ∉ dom C m → delete i (<[i:=x]>m) = m. Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed. Lemma insert_delete (m : M A) i x : m !! i = Some x → <[i:=x]>(delete i m) = m. Proof. intros Hmi. unfold delete, finmap_delete, insert, finmap_insert. rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi. `````` Robbert Krebbers committed Oct 19, 2012 257 `````` by apply partial_alter_self_alt. `````` Robbert Krebbers committed Aug 21, 2012 258 259 260 261 262 263 ``````Qed. Lemma elem_of_dom_delete C `{Collection K C} (m : M A) i j : i ∈ dom C (delete j m) ↔ i ≠ j ∧ i ∈ dom C m. Proof. rewrite !(elem_of_dom C). unfold is_Some. `````` Robbert Krebbers committed Oct 19, 2012 264 `````` setoid_rewrite lookup_delete_Some. naive_solver. `````` Robbert Krebbers committed Aug 21, 2012 265 266 267 268 ``````Qed. Lemma not_elem_of_dom_delete C `{Collection K C} (m : M A) i : i ∉ dom C (delete i m). Proof. apply (not_elem_of_dom C), lookup_delete. Qed. `````` Robbert Krebbers committed Jun 11, 2012 269 `````` `````` Robbert Krebbers committed Aug 29, 2012 270 271 272 273 274 275 276 277 278 279 280 281 ``````(** * Induction principles *) (** We use the induction principle on finite collections to prove the following induction principle on finite maps. *) Lemma finmap_ind_alt C (P : M A → Prop) `{FinCollection K C} : P ∅ → (∀ i x m, i ∉ dom C m → P m → P (<[i:=x]>m)) → ∀ m, P m. Proof. intros Hemp Hinsert m. apply (collection_ind (λ X, ∀ m, dom C m ≡ X → P m)) with (dom C m). * solve_proper. * clear m. intros m Hm. rewrite finmap_empty. `````` Robbert Krebbers committed Oct 19, 2012 282 `````` + done. `````` Robbert Krebbers committed Aug 29, 2012 283 `````` + intros. rewrite <-(not_elem_of_dom C), Hm. `````` Robbert Krebbers committed Oct 19, 2012 284 `````` by solve_elem_of. `````` Robbert Krebbers committed Aug 29, 2012 285 286 287 288 `````` * clear m. intros i X Hi IH m Hdom. assert (is_Some (m !! i)) as [x Hx]. { apply (elem_of_dom C). rewrite Hdom. clear Hdom. `````` Robbert Krebbers committed Oct 19, 2012 289 290 `````` by solve_elem_of. } rewrite <-(insert_delete m i x) by done. `````` Robbert Krebbers committed Aug 29, 2012 291 `````` apply Hinsert. `````` Robbert Krebbers committed Oct 19, 2012 292 `````` { by apply (not_elem_of_dom_delete C). } `````` Robbert Krebbers committed Aug 29, 2012 293 294 295 `````` apply IH. apply elem_of_equiv. intros. rewrite (elem_of_dom_delete C). esolve_elem_of. `````` Robbert Krebbers committed Oct 19, 2012 296 `````` * done. `````` Robbert Krebbers committed Aug 29, 2012 297 298 299 300 301 302 303 304 305 306 307 308 309 310 ``````Qed. (** We use the [listset] implementation to prove an induction principle that does not mention the map's domain. *) Lemma finmap_ind (P : M A → Prop) : P ∅ → (∀ i x m, m !! i = None → P m → P (<[i:=x]>m)) → ∀ m, P m. Proof. setoid_rewrite <-(not_elem_of_dom (listset _)). apply (finmap_ind_alt (listset _) P). Qed. (** * Deleting and inserting multiple elements *) `````` Robbert Krebbers committed Aug 21, 2012 311 312 313 ``````Lemma lookup_delete_list (m : M A) is j : In j is → delete_list is m !! j = None. Proof. `````` Robbert Krebbers committed Oct 19, 2012 314 `````` induction is as [|i is]; simpl; [done |]. `````` Robbert Krebbers committed Aug 21, 2012 315 `````` intros [?|?]. `````` Robbert Krebbers committed Oct 19, 2012 316 `````` * subst. by rewrite lookup_delete. `````` Robbert Krebbers committed Aug 21, 2012 317 `````` * destruct (decide (i = j)). `````` Robbert Krebbers committed Oct 19, 2012 318 `````` + subst. by rewrite lookup_delete. `````` Robbert Krebbers committed Aug 21, 2012 319 320 321 322 323 `````` + rewrite lookup_delete_ne; auto. Qed. Lemma lookup_delete_list_notin (m : M A) is j : ¬In j is → delete_list is m !! j = m !! j. Proof. `````` Robbert Krebbers committed Oct 19, 2012 324 `````` induction is; simpl; [done |]. `````` Robbert Krebbers committed Aug 21, 2012 325 326 327 328 329 330 `````` intros. rewrite lookup_delete_ne; tauto. Qed. Lemma delete_list_notin (m : M A) is : Forall (λ i, m !! i = None) is → delete_list is m = m. Proof. `````` Robbert Krebbers committed Oct 19, 2012 331 `````` induction 1; simpl; [done |]. `````` Robbert Krebbers committed Aug 21, 2012 332 333 334 335 336 `````` rewrite delete_notin; congruence. Qed. Lemma delete_list_insert_comm (m : M A) is j x : ¬In j is → delete_list is (<[j:=x]>m) = <[j:=x]>(delete_list is m). Proof. `````` Robbert Krebbers committed Oct 19, 2012 337 `````` induction is; simpl; [done |]. `````` Robbert Krebbers committed Aug 21, 2012 338 339 340 `````` intros. rewrite IHis, delete_insert_comm; tauto. Qed. `````` Robbert Krebbers committed Aug 29, 2012 341 342 ``````Lemma lookup_insert_list (m : M A) l1 l2 i x : (∀y, ¬In (i,y) l1) → insert_list (l1 ++ (i,x) :: l2) m !! i = Some x. `````` Robbert Krebbers committed Aug 21, 2012 343 ``````Proof. `````` Robbert Krebbers committed Aug 29, 2012 344 `````` induction l1 as [|[j y] l1 IH]; simpl. `````` Robbert Krebbers committed Oct 19, 2012 345 `````` * intros. by rewrite lookup_insert. `````` Robbert Krebbers committed Aug 29, 2012 346 347 348 349 350 351 352 `````` * intros Hy. rewrite lookup_insert_ne; naive_solver. Qed. Lemma lookup_insert_list_not_in (m : M A) l i : (∀y, ¬In (i,y) l) → insert_list l m !! i = m !! i. Proof. induction l as [|[j y] l IH]; simpl. `````` Robbert Krebbers committed Oct 19, 2012 353 `````` * done. `````` Robbert Krebbers committed Aug 29, 2012 354 `````` * intros Hy. rewrite lookup_insert_ne; naive_solver. `````` Robbert Krebbers committed Aug 21, 2012 355 356 ``````Qed. `````` Robbert Krebbers committed Aug 29, 2012 357 ``````(** * Properties of the merge operation *) `````` Robbert Krebbers committed Aug 21, 2012 358 359 360 361 ``````Section merge. Context (f : option A → option A → option A). Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f). `````` Robbert Krebbers committed Jun 11, 2012 362 `````` Proof. `````` Robbert Krebbers committed Aug 21, 2012 363 `````` intros ??. apply finmap_eq. intros. `````` Robbert Krebbers committed Oct 19, 2012 364 `````` by rewrite !(merge_spec f), lookup_empty, (left_id None f). `````` Robbert Krebbers committed Jun 11, 2012 365 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 366 `````` Global Instance: RightId (=) None f → RightId (=) ∅ (merge f). `````` Robbert Krebbers committed Jun 11, 2012 367 `````` Proof. `````` Robbert Krebbers committed Aug 21, 2012 368 `````` intros ??. apply finmap_eq. intros. `````` Robbert Krebbers committed Oct 19, 2012 369 `````` by rewrite !(merge_spec f), lookup_empty, (right_id None f). `````` Robbert Krebbers committed Jun 11, 2012 370 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 371 `````` Global Instance: Idempotent (=) f → Idempotent (=) (merge f). `````` Robbert Krebbers committed Oct 19, 2012 372 `````` Proof. intros ??. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed. `````` Robbert Krebbers committed Aug 21, 2012 373 374 375 376 377 `````` Context `{!PropHolds (f None None = None)}. Lemma merge_spec_alt m1 m2 m : (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m. `````` Robbert Krebbers committed Jun 11, 2012 378 `````` Proof. `````` Robbert Krebbers committed Aug 21, 2012 379 380 381 `````` split; [| intro; subst; apply (merge_spec _) ]. intros Hlookup. apply finmap_eq. intros. rewrite Hlookup. apply (merge_spec _). `````` Robbert Krebbers committed Jun 11, 2012 382 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 383 384 385 386 `````` Lemma merge_comm m1 m2 : (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) → merge f m1 m2 = merge f m2 m1. `````` Robbert Krebbers committed Oct 19, 2012 387 `````` Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed. `````` Robbert Krebbers committed Aug 21, 2012 388 `````` Global Instance: Commutative (=) f → Commutative (=) (merge f). `````` Robbert Krebbers committed Oct 19, 2012 389 `````` Proof. intros ???. apply merge_comm. intros. by apply (commutative f). Qed. `````` Robbert Krebbers committed Aug 21, 2012 390 391 `````` Lemma merge_assoc m1 m2 m3 : `````` Robbert Krebbers committed Aug 29, 2012 392 393 `````` (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) = f (f (m1 !! i) (m2 !! i)) (m3 !! i)) → `````` Robbert Krebbers committed Aug 21, 2012 394 `````` merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3. `````` Robbert Krebbers committed Oct 19, 2012 395 `````` Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed. `````` Robbert Krebbers committed Aug 21, 2012 396 `````` Global Instance: Associative (=) f → Associative (=) (merge f). `````` Robbert Krebbers committed Oct 19, 2012 397 `````` Proof. intros ????. apply merge_assoc. intros. by apply (associative f). Qed. `````` Robbert Krebbers committed Aug 21, 2012 398 399 ``````End merge. `````` Robbert Krebbers committed Aug 29, 2012 400 ``````(** * Properties of the union and intersection operation *) `````` Robbert Krebbers committed Aug 21, 2012 401 402 403 ``````Section union_intersection. Context (f : A → A → A). `````` Robbert Krebbers committed Oct 10, 2012 404 `````` Lemma finmap_union_with_merge m1 m2 i x y : `````` Robbert Krebbers committed Aug 29, 2012 405 406 407 `````` m1 !! i = Some x → m2 !! i = Some y → union_with f m1 m2 !! i = Some (f x y). `````` Robbert Krebbers committed Jun 14, 2012 408 `````` Proof. `````` Robbert Krebbers committed Oct 10, 2012 409 `````` intros Hx Hy. unfold union_with, finmap_union_with. `````` Robbert Krebbers committed Oct 19, 2012 410 `````` by rewrite (merge_spec _), Hx, Hy. `````` Robbert Krebbers committed Aug 29, 2012 411 `````` Qed. `````` Robbert Krebbers committed Oct 10, 2012 412 `````` Lemma finmap_union_with_l m1 m2 i x : `````` Robbert Krebbers committed Aug 21, 2012 413 `````` m1 !! i = Some x → m2 !! i = None → union_with f m1 m2 !! i = Some x. `````` Robbert Krebbers committed Jun 14, 2012 414 `````` Proof. `````` Robbert Krebbers committed Oct 10, 2012 415 `````` intros Hx Hy. unfold union_with, finmap_union_with. `````` Robbert Krebbers committed Oct 19, 2012 416 `````` by rewrite (merge_spec _), Hx, Hy. `````` Robbert Krebbers committed Jun 14, 2012 417 `````` Qed. `````` Robbert Krebbers committed Oct 10, 2012 418 `````` Lemma finmap_union_with_r m1 m2 i y : `````` Robbert Krebbers committed Aug 21, 2012 419 `````` m1 !! i = None → m2 !! i = Some y → union_with f m1 m2 !! i = Some y. `````` Robbert Krebbers committed Jun 11, 2012 420 `````` Proof. `````` Robbert Krebbers committed Oct 10, 2012 421 `````` intros Hx Hy. unfold union_with, finmap_union_with. `````` Robbert Krebbers committed Oct 19, 2012 422 `````` by rewrite (merge_spec _), Hx, Hy. `````` Robbert Krebbers committed Jun 11, 2012 423 `````` Qed. `````` Robbert Krebbers committed Oct 10, 2012 424 `````` Lemma finmap_union_with_None m1 m2 i : `````` Robbert Krebbers committed Aug 21, 2012 425 `````` union_with f m1 m2 !! i = None ↔ m1 !! i = None ∧ m2 !! i = None. `````` Robbert Krebbers committed Jun 11, 2012 426 `````` Proof. `````` Robbert Krebbers committed Oct 10, 2012 427 `````` unfold union_with, finmap_union_with. rewrite (merge_spec _). `````` Robbert Krebbers committed Aug 21, 2012 428 `````` destruct (m1 !! i), (m2 !! i); compute; intuition congruence. `````` Robbert Krebbers committed Jun 11, 2012 429 430 `````` Qed. `````` Robbert Krebbers committed Aug 21, 2012 431 432 433 434 435 436 437 438 439 `````` Global Instance: LeftId (=) ∅ (union_with f : M A → M A → M A) := _. Global Instance: RightId (=) ∅ (union_with f : M A → M A → M A) := _. Global Instance: Commutative (=) f → Commutative (=) (union_with f : M A → M A → M A) := _. Global Instance: Associative (=) f → Associative (=) (union_with f : M A → M A → M A) := _. Global Instance: Idempotent (=) f → Idempotent (=) (union_with f : M A → M A → M A) := _. End union_intersection. `````` Robbert Krebbers committed Oct 10, 2012 440 441 442 443 444 445 446 447 448 449 450 451 `````` Lemma finmap_union_Some (m1 m2 : M A) i x : (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x). Proof. unfold union, finmap_union, union_with, finmap_union_with. rewrite (merge_spec _). destruct (m1 !! i), (m2 !! i); compute; try intuition congruence. Qed. Lemma finmap_union_None (m1 m2 : M A) b : (m1 ∪ m2) !! b = None ↔ m1 !! b = None ∧ m2 !! b = None. Proof. apply finmap_union_with_None. Qed. `````` Robbert Krebbers committed Jun 11, 2012 452 ``````End finmap. `````` Robbert Krebbers committed Aug 21, 2012 453 `````` `````` Robbert Krebbers committed Aug 29, 2012 454 455 ``````(** * The finite map tactic *) (** The tactic [simplify_map by tac] simplifies finite map expressions `````` Robbert Krebbers committed Oct 19, 2012 456 ``````occuring in the conclusion and hypotheses. It uses [tac] to discharge generated `````` Robbert Krebbers committed Aug 29, 2012 457 ``````inequalities. *) `````` Robbert Krebbers committed Oct 19, 2012 458 ``````Tactic Notation "simplify_map" "by" tactic3(tac) := repeat `````` Robbert Krebbers committed Aug 21, 2012 459 `````` match goal with `````` Robbert Krebbers committed Oct 19, 2012 460 461 `````` | H1 : ?m !! ?i = Some ?x, H2 : ?m !! ?i = Some ?y |- _ => assert (x = y) by congruence; subst y; clear H2 `````` Robbert Krebbers committed Aug 21, 2012 462 463 `````` | H : context[ ∅ !! _ ] |- _ => rewrite lookup_empty in H | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert in H `````` Robbert Krebbers committed Oct 19, 2012 464 `````` | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert_ne in H by tac `````` Robbert Krebbers committed Aug 21, 2012 465 `````` | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete in H `````` Robbert Krebbers committed Oct 19, 2012 466 `````` | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete_ne in H by tac `````` Robbert Krebbers committed Aug 21, 2012 467 `````` | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton in H `````` Robbert Krebbers committed Oct 19, 2012 468 `````` | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton_ne in H by tac `````` Robbert Krebbers committed Aug 21, 2012 469 470 `````` | |- context[ ∅ !! _ ] => rewrite lookup_empty | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert `````` Robbert Krebbers committed Oct 19, 2012 471 `````` | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert_ne by tac `````` Robbert Krebbers committed Aug 21, 2012 472 `````` | |- context[ (delete _ _) !! _ ] => rewrite lookup_delete `````` Robbert Krebbers committed Oct 19, 2012 473 `````` | |- context[ (delete _ _) !! _ ] => rewrite lookup_delete_ne by tac `````` Robbert Krebbers committed Aug 21, 2012 474 `````` | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton `````` Robbert Krebbers committed Oct 19, 2012 475 `````` | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton_ne by tac `````` Robbert Krebbers committed Aug 21, 2012 476 477 `````` end. Tactic Notation "simplify_map" := simplify_map by auto. `````` Robbert Krebbers committed Oct 19, 2012 478 479 480 481 `````` Tactic Notation "simplify_map_equality" "by" tactic3(tac) := repeat first [ progress (simplify_map by tac) | progress simplify_equality ]. Tactic Notation "simplify_map_equality" := simplify_map_equality by auto.``````