(* stdpp/hashset.v *)
Instance hashset_fin_set : FinSet A (hashset hash).
Proof.
  split; [split; [split| |]| |].
  - intros ? (?&?&?); simplify_map_eq/=.
  - unfold elem_of, hashset_elem_of, singleton, hashset_singleton; simpl.
    intros x y. setoid_rewrite lookup_singleton_Some. split.
    { by intros (?&[? <-]&?); decompose_list_elem_of. }
    intros ->; eexists [y]. by rewrite list_elem_of_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_eq/=; eauto.
      rewrite list_elem_of_union in Hx; destruct Hx; eauto. }
    intros [(l&?&?)|(k&?&?)].
    + destruct (m2 !! hash x) as [k|]; eauto.
      exists (list_union l k). rewrite list_elem_of_union. naive_solver.
    + destruct (m1 !! hash x) as [l|]; eauto 6.
      exists (list_union l k). rewrite list_elem_of_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_eq.
      rewrite list_elem_of_intersection in Hx; naive_solver. }
    intros [(l&?&?) (k&?&?)]. assert (x ∈ list_intersection l k)
      by (by rewrite list_elem_of_intersection).
    exists (list_intersection l k); split; [exists l, k|]; split_and?; 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_eq;
        rewrite ?list_elem_of_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 list_elem_of_difference).
    exists (list_difference l k); split; [right; exists l,k|]; split_and?; auto.
    by rewrite option_guard_True by eauto using elem_of_not_nil.
  - unfold elem_of at 2, hashset_elem_of, elements, hashset_elements.
    intros [m Hm] x; simpl. setoid_rewrite list_elem_of_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_elements. intros [m Hm]; simpl.
    rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
    induction Hm as [|[n l] m' [??] Hm];
      csimpl; inv 1 as [|?? Hn]; [constructor|].
    apply NoDup_app; split_and?; eauto.
    setoid_rewrite list_elem_of_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 list_elem_of_fmap; exists (hash x, l'); eauto.
Qed.