mapset.v 5.75 KB
 Robbert Krebbers committed Nov 11, 2015 1 2 3 4 5 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This files gives an implementation of finite sets using finite maps with elements of the unit type. Since maps enjoy extensional equality, the constructed finite sets do so as well. *) `````` Robbert Krebbers committed Mar 10, 2016 6 ``````From iris.prelude Require Export fin_map_dom. `````` Robbert Krebbers committed Nov 11, 2015 7 8 9 10 11 12 13 14 15 16 17 18 19 `````` Record mapset (M : Type → Type) : Type := Mapset { mapset_car: M (unit : Type) }. Arguments Mapset {_} _. Arguments mapset_car {_} _. Section mapset. Context `{FinMap K M}. Instance mapset_elem_of: ElemOf K (mapset M) := λ x X, mapset_car X !! x = Some (). Instance mapset_empty: Empty (mapset M) := Mapset ∅. Instance mapset_singleton: Singleton K (mapset M) := λ x, `````` Robbert Krebbers committed Feb 17, 2016 20 `````` Mapset {[ x := () ]}. `````` Robbert Krebbers committed Nov 11, 2015 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 ``````Instance mapset_union: Union (mapset M) := λ X1 X2, let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∪ m2). Instance mapset_intersection: Intersection (mapset M) := λ X1 X2, let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∩ m2). Instance mapset_difference: Difference (mapset M) := λ X1 X2, let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∖ m2). Instance mapset_elems: Elements K (mapset M) := λ X, let (m) := X in (map_to_list m).*1. Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2. Proof. split; [by intros ->|]. destruct X1 as [m1], X2 as [m2]. simpl. intros E. f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E. Qed. Instance: Collection K (mapset M). Proof. split; [split | | ]. `````` Robbert Krebbers committed Feb 17, 2016 40 `````` - unfold empty, elem_of, mapset_empty, mapset_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 41 `````` simpl. intros. by simpl_map. `````` Robbert Krebbers committed Feb 17, 2016 42 `````` - unfold singleton, elem_of, mapset_singleton, mapset_elem_of. `````` Robbert Krebbers committed Feb 17, 2016 43 `````` simpl. by split; intros; simplify_map_eq. `````` Robbert Krebbers committed Feb 17, 2016 44 `````` - unfold union, elem_of, mapset_union, mapset_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 45 46 `````` intros [m1] [m2] ?. simpl. rewrite lookup_union_Some_raw. destruct (m1 !! x) as [[]|]; tauto. `````` Robbert Krebbers committed Feb 17, 2016 47 `````` - unfold intersection, elem_of, mapset_intersection, mapset_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 48 49 50 51 `````` intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some. assert (is_Some (m2 !! x) ↔ m2 !! x = Some ()). { split; eauto. by intros [[] ?]. } naive_solver. `````` Robbert Krebbers committed Feb 17, 2016 52 `````` - unfold difference, elem_of, mapset_difference, mapset_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 53 54 55 `````` intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some. destruct (m2 !! x) as [[]|]; intuition congruence. Qed. `````` Robbert Krebbers committed Jul 22, 2016 56 57 ``````Global Instance: LeibnizEquiv (mapset M). Proof. intros ??. apply mapset_eq. Qed. `````` Robbert Krebbers committed Nov 11, 2015 58 59 60 ``````Global Instance: FinCollection K (mapset M). Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 61 62 `````` - apply _. - unfold elements, elem_of at 2, mapset_elems, mapset_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 63 64 65 `````` intros [m] x. simpl. rewrite elem_of_list_fmap. split. + intros ([y []] &?& Hy). subst. by rewrite <-elem_of_map_to_list. + intros. exists (x, ()). by rewrite elem_of_map_to_list. `````` Robbert Krebbers committed Feb 17, 2016 66 `````` - unfold elements, mapset_elems. intros [m]. simpl. `````` Robbert Krebbers committed Nov 11, 2015 67 68 69 `````` apply NoDup_fst_map_to_list. Qed. `````` Robbert Krebbers committed Jul 22, 2016 70 ``````Section deciders. `````` Robbert Krebbers committed Sep 20, 2016 71 72 `````` Context `{EqDecision (M unit)}. Global Instance mapset_eq_dec : EqDecision (mapset M) | 1. `````` Robbert Krebbers committed Jul 22, 2016 73 `````` Proof. `````` Robbert Krebbers committed Sep 20, 2016 74 75 `````` refine (λ X1 X2, match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end); `````` Robbert Krebbers committed Jul 22, 2016 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 `````` abstract congruence. Defined. Global Instance mapset_equiv_dec (X1 X2 : mapset M) : Decision (X1 ≡ X2) | 1. Proof. refine (cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined. Global Instance mapset_elem_of_dec x (X : mapset M) : Decision (x ∈ X) | 1. Proof. solve_decision. Defined. Global Instance mapset_disjoint_dec (X1 X2 : mapset M) : Decision (X1 ⊥ X2). Proof. refine (cast_if (decide (X1 ∩ X2 = ∅))); abstract (by rewrite disjoint_intersection_L). Defined. Global Instance mapset_subseteq_dec (X1 X2 : mapset M) : Decision (X1 ⊆ X2). Proof. refine (cast_if (decide (X1 ∪ X2 = X2))); abstract (by rewrite subseteq_union_L). Defined. End deciders. `````` Robbert Krebbers committed Nov 11, 2015 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 ``````Definition mapset_map_with {A B} (f : bool → A → option B) (X : mapset M) : M A → M B := let (mX) := X in merge (λ x y, match x, y with | Some _, Some a => f true a | None, Some a => f false a | _, None => None end) mX. Definition mapset_dom_with {A} (f : A → bool) (m : M A) : mapset M := Mapset \$ merge (λ x _, match x with | Some a => if f a then Some () else None | None => None end) m (@empty (M A) _). Lemma lookup_mapset_map_with {A B} (f : bool → A → option B) X m i : mapset_map_with f X m !! i = m !! i ≫= f (bool_decide (i ∈ X)). Proof. destruct X as [mX]. unfold mapset_map_with, elem_of, mapset_elem_of. rewrite lookup_merge by done. simpl. by case_bool_decide; destruct (mX !! i) as [[]|], (m !! i). Qed. Lemma elem_of_mapset_dom_with {A} (f : A → bool) m i : i ∈ mapset_dom_with f m ↔ ∃ x, m !! i = Some x ∧ f x. Proof. unfold mapset_dom_with, elem_of, mapset_elem_of. simpl. rewrite lookup_merge by done. destruct (m !! i) as [a|]. `````` Robbert Krebbers committed Feb 17, 2016 118 119 `````` - destruct (Is_true_reflect (f a)); naive_solver. - naive_solver. `````` Robbert Krebbers committed Nov 11, 2015 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 ``````Qed. Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true). Instance mapset_dom_spec: FinMapDom K M (mapset M). Proof. split; try apply _. intros. unfold dom, mapset_dom, is_Some. rewrite elem_of_mapset_dom_with; naive_solver. Qed. End mapset. (** These instances are declared using [Hint Extern] to avoid too eager type class search. *) Hint Extern 1 (ElemOf _ (mapset _)) => eapply @mapset_elem_of : typeclass_instances. Hint Extern 1 (Empty (mapset _)) => eapply @mapset_empty : typeclass_instances. Hint Extern 1 (Singleton _ (mapset _)) => eapply @mapset_singleton : typeclass_instances. Hint Extern 1 (Union (mapset _)) => eapply @mapset_union : typeclass_instances. Hint Extern 1 (Intersection (mapset _)) => eapply @mapset_intersection : typeclass_instances. Hint Extern 1 (Difference (mapset _)) => eapply @mapset_difference : typeclass_instances. Hint Extern 1 (Elements _ (mapset _)) => eapply @mapset_elems : typeclass_instances. Arguments mapset_eq_dec _ _ _ _ : simpl never.``````