summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r--backends/lean/Base/Progress/Progress.lean34
1 files changed, 28 insertions, 6 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index a2c7764f..4a406bdf 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -1,6 +1,7 @@
import Lean
import Base.Arith
import Base.Progress.Base
+import Base.Primitives -- TODO: remove?
namespace Progress
@@ -41,7 +42,12 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
match th with
| .Theorem thName =>
let thDecl := env.constants.find! thName
- pure thDecl.type
+ -- We have to introduce fresh meta-variables for the universes already
+ let ul : List (Name × Level) ←
+ thDecl.levelParams.mapM (λ x => do pure (x, ← mkFreshLevelMVar))
+ let ulMap : HashMap Name Level := HashMap.ofList ul
+ let thTy := thDecl.type.instantiateLevelParamsCore (λ x => ulMap.find! x)
+ pure thTy
| .Local asmDecl => pure asmDecl.type
trace[Progress] "Looked up theorem/assumption type: {thTy}"
-- TODO: the tactic fails if we uncomment withNewMCtxDepth
@@ -129,15 +135,16 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
Split the remaining conjunctions by using fresh ids if the user
instructed to fully split the post-condition, otherwise stop -/
if splitPost then
- splitFullConjTac hPost (λ _ => pure .Ok)
+ splitFullConjTac true hPost (λ _ => pure .Ok)
else pure .Ok
| nid :: ids => do
- trace[Progress] "Splitting post: {hPost}"
+ trace[Progress] "Splitting post: {← inferType hPost}"
-- Split
let nid ← do
match nid with
| none => mkFreshUserName `h
| 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")
@@ -323,7 +330,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
elab "progress" args:progressArgs : tactic =>
evalProgress args
-/- namespace Test
+namespace Test
open Primitives Result
set_option trace.Progress true
@@ -336,10 +343,25 @@ elab "progress" args:progressArgs : tactic =>
(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 as ⟨ x, h1 .. ⟩
simp [*]
-end Test -/
+ 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 ⟩
+ simp [*]
+
+ /- Checking that universe instantiation works: the original spec uses
+ `α : Type u` where u is quantified, while here we use `α : Type 0` -/
+ example {α : Type} (v: Vec α) (i: Usize) (x : α)
+ (hbounds : i.val < v.length) :
+ ∃ nv, v.index_mut_back α i x = ret nv ∧
+ nv.val = v.val.update i.val x := by
+ progress
+ simp [*]
+
+end Test
end Progress