mapset.v 5.77 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
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. *)
6
From iris.prelude Require Export fin_map_dom.
Robbert Krebbers's avatar
Robbert Krebbers committed
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,
20
  Mapset {[ x := () ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 | | ].
40
  - unfold empty, elem_of, mapset_empty, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
    simpl. intros. by simpl_map.
42
  - unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
43
    simpl. by split; intros; simplify_map_eq.
44
  - unfold union, elem_of, mapset_union, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46
    intros [m1] [m2] ?. simpl. rewrite lookup_union_Some_raw.
    destruct (m1 !! x) as [[]|]; tauto.
47
  - unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
52
  - unfold difference, elem_of, mapset_difference, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54 55
    intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
    destruct (m2 !! x) as [[]|]; intuition congruence.
Qed.
56 57
Global Instance: LeibnizEquiv (mapset M).
Proof. intros ??. apply mapset_eq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59 60
Global Instance: FinCollection K (mapset M).
Proof.
  split.
61 62
  - apply _.
  - unfold elements, elem_of at 2, mapset_elems, mapset_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
66
  - unfold elements, mapset_elems. intros [m]. simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68 69
    apply NoDup_fst_map_to_list.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
Section deciders.
  Context `{ m1 m2 : M unit, Decision (m1 = m2)}.
  Global Instance mapset_eq_dec (X1 X2 : mapset M) : Decision (X1 = X2) | 1.
  Proof.
   refine
    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.

Robbert Krebbers's avatar
Robbert Krebbers committed
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|].
118 119
  - destruct (Is_true_reflect (f a)); naive_solver.
  - naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.