diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Arith/Arith.lean | 42 | ||||
| -rw-r--r-- | backends/lean/Base/Diverge/Base.lean | 22 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 2 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 107 | ||||
| -rw-r--r-- | backends/lean/Base/Utils.lean | 62 |
5 files changed, 140 insertions, 95 deletions
diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean index 20420f36..ab4fd182 100644 --- a/backends/lean/Base/Arith/Arith.lean +++ b/backends/lean/Base/Arith/Arith.lean @@ -11,49 +11,9 @@ import Base.Primitives import Base.Utils import Base.Arith.Base -/- -Mathlib tactics: -- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases -- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs -- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num -- should we use linarith or omega? -- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint -- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical --/ - -namespace List - - -- TODO: I could not find this function?? - @[simp] def flatten {a : Type u} : List (List a) → List a - | [] => [] - | x :: ls => x ++ flatten ls - -end List - -namespace Lean - -namespace LocalContext - - open Lean Lean.Elab Command Term Lean.Meta - - -- Small utility: return the list of declarations in the context, from - -- the last to the first. - def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := - lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) [] - - -- Return the list of declarations in the context, but filter the - -- declarations which are considered as implementation details - def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do - let ls ← lctx.getAllDecls - pure (ls.filter (fun d => not d.isImplementationDetail)) - -end LocalContext - -end Lean - namespace Arith -open Primitives +open Primitives Utils -- TODO: move? theorem ne_zero_is_lt_or_gt {x : Int} (hne : x ≠ 0) : x < 0 ∨ x > 0 := by diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean index d2c91ff8..0a9ea4c4 100644 --- a/backends/lean/Base/Diverge/Base.lean +++ b/backends/lean/Base/Diverge/Base.lean @@ -6,28 +6,6 @@ import Mathlib.Tactic.Linarith import Base.Primitives -/- -TODO: -- we want an easier to use cases: - - keeps in the goal an equation of the shape: `t = case` - - if called on Prop terms, uses Classical.em - Actually, the cases from mathlib seems already quite powerful - (https://leanprover-community.github.io/mathlib_docs/tactics.html#cases) - For instance: cases h : e - Also: **casesm** -- better split tactic -- we need conversions to operate on the head of applications. - Actually, something like this works: - ``` - conv at Hl => - apply congr_fun - simp [fix_fuel_P] - ``` - Maybe we need a rpt ... ; focus? -- simplifier/rewriter have a strange behavior sometimes --/ - - /- TODO: this is very useful, but is there more? -/ set_option profiler true set_option profiler.threshold 100 diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index 613f38f8..a288d889 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -60,7 +60,7 @@ section Methods trace[Progress] "Theorem: {th}" -- Dive into the quantified variables and the assumptions forallTelescope th fun fvars th => do - trace[Progress] "All argumens: {fvars}" + trace[Progress] "All arguments: {fvars}" /- -- Filter the argumens which are not propositions let rec getFirstPropIdx (i : Nat) : MetaM Nat := do if i ≥ fargs.size then pure i diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index a4df5c96..b0db465d 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -21,24 +21,11 @@ namespace Test #eval pspecAttr.find? ``Primitives.Vec.index end Test -def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do - withMainContext do - -- Retrieve the goal - let mgoal ← Tactic.getMainGoal - let goalTy ← mgoal.getType - -- Dive into the goal to lookup the theorem - let (fName, fLevels, args) ← do - withPSpec goalTy fun desc => - -- TODO: check that no universally quantified variables in the arguments - pure (desc.fName, desc.fLevels, desc.args) - -- TODO: also try the assumptions - trace[Progress] "Function: {fName}" - -- TODO: use a list of theorems, and try them one by one? - let thName ← do - match ← pspecAttr.find? fName with - | none => throwError "Could not find a pspec theorem for {fName}" - | some thName => pure thName - trace[Progress] "Lookuped up: {thName}" +inductive TheoremOrLocal where +| Theorem (thName : Name) +| Local (asm : LocalDecl) + +def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do /- Apply the theorem We try to match the theorem with the goal In order to do so, we introduce meta-variables for all the parameters @@ -48,10 +35,14 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do quantified). We also make sure that all the meta variables which appear in the function arguments have been instantiated - -/ + -/ let env ← getEnv - let thDecl := env.constants.find! thName - let thTy := thDecl.type + let thTy ← do + match th with + | .Theorem thName => + let thDecl := env.constants.find! thName + pure thDecl.type + | .Local asmDecl => pure asmDecl.type -- TODO: the tactic fails if we uncomment withNewMCtxDepth -- withNewMCtxDepth do let (mvars, binders, thExBody) ← forallMetaTelescope thTy @@ -63,18 +54,19 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do -- There shouldn't be any existential variables in thBody pure thBody -- Match the body with the target - let target := mkAppN (.const fName fLevels) args - trace[Progress] "mvars:\n{mvars.map Expr.mvarId!}" - trace[Progress] "thBody: {thBody}" - trace[Progress] "target: {target}" - let ok ← isDefEq thBody target - if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {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}" + let mgoal ← Tactic.getMainGoal postprocessAppMVars `progress mgoal mvars binders true true Term.synthesizeSyntheticMVarsNoPostponing let thBody ← instantiateMVars thBody trace[Progress] "thBody (after instantiation): {thBody}" -- Add the instantiated theorem to the assumptions (we apply it on the metavariables). - let th ← mkAppOptM thName (mvars.map some) + let th ← do + match th with + | .Theorem thName => mkAppOptM thName (mvars.map some) + | .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some) let asmName ← mkFreshUserName `h let thTy ← inferType th let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false) @@ -112,18 +104,71 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do -- pure () -elab "progress" : tactic => do - progressLookupTheorem (firstTac [assumptionTac, Arith.scalarTac]) +-- The array of ids are identifiers to use when introducing fresh variables +def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do + withMainContext do + -- Retrieve the goal + let mgoal ← Tactic.getMainGoal + let goalTy ← mgoal.getType + -- Dive into the goal to lookup the theorem + let (fName, fLevels, 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 + trace[Progress] "Function: {fName}" + -- Try all the assumptions one by one and if it fails try to lookup a theorem + let ctx ← Lean.MonadLCtx.getLCtx + let decls ← ctx.getDecls + for decl in decls.reverse do + trace[Progress] "Trying assumption: {decl.userName} : {decl.type}" + try + progressWith fnExpr (.Local decl) ids asmTac + return () + catch _ => continue + -- It failed: try to lookup a theorem + -- TODO: use a list of theorems, and try them one by one? + trace[Progress] "No assumption succeeded: trying to lookup a theorem" + let thName ← do + match ← pspecAttr.find? fName with + | none => throwError "Could not find a pspec theorem for {fName}" + | some thName => pure thName + trace[Progress] "Lookuped up: {thName}" + -- Apply the theorem + progressWith fnExpr (.Theorem thName) ids asmTac + +#check Syntax +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}" + let args := args.getArgs + let ids := + if args.size > 0 then + let args := (args.get! 0).getArgs + let args := (args.get! 2).getArgs + args.map Syntax.getId + else #[] + trace[Progress] "Ids: {ids}" + --if args[0] ≠ some "as" then throwError "Invalid syntax: should be: `progress as ⟨ ... ⟩`" + progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac]) + +elab "progress" args:progressArgs : tactic => + evalProgress args namespace Test open Primitives set_option trace.Progress true + set_option pp.rawOnError true @[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 + progress as ⟨ x y z ⟩ simp set_option trace.Progress false diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index 14feb567..505412b9 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -2,6 +2,68 @@ import Lean import Mathlib.Tactic.Core import Mathlib.Tactic.LeftRight +/- +Mathlib tactics: +- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases +- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs +- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num +- should we use linarith or omega? +- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint +- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical +-/ + +/- +TODO: +- we want an easier to use cases: + - keeps in the goal an equation of the shape: `t = case` + - if called on Prop terms, uses Classical.em + Actually, the cases from mathlib seems already quite powerful + (https://leanprover-community.github.io/mathlib_docs/tactics.html#cases) + For instance: cases h : e + Also: **casesm** +- better split tactic +- we need conversions to operate on the head of applications. + Actually, something like this works: + ``` + conv at Hl => + apply congr_fun + simp [fix_fuel_P] + ``` + Maybe we need a rpt ... ; focus? +- simplifier/rewriter have a strange behavior sometimes +-/ + + +namespace List + + -- TODO: I could not find this function?? + @[simp] def flatten {a : Type u} : List (List a) → List a + | [] => [] + | x :: ls => x ++ flatten ls + +end List + +namespace Lean + +namespace LocalContext + + open Lean Lean.Elab Command Term Lean.Meta + + -- Small utility: return the list of declarations in the context, from + -- the last to the first. + def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := + lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) [] + + -- Return the list of declarations in the context, but filter the + -- declarations which are considered as implementation details + def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do + let ls ← lctx.getAllDecls + pure (ls.filter (fun d => not d.isImplementationDetail)) + +end LocalContext + +end Lean + namespace Utils open Lean Elab Term Meta Tactic |