From 2dd56a51df01421fe7766858c9d37998db4123b5 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 25 Jul 2023 11:53:49 +0200 Subject: Improve the syntax of progress: `as ⟨ x, y .. ⟩` --- backends/lean/Base/Progress/Progress.lean | 77 ++++++++++++++++++------------- backends/lean/Base/Utils.lean | 61 ++++++++++++++++++------ tests/lean/Hashmap/Properties.lean | 34 ++------------ 3 files changed, 98 insertions(+), 74 deletions(-) diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 1c509775..c8f94e9e 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -23,7 +23,8 @@ inductive ProgressError | Error (msg : MessageData) deriving Inhabited -def progressWith (fExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids : Array Name) +def progressWith (fExpr : Expr) (th : TheoremOrLocal) + (keep : Option Name) (ids : Array Name) (splitPost : Bool) (asmTac : TacticM Unit) : TacticM ProgressError := do /- Apply the theorem We try to match the theorem with the goal @@ -112,24 +113,31 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids mgoal.tryClearMany #[hEq.fvarId!] setGoals (mgoal :: (← getUnsolvedGoals)) trace[Progress] "Goal after splitting eq and post and simplifying the target: {mgoal}" - -- Continue splitting following the ids provided by the user - if ¬ ids.isEmpty then - let hPost ← - match hPost with - | none => do return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split") - | some hPost => pure hPost - let rec splitPost (prevId : Name) (hPost : Expr) (ids : List Name) : TacticM ProgressError := do + -- Continue splitting following the post following the user's instructions + match hPost with + | none => + -- Sanity check + if ¬ ids.isEmpty then + return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split") + else return .Ok + | some hPost => do + let rec splitPostWithIds (prevId : Name) (hPost : Expr) (ids : List Name) : TacticM ProgressError := do match ids with - | [] => pure .Ok -- Stop + | [] => + /- We used all the user provided ids. + Split the remaining conjunctions by using fresh ids if the user + instructed to fully split the post-condition, otherwise stop -/ + if splitPost then + splitFullConjTac hPost (λ _ => pure .Ok) + else pure .Ok | nid :: ids => do trace[Progress] "Splitting post: {hPost}" -- Split if ← isConj (← inferType hPost) then - splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPost nid nhPost ids) + splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPostWithIds nid nhPost ids) else return (.Error m!"Too many ids provided ({nid :: ids}) not enough conjuncts to split in the postcondition") let curPostId := (← hPost.fvarId!.getDecl).userName - splitPost curPostId hPost ids - else return .Ok + splitPostWithIds curPostId hPost ids match res with | .Error _ => return res -- Can we get there? We're using "return" | .Ok => @@ -160,7 +168,8 @@ 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) (fExpr : Expr) +def tryLookupApply (keep : Option Name) (ids : Array Name) (splitPost : Bool) + (asmTac : TacticM Unit) (fExpr : Expr) (kind : String) (th : Option TheoremOrLocal) (x : TacticM Unit) : TacticM Unit := do let res ← do match th with @@ -172,7 +181,7 @@ def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Uni -- Apply the theorem let res ← do try - let res ← progressWith fExpr th keep ids asmTac + let res ← progressWith fExpr th keep ids splitPost asmTac pure (some res) catch _ => none match res with @@ -181,7 +190,8 @@ def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Uni | none => x -- The array of ids are identifiers to use when introducing fresh variables -def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do +def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal) + (ids : Array Name) (splitPost : Bool) (asmTac : TacticM Unit) : TacticM Unit := do withMainContext do -- Retrieve the goal let mgoal ← Tactic.getMainGoal @@ -197,7 +207,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL -- Otherwise, lookup one. match withTh with | some th => do - match ← progressWith fExpr th keep ids asmTac with + match ← progressWith fExpr th keep ids splitPost asmTac with | .Ok => return () | .Error msg => throwError msg | none => @@ -206,7 +216,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 fExpr (.Local decl) keep ids asmTac catch _ => continue + let res ← do try progressWith fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue match res with | .Ok => return () | .Error msg => throwError msg @@ -216,7 +226,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 fExpr "pspec theorem" pspec do + tryLookupApply keep ids splitPost 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 @@ -225,7 +235,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 fExpr "pspec class expr theorem" pspecClassExpr do + tryLookupApply keep ids splitPost asmTac fExpr "pspec class expr theorem" pspecClassExpr do -- It failed: try to lookup a *class* spec theorem let pspecClass ← do match ← getFirstArgAppName args with @@ -233,7 +243,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 fExpr "pspec class theorem" pspecClass do + tryLookupApply keep ids splitPost 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 @@ -241,14 +251,14 @@ 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 fExpr (.Local decl) keep ids asmTac catch _ => continue + let res ← do try progressWith fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue match res with | .Ok => return () | .Error msg => throwError msg -- Nothing worked: failed throwError "Progress failed" -syntax progressArgs := ("keep" ("as" (ident))?)? ("with" ident)? ("as" " ⟨ " (ident)+ " ⟩")? +syntax progressArgs := ("keep" ("as" (ident))?)? ("with" ident)? ("as" " ⟨ " ident,* " .."? " ⟩")? def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do let args := args.raw @@ -263,8 +273,8 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do else do pure (some (← mkFreshUserName `h)) else pure none trace[Progress] "Keep: {keep}" - let withArg := (args.get! 1).getArgs let withArg ← do + let withArg := (args.get! 1).getArgs if withArg.size > 0 then let id := withArg.get! 1 trace[Progress] "With arg: {id}" @@ -283,20 +293,25 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do | id :: _ => pure (some (.Theorem id)) else pure none - let args := (args.get! 2).getArgs - let args := (args.get! 2).getArgs - let ids := args.map Syntax.getId + let ids := + let args := (args.get! 2).getArgs + let args := (args.get! 2).getSepArgs + args.map Syntax.getId trace[Progress] "User-provided ids: {ids}" - progressAsmsOrLookupTheorem keep withArg ids (firstTac [assumptionTac, Arith.scalarTac]) + let splitPost : Bool := + let args := (args.get! 2).getArgs + (args.get! 3).getArgs.size > 0 + trace[Progress] "Split post: {splitPost}" + progressAsmsOrLookupTheorem keep withArg ids splitPost (firstTac [assumptionTac, Arith.scalarTac]) elab "progress" args:progressArgs : tactic => evalProgress args -/- -namespace Test +/-namespace Test open Primitives Result set_option trace.Progress true + set_option pp.rawOnError true #eval showStoredPSpec #eval showStoredPSpecClass @@ -306,9 +321,9 @@ namespace Test (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 + progress keep as h as ⟨ z, h1 .. ⟩ simp [*] -end Test -/ +end Test-/ end Progress diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index f014e112..3b3d4729 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -499,7 +499,10 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr -- Try to use the user-provided names let altVarNames ← match optIds with - | none => pure #[] + | none => do + let id0 ← mkFreshUserName `h + let id1 ← mkFreshUserName `h + pure #[{ varNames := [id0, id1] }] | some (id0, id1) => do pure #[{ varNames := [id0, id1] }] let newGoals ← goal.cases h.fvarId! altVarNames @@ -518,29 +521,61 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr else throwError "Not a conjunction" -elab "split_conj " n:ident : tactic => do +-- Tactic to fully split a conjunction +partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (l : List Expr) (h : Expr) (k : List Expr → TacticM α) : TacticM α := do + try + splitConjTac h none (λ h1 h2 => + splitFullConjTacAux l h1 (λ l1 => + splitFullConjTacAux l1 h2 (λ l2 => + k l2))) + catch _ => + k (h :: l) + +-- Tactic to fully split a conjunction +def splitFullConjTac [Inhabited α] [Nonempty α] (h : Expr) (k : List Expr → TacticM α) : TacticM α := do + splitFullConjTacAux [] h (λ l => k l.reverse) + +syntax optAtArgs := ("at" ident)? +def elabOptAtArgs (args : TSyntax `Utils.optAtArgs) : TacticM (Option Expr) := do withMainContext do - let decl ← Lean.Meta.getLocalDeclFromUserName n.getId - let fvar := mkFVar decl.fvarId - splitConjTac fvar none (fun _ _ => pure ()) + let args := (args.raw.getArgs.get! 0).getArgs + if args.size > 0 then do + let n := (args.get! 1).getId + let decl ← Lean.Meta.getLocalDeclFromUserName n + let fvar := mkFVar decl.fvarId + pure (some fvar) + else + pure none -elab "split_all_exists " n:ident : tactic => do +elab "split_conj" args:optAtArgs : tactic => do + withMainContext do + match ← elabOptAtArgs args with + | some fvar => + splitConjTac fvar none (fun _ _ => pure ()) + | none => + splitConjTarget + +elab "split_conjs" args:optAtArgs : tactic => do + withMainContext do + match ← elabOptAtArgs args with + | some fvar => + splitFullConjTac fvar (fun _ => pure ()) + | none => + repeatTac splitConjTarget + +elab "split_existsl" " at " n:ident : tactic => do withMainContext do let decl ← Lean.Meta.getLocalDeclFromUserName n.getId let fvar := mkFVar decl.fvarId splitAllExistsTac fvar [] (fun _ _ => pure ()) -elab "split_target_conjs" : tactic => - withMainContext do - repeatTac splitConjTarget - example (h : a ∧ b) : a := by - split_all_exists h - split_conj h + split_existsl at h + split_conj at h assumption example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by - split_all_exists h + split_existsl at h rename_i x y z exists x + y + z diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index dce33fa4..de6bf636 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -94,7 +94,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 as heq as ⟨ b, hi ⟩ simp only [insert_in_list] at heq exists b @@ -116,35 +116,9 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) conv => 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 ⟩ + progress as ⟨ b, h ⟩ simp [*] -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 - l1.lookup key = value ∧ - (∀ k, k ≠ key → l1.lookup k = l0.lookup k) - := match l0 with - | .Nil => by - simp (config := {contextual := true}) [insert_in_list_back, insert_in_list_loop_back] - | .Cons k v tl => - if h: k = key then - by - simp [insert_in_list_back] - rw [insert_in_list_loop_back] - simp [h] - intro k1 h1 - simp [*] - else - by - simp [insert_in_list_back] - rw [insert_in_list_loop_back] - simp [h] - progress keep as heq as ⟨ tl hp1 hp2 ⟩ - simp [insert_in_list_back] at heq - simp (config := {contextual := true}) [*] - 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 := @@ -190,7 +164,7 @@ theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value: simp [insert_in_list_back] rw [insert_in_list_loop_back] simp [h] - split_target_conjs + split_conjs . intros; simp [*] . simp [List.v, slot_s_inv_hash] at * simp [*] @@ -206,7 +180,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 hp1 hp2 hp3 hp4 hp5 hp6 ⟩ + progress keep as 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 * -- cgit v1.2.3