hashset.v 7.18 KB
Newer Older
1
2
3
(** 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. *)
4
5
From stdpp Require Export fin_maps listset.
From stdpp Require Import zmap.
6
Set Default Proof Using "Type".
7
8
9
10
11
12

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
}.
13
14
Arguments Hashset {_ _} _ _ : assert.
Arguments hashset_car {_ _} _ : assert.
15
16

Section hashset.
17
Context `{EqDecision A} (hash : A  Z).
18

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

22
Global Program Instance hashset_empty: Empty (hashset hash) := Hashset  _.
23
Next Obligation. by intros n X; simpl_map. Qed.
24
Global Program Instance hashset_singleton: Singleton A (hashset hash) := λ x,
25
  Hashset {[ hash x := [x] ]} _.
26
Next Obligation.
27
  intros x n l [<- <-]%lookup_singleton_Some.
28
29
  rewrite Forall_singleton; auto using NoDup_singleton.
Qed.
30
Global Program Instance hashset_union: Union (hashset hash) := λ m1 m2,
31
  let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
Michael Sammler's avatar
Michael Sammler committed
32
  Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _.
33
Next Obligation.
34
  intros _ _ m1 Hm1 m2 Hm2 n l'; rewrite lookup_union_with_Some.
35
  intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_eq/=; auto.
36
37
38
  split; [apply Forall_list_union|apply NoDup_list_union];
    first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
39
Global Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
40
41
42
43
  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.
44
  intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_intersection_with_Some.
45
  intros (?&?&?&?&?); simplify_option_eq.
46
47
48
  split; [apply Forall_list_intersection|apply NoDup_list_intersection];
    first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
49
Global Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
50
51
52
53
  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.
54
  intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_difference_with_Some.
55
  intros [[??]|(?&?&?&?&?)]; simplify_option_eq; auto.
56
57
58
  split; [apply Forall_list_difference|apply NoDup_list_difference];
    first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
59
Global Instance hashset_elements: Elements A (hashset hash) := λ m,
60
61
  map_to_list (hashset_car m) = snd.

62
Global Instance hashset_fin_set : FinSet A (hashset hash).
63
64
Proof.
  split; [split; [split| |]| |].
65
  - intros ? (?&?&?); simplify_map_eq/=.
66
  - unfold elem_of, hashset_elem_of, singleton, hashset_singleton; simpl.
67
68
69
    intros x y. setoid_rewrite lookup_singleton_Some. split.
    { by intros (?&[? <-]&?); decompose_elem_of_list. }
    intros ->; eexists [y]. by rewrite elem_of_list_singleton.
70
  - unfold elem_of, hashset_elem_of, union, hashset_union.
71
72
    intros [m1 Hm1] [m2 Hm2] x; simpl; setoid_rewrite lookup_union_with_Some.
    split.
73
    { intros (?&[[]|[[]|(l&k&?&?&?)]]&Hx); simplify_eq/=; eauto.
74
75
76
77
78
79
      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.
80
  - unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
81
82
    intros [m1 ?] [m2 ?] x; simpl.
    setoid_rewrite lookup_intersection_with_Some. split.
83
    { intros (?&(l&k&?&?&?)&Hx); simplify_option_eq.
84
85
86
      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).
87
    exists (list_intersection l k); split; [exists l, k|]; split_and?; auto.
88
    by rewrite option_guard_True by eauto using elem_of_not_nil.
89
  - unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
90
91
    intros [m1 ?] [m2 ?] x; simpl.
    setoid_rewrite lookup_difference_with_Some. split.
92
    { intros (l'&[[??]|(l&k&?&?&?)]&Hx); simplify_option_eq;
93
94
95
96
        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).
97
    exists (list_difference l k); split; [right; exists l,k|]; split_and?; auto.
98
    by rewrite option_guard_True by eauto using elem_of_not_nil.
99
  - unfold elem_of at 2, hashset_elem_of, elements, hashset_elements.
100
101
102
103
104
    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.
105
  - unfold elements, hashset_elements. intros [m Hm]; simpl.
106
    rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
107
    (* FIXME: trailing [?] works around Coq bug #12944. *)
108
    induction Hm as [|[n l] m' [??] Hm ?];
109
      csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
110
    apply NoDup_app; split_and?; eauto.
111
112
113
114
115
116
117
118
119
    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.

120
121
Typeclasses Opaque hashset_elem_of.

122
Section remove_duplicates.
123
Context `{EqDecision A} (hash : A  Z).
124
125
126
127
128
129

Definition remove_dups_fast (l : list A) : list A :=
  match l with
  | [] => []
  | [x] => [x]
  | _ =>
Robbert Krebbers's avatar
Robbert Krebbers committed
130
     let n : Z := length l in
131
     elements (foldr (λ x, ({[ x ]} .))  l :
Robbert Krebbers's avatar
Robbert Krebbers committed
132
       hashset (λ x, hash x `mod` (2 * n))%Z)
133
134
135
136
137
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
  generalize (λ x, hash x `mod` (2 * length l))%Z; intros f.
139
  rewrite elem_of_elements; split.
140
  - revert x. induction l as [|y l IH]; intros x; simpl.
141
142
    { by rewrite elem_of_empty. }
    rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
143
  - induction 1; set_solver.
144
145
146
147
148
149
150
151
152
153
154
155
156
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.