summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
authorSon Ho2023-07-26 15:00:29 +0200
committerSon Ho2023-07-26 15:00:29 +0200
commit31de6eb8a82e17b4113262a18abf61e6233b55df (patch)
tree885e66d652b5383b1c34ceb04532eb096fd6b30d /tests/lean
parent3337c4ac3326c3132dcc322f55f23a7d2054ceb0 (diff)
Make a minor modification to a hashmap proof
Diffstat (limited to '')
-rw-r--r--tests/lean/Hashmap/Properties.lean14
1 files changed, 9 insertions, 5 deletions
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 5d340b5c..ee63a065 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -271,6 +271,10 @@ theorem if_update_eq
:= by
split <;> simp [Pure.pure]
+-- TODO: move: small helper
+def mk_opaque {α : Sort u} (x : α) : { y : α // y = x} :=
+ ⟨ x, by simp ⟩
+
theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α)
(hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) :
∃ nhm, hm.insert_no_resize α key value = ret nhm ∧
@@ -342,10 +346,10 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
progress as ⟨ l0, _, _, _, hlen .. ⟩
progress keep hv as ⟨ v, h_veq ⟩
-- TODO: update progress to automate that
- let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v }
- exists nhm
-- TODO: later I don't want to inline nhm - we need to control simp: deactivate
- -- zeta reduction?
+ -- 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
simp [lookup, List.lookup] at *
simp_all
@@ -406,7 +410,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
. simp [slots_t_inv, slot_t_inv] at *
intro i hipos _
have _ := hinv.right.left i hipos (by simp_all)
- simp [hhm, h_veq] at * -- TODO: annoying, we do that because simp_all fails below
+ simp [hhm, h_veq, nhm_eq] at * -- TODO: annoying, we do that because simp_all fails below
-- We need a case disjunction
if h_ieq : i = key.val % _root_.List.len hm.slots.val then
-- TODO: simp_all fails: "(deterministic) timeout at 'whnf'"
@@ -419,7 +423,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
else
simp [*]
. -- TODO: simp[*] fails: "(deterministic) timeout at 'whnf'"
- simp [hinv, h_veq]
+ simp [hinv, h_veq, nhm_eq]
simp_all
end HashMap