hashset.v 7.79 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
2 3 4 5
(* 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
Require Export fin_maps listset.
7 8 9 10 11 12 13 14 15 16 17
Require Import zmap.

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.
18
Context `{ x y : A, Decision (x = y)} (hash : A  Z).
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 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 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108

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,
  Hashset {[ hash x, [x] ]} _.
Next Obligation.
  intros n l. rewrite lookup_singleton_Some. intros [<- <-].
  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.
  intros n l'. rewrite lookup_union_with_Some.
  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.
  intros n l'. rewrite lookup_intersection_with_Some.
  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.
  intros n l'. rewrite lookup_difference_with_Some.
  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).
    exists (list_intersection l k); split; [exists l k|]; split_ands; auto.
    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).
    exists (list_difference l k); split; [right; exists l k|]; split_ands; auto.
    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' [??]];
109
      csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
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
    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.
136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171

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` 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` 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.
  * induction 1; esolve_elem_of.
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.