diff options
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 2 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 2 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 41 | ||||
| -rw-r--r-- | backends/lean/Base/Utils.lean | 12 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 171 |
5 files changed, 117 insertions, 111 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index 48a30a49..7a5bbe98 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -147,7 +147,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) let hs ← collectInstancesFromMainCtx lookup hs.toArray.mapM fun e => do let type ← inferType e - let name ← mkFreshUserName `h + let name ← mkFreshAnonPropUserName -- Add a declaration let nval ← Utils.addDeclTac name e type (asLet := false) -- Simplify to unfold the declaration to unfold (i.e., the projector) diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean index 6f4a8eba..b792ff21 100644 --- a/backends/lean/Base/Arith/Scalar.lean +++ b/backends/lean/Base/Arith/Scalar.lean @@ -12,7 +12,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do -- Inroduce the bounds for the isize/usize types let add (e : Expr) : Tactic.TacticM Unit := do let ty ← inferType e - let _ ← Utils.addDeclTac (← mkFreshUserName `h) e ty (asLet := false) + let _ ← Utils.addDeclTac (← Utils.mkFreshAnonPropUserName) e ty (asLet := false) add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []]) add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []]) add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []]) diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 4a406bdf..9300edff 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -79,7 +79,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) match th with | .Theorem thName => mkAppOptM thName (mvars.map some) | .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some) - let asmName ← do match keep with | none => mkFreshUserName `h | some n => do pure n + let asmName ← do match keep with | none => mkFreshAnonPropUserName | some n => do pure n let thTy ← inferType th let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false) withMainContext do -- The context changed - TODO: remove once addDeclTac is updated @@ -101,8 +101,8 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) let hName := (← h.fvarId!.getDecl).userName let (optIds, ids) ← do match ids with - | [] => do pure (some (hName, ← mkFreshUserName `h), []) - | none :: ids => do pure (some (hName, ← mkFreshUserName `h), ids) + | [] => do pure (some (hName, ← mkFreshAnonPropUserName), []) + | none :: ids => do pure (some (hName, ← mkFreshAnonPropUserName), ids) | some id :: ids => do pure (some (hName, id), ids) splitConjTac h optIds (fun hEq hPost => k hEq (some hPost) ids) else k h none ids @@ -142,7 +142,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) -- Split let nid ← do match nid with - | none => mkFreshUserName `h + | none => mkFreshAnonPropUserName | some nid => pure nid trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}" if ← isConj (← inferType hPost) then @@ -270,23 +270,26 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL -- Nothing worked: failed throwError "Progress failed" -syntax progressArgs := ("keep" ("as" (ident))?)? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")? +syntax progressArgs := ("keep" (ident <|> "_"))? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")? def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do let args := args.raw -- Process the arguments to retrieve the identifiers to use trace[Progress] "Progress arguments: {args}" - let args := args.getArgs + let (keepArg, withArg, asArgs) ← + match args.getArgs.toList with + | [keepArg, withArg, asArgs] => do pure (keepArg, withArg, asArgs) + | _ => throwError "Unexpected: invalid arguments" let keep : Option Name ← do - let args := (args.get! 0).getArgs - if args.size > 0 then do - let args := (args.get! 1).getArgs - if args.size > 0 then pure (some (args.get! 1).getId) - else do pure (some (← mkFreshUserName `h)) - else pure none + 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)) trace[Progress] "Keep: {keep}" let withArg ← do - let withArg := (args.get! 1).getArgs + let withArg := withArg.getArgs if withArg.size > 0 then let id := withArg.get! 1 trace[Progress] "With arg: {id}" @@ -306,12 +309,12 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do pure (some (.Theorem id)) else pure none let ids := - let args := (args.get! 2).getArgs + let args := asArgs.getArgs let args := (args.get! 2).getSepArgs args.map (λ s => if s.isIdent then some s.getId else none) trace[Progress] "User-provided ids: {ids}" let splitPost : Bool := - let args := (args.get! 2).getArgs + let args := asArgs.getArgs (args.get! 3).getArgs.size > 0 trace[Progress] "Split post: {splitPost}" /- For scalarTac we have a fast track: if the goal is not a linear @@ -343,15 +346,15 @@ namespace Test (hmin : Scalar.min ty ≤ x.val + y.val) (hmax : x.val + y.val ≤ Scalar.max ty) : ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by - progress keep as h as ⟨ x, h1 .. ⟩ - simp [*] + progress keep _ as ⟨ z, h1 .. ⟩ + simp [*, h1] example {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ x.val + y.val) (hmax : x.val + y.val ≤ Scalar.max ty) : ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by - progress keep as h with Scalar.add_spec as ⟨ z ⟩ - simp [*] + progress keep h with Scalar.add_spec as ⟨ z ⟩ + simp [*, h] /- Checking that universe instantiation works: the original spec uses `α : Type u` where u is quantified, while here we use `α : Type 0` -/ diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index f6dc45c7..1f8f1455 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -201,6 +201,10 @@ partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr : | .proj _ _ b => return e.updateProj! (← visit (i + 1) b) visit 0 e +-- Generate a fresh user name for an anonymous proposition to introduce in the +-- assumptions +def mkFreshAnonPropUserName := mkFreshUserName `_ + section Methods variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadError m] variable {a : Type} @@ -411,7 +415,7 @@ def splitDisjTac (h : Expr) (kleft kright : TacticM Unit) : TacticM Unit := do trace[Arith] "left: {inl}: {mleft}" trace[Arith] "right: {inr}: {mright}" -- Create the match expression - withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do + withLocalDeclD (← mkFreshAnonPropUserName) hTy fun hVar => do let motive ← mkLambdaFVars #[hVar] goalType let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr] let mgoal ← getMainGoal @@ -505,8 +509,8 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr let altVarNames ← match optIds with | none => do - let id0 ← mkFreshUserName `h - let id1 ← mkFreshUserName `h + let id0 ← mkFreshAnonPropUserName + let id1 ← mkFreshAnonPropUserName pure #[{ varNames := [id0, id1] }] | some (id0, id1) => do pure #[{ varNames := [id0, id1] }] @@ -532,7 +536,7 @@ partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (keepCurrentName : let ids ← do if keepCurrentName then do let cur := (← h.fvarId!.getDecl).userName - let nid ← mkFreshUserName `h + let nid ← mkFreshAnonPropUserName pure (some (cur, nid)) else pure none diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index 208875a6..96b8193d 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -95,7 +95,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 heq as ⟨ b, hi ⟩ simp only [insert_in_list] at heq exists b @@ -219,7 +219,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 .. ⟩ + progress keep 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 * @@ -289,8 +289,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint intro simp_all [inv] - -- TODO: progress keep as ⟨ ... ⟩ : conflict - progress keep as h as ⟨ hash_mod, hhm ⟩ + progress keep _ as ⟨ hash_mod, hhm ⟩ have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac have _ : hash_mod.val < Vec.length hm.slots := by have : 0 < hm.slots.val.len := by @@ -324,11 +323,12 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value 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 + 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 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 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 [inv, slots_t_inv, slot_t_inv] at hinv have h := hinv.right.left hash_mod.val (by assumption) (by assumption) @@ -337,88 +337,87 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value -- TODO: allow providing terms to progress to instantiate the meta variables -- which are not propositions progress as ⟨ l0, _, _, _, hlen .. ⟩ - . checkpoint exact hm.slots.length - . checkpoint simp_all - . -- Finishing the proof - progress keep as 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 - have hupdt : lookup nhm key = some value := by checkpoint - simp [lookup, List.lookup] at * + -- 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 + 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 + simp [lookup, List.lookup] at * + intro k hk + -- We have to make a case disjunction: either the hashes are different, + -- in which case we don't even lookup the same slots, or the hashes + -- 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 < 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 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, - -- in which case we don't even lookup the same slots, or the hashes - -- 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 < 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 + 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 + simp_all + have _ : + match hm.lookup key with + | none => nhm.len_s = hm.len_s + 1 + | some _ => nhm.len_s = hm.len_s := by checkpoint + simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_t_lookup] at * + -- We have to do a case disjunction + simp_all + simp [_root_.List.update_map_eq] + -- TODO: dependent rewrites + have _ : key.val % hm.slots.val.len < (List.map List.v hm.slots.val).len := by + simp [*] + simp [_root_.List.len_flatten_update_eq, *] + split <;> + 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 + -- somewhere in mathlib?) + simp [Int.add_assoc, Int.add_comm, Int.add_left_comm] <;> + int_tac + have hinv : inv nhm := by + simp [inv] at * + split_conjs + . match h: lookup hm key with + | none => + simp [h, lookup] at * simp_all + | some _ => + simp_all [lookup] + . 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 + -- 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'" + -- Also, it is annoying to do this kind + -- of rewritings by hand. We could have a different simp + -- which safely substitutes variables when we have an + -- equality `x = ...` and `x` doesn't appear in the rhs + simp [h_ieq] at * + simp [*] else - simp_all - have _ : - match hm.lookup key with - | none => nhm.len_s = hm.len_s + 1 - | some _ => nhm.len_s = hm.len_s := by checkpoint - simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_t_lookup] at * - -- We have to do a case disjunction - simp_all - simp [_root_.List.update_map_eq] - -- TODO: dependent rewrites - have _ : key.val % hm.slots.val.len < (List.map List.v hm.slots.val).len := by simp [*] - simp [_root_.List.len_flatten_update_eq, *] - split <;> - 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 - -- somewhere in mathlib?) - simp [Int.add_assoc, Int.add_comm, Int.add_left_comm] <;> - int_tac - have hinv : inv nhm := by - simp [inv] at * - split_conjs - . match h: lookup hm key with - | none => - simp [h, lookup] at * - simp_all - | some _ => - simp_all [lookup] - . 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 - -- We need a case disjunction - if h_ieq : i = key.val % _root_.List.len hm.slots.val then - -- TODO: simp_all loops (investigate). - -- Also, it is annoying to do this kind - -- of rewritings by hand. We could have a different simp - -- which safely substitutes variables when we have an - -- equality `x = ...` and `x` doesn't appear in the rhs - simp [h_ieq] at * - simp [*] - else - simp [*] - . simp [*] - simp_all + . -- TODO: simp[*] fails: "(deterministic) timeout at 'whnf'" + simp [hinv, h_veq] + simp_all end HashMap |