summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backends/lean/Base/Progress/Base.lean11
-rw-r--r--backends/lean/Base/Progress/Progress.lean11
-rw-r--r--backends/lean/Base/Utils.lean4
-rw-r--r--tests/lean/Hashmap/Properties.lean24
4 files changed, 32 insertions, 18 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 00b0a478..7eace667 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -58,10 +58,10 @@ section Methods
def withPSpec [Inhabited (m a)] [Nonempty (m a)] (th : Expr) (k : PSpecDesc → m a)
(sanityChecks : Bool := false) :
m a := do
- trace[Progress] "Theorem: {th}"
+ trace[Progress] "Proposition: {th}"
-- Dive into the quantified variables and the assumptions
forallTelescope th fun fvars th => do
- trace[Progress] "All arguments: {fvars}"
+ trace[Progress] "Universally quantified arguments and assumptions: {fvars}"
/- -- Filter the argumens which are not propositions
let rec getFirstPropIdx (i : Nat) : MetaM Nat := do
if i ≥ fargs.size then pure i
@@ -83,12 +83,16 @@ section Methods
-- Dive into the existentials
existsTelescope th 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
+ trace[Progress] "After splitting the conjunction:\n- eq: {th}\n- post: {post}"
-- Destruct the equality
let (th, ret) ← destEq th
+ trace[Progress] "After splitting the equality:\n- lhs: {th}\n- rhs: {ret}"
-- Destruct the application to get the name
- th.withApp fun f args => do
+ th.consumeMData.withApp fun f args => do
+ trace[Progress] "After stripping the arguments:\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
@@ -114,6 +118,7 @@ section Methods
post := post
}
k thDesc
+
end Methods
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 001967e5..ace92f4f 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -55,14 +55,20 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
let thDecl := env.constants.find! thName
pure thDecl.type
| .Local asmDecl => pure asmDecl.type
+ trace[Progress] "theorem/assumption type: {thTy}"
-- TODO: the tactic fails if we uncomment withNewMCtxDepth
-- withNewMCtxDepth do
let (mvars, binders, thExBody) ← forallMetaTelescope thTy
+ trace[Progress] "After stripping foralls: {thExBody}"
-- Introduce the existentially quantified variables and the post-condition
-- in the context
let thBody ←
existsTelescope thExBody fun _evars thBody => do
+ trace[Progress] "After stripping existentials: {thBody}"
+ let (thBody, _) ← optSplitConj thBody
+ trace[Progress] "After splitting the conjunction: {thBody}"
let (thBody, _) ← destEq thBody
+ trace[Progress] "After splitting equality: {thBody}"
-- There shouldn't be any existential variables in thBody
pure thBody
-- Match the body with the target
@@ -152,6 +158,7 @@ def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : Tac
-- Retrieve the goal
let mgoal ← Tactic.getMainGoal
let goalTy ← mgoal.getType
+ trace[Progress] "goal: {goalTy}"
-- Dive into the goal to lookup the theorem
let (fName, fLevels, args) ← do
withPSpec goalTy fun desc =>
@@ -188,7 +195,7 @@ syntax progressArgs := ("as" " ⟨ " (ident)+ " ⟩")?
def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
let args := args.raw
-- Process the arguments to retrieve the identifiers to use
- trace[Progress] "Progressing arguments: {args}"
+ trace[Progress] "Progress arguments: {args}"
let args := args.getArgs
let ids :=
if args.size > 0 then
@@ -196,7 +203,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
let args := (args.get! 2).getArgs
args.map Syntax.getId
else #[]
- trace[Progress] "Ids: {ids}"
+ trace[Progress] "User-provided ids: {ids}"
progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac])
elab "progress" args:progressArgs : tactic =>
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 599c3a9f..9cd0db23 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -43,6 +43,10 @@ namespace List
end List
+-- TODO: move?
+@[simp]
+theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all
+
namespace Lean
namespace LocalContext
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 1db39422..ee22bebd 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -105,6 +105,8 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) :
simp [h]
else
by
+ -- TODO: use progress: detect that this is a recursive call, or give
+ -- the possibility of specifying an identifier
have ⟨ b, hi ⟩ := insert_in_list_spec key value tl
exists b
simp [insert_in_list, List.lookup]
@@ -112,13 +114,12 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) :
simp [h]
simp [insert_in_list] at hi
exact hi
-
-/--
+
@[pspec]
theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) :
∃ b,
insert_in_list α key value ls = ret b ∧
- (b = (List.lookup ls.v key = none))
+ (b ↔ (List.lookup ls.v key = none))
:= by
induction ls
case Nil => simp [insert_in_list, insert_in_list_loop, List.lookup]
@@ -130,11 +131,12 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α)
simp [h]
else
conv =>
- rhs; ext; arg 1; simp [h] -- TODO: Simplify
- simp [insert_in_list] at ih;
- progress -- TODO: Does not work
---/
-
+ rhs; ext; left; simp [h] -- TODO: Simplify
+ simp only [insert_in_list] at ih;
+ -- TODO: give the possibility of using underscores
+ progress as ⟨ b h ⟩
+ simp [*]
+
@[pspec]
theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List α) :
∃ l1,
@@ -150,8 +152,7 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List
rw [insert_in_list_loop_back]
simp [h, List.lookup]
intro k1 h1
- have h2 : ¬(key = k1) := by tauto -- TODO: Why is the order of args in eq swapped
- simp [h2]
+ simp [*]
else
by
simp [insert_in_list_back, List.lookup]
@@ -159,12 +160,9 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List
simp [h, List.lookup]
have ⟨tl0 , _, _ ⟩ := insert_in_list_back_spec key value tl -- TODO: Use progress
simp [insert_in_list_back] at *
- simp [*]
- have : ¬ (key = k) := by tauto
simp [List.lookup, *]
simp (config := {contextual := true}) [*]
end HashMap
--- def distinct_keys {α : Type u}
end hashmap