From ed1ccaf3a21fa6d724b048e3014f2af0202ef605 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 3 Dec 2019 15:20:11 +0100
Subject: [PATCH] bump to master
---
theories/examples/abs_hashtable.v | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/theories/examples/abs_hashtable.v b/theories/examples/abs_hashtable.v
index 3ef61ba0..6fb5d1e5 100644
--- a/theories/examples/abs_hashtable.v
+++ b/theories/examples/abs_hashtable.v
@@ -162,8 +162,9 @@ Lemma index_of'_spec (k : Z) (m: list Z) :
Proof.
destruct (index_of' m k) as [i|] eqn: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. repeat split.
+ have FA := list_find_slice _ _ _ _ Eq1.
+ apply list_find_Some in Eq1 as [Eq2 Eq3].
+ repeat split.
+ by eapply lookup_lt_Some.
+ apply (nth_lookup_Some _ _ 0%Z) in Eq2. naive_solver.
+ eapply Forall_impl; last eauto. move => /= z0. naive_solver.
@@ -246,7 +247,7 @@ Qed.
Section Hashtable.
Context {hf : hash_fun}.
-Hint Resolve size_pos hash_range.
+Hint Resolve size_pos hash_range : core.
Definition hlookup (m : list Z) (k : Z) :=
(index_of' (rebase m (hash k)) k) ≫= (λ i, Some $ (i + hash k) `mod` size).
--
GitLab