summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorSon Ho2023-07-26 15:00:11 +0200
committerSon Ho2023-07-26 15:00:11 +0200
commit3337c4ac3326c3132dcc322f55f23a7d2054ceb0 (patch)
tree4753f8a49b2b28917600a872caa3d31964cb6fd8 /backends/lean
parent81e991822879a942af34489b7a072f31739f28f6 (diff)
Update some of the Vec function specs
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives/Vec.lean13
-rw-r--r--backends/lean/Base/Progress/Progress.lean17
2 files changed, 21 insertions, 9 deletions
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 523372bb..a09d6ac2 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -85,14 +85,19 @@ def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
| none => fail .arrayOutOfBounds
| some x => ret x
+/- In the theorems below: we don't always need the `∃ ..`, but we use one
+ so that `progress` introduces an opaque variable and an equality. This
+ helps control the context.
+ -/
+
@[pspec]
theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
(hbound : i.val < v.length) :
- v.index α i = ret (v.val.index i.val) := by
+ ∃ x, v.index α i = ret x ∧ x = v.val.index i.val := by
simp only [index]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
- simp only [*]
+ simp [*]
-- This shouldn't be used
def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
@@ -109,11 +114,11 @@ def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α :=
@[pspec]
theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
(hbound : i.val < v.length) :
- v.index_mut α i = ret (v.val.index i.val) := by
+ ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by
simp only [index_mut]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
- simp only [*]
+ simp [*]
instance {α : Type u} (p : Vec α → Prop) : Arith.HasIntProp (Subtype p) where
prop_ty := λ x => p x
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 9300edff..6a4729dc 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -162,6 +162,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
allGoals asmTac
let newGoals ← getUnsolvedGoals
setGoals (newGoals ++ curGoals)
+ trace[Progress] "progress: replaced the goals"
--
pure .Ok
@@ -281,12 +282,15 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
| [keepArg, withArg, asArgs] => do pure (keepArg, withArg, asArgs)
| _ => throwError "Unexpected: invalid arguments"
let keep : Option Name ← do
+ trace[Progress] "Keep arg: {keepArg}"
let args := keepArg.getArgs
- trace[Progress] "Keep args: {args}"
- let arg := args.get! 1
- trace[Progress] "Keep arg: {arg}"
- if arg.isIdent then pure (some arg.getId)
- else do pure (some (← mkFreshAnonPropUserName))
+ if args.size > 0 then do
+ trace[Progress] "Keep args: {args}"
+ let arg := args.get! 1
+ trace[Progress] "Keep arg: {arg}"
+ if arg.isIdent then pure (some arg.getId)
+ else do pure (some (← mkFreshAnonPropUserName))
+ else do pure none
trace[Progress] "Keep: {keep}"
let withArg ← do
let withArg := withArg.getArgs
@@ -328,7 +332,10 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
else
throwError "Not a linear arithmetic goal"
progressAsmsOrLookupTheorem keep withArg ids splitPost (
+ withMainContext do
+ trace[Progress] "trying to solve assumption: {← getMainGoal}"
firstTac [assumptionTac, scalarTac])
+ trace[Diverge] "Progress done"
elab "progress" args:progressArgs : tactic =>
evalProgress args