summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base')
-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
6 files changed, 36 insertions, 33 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 16:57:57 +0000