From 78a2731924aa13989998c6be4a5a6865ce5098aa Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Sep 2023 07:33:30 +0200
Subject: Make minor modifications

---
 tests/lean/Hashmap/Properties.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'tests/lean/Hashmap/Properties.lean')

diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index ab95b854..6bc821d3 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -303,19 +303,17 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
    | some _ => nhm.len_s = hm.len_s) := by
   rw [insert_no_resize]
   simp only [hash_key, bind_tc_ret] -- TODO: annoying
-  have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint
+  have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by
    intro
    simp_all [inv]
-  progress keep _ as ⟨ hash_mod, hhm ⟩
-  have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac
+  progress as ⟨ hash_mod, hhm ⟩
+  have _ : 0 ≤ hash_mod.val := by scalar_tac
   have _ : hash_mod.val < Vec.length hm.slots := by
     have : 0 < hm.slots.val.len := by
       simp [inv] at hinv
       simp [hinv]
     -- TODO: we want to automate that
     simp [*, Int.emod_lt_of_pos]
-  -- TODO: change the spec of Vec.index_mut to introduce a let-binding.
-  -- or: make progress introduce the let-binding by itself (this is clearer)
   progress as ⟨ l, h_leq ⟩
   -- TODO: make progress use the names written in the goal
   progress as ⟨ inserted ⟩
-- 
cgit v1.2.3


From 00705bba68fed61d3b0bcde2c5fe0ecc83880870 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 18:37:07 +0100
Subject: Update the failing proofs

---
 tests/lean/Hashmap/Properties.lean | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'tests/lean/Hashmap/Properties.lean')

diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 4db54316..e79c422d 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -157,7 +157,7 @@ instance : Inhabited (List α) where
 def slots_s_inv (s : Core.List (List α)) : Prop :=
   ∀ (i : Int), 0 ≤ i → i < s.len → slot_t_inv s.len i (s.index i)
 
-def slots_t_inv (s : Vec (List α)) : Prop :=
+def slots_t_inv (s : alloc.vec.Vec (List α)) : Prop :=
   slots_s_inv s.v
 
 @[simp]
@@ -302,13 +302,14 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
    | none => nhm.len_s = hm.len_s + 1
    | some _ => nhm.len_s = hm.len_s) := by
   rw [insert_no_resize]
-  simp only [hash_key, bind_tc_ret] -- TODO: annoying
-  have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by
+  -- Simplify. Note that this also simplifies some function calls, like array index
+  simp [hash_key, bind_tc_ret]
+  have _ : (alloc.vec.Vec.len (List α) hm.slots).val ≠ 0 := by
    intro
    simp_all [inv]
   progress as ⟨ hash_mod, hhm ⟩
   have _ : 0 ≤ hash_mod.val := by scalar_tac
-  have _ : hash_mod.val < Vec.length hm.slots := by
+  have _ : hash_mod.val < alloc.vec.Vec.length hm.slots := by
     have : 0 < hm.slots.val.len := by
       simp [inv] at hinv
       simp [hinv]
@@ -374,7 +375,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
       -- TODO: we want to automate this
       simp
       apply Int.emod_nonneg k.val hvnz
-    have _ : k_hash_mod < Vec.length hm.slots := by
+    have _ : k_hash_mod < alloc.vec.Vec.length hm.slots := by
       -- TODO: we want to automate this
       simp
       have h := Int.emod_lt_of_pos k.val hvpos
-- 
cgit v1.2.3