Skip to content
Snippets Groups Projects
Commit ed1ccaf3 authored by Hai Dang's avatar Hai Dang
Browse files

bump to master

parent 7a2b18fd
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/examples/abs_hashtable.v
+ 4
− 3
View file @ ed1ccaf3
...@@ -162,8 +162,9 @@ Lemma index_of'_spec (k : Z) (m: list Z) : ...@@ -162,8 +162,9 @@ Lemma index_of'_spec (k : Z) (m: list Z) :
Proof. Proof.
destruct (index_of' m k) as [i|] eqn:Eq. destruct (index_of' m k) as [i|] eqn:Eq.
- apply bind_Some in Eq as [[??] [Eq1 Eq2]]. simpl in Eq2. simplify_eq. - apply bind_Some in Eq as [[??] [Eq1 Eq2]]. simpl in Eq2. simplify_eq.
destruct (list_find_Some _ _ _ _ Eq1) as [Eq2 Eq3]. have FA := list_find_slice _ _ _ _ Eq1.
have FA := list_find_slice _ _ _ _ Eq1. repeat split. apply list_find_Some in Eq1 as [Eq2 Eq3].
repeat split.
+ by eapply lookup_lt_Some. + by eapply lookup_lt_Some.
+ apply (nth_lookup_Some _ _ 0%Z) in Eq2. naive_solver. + apply (nth_lookup_Some _ _ 0%Z) in Eq2. naive_solver.
+ eapply Forall_impl; last eauto. move => /= z0. naive_solver. + eapply Forall_impl; last eauto. move => /= z0. naive_solver.
...@@ -246,7 +247,7 @@ Qed. ...@@ -246,7 +247,7 @@ Qed.
Section Hashtable. Section Hashtable.
Context {hf : hash_fun}. Context {hf : hash_fun}.
Hint Resolve size_pos hash_range. Hint Resolve size_pos hash_range : core.
Definition hlookup (m : list Z) (k : Z) := Definition hlookup (m : list Z) (k : Z) :=
(index_of' (rebase m (hash k)) k) ≫= (λ i, Some $ (i + hash k) `mod` size). (index_of' (rebase m (hash k)) k) ≫= (λ i, Some $ (i + hash k) `mod` size).
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment