diff options
| -rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 13 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 17 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 35 |
3 files changed, 40 insertions, 25 deletions
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index 523372bb..a09d6ac2 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -85,14 +85,19 @@ def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α := | none => fail .arrayOutOfBounds | some x => ret x +/- In the theorems below: we don't always need the `∃ ..`, but we use one + so that `progress` introduces an opaque variable and an equality. This + helps control the context. + -/ + @[pspec] theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) (hbound : i.val < v.length) : - v.index α i = ret (v.val.index i.val) := by + ∃ x, v.index α i = ret x ∧ x = v.val.index i.val := by simp only [index] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) - simp only [*] + simp [*] -- This shouldn't be used def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit := @@ -109,11 +114,11 @@ def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α := @[pspec] theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) (hbound : i.val < v.length) : - v.index_mut α i = ret (v.val.index i.val) := by + ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by simp only [index_mut] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) - simp only [*] + simp [*] instance {α : Type u} (p : Vec α → Prop) : Arith.HasIntProp (Subtype p) where prop_ty := λ x => p x diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 9300edff..6a4729dc 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -162,6 +162,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) allGoals asmTac let newGoals ← getUnsolvedGoals setGoals (newGoals ++ curGoals) + trace[Progress] "progress: replaced the goals" -- pure .Ok @@ -281,12 +282,15 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do | [keepArg, withArg, asArgs] => do pure (keepArg, withArg, asArgs) | _ => throwError "Unexpected: invalid arguments" let keep : Option Name ← do + trace[Progress] "Keep arg: {keepArg}" let args := keepArg.getArgs - trace[Progress] "Keep args: {args}" - let arg := args.get! 1 - trace[Progress] "Keep arg: {arg}" - if arg.isIdent then pure (some arg.getId) - else do pure (some (← mkFreshAnonPropUserName)) + if args.size > 0 then do + trace[Progress] "Keep args: {args}" + let arg := args.get! 1 + trace[Progress] "Keep arg: {arg}" + if arg.isIdent then pure (some arg.getId) + else do pure (some (← mkFreshAnonPropUserName)) + else do pure none trace[Progress] "Keep: {keep}" let withArg ← do let withArg := withArg.getArgs @@ -328,7 +332,10 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do else throwError "Not a linear arithmetic goal" progressAsmsOrLookupTheorem keep withArg ids splitPost ( + withMainContext do + trace[Progress] "trying to solve assumption: {← getMainGoal}" firstTac [assumptionTac, scalarTac]) + trace[Diverge] "Progress done" elab "progress" args:progressArgs : tactic => evalProgress args diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 96b8193d..5d340b5c 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -285,7 +285,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value | none => nhm.len_s = hm.len_s + 1 | some _ => nhm.len_s = hm.len_s) := by rw [insert_no_resize] - simp [hash_key] + simp only [hash_key, bind_tc_ret] -- TODO: annoying have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint intro simp_all [inv] @@ -297,10 +297,9 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value 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) - progress + progress as ⟨ l, h_leq ⟩ -- TODO: make progress use the names written in the goal progress as ⟨ inserted ⟩ rw [if_update_eq] -- TODO: necessary because we don't have a join @@ -311,38 +310,42 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value := by if inserted then simp [*] - have : hm.num_entries.val + (Usize.ofInt 1).val ≤ Usize.max := by + have hbounds : 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 + -- TODO: progress fails in command line mode with "index out of bounds" + -- and I have no idea how to fix this. The error happens after progress + -- introduced the new goals. It must be when we exit the "withApp", etc. + -- helpers. + have ⟨ z, hp ⟩ := Usize.add_spec hbounds + simp [hp] else - simp_all [Pure.pure] + simp [*, 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_key key hm.slots.length) - (List.v (List.index (hm.slots.val) hash_mod.val)) := by + have h_slot : slot_s_inv_hash hm.slots.length (hash_mod_key key hm.slots.length) l.v + := by simp [inv] at hinv have h := (hinv.right.left hash_mod.val (by assumption) (by assumption)).right simp [slot_t_inv, hhm] at h - simp [h, hhm] - have hd : distinct_keys (hm.slots.v.index hash_mod.val).v := by checkpoint + simp [h, hhm, h_leq] + have hd : distinct_keys l.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) - simp [h] + simp [h, h_leq] -- TODO: hide the variables and only keep the props -- TODO: allow providing terms to progress to instantiate the meta variables -- which are not propositions progress as ⟨ l0, _, _, _, hlen .. ⟩ - -- Finishing the proof 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 + -- TODO: later I don't want to inline nhm - we need to control simp: deactivate + -- zeta reduction? have hupdt : lookup nhm key = some value := by checkpoint simp [lookup, List.lookup] at * simp_all @@ -387,7 +390,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value rename_i heq <;> simp [heq] at hlen <;> -- TODO: canonize addition by default? We need a tactic to simplify arithmetic equalities - -- with addition and substractions ((ℤ, +) is a ring or something - there should exist a tactic + -- with addition and substractions ((ℤ, +) is a group or something - there should exist a tactic -- somewhere in mathlib?) simp [Int.add_assoc, Int.add_comm, Int.add_left_comm] <;> int_tac @@ -403,7 +406,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 + simp [hhm, h_veq] 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'" |