From Coq Require Import List Uint63 Bool.

Require Table.

Import ListNotations.

Open Scope uint63_scope.

Module Type HashI.
  Parameter A: Set.
  Parameter eq: A → A → bool.
  Parameter eq_spec: ∀ x y : A, reflect (x = y) (eq x y).

  Parameter hash: A → int.
End HashI.

Module HashTable (T: HashI).
  Definition t := @Table.t T.A.
  Definition create (B: Set) (initial_size: int) : t B :=
    @Table.create T.A B initial_size.

  Definition add {B: Set} (h: t B) (key: T.A) (v: B) :=
    Table.add T.hash h key v.

  Definition find {B: Set} (h: t B) (key: T.A): option B :=
    Table.find T.eq T.hash h key.

  Definition find_all {B: Set} (h: t B) (key: T.A) :=
    Table.find_all T.eq T.hash h key.

  Definition mem {B: Set} (h: t B) (key: T.A) :=
    Table.mem T.eq T.hash h key.

  Definition remove {B: Set} (h: t B) (key: T.A) :=
    Table.remove T.eq T.hash h key.

  Definition replace {B: Set} (h: t B) (key: T.A) (v: B) :=
    Table.replace T.eq T.hash h key v.

  Theorem find_spec:
    ∀ B (ht: t B) key,
    find ht key = List.hd_error (find_all ht key).

  Theorem find_empty:
    ∀ B k s, find (create B s) k = None.

  Theorem mem_spec:
    ∀ B (ht: t B) key v,
    (find ht key = Some v → mem ht key = true) ∧
    (find ht key = None → mem ht key = false).

  Theorem add_same:
    ∀ B (h: t B) k v,
    find_all (add h k v) k = v :: (find_all h k).

  Theorem add_other:
    ∀ B (h: t B) k k' v,
    k' ≠ k → find_all (add h k v) k' = find_all h k'.

  Theorem remove_same:
    ∀ B (t: t B) k,
    find_all (remove t k) k = List.tl (find_all t k).

  Theorem remove_other:
    ∀ B (t: t B) k k',
    k' ≠ k → find_all (remove t k) k' = find_all t k'.

  Theorem replace_other:
    ∀ B (ht: t B) k1 k2 v,
    k1 ≠ k2 → find_all (replace ht k1 v) k2 = find_all ht k2.

End HashTable.