From 75149c391fc92398c7d4d409c97cb3ac59d2876a Mon Sep 17 00:00:00 2001 From: Yakov Pechersky Date: Fri, 19 Feb 2021 04:14:29 +0000 Subject: [PATCH] feat(data/list/basic): tail_drop, cons_nth_le_drop_succ (#6265) --- src/data/list/basic.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean index 88aee8d86940a..1c967a6bd5ebb 100644 --- a/src/data/list/basic.lean +++ b/src/data/list/basic.lean @@ -1580,6 +1580,26 @@ end l.drop k = [] := by simpa [←length_eq_zero] using nat.sub_eq_zero_of_le h +lemma tail_drop (l : list α) (n : ℕ) : (l.drop n).tail = l.drop (n + 1) := +begin + induction l with hd tl hl generalizing n, + { simp }, + { cases n, + { simp }, + { simp [hl] } } +end + +lemma cons_nth_le_drop_succ {l : list α} {n : ℕ} (hn : n < l.length) : + l.nth_le n hn :: l.drop (n + 1) = l.drop n := +begin + induction l with hd tl hl generalizing n, + { exact absurd n.zero_le (not_le_of_lt (by simpa using hn)) }, + { cases n, + { simp }, + { simp only [nat.succ_lt_succ_iff, list.length] at hn, + simpa [list.nth_le, list.drop] using hl hn } } +end + theorem drop_nil : ∀ n, drop n [] = ([] : list α) := λ _, drop_eq_nil_of_le (nat.zero_le _)