summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2023-07-25 11:53:49 +0200
committerSon Ho2023-07-25 11:53:49 +0200
commit2dd56a51df01421fe7766858c9d37998db4123b5 (patch)
treef34ec2b4ccce04c6bfa5eb8e670a663a05d56e73 /tests
parentc5536f372194240d164583cecee5265213b3e671 (diff)
Improve the syntax of progress: `as ⟨ x, y .. ⟩`
Diffstat (limited to 'tests')
-rw-r--r--tests/lean/Hashmap/Properties.lean34
1 files changed, 4 insertions, 30 deletions
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index dce33fa4..de6bf636 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -94,7 +94,7 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α)
simp only [insert_in_list]
rw [insert_in_list_loop]
conv => rhs; ext; simp [*]
- progress keep as heq as ⟨ b hi ⟩
+ progress keep as heq as ⟨ b, hi ⟩
simp only [insert_in_list] at heq
exists b
@@ -116,35 +116,9 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α)
conv => rhs; ext; left; simp [h] -- TODO: Simplify
simp only [insert_in_list] at ih;
-- TODO: give the possibility of using underscores
- progress as ⟨ b h ⟩
+ progress as ⟨ b, h ⟩
simp [*]
-theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List α) :
- ∃ l1,
- insert_in_list_back α key value l0 = ret l1 ∧
- -- We update the binding
- l1.lookup key = value ∧
- (∀ k, k ≠ key → l1.lookup k = l0.lookup k)
- := match l0 with
- | .Nil => by
- simp (config := {contextual := true}) [insert_in_list_back, insert_in_list_loop_back]
- | .Cons k v tl =>
- if h: k = key then
- by
- simp [insert_in_list_back]
- rw [insert_in_list_loop_back]
- simp [h]
- intro k1 h1
- simp [*]
- else
- by
- simp [insert_in_list_back]
- rw [insert_in_list_loop_back]
- simp [h]
- progress keep as heq as ⟨ tl hp1 hp2 ⟩
- simp [insert_in_list_back] at heq
- simp (config := {contextual := true}) [*]
-
def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x.fst ≠ y.fst)
def hash_mod_key (k : Usize) (l : Int) : Int :=
@@ -190,7 +164,7 @@ theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value:
simp [insert_in_list_back]
rw [insert_in_list_loop_back]
simp [h]
- split_target_conjs
+ split_conjs
. intros; simp [*]
. simp [List.v, slot_s_inv_hash] at *
simp [*]
@@ -206,7 +180,7 @@ theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value:
have : distinct_keys (List.v tl0) := by checkpoint
simp [distinct_keys] at hdk
simp [hdk, distinct_keys]
- progress keep as heq as ⟨ tl1 hp1 hp2 hp3 hp4 hp5 hp6 ⟩
+ progress keep as heq as ⟨ tl1 .. ⟩
simp only [insert_in_list_back] at heq
have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by checkpoint
simp [List.v, slot_s_inv_hash] at *