summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
authorSon Ho2023-07-20 14:14:34 +0200
committerSon Ho2023-07-20 14:14:34 +0200
commit03492250b45855fe9db5e0a28a96166607cd84a1 (patch)
tree6ea4a188d630cf2d25704f09d6dc301aa6576a09 /backends/lean/Base
parent6ef1d360b89fd9f9383e63609888bf925a6a16ab (diff)
Make some proofs in Hashmap/Properties.lean and improve progress
Diffstat (limited to 'backends/lean/Base')
-rw-r--r--backends/lean/Base/Arith/Int.lean2
-rw-r--r--backends/lean/Base/Progress/Base.lean25
-rw-r--r--backends/lean/Base/Progress/Progress.lean68
-rw-r--r--backends/lean/Base/Utils.lean32
4 files changed, 64 insertions, 63 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index ac011998..fa957293 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -198,7 +198,7 @@ def intTac (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
-- Split the conjunctions in the goal
Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
-- Call linarith
- let linarith :=
+ let linarith := do
let cfg : Linarith.LinarithConfig := {
-- We do this with our custom preprocessing
splitNe := false
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 2fbd24dd..b54bdf7a 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -19,6 +19,7 @@ structure PSpecDesc where
-- The existentially quantified variables
evars : Array Expr
-- The function
+ fExpr : Expr
fName : Name
-- The function arguments
fLevels : List Level
@@ -60,21 +61,30 @@ section Methods
m a := do
trace[Progress] "Proposition: {th}"
-- Dive into the quantified variables and the assumptions
- forallTelescope th fun fvars th => do
+ forallTelescope th.consumeMData fun fvars th => do
trace[Progress] "Universally quantified arguments and assumptions: {fvars}"
-- Dive into the existentials
- existsTelescope th fun evars th => do
+ existsTelescope th.consumeMData fun evars th => do
trace[Progress] "Existentials: {evars}"
trace[Progress] "Proposition after stripping the quantifiers: {th}"
-- Take the first conjunct
- let (th, post) ← optSplitConj th
+ let (th, post) ← optSplitConj th.consumeMData
trace[Progress] "After splitting the conjunction:\n- eq: {th}\n- post: {post}"
-- Destruct the equality
- let (th, ret) ← destEq th
+ let (mExpr, ret) ← destEq th.consumeMData
trace[Progress] "After splitting the equality:\n- lhs: {th}\n- rhs: {ret}"
- -- Destruct the application to get the name
- th.consumeMData.withApp fun f args => do
- trace[Progress] "After stripping the arguments:\n- f: {f}\n- args: {args}"
+ -- Destruct the monadic application to dive into the bind, if necessary (this
+ -- is for when we use `withPSpec` inside of the `progress` tactic), and
+ -- destruct the application to get the function name
+ mExpr.consumeMData.withApp fun mf margs => do
+ trace[Progress] "After stripping the arguments of the monad expression:\n- mf: {mf}\n- margs: {margs}"
+ let (fExpr, f, args) ← do
+ if mf.isConst ∧ mf.constName = ``Bind.bind then do
+ -- Dive into the bind
+ let fExpr := margs.get! 4
+ fExpr.consumeMData.withApp fun f args => pure (fExpr, f, args)
+ else pure (mExpr, mf, margs)
+ 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}"
-- Compute the set of universally quantified variables which appear in the function arguments
let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty
@@ -94,6 +104,7 @@ section Methods
let thDesc := {
fvars := fvars
evars := evars
+ fExpr
fName := f.constName!
fLevels := f.constLevels!
args := args
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 1f734415..dabd25b8 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -7,22 +7,6 @@ namespace Progress
open Lean Elab Term Meta Tactic
open Utils
-/-
--- TODO: remove
-namespace Test
- open Primitives
-
- set_option trace.Progress true
-
- @[pspec]
- theorem vec_index_test (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
- ∃ x, v.index α i = .ret x := by
- sorry
-
- #eval pspecAttr.find? ``Primitives.Vec.index
-end Test
--/
-
inductive TheoremOrLocal where
| Theorem (thName : Name)
| Local (asm : LocalDecl)
@@ -39,7 +23,7 @@ inductive ProgressError
| Error (msg : MessageData)
deriving Inhabited
-def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids : Array Name)
+def progressWith (fExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids : Array Name)
(asmTac : TacticM Unit) : TacticM ProgressError := do
/- Apply the theorem
We try to match the theorem with the goal
@@ -66,7 +50,7 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids
-- Introduce the existentially quantified variables and the post-condition
-- in the context
let thBody ←
- existsTelescope thExBody fun _evars thBody => do
+ existsTelescope thExBody.consumeMData fun _evars thBody => do
trace[Progress] "After stripping existentials: {thBody}"
let (thBody, _) ← optSplitConj thBody
trace[Progress] "After splitting the conjunction: {thBody}"
@@ -75,9 +59,9 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids
-- There shouldn't be any existential variables in thBody
pure thBody
-- Match the body with the 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}"
+ trace[Progress] "Matching `{thBody}` with `{fExpr}`"
+ let ok ← isDefEq thBody fExpr
+ if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {fExpr}"
let mgoal ← Tactic.getMainGoal
postprocessAppMVars `progress mgoal mvars binders true true
Term.synthesizeSyntheticMVarsNoPostponing
@@ -139,8 +123,9 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids
match ids with
| [] => pure .Ok -- Stop
| nid :: ids => do
+ trace[Progress] "Splitting post: {hPost}"
-- Split
- if ← isConj hPost then
+ if ← isConj (← inferType hPost) then
splitConjTac hPost (some (nid, curPostId)) (λ _ nhPost => splitPost nhPost ids)
else return (.Error m!"Too many ids provided ({nid :: ids}) not enough conjuncts to split in the postcondition")
splitPost hPost ids
@@ -175,7 +160,7 @@ def getFirstArg (args : Array Expr) : Option Expr := do
/- Helper: try to lookup a theorem and apply it, or continue with another tactic
if it fails -/
-def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr)
+def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Unit) (fExpr : Expr)
(kind : String) (th : Option TheoremOrLocal) (x : TacticM Unit) : TacticM Unit := do
let res ← do
match th with
@@ -187,7 +172,7 @@ def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Uni
-- Apply the theorem
let res ← do
try
- let res ← progressWith fnExpr th keep ids asmTac
+ let res ← progressWith fExpr th keep ids asmTac
pure (some res)
catch _ => none
match res with
@@ -203,18 +188,16 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
let goalTy ← mgoal.getType
trace[Progress] "goal: {goalTy}"
-- Dive into the goal to lookup the theorem
- let (fName, fLevels, args) ← do
+ let (fExpr, fName, 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
+ -- TODO: check that no quantified variables in the arguments
+ pure (desc.fExpr, desc.fName, desc.args)
trace[Progress] "Function: {fName}"
-- If the user provided a theorem/assumption: use it.
-- Otherwise, lookup one.
match withTh with
| some th => do
- match ← progressWith fnExpr th keep ids asmTac with
+ match ← progressWith fExpr th keep ids asmTac with
| .Ok => return ()
| .Error msg => throwError msg
| none =>
@@ -223,7 +206,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
let decls ← ctx.getDecls
for decl in decls.reverse do
trace[Progress] "Trying assumption: {decl.userName} : {decl.type}"
- let res ← do try progressWith fnExpr (.Local decl) keep ids asmTac catch _ => continue
+ let res ← do try progressWith fExpr (.Local decl) keep ids asmTac catch _ => continue
match res with
| .Ok => return ()
| .Error msg => throwError msg
@@ -233,7 +216,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
let pspec ← do
let thName ← pspecAttr.find? fName
pure (thName.map fun th => .Theorem th)
- tryLookupApply keep ids asmTac fnExpr "pspec theorem" pspec do
+ tryLookupApply keep ids asmTac fExpr "pspec theorem" pspec do
-- It failed: try to lookup a *class* expr spec theorem (those are more
-- specific than class spec theorems)
let pspecClassExpr ← do
@@ -242,7 +225,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
| some arg => do
let thName ← pspecClassExprAttr.find? fName arg
pure (thName.map fun th => .Theorem th)
- tryLookupApply keep ids asmTac fnExpr "pspec class expr theorem" pspecClassExpr do
+ tryLookupApply keep ids asmTac fExpr "pspec class expr theorem" pspecClassExpr do
-- It failed: try to lookup a *class* spec theorem
let pspecClass ← do
match ← getFirstArgAppName args with
@@ -250,7 +233,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
| some argName => do
let thName ← pspecClassAttr.find? fName argName
pure (thName.map fun th => .Theorem th)
- tryLookupApply keep ids asmTac fnExpr "pspec class theorem" pspecClass do
+ tryLookupApply keep ids asmTac fExpr "pspec class theorem" pspecClass do
-- Try a recursive call - we try the assumptions of kind "auxDecl"
let ctx ← Lean.MonadLCtx.getLCtx
let decls ← ctx.getAllDecls
@@ -258,7 +241,7 @@ 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 fnExpr (.Local decl) keep ids asmTac catch _ => continue
+ let res ← do try progressWith fExpr (.Local decl) keep ids asmTac catch _ => continue
match res with
| .Ok => return ()
| .Error msg => throwError msg
@@ -310,7 +293,6 @@ elab "progress" args:progressArgs : tactic =>
evalProgress args
/-
--- TODO: remove
namespace Test
open Primitives Result
@@ -319,22 +301,14 @@ namespace Test
#eval showStoredPSpec
#eval showStoredPSpecClass
- theorem Scalar.add_spec1 {ty} {x y : Scalar ty}
+ example {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ x.val + y.val)
(hmax : x.val + y.val ≤ Scalar.max ty) :
∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
- progress keep as h with Scalar.add_spec as ⟨ z ⟩
+-- progress keep as h with Scalar.add_spec as ⟨ z ⟩
+ progress keep as h
simp [*]
-/-
- @[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 with vec_index_test as ⟨ x ⟩
- simp
-
- set_option trace.Progress false
--/
end Test -/
end Progress
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 8aa76d8e..44590176 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -308,8 +308,23 @@ def firstTac (tacl : List (TacticM Unit)) : TacticM Unit := do
match tacl with
| [] => pure ()
| tac :: tacl =>
- try tac
+ -- Should use try ... catch or Lean.observing?
+ -- Generally speaking we should use Lean.observing? to restore the state,
+ -- but with tactics the try ... catch variant seems to work
+ try do
+ tac
+ -- Check that there are no remaining goals
+ let gl ← Tactic.getUnsolvedGoals
+ if ¬ gl.isEmpty then throwError "tactic failed"
catch _ => firstTac tacl
+/- let res ← Lean.observing? do
+ tac
+ -- Check that there are no remaining goals
+ let gl ← Tactic.getUnsolvedGoals
+ if ¬ gl.isEmpty then throwError "tactic failed"
+ match res with
+ | some _ => pure ()
+ | none => firstTac tacl -/
-- Split the goal if it is a conjunction
def splitConjTarget : TacticM Unit := do
@@ -424,12 +439,13 @@ def splitExistsTac (h : Expr) (optId : Option Name) (k : Expr → Expr → Tacti
let hTy ← inferType h
if isExists hTy then do
-- Try to use the user-provided names
- let altVarNames ←
- match optId with
- | none => pure #[]
- | some id => do
- let hDecl ← h.fvarId!.getDecl
- pure #[{ varNames := [id, hDecl.userName] }]
+ let altVarNames ← do
+ let hDecl ← h.fvarId!.getDecl
+ let id ← do
+ match optId with
+ | none => mkFreshUserName `x
+ | some id => pure id
+ pure #[{ varNames := [id, hDecl.userName] }]
let newGoals ← goal.cases h.fvarId! altVarNames
-- There should be exactly one goal
match newGoals.toList with
@@ -511,7 +527,7 @@ example (h : a ∧ b) : a := by
example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by
split_all_exists h
- rename_i x y z h
+ rename_i x y z
exists x + y + z
/- Call the simp tactic.