diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 30 | ||||
| -rw-r--r-- | tests/lean/lake-manifest.json | 26 | ||||
| -rw-r--r-- | tests/lean/lean-toolchain | 2 |
3 files changed, 29 insertions, 29 deletions
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 |