From 1021cdea98043dd935dbc8dbe633b90fda68047d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jun 2024 07:15:26 +0200
Subject: Update the tests

---
 tests/lean/Hashmap/Funs.lean       | 8 ++++++++
 tests/lean/Hashmap/Properties.lean | 3 +--
 2 files changed, 9 insertions(+), 2 deletions(-)

(limited to 'tests/lean/Hashmap')

diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 7d8f73a7..f5d028db 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -28,6 +28,7 @@ divergent def HashMap.allocate_slots_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
    Source: 'tests/src/hashmap.rs', lines 61:4-61:78 -/
+@[reducible]
 def HashMap.allocate_slots
   (T : Type) (slots : alloc.vec.Vec (AList T)) (n : Usize) :
   Result (alloc.vec.Vec (AList T))
@@ -106,6 +107,7 @@ divergent def HashMap.insert_in_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
    Source: 'tests/src/hashmap.rs', lines 108:4-108:72 -/
+@[reducible]
 def HashMap.insert_in_list
   (T : Type) (key : Usize) (value : T) (ls : AList T) :
   Result (Bool × (AList T))
@@ -150,6 +152,7 @@ divergent def HashMap.move_elements_from_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
    Source: 'tests/src/hashmap.rs', lines 194:4-194:73 -/
+@[reducible]
 def HashMap.move_elements_from_list
   (T : Type) (ntable : HashMap T) (ls : AList T) : Result (HashMap T) :=
   HashMap.move_elements_from_list_loop T ntable ls
@@ -177,6 +180,7 @@ divergent def HashMap.move_elements_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements]:
    Source: 'tests/src/hashmap.rs', lines 182:4-182:96 -/
+@[reducible]
 def HashMap.move_elements
   (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) (i : Usize)
   :
@@ -234,6 +238,7 @@ divergent def HashMap.contains_key_in_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]:
    Source: 'tests/src/hashmap.rs', lines 217:4-217:69 -/
+@[reducible]
 def HashMap.contains_key_in_list
   (T : Type) (key : Usize) (ls : AList T) : Result Bool :=
   HashMap.contains_key_in_list_loop T key ls
@@ -265,6 +270,7 @@ divergent def HashMap.get_in_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::get_in_list]:
    Source: 'tests/src/hashmap.rs', lines 235:4-235:71 -/
+@[reducible]
 def HashMap.get_in_list (T : Type) (key : Usize) (ls : AList T) : Result T :=
   HashMap.get_in_list_loop T key ls
 
@@ -306,6 +312,7 @@ divergent def HashMap.get_mut_in_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
    Source: 'tests/src/hashmap.rs', lines 256:4-256:87 -/
+@[reducible]
 def HashMap.get_mut_in_list
   (T : Type) (ls : AList T) (key : Usize) :
   Result (T × (T → Result (AList T)))
@@ -356,6 +363,7 @@ divergent def HashMap.remove_from_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
    Source: 'tests/src/hashmap.rs', lines 276:4-276:70 -/
+@[reducible]
 def HashMap.remove_from_list
   (T : Type) (key : Usize) (ls : AList T) : Result ((Option T) × (AList T)) :=
   HashMap.remove_from_list_loop T key ls
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index a2fa0d7d..29b5834b 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -165,8 +165,7 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (
        have : distinct_keys (AList.v tl0) := by
          simp [distinct_keys] at hdk
          simp [hdk, distinct_keys]
-       progress keep heq as ⟨ b, tl1 .. ⟩
-       simp only [insert_in_list] at heq
+       progress as ⟨ b, tl1 .. ⟩
        have : slot_s_inv_hash l (hash_mod_key key l) (AList.v (AList.Cons k v tl1)) := by
          simp [AList.v, slot_s_inv_hash] at *
          simp [*]
-- 
cgit v1.2.3