summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon HO2024-06-22 13:22:32 +0200
committerGitHub2024-06-22 13:22:32 +0200
commit8144c39f4d37aa1fa14a8a061eb7ed60e153fb4c (patch)
treeb3de971e89c369f30de349806c87913edeb17333
parent4d30546c809cb2c512e0c3fd8ee540fff1330eab (diff)
Improve `scalar_tac` and `scalar_decr_tac` (#256)
* Fix an issue in a proof of the hashmap * Improve scalar_decr_tac * Improve the error message of scalar_tac and add the missing Termination.lean
-rw-r--r--backends/lean/Base.lean9
-rw-r--r--backends/lean/Base/Arith/Int.lean19
-rw-r--r--backends/lean/Base/Arith/Scalar.lean11
-rw-r--r--backends/lean/Base/IList/IList.lean61
-rw-r--r--backends/lean/Base/Primitives/Vec.lean7
-rw-r--r--backends/lean/Base/Termination.lean94
-rw-r--r--backends/lean/Base/Utils.lean4
-rw-r--r--tests/lean/Hashmap/Properties.lean100
8 files changed, 179 insertions, 126 deletions
diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean
index 2077d410..53baae1e 100644
--- a/backends/lean/Base.lean
+++ b/backends/lean/Base.lean
@@ -1,6 +1,7 @@
-import Base.Utils
-import Base.Primitives
-import Base.Diverge
import Base.Arith
-import Base.Progress
+import Base.Diverge
import Base.IList
+import Base.Primitives
+import Base.Progress
+import Base.Utils
+import Base.Termination
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index b1927cfd..958e31c9 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -106,19 +106,26 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
Tactic.withMainContext do
-- Get the local context
let ctx ← Lean.MonadLCtx.getLCtx
- -- Just a matter of precaution
- let ctx ← instantiateLCtxMVars ctx
-- Initialize the hashset
let hs := HashSet.empty
-- Explore the declarations
let decls ← ctx.getDecls
let hs ← decls.foldlM (fun hs d => do
-- Collect instances over all subexpressions in the context.
- -- Note that we explore the *type* of the local declarations: if we have
+ -- Note that if the local declaration is
+ -- Note that we explore the *type* of propositions: if we have
-- for instance `h : A ∧ B` in the context, the expression itself is simply
-- `h`; the information we are interested in is its type.
- let ty ← Lean.Meta.inferType d.toExpr
- collectInstances k hs ty
+ -- However, if the decl is not a proposition, we explore it directly.
+ -- For instance: `x : U32`
+ -- TODO: case disjunction on whether the local decl is a Prop or not. If prop,
+ -- we need to explore its type.
+ let d := d.toExpr
+ if d.isProp then
+ collectInstances k hs d
+ else
+ let ty ← Lean.Meta.inferType d
+ collectInstances k hs ty
) hs
-- Also explore the goal
collectInstances k hs (← Tactic.getMainTarget)
@@ -296,7 +303,7 @@ def intTac (tacName : String) (splitGoalConjs : Bool) (extraPreprocess : Tactic
try do Tactic.Omega.omegaTactic {}
catch _ =>
let g ← Tactic.getMainGoal
- throwError "{tacName} failed to prove the goal:\n{g}"
+ throwError "{tacName} failed to prove the goal below.\n\nNote that {tacName} is equivalent to:\n {tacName}_preprocess; omega\n\nGoal: \n{g}"
elab "int_tac" args:(" split_goal"?): tactic =>
let split := args.raw.getArgs.size > 0
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 31110b95..a36aadf3 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -44,17 +44,6 @@ def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do
elab "scalar_tac" : tactic =>
scalarTac false
--- For termination proofs
-syntax "scalar_decr_tac" : tactic
-macro_rules
- | `(tactic| scalar_decr_tac) =>
- `(tactic|
- simp_wf;
- -- TODO: don't use a macro (namespace problems)
- (first | apply Arith.to_int_to_nat_lt
- | apply Arith.to_int_sub_to_nat_lt) <;>
- simp_all <;> scalar_tac)
-
instance (ty : ScalarTy) : HasIntProp (Scalar ty) where
-- prop_ty is inferred
prop := λ x => And.intro x.hmin x.hmax
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index ab71daed..c77f075f 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -4,8 +4,29 @@
import Base.Arith
import Base.Utils
+-- TODO: move?
+-- This lemma is generally useful. It often happens that (because we
+-- make a split on a condition for instance) we have `x ≠ y` in the context
+-- and need to simplify `y ≠ x` somewhere.
+@[simp]
+theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all
+
namespace List
+-- Small helper
+-- We cover a set of cases which might imply inequality, to make sure that using
+-- this as the precondition of a `simp` lemma will allow the lemma to get correctly
+-- triggered.
+-- TODO: there should be something more systematic to do, with discharged procedures
+-- or simprocs I guess.
+@[simp]
+abbrev Int.not_eq (i j : Int) : Prop :=
+ i ≠ j ∨ j ≠ i ∨ i < j ∨ j < i
+
+theorem Int.not_eq_imp_not_eq {i j} : Int.not_eq i j → i ≠ j := by
+ intro h g
+ simp_all
+
def len (ls : List α) : Int :=
match ls with
| [] => 0
@@ -32,7 +53,7 @@ def indexOpt (ls : List α) (i : Int) : Option α :=
@[simp] theorem indexOpt_nil : indexOpt ([] : List α) i = none := by simp [indexOpt]
@[simp] theorem indexOpt_zero_cons : indexOpt ((x :: tl) : List α) 0 = some x := by simp [indexOpt]
-@[simp] theorem indexOpt_nzero_cons (hne : i ≠ 0) : indexOpt ((x :: tl) : List α) i = indexOpt tl (i - 1) := by simp [*, indexOpt]
+@[simp] theorem indexOpt_nzero_cons (hne : Int.not_eq i 0) : indexOpt ((x :: tl) : List α) i = indexOpt tl (i - 1) := by simp [indexOpt]; intro; simp_all
-- Remark: if i < 0, then the result is the default element
def index [Inhabited α] (ls : List α) (i : Int) : α :=
@@ -42,10 +63,7 @@ def index [Inhabited α] (ls : List α) (i : Int) : α :=
if i = 0 then x else index tl (i - 1)
@[simp] theorem index_zero_cons [Inhabited α] : index ((x :: tl) : List α) 0 = x := by simp [index]
-@[simp] theorem index_nzero_cons [Inhabited α] (hne : i ≠ 0) : index ((x :: tl) : List α) i = index tl (i - 1) := by simp [*, index]
-@[simp] theorem index_zero_lt_cons [Inhabited α] (hne : 0 < i) : index ((x :: tl) : List α) i = index tl (i - 1) := by
- have : i ≠ 0 := by scalar_tac
- simp [*, index]
+@[simp] theorem index_nzero_cons [Inhabited α] (hne : Int.not_eq i 0) : index ((x :: tl) : List α) i = index tl (i - 1) := by simp [index]; intro; simp_all
theorem indexOpt_bounds (ls : List α) (i : Int) :
ls.indexOpt i = none ↔ i < 0 ∨ ls.len ≤ i :=
@@ -128,15 +146,15 @@ decreasing_by int_decr_tac
@[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update]
@[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update]
-@[simp] theorem update_nzero_cons (hne : i ≠ 0) : update ((x :: tl) : List α) i y = x :: update tl (i - 1) y := by simp [*, update]
+@[simp] theorem update_nzero_cons (hne : Int.not_eq i 0) : update ((x :: tl) : List α) i y = x :: update tl (i - 1) y := by simp [update]; intro; simp_all
@[simp] theorem idrop_nil : idrop i ([] : List α) = [] := by simp [idrop]
@[simp] theorem idrop_zero : idrop 0 (ls : List α) = ls := by cases ls <;> simp [idrop]
-@[simp] theorem idrop_nzero_cons (hne : i ≠ 0) : idrop i ((x :: tl) : List α) = idrop (i - 1) tl := by simp [*, idrop]
+@[simp] theorem idrop_nzero_cons (hne : Int.not_eq i 0) : idrop i ((x :: tl) : List α) = idrop (i - 1) tl := by simp [idrop]; intro; simp_all
@[simp] theorem itake_nil : itake i ([] : List α) = [] := by simp [itake]
@[simp] theorem itake_zero : itake 0 (ls : List α) = [] := by cases ls <;> simp [itake]
-@[simp] theorem itake_nzero_cons (hne : i ≠ 0) : itake i ((x :: tl) : List α) = x :: itake (i - 1) tl := by simp [*, itake]
+@[simp] theorem itake_nzero_cons (hne : Int.not_eq i 0) : itake i ((x :: tl) : List α) = x :: itake (i - 1) tl := by simp [itake]; intro; simp_all
@[simp] theorem slice_nil : slice i j ([] : List α) = [] := by simp [slice]
@[simp] theorem slice_zero : slice 0 0 (ls : List α) = [] := by cases ls <;> simp [slice]
@@ -146,20 +164,21 @@ decreasing_by int_decr_tac
rw [ireplicate]; simp [*]
@[simp]
-theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : slice i j ((x :: tl) : List α) = slice (i - 1) (j - 1) tl :=
+theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : Int.not_eq i 0) :
+ slice i j ((x :: tl) : List α) = slice (i - 1) (j - 1) tl := by
+ apply Int.not_eq_imp_not_eq at hne
match tl with
- | [] => by simp [slice]; simp [*]
+ | [] => simp [slice]; simp [*]
| hd :: tl =>
- if h: i - 1 = 0 then by
+ if h: i - 1 = 0 then
have : i = 1 := by int_tac
simp [*, slice]
else
- have hi := slice_nzero_cons (i - 1) (j - 1) hd tl h
- by
- conv => lhs; simp [slice, *]
- conv at hi => lhs; simp [slice, *]
- simp [slice]
- simp [*]
+ have hi := slice_nzero_cons (i - 1) (j - 1) hd tl (by simp_all)
+ conv => lhs; simp [slice, *]
+ conv at hi => lhs; simp [slice, *]
+ simp [slice]
+ simp [*]
@[simp]
theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) :
@@ -319,7 +338,8 @@ theorem itake_len_le (i : Int) (ls : List α) : (ls.itake i).len ≤ ls.len :=
by simp [*]
@[simp]
-theorem itake_len (i : Int) (ls : List α) (_ : 0 ≤ i) (_ : i ≤ ls.len) : (ls.itake i).len = i :=
+theorem itake_len (i : Int) (ls : List α) (_ : 0 ≤ i) (_ : i ≤ ls.len) :
+ (ls.itake i).len = i :=
match ls with
| [] => by simp_all; int_tac
| hd :: tl =>
@@ -359,7 +379,8 @@ theorem index_itake [Inhabited α] (i : Int) (j : Int) (ls : List α)
| [] => by simp at *
| hd :: tl =>
have : ¬ 0 = i := by int_tac -- TODO: this is slightly annoying
- if h: j = 0 then by simp [*] at *
+ if h: j = 0 then by
+ simp_all
else by
simp [*]
-- TODO: rewriting rule: ¬ i = 0 → 0 ≤ i → 0 < i ?
@@ -422,7 +443,7 @@ theorem index_itake_append_end [Inhabited α] (i j : Int) (l0 l1 : List α)
@[simp]
theorem index_update_ne
{α : Type u} [Inhabited α] (l: List α) (i: ℤ) (j: ℤ) (x: α) :
- j ≠ i → (l.update i x).index j = l.index j
+ Int.not_eq i j → (l.update i x).index j = l.index j
:=
λ _ => match l with
| [] => by simp at *
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index e584777a..12789fa9 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -48,10 +48,7 @@ abbrev Vec.len (α : Type u) (v : Vec α) : Usize :=
theorem Vec.len_val {α : Type u} (v : Vec α) : (Vec.len α v).val = v.length :=
by rfl
--- This shouldn't be used
-def Vec.push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := ()
-
--- This is actually the backward function
+@[irreducible]
def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
:=
let nlen := List.length v.val + 1
@@ -68,7 +65,7 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
theorem Vec.push_spec {α : Type u} (v : Vec α) (x : α) (h : v.val.len < Usize.max) :
∃ v1, v.push α x = ok v1 ∧
v1.val = v.val ++ [x] := by
- simp [push]
+ rw [push]; simp
split <;> simp_all [List.len_eq_length]
scalar_tac
diff --git a/backends/lean/Base/Termination.lean b/backends/lean/Base/Termination.lean
new file mode 100644
index 00000000..de8e678f
--- /dev/null
+++ b/backends/lean/Base/Termination.lean
@@ -0,0 +1,94 @@
+/- Some utilities to prove termination -/
+import Lean
+import Mathlib.Tactic.Core
+import Base.Utils
+import Base.Arith
+
+namespace Utils
+
+open Lean Lean.Elab Command Term Lean.Meta Tactic
+
+-- Inspired by the `clear` tactic
+def clearFvarIds (fvarIds : Array FVarId) : TacticM Unit := do
+ let fvarIds ← withMainContext <| sortFVarIds fvarIds
+ for fvarId in fvarIds.reverse do
+ withMainContext do
+ let mvarId ← (← getMainGoal).clear fvarId
+ replaceMainGoal [mvarId]
+
+/- Utility function for proofs of termination (i.e., inside `decreasing_by`).
+
+ Clean up the local context by removing all assumptions containing occurrences
+ of `invImage` (those are introduced automatically when doing proofs of
+ termination). We do so because we often need to simplify the context in the
+ proofs, and if we simplify those assumptions they tend to make the context
+ blow up.
+-/
+def removeInvImageAssumptions : TacticM Unit := do
+ withMainContext do
+ -- Get the local declarations
+ let ctx ← Lean.MonadLCtx.getLCtx
+ let decls ← ctx.getDecls
+ -- Retrieve the list of local declarations which contain `invertImage`
+ let containsInvertImage (decl : LocalDecl) : MetaM Bool := do
+ let expr := decl.toExpr
+ reduceVisit (
+ fun _ b e =>
+ pure (
+ b ||
+ match e with
+ | .const name _ => name == ``invImage
+ | _ => false)) false (← inferType expr)
+ let filtDecls ← liftM (decls.filterM containsInvertImage)
+ -- It can happen that other variables depend on the variables we want to clear:
+ -- filter them.
+ let allFVarsInTypes ← decls.foldlM (fun hs d => do
+ let hs ← getFVarIds (← inferType d.toExpr) hs
+ -- Explore the body if it is not opaque
+ match d.value? with
+ | none => pure hs
+ | some e => getFVarIds e hs
+ ) HashSet.empty
+ let fvarIds := filtDecls.map fun d => d.fvarId
+ let fvarIds := fvarIds.filter (fun id => ¬ allFVarsInTypes.contains id)
+ -- Clear them
+ clearFvarIds fvarIds.toArray
+
+elab "remove_invImage_assumptions" : tactic =>
+ removeInvImageAssumptions
+
+-- Auxiliary function
+def scalarDecrTac_apply_lemmas : TacticM Unit := do
+ withMainContext do
+ let goal ← getMainGoal
+ let rec applyFirst (names : List Name) : TacticM (List MVarId) :=
+ match names with
+ | [] => pure [goal]
+ | name :: names =>
+ -- Should use try ... catch or Lean.observing?
+ -- Generally speaking we should use Lean.observing? to restore the state,
+ -- but with tactics the try ... catch variant seems to work
+ try do
+ let th ← mkConstWithFreshMVarLevels name
+ goal.apply th
+ catch _ => do applyFirst names
+ let ngoals ← applyFirst [``Arith.to_int_to_nat_lt, ``Arith.to_int_sub_to_nat_lt]
+ setGoals ngoals
+
+elab "scalar_decr_tac_apply_lemmas" : tactic =>
+ scalarDecrTac_apply_lemmas
+
+-- For termination proofs
+syntax "scalar_decr_tac" : tactic
+macro_rules
+ | `(tactic| scalar_decr_tac) =>
+ `(tactic|
+ simp_wf <;>
+ -- Simplify the context - otherwise simp_all below will blow up
+ remove_invImage_assumptions <;>
+ -- Transform the goal a bit
+ scalar_decr_tac_apply_lemmas <;>
+ -- Finish
+ simp_all <;> scalar_tac)
+
+end Utils
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index b9de2fd1..2352979b 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -42,10 +42,6 @@ namespace List
end List
--- TODO: move?
-@[simp]
-theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all
-
namespace Lean
namespace LocalContext
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 246041f4..d9be15dd 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -168,9 +168,9 @@ def frame_load (hm nhm : 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
+-- The proofs below are a bit expensive, so we deactivate the heart bits limit
+set_option maxHeartbeats 0
+
open AList
@[pspec]
@@ -201,15 +201,7 @@ theorem allocate_slots_spec {α : Type} (slots : alloc.vec.Vec (AList α)) (n :
simp [*]
have Hslots1Len : alloc.vec.Vec.len (AList α) slots1 + n1.val ≤ Usize.max := by
simp_all
- -- TODO: progress fails here (maximum recursion depth reached)
- -- This probably comes from the fact that allocate_slots is reducible and applied an infinite number
- -- of times
- -- progress as ⟨ slots2 .. ⟩
- -- TODO: bug here as well
- stop
- have ⟨ slots2, hEq, _, _ ⟩ := allocate_slots_spec slots1 n1 (by assumption) (by assumption)
- stop
- rw [allocate_slots] at hEq; rw [hEq]; clear hEq
+ progress as ⟨ slots2 .. ⟩
simp
constructor
. intro i h0 h1
@@ -219,6 +211,8 @@ theorem allocate_slots_spec {α : Type} (slots : alloc.vec.Vec (AList α)) (n :
simp [h]
simp_all
scalar_tac
+termination_by n.val.toNat
+decreasing_by scalar_decr_tac -- TODO: this is expensive
theorem forall_nil_imp_flatten_len_zero (slots : List (List α))
(Hnil : ∀ i, 0 ≤ i → i < slots.len → slots.index i = []) :
@@ -373,21 +367,13 @@ theorem if_update_eq
split <;> simp [Pure.pure]
-- Small helper
--- TODO: move, and introduce a better solution with nice syntax
+-- TODO: let bindings now work
def mk_opaque {α : Sort u} (x : α) : { y : α // y = x} :=
⟨ x, by simp ⟩
---set_option profiler true
---set_option profiler.threshold 10
---set_option trace.profiler true
-
-- For pretty printing (useful when copy-pasting goals)
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
--- of heart beats
-set_option maxHeartbeats 2000000
-
@[pspec]
theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α)
(hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) :
@@ -484,15 +470,8 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
-- TODO: we want to automate this
simp only [k_hash_mod]
have h := Int.emod_lt_of_pos k.val hvpos
- simp_all only [ok.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 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 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]
+ simp_all
+ cases h_hm: k_hash_mod == hash_mod.val <;> simp_all (config := {zetaDelta := true})
have _ :
match hm.lookup key with
| none => nhm.len_s = hm.len_s + 1
@@ -529,7 +508,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
. simp_all [frame_load, inv_base, inv_load]
simp_all
-theorem slot_allP_not_key_lookup (slot : AList T) (h : slot.v.allP fun (k', _) => ¬k = k') :
+private theorem slot_allP_not_key_lookup (slot : AList T) (h : slot.v.allP fun (k', _) => ¬k = k') :
slot.lookup k = none := by
induction slot <;> simp_all
@@ -628,7 +607,7 @@ theorem move_elements_from_list_spec
simp_all
. scalar_tac
-theorem slots_forall_nil_imp_lookup_none (slots : Slots T) (hLen : slots.val.len ≠ 0)
+private theorem slots_forall_nil_imp_lookup_none (slots : Slots T) (hLen : slots.val.len ≠ 0)
(hEmpty : ∀ j, 0 ≤ j → j < slots.val.len → slots.val.index j = AList.Nil) :
∀ key, slots.lookup key = none := by
intro key
@@ -641,7 +620,7 @@ theorem slots_forall_nil_imp_lookup_none (slots : Slots T) (hLen : slots.val.len
have := hEmpty (key.val % slots.val.len) (by assumption) (by assumption)
simp [*]
-theorem slots_index_len_le_flatten_len (slots : List (AList α)) (i : Int) (h : 0 ≤ i ∧ i < slots.len) :
+private theorem slots_index_len_le_flatten_len (slots : List (AList α)) (i : Int) (h : 0 ≤ i ∧ i < slots.len) :
(slots.index i).len ≤ (List.map AList.v slots).flatten.len := by
match slots with
| [] =>
@@ -659,7 +638,7 @@ theorem slots_index_len_le_flatten_len (slots : List (AList α)) (i : Int) (h :
be equal to the slot index.
TODO: remove?
-/
-theorem slots_inv_lookup_imp_eq (slots : Slots α) (hInv : slots_t_inv slots)
+private theorem slots_inv_lookup_imp_eq (slots : Slots α) (hInv : slots_t_inv slots)
(i : Int) (hi : 0 ≤ i ∧ i < slots.val.len) (key : Usize) :
(slots.val.index i).lookup key ≠ none → i = key.val % slots.val.len := by
suffices hSlot : ∀ (slot : List (Usize × α)),
@@ -676,23 +655,7 @@ theorem slots_inv_lookup_imp_eq (slots : Slots α) (hInv : slots_t_inv slots)
intros; simp_all
split at * <;> simp_all
--- TODO: remove?
-theorem slots_update_lookup_equiv (slots : Slots α) (hInv : slots_t_inv slots)
- (i : Int) (hi : 0 ≤ i ∧ i < slots.val.len) (key : Usize) :
- let slot := slots.val.index i
- slot.lookup key ≠ none ∨ slots_s_lookup (slots.val.update i .Nil) key ≠ none ↔
- slots.lookup key ≠ none := by
- -- We need the following lemma to derive a contradiction
- have := slots_inv_lookup_imp_eq slots hInv i hi key
- cases hi : (key.val % slots.val.len) == i <;>
- simp_all [Slots.lookup]
-
-/-theorem slots_update_lookup_imp
- (slots slots1 : Slots α) (slot : AList α) (hInv : slots_t_inv slots) (i : Int) (hi : 0 ≤ i ∧ i < slots.val.len)
- (hSlotsEq : slots.val = slots.val.update i slot) :
- ∀ key v, slots1.lookup key = some v → slots.lookup key = some v ∨ slot.lookup key = some v-/
-
-theorem move_slots_updated_table_lookup_imp
+private theorem move_slots_updated_table_lookup_imp
(ntable ntable1 ntable2 : HashMap α) (slots slots1 : Slots α) (slot : AList α)
(hi : 0 ≤ i ∧ i < slots.val.len)
(hSlotsInv : slots_t_inv slots)
@@ -717,12 +680,9 @@ theorem move_slots_updated_table_lookup_imp
| inr hTable1Lookup =>
right
-- The key can't be for the slot we replaced
- if heq : key.val % slots.val.len = i then
- simp_all [Slots.lookup]
- else
- simp_all [Slots.lookup]
+ cases heq : key.val % slots.val.len == i <;> simp_all [Slots.lookup]
-theorem move_one_slot_lookup_equiv {α : Type} (ntable ntable1 ntable2 : HashMap α)
+private theorem move_one_slot_lookup_equiv {α : Type} (ntable ntable1 ntable2 : HashMap α)
(slot : AList α)
(slots slots1 : Slots α)
(i : Int) (h1 : i < slots.len)
@@ -749,7 +709,7 @@ theorem move_one_slot_lookup_equiv {α : Type} (ntable ntable1 ntable2 : HashMap
have := hLookup3 key v
simp_all
-theorem slots_lookup_none_imp_slot_lookup_none
+private theorem slots_lookup_none_imp_slot_lookup_none
(slots : Slots α) (hInv : slots_t_inv slots) (i : Int) (hi : 0 ≤ i ∧ i < slots.val.len) :
∀ (key : Usize), slots.lookup key = none → (slots.val.index i).lookup key = none := by
intro key hLookup
@@ -760,14 +720,14 @@ theorem slots_lookup_none_imp_slot_lookup_none
by_contra
simp_all
-theorem slot_lookup_not_none_imp_slots_lookup_not_none
+private theorem slot_lookup_not_none_imp_slots_lookup_not_none
(slots : Slots α) (hInv : slots_t_inv slots) (i : Int) (hi : 0 ≤ i ∧ i < slots.val.len) :
∀ (key : Usize), (slots.val.index i).lookup key ≠ none → slots.lookup key ≠ none := by
intro key hLookup hNone
have := slots_lookup_none_imp_slot_lookup_none slots hInv i hi key hNone
apply hLookup this
-theorem slots_forall_nil_imp_al_v_nil (slots : Slots α)
+private theorem slots_forall_nil_imp_al_v_nil (slots : Slots α)
(hEmpty : ∀ i, 0 ≤ i → i < slots.val.len → slots.val.index i = AList.Nil) :
slots.al_v = [] := by
suffices h :
@@ -790,10 +750,8 @@ theorem slots_forall_nil_imp_al_v_nil (slots : Slots α)
simp_all
theorem move_elements_loop_spec
- (n : Nat) -- We need this, otherwise we can't prove termination (the termination_by clauses can be expensive)
{α : Type} (ntable : HashMap α) (slots : Slots α)
(i : Usize)
- (hn : n = slots.val.len - i.val) -- Condition for termination
(hi : i ≤ alloc.vec.Vec.len (AList α) slots)
(hinv : ntable.inv)
(hSlotsNonZero : slots.val.len ≠ 0)
@@ -814,9 +772,6 @@ theorem move_elements_loop_spec
rw [move_elements_loop]
simp
if hi: i.val < slots.val.len then
- -- Proof of termination: eliminate the case: n = 0
- cases n; scalar_tac
- rename ℕ => n
-- Continue the proof
have hIneq : 0 ≤ i.val ∧ i.val < slots.val.len := by scalar_tac
simp [hi]
@@ -887,8 +842,6 @@ theorem move_elements_loop_spec
have : i.val < (List.map AList.v slots.val).len := by simp; scalar_tac
simp_all [Slots.al_v, List.len_flatten_update_eq, List.map_update_eq]
- have : n = slots1.val.len - i'.val := by simp_all; scalar_tac
-
progress as ⟨ ntable2, slots2, _, _, hLookup2Rev, hLookup21, hLookup22, hIndexNil ⟩
simp [and_assoc]
@@ -921,6 +874,8 @@ theorem move_elements_loop_spec
have hLookupEmpty := slots_forall_nil_imp_lookup_none slots hLenNonZero hEmpty
simp [hNil, hLookupEmpty]
apply hEmpty
+termination_by (slots.val.len - i.val).toNat
+decreasing_by scalar_decr_tac -- TODO: this is expensive
@[pspec]
theorem move_elements_spec
@@ -939,16 +894,8 @@ theorem move_elements_spec
(∀ key v, ntable1.lookup key = some v ↔ slots.lookup key = some v)
:= by
rw [move_elements]
- let n := (slots.val.len - 0).toNat
- have hn : n = slots.val.len - 0 := by
- -- TODO: scalar_tac should succeed here
- scalar_tac_preprocess
- simp [n] at *
- norm_cast at *
- have := @Int.le_toNat n (slots.val.len - OfNat.ofNat 0) (by simp; scalar_tac)
- simp_all
have ⟨ ntable1, slots1, hEq, _, _, ntable1Lookup, slotsLookup, _, _ ⟩ :=
- move_elements_loop_spec (slots.val.len - 0).toNat ntable slots 0#usize hn (by scalar_tac) hinv
+ move_elements_loop_spec ntable slots 0#usize (by scalar_tac) hinv
(by scalar_tac)
hSlotsInv
(by intro j h0 h1; scalar_tac)
@@ -1187,12 +1134,13 @@ theorem remove_from_list_spec {α} (key : Usize) (slot : AList α) {l i} (hInv :
simp_all
. cases v1 <;> simp_all
+-- TODO: move?
theorem lookup'_not_none_imp_len_pos (l : List (Usize × α)) (key : Usize) (hLookup : l.lookup' key ≠ none) :
0 < l.len := by
induction l <;> simp_all
scalar_tac
-theorem lookup_not_none_imp_len_s_pos (hm : HashMap α) (key : Usize) (hLookup : hm.lookup key ≠ none)
+private theorem lookup_not_none_imp_len_s_pos (hm : HashMap α) (key : Usize) (hLookup : hm.lookup key ≠ none)
(hNotEmpty : 0 < hm.slots.val.len) :
0 < hm.len_s := by
have : 0 ≤ key.val % hm.slots.val.len := by -- TODO: automate