summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base/Progress/Base.lean16
-rw-r--r--backends/lean/Base/Progress/Progress.lean178
2 files changed, 112 insertions, 82 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 935af3f5..a64212a5 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -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
@@ -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
@@ -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
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 0fb276aa..dc30c441 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -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
@@ -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 =>
@@ -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)
@@ -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 <|> "_"),* " .."? " ⟩")?
@@ -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