diff options
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 11 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 11 | ||||
| -rw-r--r-- | backends/lean/Base/Utils.lean | 4 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 24 |
4 files changed, 32 insertions, 18 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index 00b0a478..7eace667 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -58,10 +58,10 @@ section Methods def withPSpec [Inhabited (m a)] [Nonempty (m a)] (th : Expr) (k : PSpecDesc → m a) (sanityChecks : Bool := false) : m a := do - trace[Progress] "Theorem: {th}" + trace[Progress] "Proposition: {th}" -- Dive into the quantified variables and the assumptions forallTelescope th fun fvars th => do - trace[Progress] "All arguments: {fvars}" + trace[Progress] "Universally quantified arguments and assumptions: {fvars}" /- -- Filter the argumens which are not propositions let rec getFirstPropIdx (i : Nat) : MetaM Nat := do if i ≥ fargs.size then pure i @@ -83,12 +83,16 @@ section Methods -- Dive into the existentials existsTelescope th 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 + trace[Progress] "After splitting the conjunction:\n- eq: {th}\n- post: {post}" -- Destruct the equality let (th, ret) ← destEq th + trace[Progress] "After splitting the equality:\n- lhs: {th}\n- rhs: {ret}" -- Destruct the application to get the name - th.withApp fun f args => do + th.consumeMData.withApp fun f args => do + trace[Progress] "After stripping the arguments:\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 @@ -114,6 +118,7 @@ section Methods post := post } k thDesc + end Methods diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 001967e5..ace92f4f 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -55,14 +55,20 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name) let thDecl := env.constants.find! thName pure thDecl.type | .Local asmDecl => pure asmDecl.type + trace[Progress] "theorem/assumption type: {thTy}" -- TODO: the tactic fails if we uncomment withNewMCtxDepth -- withNewMCtxDepth do let (mvars, binders, thExBody) ← forallMetaTelescope thTy + trace[Progress] "After stripping foralls: {thExBody}" -- Introduce the existentially quantified variables and the post-condition -- in the context let thBody ← existsTelescope thExBody fun _evars thBody => do + trace[Progress] "After stripping existentials: {thBody}" + let (thBody, _) ← optSplitConj thBody + trace[Progress] "After splitting the conjunction: {thBody}" let (thBody, _) ← destEq thBody + trace[Progress] "After splitting equality: {thBody}" -- There shouldn't be any existential variables in thBody pure thBody -- Match the body with the target @@ -152,6 +158,7 @@ def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : Tac -- Retrieve the goal let mgoal ← Tactic.getMainGoal let goalTy ← mgoal.getType + trace[Progress] "goal: {goalTy}" -- Dive into the goal to lookup the theorem let (fName, fLevels, args) ← do withPSpec goalTy fun desc => @@ -188,7 +195,7 @@ syntax progressArgs := ("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] "Progressing arguments: {args}" + trace[Progress] "Progress arguments: {args}" let args := args.getArgs let ids := if args.size > 0 then @@ -196,7 +203,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do let args := (args.get! 2).getArgs args.map Syntax.getId else #[] - trace[Progress] "Ids: {ids}" + trace[Progress] "User-provided ids: {ids}" progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac]) elab "progress" args:progressArgs : tactic => diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index 599c3a9f..9cd0db23 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -43,6 +43,10 @@ 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 1db39422..ee22bebd 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -105,6 +105,8 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : simp [h] else by + -- TODO: use progress: detect that this is a recursive call, or give + -- the possibility of specifying an identifier have ⟨ b, hi ⟩ := insert_in_list_spec key value tl exists b simp [insert_in_list, List.lookup] @@ -112,13 +114,12 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) : simp [h] simp [insert_in_list] at hi exact hi - -/-- + @[pspec] theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ - (b = (List.lookup ls.v key = none)) + (b ↔ (List.lookup ls.v key = none)) := by induction ls case Nil => simp [insert_in_list, insert_in_list_loop, List.lookup] @@ -130,11 +131,12 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) simp [h] else conv => - rhs; ext; arg 1; simp [h] -- TODO: Simplify - simp [insert_in_list] at ih; - progress -- TODO: Does not work ---/ - + rhs; ext; left; simp [h] -- TODO: Simplify + simp only [insert_in_list] at ih; + -- TODO: give the possibility of using underscores + progress as ⟨ b h ⟩ + simp [*] + @[pspec] theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List α) : ∃ l1, @@ -150,8 +152,7 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List rw [insert_in_list_loop_back] simp [h, List.lookup] intro k1 h1 - have h2 : ¬(key = k1) := by tauto -- TODO: Why is the order of args in eq swapped - simp [h2] + simp [*] else by simp [insert_in_list_back, List.lookup] @@ -159,12 +160,9 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List simp [h, List.lookup] have ⟨tl0 , _, _ ⟩ := insert_in_list_back_spec key value tl -- TODO: Use progress simp [insert_in_list_back] at * - simp [*] - have : ¬ (key = k) := by tauto simp [List.lookup, *] simp (config := {contextual := true}) [*] end HashMap --- def distinct_keys {α : Type u} end hashmap |