From Coq Require Import ZArith List Bool.

Require Radix.

Import ListNotations.

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

  Parameter hash: A → positive.
End HashP.

Module HashTablePositive (T: HashP).
  Definition t := @Radix.tree T.A.
  Definition create (B: Set) : t B :=
    Radix.empty T.A B.

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

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

  Definition find_all {B: Set} (h: t B) (k: T.A) : list B :=
    Radix.find_all T.A T.eq B T.hash h k.

  Definition mem {B: Set} (h: t B) (k: T.A) : bool :=
    Radix.mem T.A T.eq B T.hash h k.

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

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

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

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

  Theorem mem_spec:
    ∀ B (ht: t B) k v,
    (find ht k = Some v → mem ht k = true) ∧
    (find ht k = None → mem ht k = 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_same:
    ∀ B (ht: t B) k v,
    find_all (replace ht k v) k = v :: (List.tl (find_all ht 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 HashTablePositive.