Skip to content

Commit

Permalink
Fix a minor issue with the progress tactic
Browse files Browse the repository at this point in the history
  • Loading branch information
sonmarcho committed Jan 27, 2024
1 parent 9f0e460 commit c709ead
Show file tree
Hide file tree
Showing 2 changed files with 112 additions and 82 deletions.
16 changes: 11 additions & 5 deletions backends/lean/Base/Progress/Base.lean
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,9 @@ structure PSpecDesc where
evars : Array Expr
-- The function applied to its arguments
fArgsExpr : Expr
-- The function
fName : Name
-- ⊤ if the function is a constant (must be if we are registering a theorem,
-- but is not necessarily the case if we are looking at a goal)
fIsConst : Bool
-- The function arguments
fLevels : List Level
args : Array Expr
Expand Down Expand Up @@ -98,7 +99,12 @@ section Methods
pure (mExpr, mf, margs)
let (fArgsExpr, f, args) ← strip_monad mExpr
trace[Progress] "After stripping the arguments of the function call:\n- f: {f}\n- args: {args}"
if ¬ f.isConst then throwError "Not a constant: {f}"
let fLevels ← do
-- If we are registering a theorem, then the function must be a constant
if ¬ f.isConst then
if isGoal then pure []
else throwError "Not a constant: {f}"
else pure f.constLevels!
-- *Sanity check* (activated if we are analyzing a theorem to register it in a DB)
-- Check if some existentially quantified variables
let _ := do
Expand All @@ -117,8 +123,8 @@ section Methods
fvars := fvars
evars := evars
fArgsExpr
fName := f.constName!
fLevels := f.constLevels!
fIsConst := f.isConst
fLevels
args := args
ret := ret
post := post
Expand Down
178 changes: 101 additions & 77 deletions backends/lean/Base/Progress/Progress.lean
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
withMainContext do -- The context changed - TODO: remove once addDeclTac is updated
let ngoal ← getMainGoal
trace[Progress] "current goal: {ngoal}"
trace[Progress] "current goal: {← ngoal.isAssigned}"
trace[Progress] "current goal is assigned: {← ngoal.isAssigned}"
-- The assumption should be of the shape:
-- `∃ x1 ... xn, f args = ... ∧ ...`
-- We introduce the existentially quantified variables and split the top-most
Expand All @@ -131,50 +131,59 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
-- then continue splitting the post-condition
splitEqAndPost fun hEq hPost ids => do
trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}"
tryTac (
simpAt true []
[``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
[hEq.fvarId!] (.targets #[] true))
-- TODO: remove this (some types get unfolded too much: we "fold" them back)
tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
-- Clear the equality, unless the user requests not to do so
let mgoal ← do
if keep.isSome then getMainGoal
else do
let mgoal ← getMainGoal
mgoal.tryClearMany #[hEq.fvarId!]
setGoals (mgoal :: (← getUnsolvedGoals))
trace[Progress] "Goal after splitting eq and post and simplifying the target: {mgoal}"
-- 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) (ids0 : List (Option Name)) : TacticM ProgressError := do
match ids0 with
| [] =>
/- 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 true hPost (λ _ => pure .Ok)
else pure .Ok
| nid :: ids => do
trace[Progress] "Splitting post: {← inferType hPost}"
-- Split
let nid ← do
match nid with
| none => mkFreshAnonPropUserName
| some nid => pure nid
trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}"
if ← isConj (← inferType hPost) then
splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPostWithIds nid nhPost ids)
else return (.Error m!"Too many ids provided ({ids0}) not enough conjuncts to split in the postcondition")
let curPostId := (← hPost.fvarId!.getDecl).userName
splitPostWithIds curPostId hPost ids
trace[Progress] "current goal: {← getMainGoal}"
Tactic.focus do
let _ ←
tryTac
(simpAt true []
[``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
[hEq.fvarId!] (.targets #[] true))
-- It may happen that at this point the goal is already solved (though this is rare)
-- TODO: not sure this is the best way of checking it
if (← getUnsolvedGoals) == [] then pure .Ok
else
trace[Progress] "goal after applying the eq and simplifying the binds: {← getMainGoal}"
-- TODO: remove this (some types get unfolded too much: we "fold" them back)
let _ ← tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
trace[Progress] "goal after folding back scalar types: {← getMainGoal}"
-- Clear the equality, unless the user requests not to do so
let mgoal ← do
if keep.isSome then getMainGoal
else do
let mgoal ← getMainGoal
mgoal.tryClearMany #[hEq.fvarId!]
setGoals (mgoal :: (← getUnsolvedGoals))
trace[Progress] "Goal after splitting eq and post and simplifying the target: {mgoal}"
-- 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) (ids0 : List (Option Name)) : TacticM ProgressError := do
match ids0 with
| [] =>
/- 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 true hPost (λ _ => pure .Ok)
else pure .Ok
| nid :: ids => do
trace[Progress] "Splitting post: {← inferType hPost}"
-- Split
let nid ← do
match nid with
| none => mkFreshAnonPropUserName
| some nid => pure nid
trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}"
if ← isConj (← inferType hPost) then
splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPostWithIds nid nhPost ids)
else return (.Error m!"Too many ids provided ({ids0}) not enough conjuncts to split in the postcondition")
let curPostId := (← hPost.fvarId!.getDecl).userName
splitPostWithIds curPostId hPost ids
match res with
| .Error _ => return res -- Can we get there? We're using "return"
| .Ok =>
Expand Down Expand Up @@ -223,9 +232,9 @@ def tryLookupApply (keep : Option Name) (ids : Array (Option Name)) (splitPost :
pure (some res)
catch _ => none
match res with
| some .Ok => return true
| some .Ok => pure true
| some (.Error msg) => throwError msg
| none => return false
| none => pure false

-- The array of ids are identifiers to use when introducing fresh variables
def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal)
Expand Down Expand Up @@ -266,36 +275,42 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
match res with
| .Ok => return ()
| .Error msg => throwError msg
-- It failed: lookup the pspec theorems which match the expression
trace[Progress] "No assumption succeeded: trying to lookup a pspec theorem"
let pspecs : Array TheoremOrLocal ← 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)
-- Try the theorems one by one
for pspec in pspecs do
if ← tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspec then return ()
else pure ()
-- It failed: try to use the recursive assumptions
trace[Progress] "Failed using a pspec theorem: trying to use a recursive assumption"
-- We try to apply the assumptions of kind "auxDecl"
let ctx ← Lean.MonadLCtx.getLCtx
let decls ← ctx.getAllDecls
let decls := decls.filter (λ decl => match decl.kind with
| .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
match res with
| .Ok => return ()
| .Error msg => throwError msg
-- Nothing worked: failed
throwError "Progress failed"
-- It failed: lookup the pspec theorems which match the expression *only
-- if the function is a constant*
let fIsConst ← do
fExpr.consumeMData.withApp fun mf _ => do
pure mf.isConst
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 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)
-- Try the theorems one by one
for pspec in pspecs do
if ← tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspec then return ()
else pure ()
-- It failed: try to use the recursive assumptions
trace[Progress] "Failed using a pspec theorem: trying to use a recursive assumption"
-- We try to apply the assumptions of kind "auxDecl"
let ctx ← Lean.MonadLCtx.getLCtx
let decls ← ctx.getAllDecls
let decls := decls.filter (λ decl => match decl.kind with
| .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
match res with
| .Ok => return ()
| .Error msg => throwError msg
-- Nothing worked: failed
throwError "Progress failed"

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

Expand Down Expand Up @@ -434,6 +449,15 @@ namespace Test
progress
simp [*]

/- Checking the case where simplifying the goal after instantiating the
pspec theorem the goal actually solves it, and where the function is
not a constant. We also test the case where the function under scrutinee
is not a constant. -/
example {x : U32}
(f : U32 → Result Unit) (h : ∀ x, f x = .ret ()) :
f x = ret () := by
progress

end Test

end Progress

0 comments on commit c709ead

Please sign in to comment.