Update the tests

4 files changed, 29 insertions, 34 deletions

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 7225d8a3..5954f048 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -704,11 +704,6 @@ inductive Location where
   /-- Same as Tactic.Location -/
   | targets (hypotheses : Array Syntax) (type : Bool)
 
-#check Tactic.simpLocation
-#check Tactic.Location
-#check MVarId.getNondepPropHyps
-#check simpLocation
-
 -- Adapted from Tactic.simpLocation
 def customSimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none)
   (loc : Location) : TacticM Simp.Stats := do
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index fcaf5806..5be778e7 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -137,15 +137,16 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (
     distinct_keys l1.v ∧
     -- We need this auxiliary property to prove that the keys distinct properties is preserved
     (∀ k, k ≠ key → l0.v.allP (λ (k1, _) => k ≠ k1) → l1.v.allP (λ (k1, _) => k ≠ k1))
-  :=
-  match l0 with
-  | .Nil => by
+  := by
+  cases l0 with
+  | Nil =>
     exists true -- TODO: why do we need to do this?
+    simp [insert_in_list]
+    rw [insert_in_list_loop]
     simp (config := {contextual := true})
-      [insert_in_list, insert_in_list_loop,
-       List.v, slot_s_inv_hash, distinct_keys, List.pairwise_rel]
-  | .Cons k v tl0 =>
-     if h: k = key then by
+      [List.v, slot_s_inv_hash, distinct_keys, List.pairwise_rel]
+  | Cons k v tl0 =>
+     if h: k = key then
        rw [insert_in_list]
        rw [insert_in_list_loop]
        simp [h]
@@ -157,21 +158,21 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (
        . simp [*, distinct_keys] at *
          apply hdk
        . tauto
-     else by
+     else
        rw [insert_in_list]
        rw [insert_in_list_loop]
        simp [h]
-       have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by checkpoint
+       have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by
          simp_all [List.v, slot_s_inv_hash]
-       have : distinct_keys (List.v tl0) := by checkpoint
+       have : distinct_keys (List.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
-       have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by checkpoint
+       have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by
          simp [List.v, slot_s_inv_hash] at *
          simp [*]
-       have : distinct_keys ((k, v) :: List.v tl1) := by checkpoint
+       have : distinct_keys ((k, v) :: List.v tl1) := by
          simp [distinct_keys] at *
          simp [*]
        -- TODO: canonize addition by default?
@@ -231,7 +232,6 @@ def mk_opaque {α : Sort u} (x : α) : { y : α // y = x}  :=
 --set_option trace.profiler true
 
 -- For pretty printing (useful when copy-pasting goals)
-attribute [pp_dot] List.length -- use the dot notation when printing
 set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse)
 
 -- The proof below is a bit expensive, so we need to increase the maximum number
@@ -305,7 +305,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
   -- zeta reduction? For now I have to do this peculiar manipulation
   have ⟨ nhm, nhm_eq ⟩ := @mk_opaque (HashMap α) { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v }
   exists nhm
-  have hupdt : lookup nhm key = some value := by checkpoint
+  have hupdt : lookup nhm key = some value := by
     simp [lookup, List.lookup] at *
     simp_all
   have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by
@@ -340,7 +340,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
   have _ :
     match hm.lookup key with
     | none => nhm.len_s = hm.len_s + 1
-    | some _ => nhm.len_s = hm.len_s := by checkpoint
+    | some _ => nhm.len_s = hm.len_s := by
     simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_t_lookup] at *
     -- We have to do a case disjunction
     simp_all
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
index 404d3dab..b1c3c9dc 100644
--- a/tests/lean/lake-manifest.json
+++ b/tests/lean/lake-manifest.json
@@ -1,11 +1,11 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
-   "name": "std",
+   "rev": "f96a34401de084c73c787ecb45b85d4fb47bb981",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,25 +22,25 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.36",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,16 +49,16 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "d9c412b8103b5098bf8b66cbb981b81a57375925",
+   "rev": "c9f95f42b82684937a26ba395ebf7f25a81734ca",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain
index 9ad30404..0ba3faf8 100644
--- a/tests/lean/lean-toolchain
+++ b/tests/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.9.0-rc1