summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r--backends/lean/Base/Progress/Base.lean2
-rw-r--r--backends/lean/Base/Progress/Progress.lean107
2 files changed, 77 insertions, 32 deletions
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