hashset.v 7.86 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 file implements finite set using hash maps. Hash sets are represented
using radix-2 search trees. Each hash bucket is thus indexed using an binary
integer of type [Z], and contains an unordered list without duplicates. *)
6
7
Require Export prelude.fin_maps prelude.listset.
Require Import prelude.zmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

Record hashset {A} (hash : A  Z) := Hashset {
  hashset_car : Zmap (list A);
  hashset_prf :
    map_Forall (λ n l, Forall (λ x, hash x = n) l  NoDup l) hashset_car
}.
Arguments Hashset {_ _} _ _.
Arguments hashset_car {_ _} _.

Section hashset.
Context `{ x y : A, Decision (x = y)} (hash : A  Z).

Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m,  l,
  hashset_car m !! hash x = Some l  x  l.

Program Instance hashset_empty: Empty (hashset hash) := Hashset  _.
Next Obligation. by intros n X; simpl_map. Qed.
Program Instance hashset_singleton: Singleton A (hashset hash) := λ x,
26
  Hashset {[ hash x  [x] ]} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Next Obligation.
28
  intros x n l [<- <-]%lookup_singleton_Some.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
33
34
  rewrite Forall_singleton; auto using NoDup_singleton.
Qed.
Program Instance hashset_union: Union (hashset hash) := λ m1 m2,
  let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
  Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _. 
Next Obligation.
35
  intros _ _ m1 Hm1 m2 Hm2 n l'; rewrite lookup_union_with_Some.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
38
39
40
41
42
43
44
  intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_equality'; auto.
  split; [apply Forall_list_union|apply NoDup_list_union];
    first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
  let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
  Hashset (intersection_with (λ l k,
    let l' := list_intersection l k in guard (l'  []); Some l') m1 m2) _.
Next Obligation.
45
  intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_intersection_with_Some.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
48
49
50
51
52
53
54
  intros (?&?&?&?&?); simplify_option_equality.
  split; [apply Forall_list_intersection|apply NoDup_list_intersection];
    first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
  let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
  Hashset (difference_with (λ l k,
    let l' := list_difference l k in guard (l'  []); Some l') m1 m2) _.
Next Obligation.
55
  intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_difference_with_Some.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
  intros [[??]|(?&?&?&?&?)]; simplify_option_equality; auto.
  split; [apply Forall_list_difference|apply NoDup_list_difference];
    first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
Instance hashset_elems: Elements A (hashset hash) := λ m,
  map_to_list (hashset_car m) = snd.

Global Instance: FinCollection A (hashset hash).
Proof.
  split; [split; [split| |]| |].
  * intros ? (?&?&?); simplify_map_equality'.
  * unfold elem_of, hashset_elem_of, singleton, hashset_singleton; simpl.
    intros x y. setoid_rewrite lookup_singleton_Some. split.
    { by intros (?&[? <-]&?); decompose_elem_of_list. }
    intros ->; eexists [y]. by rewrite elem_of_list_singleton.
  * unfold elem_of, hashset_elem_of, union, hashset_union.
    intros [m1 Hm1] [m2 Hm2] x; simpl; setoid_rewrite lookup_union_with_Some.
    split.
    { intros (?&[[]|[[]|(l&k&?&?&?)]]&Hx); simplify_equality'; eauto.
      rewrite elem_of_list_union in Hx; destruct Hx; eauto. }
    intros [(l&?&?)|(k&?&?)].
    + destruct (m2 !! hash x) as [k|]; eauto.
      exists (list_union l k). rewrite elem_of_list_union. naive_solver.
    + destruct (m1 !! hash x) as [l|]; eauto 6.
      exists (list_union l k). rewrite elem_of_list_union. naive_solver.
  * unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
    intros [m1 ?] [m2 ?] x; simpl.
    setoid_rewrite lookup_intersection_with_Some. split.
    { intros (?&(l&k&?&?&?)&Hx); simplify_option_equality.
      rewrite elem_of_list_intersection in Hx; naive_solver. }
    intros [(l&?&?) (k&?&?)]. assert (x  list_intersection l k)
      by (by rewrite elem_of_list_intersection).
88
    exists (list_intersection l k); split; [exists l, k|]; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
91
92
93
94
95
96
97
    by rewrite option_guard_True by eauto using elem_of_not_nil.
  * unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
    intros [m1 ?] [m2 ?] x; simpl.
    setoid_rewrite lookup_difference_with_Some. split.
    { intros (l'&[[??]|(l&k&?&?&?)]&Hx); simplify_option_equality;
        rewrite ?elem_of_list_difference in Hx; naive_solver. }
    intros [(l&?&?) Hm2]; destruct (m2 !! hash x) as [k|] eqn:?; eauto.
    destruct (decide (x  k)); [destruct Hm2; eauto|].
    assert (x  list_difference l k) by (by rewrite elem_of_list_difference).
98
    exists (list_difference l k); split; [right; exists l,k|]; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
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
146
147
148
149
150
151
152
153
154
155
156
157
    by rewrite option_guard_True by eauto using elem_of_not_nil.
  * unfold elem_of at 2, hashset_elem_of, elements, hashset_elems.
    intros [m Hm] x; simpl. setoid_rewrite elem_of_list_bind. split.
    { intros ([n l]&Hx&Hn); simpl in *; rewrite elem_of_map_to_list in Hn.
      cut (hash x = n); [intros <-; eauto|].
      eapply (Forall_forall (λ x, hash x = n) l); eauto. eapply Hm; eauto. }
    intros (l&?&?). exists (hash x, l); simpl. by rewrite elem_of_map_to_list.
  * unfold elements, hashset_elems. intros [m Hm]; simpl.
    rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
    induction Hm as [|[n l] m' [??]];
      csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
    apply NoDup_app; split_ands; eauto.
    setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.
    assert (hash x = n  hash x = n') as [??]; subst.
    { split; [eapply (Forall_forall (λ x, hash x = n) l); eauto|].
      eapply (Forall_forall (λ x, hash x = n') l'); eauto.
      rewrite Forall_forall in Hm. eapply (Hm (_,_)); eauto. }
    destruct Hn; rewrite elem_of_list_fmap; exists (hash x, l'); eauto.
Qed.
End hashset.

(** These instances are declared using [Hint Extern] to avoid too
eager type class search. *)
Hint Extern 1 (ElemOf _ (hashset _)) =>
  eapply @hashset_elem_of : typeclass_instances.
Hint Extern 1 (Empty (hashset _)) =>
  eapply @hashset_empty : typeclass_instances.
Hint Extern 1 (Singleton _ (hashset _)) =>
  eapply @hashset_singleton : typeclass_instances.
Hint Extern 1 (Union (hashset _)) =>
  eapply @hashset_union : typeclass_instances.
Hint Extern 1 (Intersection (hashset _)) =>
  eapply @hashset_intersection : typeclass_instances.
Hint Extern 1 (Difference (hashset _)) =>
  eapply @hashset_difference : typeclass_instances.
Hint Extern 1 (Elements _ (hashset _)) =>
  eapply @hashset_elems : typeclass_instances.

Section remove_duplicates.
Context `{ x y : A, Decision (x = y)} (hash : A  Z).

Definition remove_dups_fast (l : list A) : list A :=
  match l with
  | [] => []
  | [x] => [x]
  | _ =>
     let n : Z := length l in
     elements (foldr (λ x, ({[ x ]} ))  l :
       hashset (λ x, hash x `mod` (2 * n))%Z)
  end.
Lemma elem_of_remove_dups_fast l x : x  remove_dups_fast l  x  l.
Proof.
  destruct l as [|x1 [|x2 l]]; try reflexivity.
  unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l.
  generalize (λ x, hash x `mod` (2 * length l))%Z; intros f.
  rewrite elem_of_elements; split.
  * revert x. induction l as [|y l IH]; intros x; simpl.
    { by rewrite elem_of_empty. }
    rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
158
  * induction 1; solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
161
162
163
164
165
166
167
168
169
170
171
Qed.
Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
Proof.
  unfold remove_dups_fast; destruct l as [|x1 [|x2 l]].
  apply NoDup_nil_2. apply NoDup_singleton. apply NoDup_elements.
Qed.
Definition listset_normalize (X : listset A) : listset A :=
  let (l) := X in Listset (remove_dups_fast l).
Lemma listset_normalize_correct X : listset_normalize X  X.
Proof.
  destruct X as [l]. apply elem_of_equiv; intro; apply elem_of_remove_dups_fast.
Qed.
End remove_duplicates.