summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon HO2023-09-14 08:19:59 +0200
committerGitHub2023-09-14 08:19:59 +0200
commit242aca3092c6594206896ea62eb40395accc8459 (patch)
tree4a105b1284821a89ca344188fdddb727de2deea3 /backends
parentda97fc1e68d147439436ff883ac865a9cdeca18e (diff)
parent743e8cb9d5366b879f53d7d0ba8adeb2f83ef72f (diff)
Merge pull request #36 from AeneasVerif/update_lean
Update the version of Lean and fix a bug in the progress tactic
Diffstat (limited to 'backends')
-rw-r--r--backends/lean/Base/Arith/Int.lean2
-rw-r--r--backends/lean/Base/Diverge/Base.lean35
-rw-r--r--backends/lean/Base/Diverge/Elab.lean2
-rw-r--r--backends/lean/Base/IList/IList.lean5
-rw-r--r--backends/lean/Base/Progress/Progress.lean21
-rw-r--r--backends/lean/Base/Utils.lean4
-rw-r--r--backends/lean/lake-manifest.json38
-rw-r--r--backends/lean/lean-toolchain2
8 files changed, 62 insertions, 47 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 531ec94f..eb6701c2 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -238,7 +238,7 @@ def intTac (splitGoalConjs : Bool) (extraPreprocess : Tactic.TacticM Unit) : Ta
-- the goal. I think before leads to a smaller proof term?
Tactic.allGoals (intTacPreprocess extraPreprocess)
-- More preprocessing
- Tactic.allGoals (Utils.simpAt [] [``nat_zero_eq_int_zero] [] .wildcard)
+ Tactic.allGoals (Utils.tryTac (Utils.simpAt [] [``nat_zero_eq_int_zero] [] .wildcard))
-- Split the conjunctions in the goal
if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
-- Call linarith
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 1d548389..6a52387d 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -270,7 +270,7 @@ namespace Fix
simp [karrow_rel, result_rel]
have hg := hg Hrgh; simp [result_rel] at hg
cases heq0: g fg <;> simp_all
- rename_i y _
+ rename_i _ y
have hh := hh y Hrgh; simp [result_rel] at hh
simp_all
@@ -546,7 +546,7 @@ namespace FixI
termination_by for_all_fin_aux n _ m h => n - m
decreasing_by
simp_wf
- apply Nat.sub_add_lt_sub <;> simp
+ apply Nat.sub_add_lt_sub <;> try simp
simp_all [Arith.add_one_le_iff_le_ne]
def for_all_fin {n : Nat} (f : Fin n → Prop) := for_all_fin_aux f 0 (by simp)
@@ -569,7 +569,6 @@ namespace FixI
intro i h3; cases i; simp_all
linarith
case succ k hi =>
- simp_all
intro m hk hmn
intro hf i hmi
have hne: m ≠ n := by
@@ -580,7 +579,6 @@ namespace FixI
-- Yes: simply use the `for_all_fin_aux` hyp
unfold for_all_fin_aux at hf
simp_all
- tauto
else
-- No: use the induction hypothesis
have hlt: m < i := by simp_all [Nat.lt_iff_le_and_ne]
@@ -726,8 +724,8 @@ namespace Ex1
theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by
intro k x
simp [list_nth_body]
- split <;> simp
- split <;> simp
+ split <;> try simp
+ split <;> try simp
def list_nth (ls : List a) (i : Int) : Result a := fix list_nth_body (ls, i)
@@ -767,8 +765,8 @@ namespace Ex2
theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by
intro k x
simp [list_nth_body]
- split <;> simp
- split <;> simp
+ split <;> try simp
+ split <;> try simp
apply is_valid_p_bind <;> intros <;> simp_all
def list_nth (ls : List a) (i : Int) : Result a := fix list_nth_body (ls, i)
@@ -845,7 +843,7 @@ namespace Ex3
∀ k x, is_valid_p k (λ k => is_even_is_odd_body k x) := by
intro k x
simp [is_even_is_odd_body]
- split <;> simp <;> split <;> simp
+ split <;> (try simp) <;> split <;> try simp
apply is_valid_p_bind; simp
intros; split <;> simp
apply is_valid_p_bind; simp
@@ -878,7 +876,7 @@ namespace Ex3
-- inductives on the fly).
-- The simplest is to repeatedly split then simplify (we identify
-- the outer match or monadic let-binding, and split on its scrutinee)
- split <;> simp
+ split <;> try simp
cases H0 : fix is_even_is_odd_body (Sum.inr (i - 1)) <;> simp
rename_i v
split <;> simp
@@ -891,7 +889,7 @@ namespace Ex3
simp [is_even, is_odd]
conv => lhs; rw [Heq]; simp; rw [is_even_is_odd_body]; simp
-- Same remark as for `even`
- split <;> simp
+ split <;> try simp
cases H0 : fix is_even_is_odd_body (Sum.inl (i - 1)) <;> simp
rename_i v
split <;> simp
@@ -938,7 +936,7 @@ namespace Ex4
intro k
apply (Funs.is_valid_p_is_valid_p tys)
simp [Funs.is_valid_p]
- (repeat (apply And.intro)) <;> intro x <;> simp at x <;>
+ (repeat (apply And.intro)) <;> intro x <;> (try simp at x) <;>
simp only [is_even_body, is_odd_body]
-- Prove the validity of the individual bodies
. split <;> simp
@@ -995,9 +993,9 @@ namespace Ex5
(ls : List a) :
is_valid_p k (λ k => map (f k) ls) := by
induction ls <;> simp [map]
- apply is_valid_p_bind <;> simp_all
+ apply is_valid_p_bind <;> try simp_all
intros
- apply is_valid_p_bind <;> simp_all
+ apply is_valid_p_bind <;> try simp_all
/- An example which uses map -/
inductive Tree (a : Type) :=
@@ -1016,8 +1014,8 @@ namespace Ex5
∀ k x, is_valid_p k (λ k => @id_body a k x) := by
intro k x
simp only [id_body]
- split <;> simp
- apply is_valid_p_bind <;> simp [*]
+ split <;> try simp
+ apply is_valid_p_bind <;> try simp [*]
-- We have to show that `map k tl` is valid
apply map_is_valid;
-- Remark: if we don't do the intro, then the last step is expensive:
@@ -1077,12 +1075,11 @@ namespace Ex6
intro k
apply (Funs.is_valid_p_is_valid_p tys)
simp [Funs.is_valid_p]
- (repeat (apply And.intro)); intro x; simp at x
+ (repeat (apply And.intro)); intro x; try simp at x
simp only [list_nth_body]
-- Prove the validity of the individual bodies
intro k x
- simp [list_nth_body]
- split <;> simp
+ split <;> try simp
split <;> simp
-- Writing the proof terms explicitly
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index f109e847..c6628486 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -1089,7 +1089,7 @@ namespace Tests
intro i hpos h
-- We can directly use `rw [list_nth]`!
rw [list_nth]; simp
- split <;> simp [*]
+ split <;> try simp [*]
. tauto
. -- TODO: we shouldn't have to do that
have hneq : 0 < i := by cases i <;> rename_i a _ <;> simp_all; cases a <;> simp_all
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 0b483e90..a940da25 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -239,7 +239,6 @@ open Arith in
have := tl.len_pos
linarith
else
- simp at hineq
have : 0 < i := by int_tac
simp [*]
apply hi
@@ -364,8 +363,8 @@ theorem index_itake_append_end [Inhabited α] (i j : Int) (l0 l1 : List α)
match l0 with
| [] => by
simp at *
- have := index_itake i j l1 (by simp_all) (by simp_all) (by simp_all; int_tac)
- simp [*]
+ have := index_itake i j l1 (by simp_all) (by simp_all) (by int_tac)
+ try simp [*]
| hd :: tl =>
have : ¬ i = 0 := by simp at *; int_tac
if hj : j = 0 then by simp_all; int_tac -- Contradiction
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 6a4729dc..4fd88e36 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -110,8 +110,9 @@ 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}"
- simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
- [hEq.fvarId!] (.targets #[] true)
+ tryTac (
+ simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
+ [hEq.fvarId!] (.targets #[] true))
-- Clear the equality, unless the user requests not to do so
let mgoal ← do
if keep.isSome then getMainGoal
@@ -314,12 +315,14 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
else pure none
let ids :=
let args := asArgs.getArgs
- let args := (args.get! 2).getSepArgs
- args.map (λ s => if s.isIdent then some s.getId else none)
+ if args.size > 2 then
+ let args := (args.get! 2).getSepArgs
+ args.map (λ s => if s.isIdent then some s.getId else none)
+ else #[]
trace[Progress] "User-provided ids: {ids}"
let splitPost : Bool :=
let args := asArgs.getArgs
- (args.get! 3).getArgs.size > 0
+ args.size > 3 ∧ (args.get! 3).getArgs.size > 0
trace[Progress] "Split post: {splitPost}"
/- For scalarTac we have a fast track: if the goal is not a linear
arithmetic goal, we skip (note that otherwise, scalarTac would try
@@ -343,11 +346,11 @@ elab "progress" args:progressArgs : tactic =>
namespace Test
open Primitives Result
- set_option trace.Progress true
- set_option pp.rawOnError true
+ -- set_option trace.Progress true
+ -- set_option pp.rawOnError true
- #eval showStoredPSpec
- #eval showStoredPSpecClass
+ -- #eval showStoredPSpec
+ -- #eval showStoredPSpecClass
example {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ x.val + y.val)
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 1f8f1455..5224e1c3 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -301,6 +301,10 @@ example : Nat := by
example (x : Bool) : Nat := by
cases x <;> custom_let x := 3 <;> apply x
+-- Attempt to apply a tactic
+def tryTac (tac : TacticM Unit) : TacticM Unit := do
+ let _ ← tryTactic tac
+
-- Repeatedly apply a tactic
partial def repeatTac (tac : TacticM Unit) : TacticM Unit := do
try
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index 5a089838..934ee2d9 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -1,39 +1,51 @@
-{"version": 4,
+{"version": 5,
"packagesDir": "lake-packages",
"packages":
[{"git":
{"url": "https://github.com/EdAyers/ProofWidgets4",
"subDir?": null,
- "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
+ "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
+ "opts": {},
"name": "proofwidgets",
- "inputRev?": "v0.0.11"}},
+ "inputRev?": "v0.0.13",
+ "inherited": true}},
{"git":
{"url": "https://github.com/mhuisi/lean4-cli.git",
"subDir?": null,
- "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+ "rev": "21dac2e9cc7e3cf7da5800814787b833e680b2fd",
+ "opts": {},
"name": "Cli",
- "inputRev?": "nightly"}},
+ "inputRev?": "nightly",
+ "inherited": true}},
{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
- "rev": "fa05951a270fef2873666c46f138e90338cd48d6",
+ "rev": "226948a52f8e19ad95ff6025a96784d7e7ed6ed0",
+ "opts": {},
"name": "mathlib",
- "inputRev?": null}},
+ "inputRev?": null,
+ "inherited": false}},
{"git":
{"url": "https://github.com/gebner/quote4",
"subDir?": null,
- "rev": "c0d9516f44d07feee01c1103c8f2f7c24a822b55",
+ "rev": "e75daed95ad1c92af4e577fea95e234d7a8401c1",
+ "opts": {},
"name": "Qq",
- "inputRev?": "master"}},
+ "inputRev?": "master",
+ "inherited": true}},
{"git":
{"url": "https://github.com/JLimperg/aesop",
"subDir?": null,
- "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
+ "rev": "1a0cded2be292b5496e659b730d2accc742de098",
+ "opts": {},
"name": "aesop",
- "inputRev?": "master"}},
+ "inputRev?": "master",
+ "inherited": true}},
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
- "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
+ "rev": "ba5e5e3af519b4fc5221ad0fa4b2c87276f1d323",
+ "opts": {},
"name": "std",
- "inputRev?": "main"}}]}
+ "inputRev?": "main",
+ "inherited": true}}]}
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index 334c5053..fbca4d37 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-12 \ No newline at end of file
+leanprover/lean4:v4.0.0 \ No newline at end of file