Commit a925aea6 by Robbert Krebbers

### Use 2*size hash buckets.

parent 8a43c1bb
 ... @@ -142,15 +142,15 @@ Definition remove_dups_fast (l : list A) : list A := ... @@ -142,15 +142,15 @@ Definition remove_dups_fast (l : list A) : list A := | [] => [] | [] => [] | [x] => [x] | [x] => [x] | _ => | _ => let n :Z := length l in let n : Z := length l in elements (foldr (λ x, ({[ x ]} ∪)) ∅ l : elements (foldr (λ x, ({[ x ]} ∪)) ∅ l : hashset (λ x, hash x `mod` n)%Z) hashset (λ x, hash x `mod` (2 * n))%Z) end. end. Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l. Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l. Proof. Proof. destruct l as [|x1 [|x2 l]]; try reflexivity. destruct l as [|x1 [|x2 l]]; try reflexivity. unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l. unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l. generalize (λ x, hash x `mod` length l)%Z; intros f. generalize (λ x, hash x `mod` (2 * length l))%Z; intros f. rewrite elem_of_elements; split. rewrite elem_of_elements; split. * revert x. induction l as [|y l IH]; intros x; simpl. * revert x. induction l as [|y l IH]; intros x; simpl. { by rewrite elem_of_empty. } { by rewrite elem_of_empty. } ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!