(* 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. *) From iris.prelude Require Export fin_map_dom. 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, Mapset {[ x := () ]}. 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 | | ]. - unfold empty, elem_of, mapset_empty, mapset_elem_of. simpl. intros. by simpl_map. - unfold singleton, elem_of, mapset_singleton, mapset_elem_of. simpl. by split; intros; simplify_map_eq. - unfold union, elem_of, mapset_union, mapset_elem_of. intros [m1] [m2] ?. simpl. rewrite lookup_union_Some_raw. destruct (m1 !! x) as [[]|]; tauto. - unfold intersection, elem_of, mapset_intersection, mapset_elem_of. intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some. assert (is_Some (m2 !! x) ↔ m2 !! x = Some ()). { split; eauto. by intros [[] ?]. } naive_solver. - unfold difference, elem_of, mapset_difference, mapset_elem_of. intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some. destruct (m2 !! x) as [[]|]; intuition congruence. Qed. Global Instance: LeibnizEquiv (mapset M). Proof. intros ??. apply mapset_eq. Qed. Global Instance: FinCollection K (mapset M). Proof. split. - apply _. - unfold elements, elem_of at 2, mapset_elems, mapset_elem_of. 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. - unfold elements, mapset_elems. intros [m]. simpl. apply NoDup_fst_map_to_list. Qed. Section deciders. Context `{EqDecision (M unit)}. Global Instance mapset_eq_dec : EqDecision (mapset M) | 1. Proof. refine (λ X1 X2, match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end); 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. 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|]. - destruct (Is_true_reflect (f a)); naive_solver. - naive_solver. 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.