Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: progress with a term #281

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

feat: progress with a term #281

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
92 changes: 52 additions & 40 deletions backends/lean/Base/Progress/Progress.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ inductive TheoremOrLocal where
| Local (asm : LocalDecl)

structure Stats where
usedTheorem : TheoremOrLocal
usedTheorem : Syntax

instance : ToMessageData TheoremOrLocal where
toMessageData := λ x => match x with | .Theorem thName => m!"{thName}" | .Local asm => m!"{asm.userName}"
Expand All @@ -51,7 +51,7 @@ inductive ProgressError
| Error (msg : MessageData)
deriving Inhabited

def progressWith (fExpr : Expr) (th : TheoremOrLocal)
def progressWith (fExpr : Expr) (thExpr : Expr)
(keep : Option Name) (ids : Array (Option Name)) (splitPost : Bool)
(asmTac : TacticM Unit) : TacticM ProgressError := do
/- Apply the theorem
Expand All @@ -64,14 +64,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
We also make sure that all the meta variables which appear in the
function arguments have been instantiated
-/
let thTy ← do
match th with
| .Theorem thName =>
-- Lookup the theorem and introduce fresh meta-variables for the universes
let th ← mkConstWithFreshMVarLevels thName
-- Retrieve the type
inferType th
| .Local asmDecl => pure asmDecl.type
let thTy ← inferType thExpr
trace[Progress] "Looked up theorem/assumption type: {thTy}"
-- TODO: the tactic fails if we uncomment withNewMCtxDepth
-- withNewMCtxDepth do
Expand All @@ -98,13 +91,10 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
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 ← do
match th with
| .Theorem thName => mkAppOptM thName (mvars.map some)
| .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some)
let th ← mkAppOptM' thExpr (mvars.map some)
trace[Progress] "Instantiated theorem reusing the metavariables: {th}"
let asmName ← do match keep with | none => mkFreshAnonPropUserName | some n => do pure n
let thTy ← inferType th
let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false)
let thAsm ← Utils.addDeclTac asmName th (← inferType th) (asLet := false)
withMainContext do -- The context changed - TODO: remove once addDeclTac is updated
let ngoal ← getMainGoal
trace[Progress] "current goal: {ngoal}"
Expand Down Expand Up @@ -219,7 +209,7 @@ def getFirstArg (args : Array Expr) : Option Expr := do
Return true if it succeeded. -/
def tryLookupApply (keep : Option Name) (ids : Array (Option Name)) (splitPost : Bool)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should rename this function to tryApply, because it doesn't perform a lookup anymore.
Also, it might make sense to move the match over the option (and the comments printed in the trace are not valid anymore I believe).

(asmTac : TacticM Unit) (fExpr : Expr)
(kind : String) (th : Option TheoremOrLocal) : TacticM Bool := do
(kind : String) (th : Option Expr) : TacticM Bool := do
let res ← do
match th with
| none =>
Expand All @@ -239,8 +229,8 @@ def tryLookupApply (keep : Option Name) (ids : Array (Option Name)) (splitPost :
| none => pure false

-- The array of ids are identifiers to use when introducing fresh variables
def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal)
(ids : Array (Option Name)) (splitPost : Bool) (asmTac : TacticM Unit) : TacticM TheoremOrLocal := do
def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option Expr)
(ids : Array (Option Name)) (splitPost : Bool) (asmTac : TacticM Unit) : TacticM Syntax := do
withMainContext do
-- Retrieve the goal
let mgoal ← Tactic.getMainGoal
Expand Down Expand Up @@ -268,17 +258,17 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
match withTh with
| some th => do
match ← progressWith fExpr th keep ids splitPost asmTac with
| .Ok => return th
| .Ok => return (← exprToSyntax th)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, I'm not so sure this is the right way to transform an expression to syntax for progress?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does it generate spurious syntax?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, just dump a metavariable I think

Copy link
Member

@sonmarcho sonmarcho Jul 11, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure I understand in which situations it dumps a metavariable: could you clarify a bit?
But if exprToSyntax doesn't work there is likely a simple way of getting the name of the theorem and transforming it to syntax.

| .Error msg => throwError msg
| none =>
-- 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}"
let res ← do try progressWith fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue
let res ← do try progressWith fExpr decl.toExpr keep ids splitPost asmTac catch _ => continue
match res with
| .Ok => return (.Local decl)
| .Ok => return (mkIdent decl.userName)
| .Error msg => throwError msg
-- It failed: lookup the pspec theorems which match the expression *only
-- if the function is a constant*
Expand All @@ -288,18 +278,20 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
if ¬ fIsConst then throwError "Progress failed"
else do
trace[Progress] "No assumption succeeded: trying to lookup a pspec theorem"
let pspecs : Array TheoremOrLocal ← do
let pspecs : Array Name ← do
let thNames ← pspecAttr.find? fExpr
-- TODO: because of reduction, there may be several valid theorems (for
-- instance for the scalars). We need to sort them from most specific to
-- least specific. For now, we assume the most specific theorems are at
-- the end.
let thNames := thNames.reverse
trace[Progress] "Looked up pspec theorems: {thNames}"
pure (thNames.map fun th => TheoremOrLocal.Theorem th)
pure thNames
-- Try the theorems one by one
for pspec in pspecs do
if ← tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspec then return pspec
-- TODO: convert pspec into an Expr.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What it this TODO?

let pspecExpr ← Term.mkConst pspec
if ← tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspecExpr then return (mkIdent pspec)
else pure ()
-- It failed: try to use the recursive assumptions
trace[Progress] "Failed using a pspec theorem: trying to use a recursive assumption"
Expand All @@ -310,14 +302,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 splitPost asmTac catch _ => continue
let res ← do try progressWith fExpr decl.toExpr keep ids splitPost asmTac catch _ => continue
match res with
| .Ok => return (.Local decl)
| .Ok => return (mkIdent decl.userName)
| .Error msg => throwError msg
-- Nothing worked: failed
throwError "Progress failed"

syntax progressArgs := ("keep" (ident <|> "_"))? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")?
syntax progressArgs := ("keep" (ident <|> "_"))? ("with" term)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")?

def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Stats := do
let args := args.raw
Expand All @@ -343,17 +335,27 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Stats := do
if withArg.size > 0 then
let id := withArg.get! 1
trace[Progress] "With arg: {id}"
-- Attempt to lookup a local declaration
match (← getLCtx).findFromUserName? id.getId with
| some decl => do
trace[Progress] "With arg: local decl"
pure (some (.Local decl))
| none => do
-- Not a local declaration: should be a theorem
trace[Progress] "With arg: theorem"
addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
let some (.const name _) ← Term.resolveId? id | throwError m!"Could not find theorem: {id}"
pure (some (.Theorem name))

-- Either, it's a local declaration or a theorem, either it's a term
-- for which we need to find a declaration

if id.isIdent then
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think we really need this case disjunction. Shouldn't it be performed by Lean's elaboration (i.e., isn't the else branch enough)?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, if I do that, something like:

set_option trace.Progress true in
  example {x: U32}
    (f : Result U32 → Result Unit)
    (h : ∀ (x: U32), ∀ (y: U32), f (x + y) = .ok ()):
      f (.ok x) = ok () := by
      have : ∀ x, f x = .ok () := by sorry
      progress with this

won't work because this elaborated := sorryAx ?m.something true and the metavariable will create an obscure failure of progress here.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(tbh, the current code does not work neither, it fails by not finding this in the context)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, this is good to know (and worth commenting in the code ;) )

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wouldn't this be a blocker though for the PR? I'm trying to make this work but I'm just diving into how the whole thing is supposed to work

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What I meant is that the fact that we need the case disjunction is good to know and should be documented. But of course, we need to make the elaboration work, generally speaking.

-- Attempt to lookup a local declaration
match (← getLCtx).findFromUserName? id.getId with
| some decl => do
trace[Progress] "With arg: local decl"
pure (some decl.toExpr)
| none => do
-- Not a local declaration: should be a theorem
trace[Progress] "With arg: theorem"
addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
let some e ← Term.resolveId? id | throwError m!"Could not find theorem: {id}"
pure (some e)
else
trace[Progress] "With arg: not an identifier (a term?)"
let e ← Tactic.elabTerm id none
trace[Progress] m!"With arg: elaborated expression {e}"
pure (some e)
else pure none
let ids :=
let args := asArgs.getArgs
Expand Down Expand Up @@ -392,9 +394,12 @@ elab tk:"progress?" args:progressArgs : tactic => do
let stats ← evalProgress args
let mut stxArgs := args.raw
if stxArgs[1].isNone then
let withArg := mkNullNode #[mkAtom "with", mkIdent stats.usedTheorem]
let withArg := mkNullNode #[mkAtom "with", stats.usedTheorem]
stxArgs := stxArgs.setArg 1 withArg
let tac := mkNode `Progress.progress #[mkAtom "progress", stxArgs]
-- if stats.usedTheorem.isInaccesisble then
-- logInfo "{...} is inaccessible, if you want to actually use the suggestion, please use `rename_i ...`"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please remove all commented code (note however that printing such a comment would be useful, if it is possible).


Meta.Tactic.TryThis.addSuggestion tk tac (origSpan? := ← getRef)

namespace Test
Expand Down Expand Up @@ -505,6 +510,13 @@ namespace Test
progress keep _ as ⟨ z, h1 .. ⟩
simp [*, h1]

/- Progress using a term -/
example {x: U32}
(f : U32 → Result Unit)
(h : ∀ x, f x = .ok ()):
f x = ok () := by
progress with (show ∀ x, f x = .ok () by exact h)

end Test

end Progress