diff options
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 2 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 25 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 68 | ||||
| -rw-r--r-- | backends/lean/Base/Utils.lean | 32 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 76 |
5 files changed, 129 insertions, 74 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index ac011998..fa957293 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -198,7 +198,7 @@ def intTac (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM Unit := do -- Split the conjunctions in the goal Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget) -- Call linarith - let linarith := + let linarith := do let cfg : Linarith.LinarithConfig := { -- We do this with our custom preprocessing splitNe := false diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index 2fbd24dd..b54bdf7a 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -19,6 +19,7 @@ structure PSpecDesc where -- The existentially quantified variables evars : Array Expr -- The function + fExpr : Expr fName : Name -- The function arguments fLevels : List Level @@ -60,21 +61,30 @@ section Methods m a := do trace[Progress] "Proposition: {th}" -- Dive into the quantified variables and the assumptions - forallTelescope th fun fvars th => do + forallTelescope th.consumeMData fun fvars th => do trace[Progress] "Universally quantified arguments and assumptions: {fvars}" -- Dive into the existentials - existsTelescope th fun evars th => do + existsTelescope th.consumeMData fun evars th => do trace[Progress] "Existentials: {evars}" trace[Progress] "Proposition after stripping the quantifiers: {th}" -- Take the first conjunct - let (th, post) ← optSplitConj th + let (th, post) ← optSplitConj th.consumeMData trace[Progress] "After splitting the conjunction:\n- eq: {th}\n- post: {post}" -- Destruct the equality - let (th, ret) ← destEq th + let (mExpr, ret) ← destEq th.consumeMData trace[Progress] "After splitting the equality:\n- lhs: {th}\n- rhs: {ret}" - -- Destruct the application to get the name - th.consumeMData.withApp fun f args => do - trace[Progress] "After stripping the arguments:\n- f: {f}\n- args: {args}" + -- Destruct the monadic application to dive into the bind, if necessary (this + -- is for when we use `withPSpec` inside of the `progress` tactic), and + -- destruct the application to get the function name + mExpr.consumeMData.withApp fun mf margs => do + trace[Progress] "After stripping the arguments of the monad expression:\n- mf: {mf}\n- margs: {margs}" + let (fExpr, f, args) ← do + if mf.isConst ∧ mf.constName = ``Bind.bind then do + -- Dive into the bind + let fExpr := margs.get! 4 + fExpr.consumeMData.withApp fun f args => pure (fExpr, f, args) + else pure (mExpr, mf, margs) + trace[Progress] "After stripping the arguments of the function call:\n- f: {f}\n- args: {args}" if ¬ f.isConst then throwError "Not a constant: {f}" -- Compute the set of universally quantified variables which appear in the function arguments let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty @@ -94,6 +104,7 @@ section Methods let thDesc := { fvars := fvars evars := evars + fExpr fName := f.constName! fLevels := f.constLevels! args := args diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 1f734415..dabd25b8 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -7,22 +7,6 @@ namespace Progress open Lean Elab Term Meta Tactic open Utils -/- --- TODO: remove -namespace Test - open Primitives - - set_option trace.Progress true - - @[pspec] - theorem vec_index_test (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) : - ∃ x, v.index α i = .ret x := by - sorry - - #eval pspecAttr.find? ``Primitives.Vec.index -end Test --/ - inductive TheoremOrLocal where | Theorem (thName : Name) | Local (asm : LocalDecl) @@ -39,7 +23,7 @@ inductive ProgressError | Error (msg : MessageData) deriving Inhabited -def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids : Array Name) +def progressWith (fExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids : Array Name) (asmTac : TacticM Unit) : TacticM ProgressError := do /- Apply the theorem We try to match the theorem with the goal @@ -66,7 +50,7 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids -- Introduce the existentially quantified variables and the post-condition -- in the context let thBody ← - existsTelescope thExBody fun _evars thBody => do + existsTelescope thExBody.consumeMData fun _evars thBody => do trace[Progress] "After stripping existentials: {thBody}" let (thBody, _) ← optSplitConj thBody trace[Progress] "After splitting the conjunction: {thBody}" @@ -75,9 +59,9 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids -- There shouldn't be any existential variables in thBody pure thBody -- Match the body with the target - trace[Progress] "Maching `{thBody}` with `{fnExpr}`" - let ok ← isDefEq thBody fnExpr - if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {fnExpr}" + trace[Progress] "Matching `{thBody}` with `{fExpr}`" + let ok ← isDefEq thBody fExpr + if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {fExpr}" let mgoal ← Tactic.getMainGoal postprocessAppMVars `progress mgoal mvars binders true true Term.synthesizeSyntheticMVarsNoPostponing @@ -139,8 +123,9 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids match ids with | [] => pure .Ok -- Stop | nid :: ids => do + trace[Progress] "Splitting post: {hPost}" -- Split - if ← isConj hPost then + if ← isConj (← inferType hPost) then splitConjTac hPost (some (nid, curPostId)) (λ _ nhPost => splitPost nhPost ids) else return (.Error m!"Too many ids provided ({nid :: ids}) not enough conjuncts to split in the postcondition") splitPost hPost ids @@ -175,7 +160,7 @@ def getFirstArg (args : Array Expr) : Option Expr := do /- Helper: try to lookup a theorem and apply it, or continue with another tactic if it fails -/ -def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr) +def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Unit) (fExpr : Expr) (kind : String) (th : Option TheoremOrLocal) (x : TacticM Unit) : TacticM Unit := do let res ← do match th with @@ -187,7 +172,7 @@ def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Uni -- Apply the theorem let res ← do try - let res ← progressWith fnExpr th keep ids asmTac + let res ← progressWith fExpr th keep ids asmTac pure (some res) catch _ => none match res with @@ -203,18 +188,16 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL let goalTy ← mgoal.getType trace[Progress] "goal: {goalTy}" -- Dive into the goal to lookup the theorem - let (fName, fLevels, args) ← do + let (fExpr, fName, args) ← do withPSpec goalTy fun desc => - -- TODO: check that no universally quantified variables in the arguments - pure (desc.fName, desc.fLevels, desc.args) - -- TODO: this should be in the pspec desc - let fnExpr := mkAppN (.const fName fLevels) args + -- TODO: check that no quantified variables in the arguments + pure (desc.fExpr, desc.fName, desc.args) trace[Progress] "Function: {fName}" -- If the user provided a theorem/assumption: use it. -- Otherwise, lookup one. match withTh with | some th => do - match ← progressWith fnExpr th keep ids asmTac with + match ← progressWith fExpr th keep ids asmTac with | .Ok => return () | .Error msg => throwError msg | none => @@ -223,7 +206,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL let decls ← ctx.getDecls for decl in decls.reverse do trace[Progress] "Trying assumption: {decl.userName} : {decl.type}" - let res ← do try progressWith fnExpr (.Local decl) keep ids asmTac catch _ => continue + let res ← do try progressWith fExpr (.Local decl) keep ids asmTac catch _ => continue match res with | .Ok => return () | .Error msg => throwError msg @@ -233,7 +216,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL let pspec ← do let thName ← pspecAttr.find? fName pure (thName.map fun th => .Theorem th) - tryLookupApply keep ids asmTac fnExpr "pspec theorem" pspec do + tryLookupApply keep ids asmTac fExpr "pspec theorem" pspec do -- It failed: try to lookup a *class* expr spec theorem (those are more -- specific than class spec theorems) let pspecClassExpr ← do @@ -242,7 +225,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL | some arg => do let thName ← pspecClassExprAttr.find? fName arg pure (thName.map fun th => .Theorem th) - tryLookupApply keep ids asmTac fnExpr "pspec class expr theorem" pspecClassExpr do + tryLookupApply keep ids asmTac fExpr "pspec class expr theorem" pspecClassExpr do -- It failed: try to lookup a *class* spec theorem let pspecClass ← do match ← getFirstArgAppName args with @@ -250,7 +233,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL | some argName => do let thName ← pspecClassAttr.find? fName argName pure (thName.map fun th => .Theorem th) - tryLookupApply keep ids asmTac fnExpr "pspec class theorem" pspecClass do + tryLookupApply keep ids asmTac fExpr "pspec class theorem" pspecClass do -- Try a recursive call - we try the assumptions of kind "auxDecl" let ctx ← Lean.MonadLCtx.getLCtx let decls ← ctx.getAllDecls @@ -258,7 +241,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL | .default | .implDetail => false | .auxDecl => true) for decl in decls.reverse do trace[Progress] "Trying recursive assumption: {decl.userName} : {decl.type}" - let res ← do try progressWith fnExpr (.Local decl) keep ids asmTac catch _ => continue + let res ← do try progressWith fExpr (.Local decl) keep ids asmTac catch _ => continue match res with | .Ok => return () | .Error msg => throwError msg @@ -310,7 +293,6 @@ elab "progress" args:progressArgs : tactic => evalProgress args /- --- TODO: remove namespace Test open Primitives Result @@ -319,22 +301,14 @@ namespace Test #eval showStoredPSpec #eval showStoredPSpecClass - theorem Scalar.add_spec1 {ty} {x y : Scalar ty} + 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 ⟩ +-- progress keep as h with Scalar.add_spec as ⟨ z ⟩ + progress keep as h simp [*] -/- - @[pspec] - theorem vec_index_test2 (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) : - ∃ (x: α), v.index α i = .ret x := by - progress with vec_index_test as ⟨ x ⟩ - simp - - set_option trace.Progress false --/ end Test -/ end Progress diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index 8aa76d8e..44590176 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -308,8 +308,23 @@ def firstTac (tacl : List (TacticM Unit)) : TacticM Unit := do match tacl with | [] => pure () | tac :: tacl => - try tac + -- 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 + tac + -- Check that there are no remaining goals + let gl ← Tactic.getUnsolvedGoals + if ¬ gl.isEmpty then throwError "tactic failed" catch _ => firstTac tacl +/- let res ← Lean.observing? do + tac + -- Check that there are no remaining goals + let gl ← Tactic.getUnsolvedGoals + if ¬ gl.isEmpty then throwError "tactic failed" + match res with + | some _ => pure () + | none => firstTac tacl -/ -- Split the goal if it is a conjunction def splitConjTarget : TacticM Unit := do @@ -424,12 +439,13 @@ def splitExistsTac (h : Expr) (optId : Option Name) (k : Expr → Expr → Tacti let hTy ← inferType h if isExists hTy then do -- Try to use the user-provided names - let altVarNames ← - match optId with - | none => pure #[] - | some id => do - let hDecl ← h.fvarId!.getDecl - pure #[{ varNames := [id, hDecl.userName] }] + let altVarNames ← do + let hDecl ← h.fvarId!.getDecl + let id ← do + match optId with + | none => mkFreshUserName `x + | some id => pure id + pure #[{ varNames := [id, hDecl.userName] }] let newGoals ← goal.cases h.fvarId! altVarNames -- There should be exactly one goal match newGoals.toList with @@ -511,7 +527,7 @@ example (h : a ∧ b) : a := by example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by split_all_exists h - rename_i x y z h + rename_i x y z exists x + y + z /- Call the simp tactic. diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index baa8f5c8..e065bb36 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -21,8 +21,9 @@ end List namespace HashMap -@[pspec] -theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : +abbrev Core.List := _root_.List + +theorem insert_in_list_spec0 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ (b ↔ List.lookup ls.v key = none) @@ -35,7 +36,7 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : rw [insert_in_list_loop] simp [h] else - have ⟨ b, hi ⟩ := insert_in_list_spec key value tl + have ⟨ b, hi ⟩ := insert_in_list_spec0 key value tl by exists b simp [insert_in_list, List.lookup] @@ -45,7 +46,6 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : exact hi -- Variation: use progress -@[pspec] theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ @@ -70,7 +70,6 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) simp [*, List.lookup] -- Variation: use tactics from the beginning -@[pspec] theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ @@ -91,10 +90,10 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) progress as ⟨ b h ⟩ simp [*] -@[pspec] theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List α) : ∃ l1, insert_in_list_back α key value l0 = ret l1 ∧ + -- We update the binding List.lookup l1.v key = value ∧ (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k) := match l0 with @@ -112,11 +111,66 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List simp [insert_in_list_back, List.lookup] rw [insert_in_list_loop_back] simp [h, List.lookup] - have ⟨tl0 , _, _ ⟩ := insert_in_list_back_spec key value tl -- TODO: Use progress - simp [insert_in_list_back] at * - simp [List.lookup, *] - simp (config := {contextual := true}) [*] - + progress keep as heq as ⟨ tl hp1 hp2 ⟩ + simp [insert_in_list_back] at heq + simp (config := {contextual := true}) [*, List.lookup] + +def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x.fst ≠ y.fst) + +def hash_mod_key (k : Usize) (l : Int) : Int := + match hash_key k with + | .ret k => k.val % l + | _ => 0 + +def slot_s_inv_hash (l i : Int) (ls : Core.List (Usize × α)) : Prop := + ls.allP (λ (k, _) => hash_mod_key k l = i) + +@[simp] +def slot_s_inv (l i : Int) (ls : Core.List (Usize × α)) : Prop := + distinct_keys ls ∧ + slot_s_inv_hash l i ls + +def slot_t_inv (l i : Int) (s : List α) : Prop := slot_s_inv l i s.v + +@[pspec] +theorem insert_in_list_back_spec1 {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α) + (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) : + ∃ l1, + insert_in_list_back α key value l0 = ret l1 ∧ + -- We update the binding + List.lookup l1.v key = value ∧ + (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k) ∧ + -- We preserve part of the key invariant + slot_s_inv_hash l (hash_mod_key key l) l1.v + := match l0 with + | .Nil => by + simp [insert_in_list_back, insert_in_list_loop_back, List.lookup, List.v, slot_s_inv_hash] + tauto + | .Cons k v tl0 => + if h: k = key then + by + simp [insert_in_list_back, List.lookup] + rw [insert_in_list_loop_back] + simp [h, List.lookup] + constructor + . intros; simp [*] + . simp [List.v, slot_s_inv_hash] at * + simp [*] + else + by + simp [insert_in_list_back, List.lookup] + rw [insert_in_list_loop_back] + simp [h, List.lookup] + have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by + simp_all [List.v, slot_s_inv_hash] + progress keep as heq as ⟨ tl1 hp1 hp2 hp3 ⟩ + 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 + simp [List.v, slot_s_inv_hash] at * + simp [*] + simp (config := {contextual := true}) [*, List.lookup] + + end HashMap end hashmap |