fin_map_dom.v 4.39 KB
 Robbert Krebbers committed Feb 08, 2015 1 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) `````` Robbert Krebbers committed Feb 19, 2013 2 3 4 5 6 7 ``````(* This file is distributed under the terms of the BSD license. *) (** This file provides an axiomatization of the domain function of finite maps. We provide such an axiomatization, instead of implementing the domain function in a generic way, to allow more efficient implementations. *) Require Export collections fin_maps. `````` Robbert Krebbers committed May 02, 2014 8 9 10 11 12 ``````Class FinMapDom K M D `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A), ∀ i j : K, Decision (i = j), ∀ A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D, Union D, Intersection D, Difference D} := { `````` Robbert Krebbers committed Feb 19, 2013 13 14 15 16 17 `````` finmap_dom_map :>> FinMap K M; finmap_dom_collection :>> Collection K D; elem_of_dom {A} (m : M A) i : i ∈ dom D m ↔ is_Some (m !! i) }. `````` Robbert Krebbers committed May 07, 2013 18 ``````Section fin_map_dom. `````` Robbert Krebbers committed Feb 19, 2013 19 20 ``````Context `{FinMapDom K M D}. `````` Robbert Krebbers committed May 02, 2014 21 22 ``````Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom D m. Proof. rewrite elem_of_dom; eauto. Qed. `````` Robbert Krebbers committed May 07, 2013 23 ``````Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom D m ↔ m !! i = None. `````` Robbert Krebbers committed Feb 19, 2013 24 ``````Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed. `````` Robbert Krebbers committed May 07, 2013 25 ``````Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom D m1 ⊆ dom D m2. `````` Robbert Krebbers committed Feb 19, 2013 26 ``````Proof. `````` Robbert Krebbers committed May 02, 2014 27 28 `````` rewrite map_subseteq_spec. intros ??. rewrite !elem_of_dom. inversion 1; eauto. `````` Robbert Krebbers committed Feb 19, 2013 29 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 30 ``````Lemma subset_dom {A} (m1 m2 : M A) : m1 ⊂ m2 → dom D m1 ⊂ dom D m2. `````` Robbert Krebbers committed Feb 19, 2013 31 ``````Proof. `````` Robbert Krebbers committed May 02, 2014 32 33 34 35 `````` intros [Hss1 Hss2]; split; [by apply subseteq_dom |]. contradict Hss2. rewrite map_subseteq_spec. intros i x Hi. specialize (Hss2 i). rewrite !elem_of_dom in Hss2. destruct Hss2; eauto. by simplify_map_equality. `````` Robbert Krebbers committed Feb 19, 2013 36 37 38 ``````Qed. Lemma dom_empty {A} : dom D (@empty (M A) _) ≡ ∅. Proof. `````` Robbert Krebbers committed May 02, 2014 39 40 `````` split; intro; [|solve_elem_of]. rewrite elem_of_dom, lookup_empty. by inversion 1. `````` Robbert Krebbers committed Feb 19, 2013 41 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 42 ``````Lemma dom_empty_inv {A} (m : M A) : dom D m ≡ ∅ → m = ∅. `````` Robbert Krebbers committed Feb 19, 2013 43 44 45 46 ``````Proof. intros E. apply map_empty. intros. apply not_elem_of_dom. rewrite E. solve_elem_of. Qed. `````` Robbert Krebbers committed May 07, 2013 47 ``````Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m. `````` Robbert Krebbers committed Feb 19, 2013 48 ``````Proof. `````` Robbert Krebbers committed May 15, 2013 49 50 `````` apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom. unfold is_Some. setoid_rewrite lookup_insert_Some. `````` Robbert Krebbers committed Feb 19, 2013 51 52 `````` destruct (decide (i = j)); esolve_elem_of. Qed. `````` Robbert Krebbers committed May 07, 2013 53 ``````Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m). `````` Robbert Krebbers committed Feb 19, 2013 54 55 ``````Proof. rewrite (dom_insert _). solve_elem_of. Qed. Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X : `````` Robbert Krebbers committed May 07, 2013 56 `````` X ⊆ dom D m → X ⊆ dom D (<[i:=x]>m). `````` Robbert Krebbers committed Feb 19, 2013 57 ``````Proof. intros. transitivity (dom D m); eauto using dom_insert_subseteq. Qed. `````` Robbert Krebbers committed May 07, 2013 58 ``````Lemma dom_singleton {A} (i : K) (x : A) : dom D {[(i, x)]} ≡ {[ i ]}. `````` Robbert Krebbers committed Feb 19, 2013 59 60 61 62 ``````Proof. unfold singleton at 1, map_singleton. rewrite dom_insert, dom_empty. solve_elem_of. Qed. `````` Robbert Krebbers committed May 07, 2013 63 ``````Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}. `````` Robbert Krebbers committed Feb 19, 2013 64 ``````Proof. `````` Robbert Krebbers committed May 15, 2013 65 66 `````` apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom. unfold is_Some. setoid_rewrite lookup_delete_Some. esolve_elem_of. `````` Robbert Krebbers committed Feb 19, 2013 67 68 69 70 71 72 73 ``````Qed. Lemma delete_partial_alter_dom {A} (m : M A) i f : i ∉ dom D m → delete i (partial_alter f i m) = m. Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed. Lemma delete_insert_dom {A} (m : M A) i x : i ∉ dom D m → delete i (<[i:=x]>m) = m. Proof. rewrite not_elem_of_dom. apply delete_insert. Qed. `````` Robbert Krebbers committed May 07, 2013 74 ``````Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ⊥ m2 ↔ dom D m1 ∩ dom D m2 ≡ ∅. `````` Robbert Krebbers committed Feb 19, 2013 75 ``````Proof. `````` Robbert Krebbers committed May 02, 2014 76 77 `````` rewrite map_disjoint_spec, elem_of_equiv_empty. setoid_rewrite elem_of_intersection. `````` Robbert Krebbers committed May 15, 2013 78 `````` setoid_rewrite elem_of_dom. unfold is_Some. naive_solver. `````` Robbert Krebbers committed Feb 19, 2013 79 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 80 ``````Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ⊥ m2 → dom D m1 ∩ dom D m2 ≡ ∅. `````` Robbert Krebbers committed Feb 19, 2013 81 ``````Proof. apply map_disjoint_dom. Qed. `````` Robbert Krebbers committed May 07, 2013 82 ``````Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ∩ dom D m2 ≡ ∅ → m1 ⊥ m2. `````` Robbert Krebbers committed Feb 19, 2013 83 ``````Proof. apply map_disjoint_dom. Qed. `````` Robbert Krebbers committed May 07, 2013 84 ``````Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 ∪ m2) ≡ dom D m1 ∪ dom D m2. `````` Robbert Krebbers committed Feb 19, 2013 85 ``````Proof. `````` Robbert Krebbers committed May 15, 2013 86 87 88 `````` apply elem_of_equiv. intros i. rewrite elem_of_union, !elem_of_dom. unfold is_Some. setoid_rewrite lookup_union_Some_raw. destruct (m1 !! i); naive_solver. `````` Robbert Krebbers committed Feb 19, 2013 89 90 91 92 ``````Qed. Lemma dom_intersection {A} (m1 m2 : M A) : dom D (m1 ∩ m2) ≡ dom D m1 ∩ dom D m2. Proof. `````` Robbert Krebbers committed May 15, 2013 93 94 `````` apply elem_of_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom. unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver. `````` Robbert Krebbers committed Feb 19, 2013 95 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 96 ``````Lemma dom_difference {A} (m1 m2 : M A) : dom D (m1 ∖ m2) ≡ dom D m1 ∖ dom D m2. `````` Robbert Krebbers committed Feb 19, 2013 97 ``````Proof. `````` Robbert Krebbers committed May 15, 2013 98 99 100 `````` apply elem_of_equiv. intros i. rewrite elem_of_difference, !elem_of_dom. unfold is_Some. setoid_rewrite lookup_difference_Some. destruct (m2 !! i); naive_solver. `````` Robbert Krebbers committed Feb 19, 2013 101 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 102 ``End fin_map_dom.``