sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

take/drop array lemmas

Browse Source
This commit is contained in:
Paul Reichert
2026-03-10 09:43:02 +01:00
parent 8dae7f3705
commit 035baff73b
1 changed files with 16 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
src/Init/Data/Array/TakeDrop.lean
View File

@@ -21,6 +21,22 @@ public section
namespace Array
@[simp, grind =] theorem take_empty {i : Nat} :
(#[] : Array α).take i = #[] := by cases i <;> rfl
@[simp, grind =] theorem take_zero {xs : Array α} :
xs.take 0 = #[] := by
simp [Array.take_eq_extract]
@[simp, grind =] theorem drop_empty : (#[] : Array α).drop i = #[] := by
simp [Array.drop_eq_extract]
@[simp, grind =] theorem drop_zero {xs : Array α} : xs.drop 0 = xs := by
simp [Array.drop_eq_extract]
theorem drop_eq_empty_of_le {xs : Array α} {i : Nat} (h : xs.size ≤ i) : xs.drop i = #[] := by
simp [Array.drop_eq_extract, Array.extract_empty_of_size_le_start h]
@[simp, grind =] theorem size_take {xs : Array α} {i : Nat} : (xs.take i).size = min i xs.size := by
simp [take_eq_extract]