diff options
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 2 | ||||
| -rw-r--r-- | backends/lean/Base/Diverge/Base.lean | 35 | ||||
| -rw-r--r-- | backends/lean/Base/Diverge/Elab.lean | 2 | ||||
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 5 | ||||
| -rw-r--r-- | backends/lean/Base/Utils.lean | 4 | ||||
| -rw-r--r-- | backends/lean/lake-manifest.json | 38 | ||||
| -rw-r--r-- | backends/lean/lean-toolchain | 2 |
7 files changed, 50 insertions, 38 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/Utils.lean b/backends/lean/Base/Utils.lean index 1f8f1455..e58198f4 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 |