Library Diqt.Radix
Radix tree for hashtable
Section Radix.
Variable A: Set.
Variable eq: A → A → bool.
Variable eq_spec: ∀ x y : A, reflect (x = y) (eq x y).
Variable B: Set.
Variable hash: A → positive.
Inductive bucket : Set :=
| B_Empty : bucket
| B_Cons : positive → A → B → bucket → bucket.
Inductive tree : Type :=
| Empty: tree
| Node: tree → bucket → tree → tree.
Definition empty : tree := Empty.
Fixpoint get (p: positive) (t: tree) : bucket :=
match p, t with
| _, Empty ⇒ B_Empty
| xH, Node _ e _ ⇒ e
| xO p', Node l _ _ ⇒ get p' l
| xI p', Node _ _ r ⇒ get p' r
end.
Fixpoint set0 (p: positive) (e: bucket) : tree :=
match p with
| xH ⇒ Node Empty e Empty
| xO p' ⇒ Node (set0 p' e) B_Empty Empty
| xI p' ⇒ Node Empty B_Empty (set0 p' e)
end.
Fixpoint set (p: positive) (e: bucket) (t: tree) : tree :=
match p, t with
| _, Empty ⇒ set0 p e
| xH, Node l _ r ⇒ Node l e r
| xO p', Node l y r ⇒ Node (set p' e l) y r
| xI p', Node l y r ⇒ Node l y (set p' e r)
end.
Theorem gempty:
∀ (i: positive), get i empty = B_Empty.
Theorem gss0:
∀ (i: positive) (x: bucket), get i (set0 i x) = x.
Theorem gos0:
∀ (i j: positive) (x: bucket),
i ≠ j → get i (set0 j x) = B_Empty.
Theorem gss:
∀ (i: positive) (x: bucket) (t: tree), get i (set i x t) = x.
Theorem gso:
∀ (i j: positive) (x: bucket) (t: tree),
i ≠ j → get i (set j x t) = get i t.
Fixpoint find_rec l h k: option B :=
match l with
| B_Empty ⇒ None
| B_Cons h' k' v tl ⇒
if if h =? h' then eq k k' else false
then Some v
else find_rec tl h k
end.
Definition find (t: tree) (k: A) : option B :=
let h := hash k in
find_rec (get h t) h k.
Fixpoint find_all_rec (l: bucket) (h: positive) (k: A) (acc: list B): list B :=
match l with
| B_Empty ⇒ List.rev' acc
| B_Cons h' k' v l' ⇒
if if h =? h' then eq k k' else false
then find_all_rec l' h k (v :: acc)
else find_all_rec l' h k acc
end.
Definition mem (h: tree) (key: A) : bool :=
match find h key with
| Some _ ⇒ true
| None ⇒ false
end.
Definition find_all (d: tree) (k: A) : list B :=
let h_k := hash k in
find_all_rec (get h_k d) h_k k nil.
Definition add (d: tree) (k: A) (e: B) : tree :=
let h_k := hash k in
match get h_k d with
| B_Empty ⇒ set h_k (B_Cons h_k k e B_Empty) d
| b ⇒ set h_k (B_Cons h_k k e b) d
end.
Fixpoint bucket_remove (b: bucket) (h: positive) (k: A) :=
match b with
| B_Empty ⇒ B_Empty
| B_Cons h' k' v b ⇒
if if h =? h' then eq k k' else false
then b
else B_Cons h' k' v (bucket_remove b h k)
end.
Definition remove (d: tree) (k: A) : tree :=
let h := hash k in
match get h d with
| B_Empty ⇒ d
| b ⇒ set h (bucket_remove b h k) d
end.
Definition replace (d: tree) (k: A) (e: B) : tree :=
let h := hash k in
match get h d with
| B_Empty ⇒ set h (B_Cons h k e B_Empty) d
| b ⇒ set h (B_Cons h k e (bucket_remove b h k)) d
end.
Lemma eq_true:
∀ (k1 k2 : A), k1 = k2 → eq k1 k2 = true.
Lemma eq_false:
∀ (k1 k2 : A), k1 ≠ k2 → eq k1 k2 = false.
Lemma eq_refl:
∀ (k : A), k = k → eq k k = true.
find_all
Fixpoint find_all_rec' (l: bucket) (h: positive) (k: A) : list B :=
match l with
| B_Empty ⇒ nil
| B_Cons h' k' v l' ⇒
if if h =? h' then eq k k' else false
then v :: find_all_rec' l' h k
else find_all_rec' l' h k
end.
Lemma find_all_rec_correct:
∀ (l: bucket) (h: positive) (key: A) acc,
find_all_rec l h key acc = rev acc ++ find_all_rec' l h key.
empty
add
Theorem find_add_same:
∀ (d: tree) (k: A) (v: B),
find_all (add d k v) k = v :: find_all d k.
Theorem find_add_other:
∀ (d: tree) (k k': A) (v: B),
k' ≠ k → find_all (add d k v) k' = find_all d k'.
find
remove
Lemma bucket_remove_same:
∀ (b: bucket) (k: A),
let h := hash k in
find_all_rec (bucket_remove b h k) h k [] =
List.tl (find_all_rec b h k []).
Lemma bucket_remove_other:
∀ (b: bucket) (k k': A),
let h := hash k in
let h' := hash k' in
k' ≠ k →
find_all_rec (bucket_remove b h k) h' k' [] =
find_all_rec b h' k' [].
Theorem remove_same:
∀ (t: tree) (k: A),
find_all (remove t k) k =
List.tl (find_all t k).
Theorem remove_other:
∀ (t: tree) (k: A) (k': A),
k' ≠ k →
find_all (remove t k) k' = find_all t k'.
replace