diff options
| author | Son Ho | 2023-10-17 09:36:55 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-17 09:48:47 +0200 |
| commit | 584726e9c4e4378129a35f6cfbbbf934448d10a9 (patch) | |
| tree | 4e9c385d1115e71acb7581ab998320af867830bc /backends/lean/Base/IList | |
| parent | 2ec2e374302c772ff2c6a26e39451b4e49e13a16 (diff) | |
Implement tactics for termination proofs which involve arithmetic
Diffstat (limited to 'backends/lean/Base/IList')
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 24 |
1 files changed, 3 insertions, 21 deletions
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean index 79de93d5..f71f2de2 100644 --- a/backends/lean/Base/IList/IList.lean +++ b/backends/lean/Base/IList/IList.lean @@ -118,13 +118,7 @@ def ireplicate {α : Type u} (i : ℤ) (x : α) : List α := if i ≤ 0 then [] else x :: ireplicate (i - 1) x termination_by ireplicate i x => i.toNat -decreasing_by - simp_wf - -- TODO: simplify this kind of proofs - simp at * - have : 0 ≤ i := by linarith - have : 1 ≤ i := by linarith - simp [Int.toNat_sub_of_le, *] +decreasing_by int_decr_tac @[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update] @[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update] @@ -173,13 +167,7 @@ theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : cases hl: l.toNat <;> simp_all conv => rhs; rw[hl] termination_by ireplicate_replicate l x h => l.toNat -decreasing_by - simp_wf - -- TODO: simplify this kind of proofs - simp at * - have : 0 ≤ l := by linarith - have : 1 ≤ l := by linarith - simp [Int.toNat_sub_of_le, *] +decreasing_by int_decr_tac @[simp] theorem ireplicate_len {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : @@ -191,13 +179,7 @@ theorem ireplicate_len {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : have hr := ireplicate_len (l - 1) x (by int_tac) simp [*] termination_by ireplicate_len l x h => l.toNat -decreasing_by - simp_wf - -- TODO: simplify this kind of proofs - simp at * - have : 0 ≤ l := by linarith - have : 1 ≤ l := by linarith - simp [Int.toNat_sub_of_le, *] +decreasing_by int_decr_tac theorem len_eq_length (ls : List α) : ls.len = ls.length := by induction ls |