summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2024-04-05 14:04:25 +0200
committerSon Ho2024-04-05 14:04:25 +0200
commit65a77968d0abc2d01da92aa8982256855e7519a6 (patch)
tree5db0aaddd797ab769dcc72f46094fc6f3dc3b8a5 /tests
parentfc0b39c4fe48fdbab06d5fd32e0a2b7dcae674e6 (diff)
Update the lean toolchain and fix the proofs
Diffstat (limited to '')
-rw-r--r--tests/lean/Hashmap/Properties.lean20
-rw-r--r--tests/lean/lake-manifest.json18
-rw-r--r--tests/lean/lean-toolchain2
3 files changed, 24 insertions, 16 deletions
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 7215e286..4e0ca509 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -113,6 +113,10 @@ def inv (hm : HashMap α) : Prop :=
-- This rewriting lemma is problematic below
attribute [-simp] Bool.exists_bool
+-- The proof below is a bit expensive, so we need to increase the maximum number
+-- of heart beats
+set_option maxHeartbeats 1000000
+
theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α)
(hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
(hdk : distinct_keys l0.v) :
@@ -232,7 +236,7 @@ set_option pp.coercions false -- do not print coercions with ↑ (this doesn't p
-- The proof below is a bit expensive, so we need to increase the maximum number
-- of heart beats
-set_option maxHeartbeats 1000000
+set_option maxHeartbeats 2000000
theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α)
(hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) :
@@ -318,17 +322,21 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
simp_all
have _ : 0 ≤ k_hash_mod := by
-- TODO: we want to automate this
- simp
+ simp only [k_hash_mod]
apply Int.emod_nonneg k.val hvnz
have _ : k_hash_mod < alloc.vec.Vec.length hm.slots := by
-- TODO: we want to automate this
- simp
+ simp only [k_hash_mod]
have h := Int.emod_lt_of_pos k.val hvpos
- simp_all
+ simp_all only [ret.injEq, exists_eq_left', List.len_update, gt_iff_lt,
+ List.index_update_eq, ne_eq, not_false_eq_true, neq_imp]
if h_hm : k_hash_mod = hash_mod.val then
- simp_all
+ simp_all only [k_hash_mod, List.len_update, gt_iff_lt, List.index_update_eq,
+ ne_eq, not_false_eq_true, neq_imp, alloc.vec.Vec.length]
else
- simp_all
+ simp_all only [k_hash_mod, List.len_update, gt_iff_lt, List.index_update_eq,
+ ne_eq, not_false_eq_true, neq_imp, ge_iff_le,
+ alloc.vec.Vec.length, List.index_update_ne]
have _ :
match hm.lookup key with
| none => nhm.len_s = hm.len_s + 1
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
index e167e841..404d3dab 100644
--- a/tests/lean/lake-manifest.json
+++ b/tests/lean/lake-manifest.json
@@ -4,7 +4,7 @@
[{"url": "https://github.com/leanprover/std4",
"type": "git",
"subDir": null,
- "rev": "276953b13323ca151939eafaaec9129bf7970306",
+ "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
"name": "std",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@@ -13,7 +13,7 @@
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
- "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+ "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
@@ -22,7 +22,7 @@
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
- "rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
+ "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
@@ -31,16 +31,16 @@
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
- "rev": "af1e86cf7a37389632a02f4a111e6b501b2b818f",
+ "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
- "inputRev": "v0.0.27",
+ "inputRev": "v0.0.30",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
- "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+ "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@@ -49,7 +49,7 @@
{"url": "https://github.com/leanprover-community/import-graph.git",
"type": "git",
"subDir": null,
- "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+ "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@@ -58,7 +58,7 @@
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
- "rev": "d04f8d39c0e47a0d73450b49f6c0665897cdcaf7",
+ "rev": "d9c412b8103b5098bf8b66cbb981b81a57375925",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": null,
@@ -70,5 +70,5 @@
"inherited": false,
"dir": "./../../backends/lean",
"configFile": "lakefile.lean"}],
- "name": "Tests",
+ "name": "tests",
"lakeDir": ".lake"}
diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain
index f96d662e..9ad30404 100644
--- a/tests/lean/lean-toolchain
+++ b/tests/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.7.0