summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean47
-rw-r--r--tests/lean/Hashmap/Properties.lean58
2 files changed, 83 insertions, 22 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 3beb7527..2e5be8bf 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -660,10 +660,8 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
simp [h] at hx hy
have hmin : 0 ≤ x.val % y.val := Int.emod_nonneg x.val hnz
have hmax : x.val % y.val ≤ Scalar.max ty := by
- have h := @Int.ediv_emod_unique x.val y.val (x.val % y.val) (x.val / y.val)
- simp at h
- have : 0 < y.val := by int_tac
- simp [*] at h
+ have h : 0 < y.val := by int_tac
+ have h := Int.emod_lt_of_pos x.val h
have := y.hmax
linarith
have hs := @rem_spec ty x y hnz
@@ -724,6 +722,47 @@ def U32.ofInt := @Scalar.ofInt .U32
def U64.ofInt := @Scalar.ofInt .U64
def U128.ofInt := @Scalar.ofInt .U128
+-- TODO: factor those lemmas out
+@[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofInt x h).val = x := by
+ simp [Scalar.ofInt, Scalar.ofIntCore]
+
+@[simp] theorem Isize.ofInt_val_eq (h : Scalar.min ScalarTy.Isize ≤ x ∧ x ≤ Scalar.max ScalarTy.Isize) : (Isize.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I8.ofInt_val_eq (h : Scalar.min ScalarTy.I8 ≤ x ∧ x ≤ Scalar.max ScalarTy.I8) : (I8.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I16.ofInt_val_eq (h : Scalar.min ScalarTy.I16 ≤ x ∧ x ≤ Scalar.max ScalarTy.I16) : (I16.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I32.ofInt_val_eq (h : Scalar.min ScalarTy.I32 ≤ x ∧ x ≤ Scalar.max ScalarTy.I32) : (I32.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I64.ofInt_val_eq (h : Scalar.min ScalarTy.I64 ≤ x ∧ x ≤ Scalar.max ScalarTy.I64) : (I64.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I128.ofInt_val_eq (h : Scalar.min ScalarTy.I128 ≤ x ∧ x ≤ Scalar.max ScalarTy.I128) : (I128.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem Usize.ofInt_val_eq (h : Scalar.min ScalarTy.Usize ≤ x ∧ x ≤ Scalar.max ScalarTy.Usize) : (Usize.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U8.ofInt_val_eq (h : Scalar.min ScalarTy.U8 ≤ x ∧ x ≤ Scalar.max ScalarTy.U8) : (U8.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U16.ofInt_val_eq (h : Scalar.min ScalarTy.U16 ≤ x ∧ x ≤ Scalar.max ScalarTy.U16) : (U16.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U32.ofInt_val_eq (h : Scalar.min ScalarTy.U32 ≤ x ∧ x ≤ Scalar.max ScalarTy.U32) : (U32.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U64.ofInt_val_eq (h : Scalar.min ScalarTy.U64 ≤ x ∧ x ≤ Scalar.max ScalarTy.U64) : (U64.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U128.ofInt_val_eq (h : Scalar.min ScalarTy.U128 ≤ x ∧ x ≤ Scalar.max ScalarTy.U128) : (U128.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+
-- Comparisons
instance {ty} : LT (Scalar ty) where
lt a b := LT.lt a.val b.val
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 92285c0d..40b5009d 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -263,11 +263,6 @@ def lookup (hm : HashMap α) (k : Usize) : Option α :=
@[simp]
abbrev len_s (hm : HashMap α) : Int := hm.al_v.len
-set_option trace.Progress true
-/-set_option pp.explicit true
-set_option pp.universes true
-set_option pp.notation false -/
-
-- Remark: α and β must live in the same universe, otherwise the
-- bind doesn't work
theorem if_update_eq
@@ -297,7 +292,12 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
-- TODO: progress keep as ⟨ ... ⟩ : conflict
progress keep as h as ⟨ hash_mod, hhm ⟩
have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac
- have _ : hash_mod.val < Vec.length hm.slots := by sorry
+ have _ : hash_mod.val < Vec.length hm.slots := by
+ have : 0 < hm.slots.val.len := by
+ simp [inv] at hinv
+ simp [hinv]
+ -- TODO: we want to automate that
+ simp [*, Int.emod_lt_of_pos]
-- have h := Primitives.Vec.index_mut_spec hm.slots hash_mod
-- TODO: change the spec of Vec.index_mut to introduce a let-binding.
-- or: make progress introduce the let-binding by itself (this is clearer)
@@ -309,11 +309,26 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
have hipost :
∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ret i0 ∧
i0.val = if inserted then hm.num_entries.val + 1 else hm.num_entries.val
- := by sorry
+ := by
+ if inserted then
+ simp [*]
+ have : hm.num_entries.val + (Usize.ofInt 1).val ≤ Usize.max := by
+ simp [lookup] at hnsat
+ simp_all
+ simp [inv] at hinv
+ int_tac
+ progress
+ simp_all
+ else
+ simp_all [Pure.pure]
progress as ⟨ i0 ⟩
-- TODO: progress "eager" to match premises with assumptions while instantiating
-- meta-variables
- have h_slot : slot_s_inv_hash hm.slots.length hash_mod.val (hm.slots.v.index hash_mod.val).v := by sorry
+ have h_slot : slot_s_inv_hash hm.slots.length hash_mod.val (hm.slots.v.index hash_mod.val).v := by
+ simp [inv] at hinv
+ have h := hinv.right.left hash_mod.val (by assumption) (by assumption)
+ simp [slot_t_inv] at h
+ simp [h]
have hd : distinct_keys (hm.slots.v.index hash_mod.val).v := by checkpoint
simp [inv, slots_t_inv, slot_t_inv] at hinv
have h := hinv.right.left hash_mod.val (by assumption) (by assumption)
@@ -329,10 +344,11 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
-- 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
have hupdt : lookup nhm key = some value := by checkpoint
simp [lookup, List.lookup] at *
simp_all
- have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by checkpoint
+ have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by
simp [lookup, List.lookup] at *
intro k hk
-- We have to make a case disjunction: either the hashes are different,
@@ -340,8 +356,19 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
-- are the same, in which case we have to reason about what happens
-- in one slot
let k_hash_mod := k.val % v.val.len
- have _ : 0 ≤ k_hash_mod := by sorry
- have _ : k_hash_mod < Vec.length hm.slots := by sorry
+ have : 0 < hm.slots.val.len := by simp_all [inv]
+ have hvpos : 0 < v.val.len := by simp_all
+ have hvnz: v.val.len ≠ 0 := by
+ simp_all
+ have _ : 0 ≤ k_hash_mod := by
+ -- TODO: we want to automate this
+ simp
+ apply Int.emod_nonneg k.val hvnz
+ have _ : k_hash_mod < Vec.length hm.slots := by
+ -- TODO: we want to automate this
+ simp
+ have h := Int.emod_lt_of_pos k.val hvpos
+ simp_all
if h_hm : k_hash_mod = hash_mod.val then
simp_all
else
@@ -377,18 +404,13 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
simp_all [lookup]
. simp [slots_t_inv, slot_t_inv] at *
intro i hipos _
- have hs := hinv.right.left i hipos (by simp_all)
+ have _ := hinv.right.left i hipos (by simp_all)
-- We need a case disjunction
if i = key.val % _root_.List.len hm.slots.val then
simp_all
else
simp_all
- . match h: lookup hm key with
- | none =>
- simp [h] at *
- simp [*]
- | some _ =>
- simp_all
+ . simp_all
simp_all
end HashMap
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 04:01:10 +0000