diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base.lean | 9 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 19 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 11 | ||||
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 61 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 7 | ||||
| -rw-r--r-- | backends/lean/Base/Termination.lean | 94 | ||||
| -rw-r--r-- | backends/lean/Base/Utils.lean | 4 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 100 |
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 |