Dropping or taking from lists on the right

Taking or removing element from the tail end of a list

Main definitions

• rdrop n: drop n : ℕ elements from the tail
• rtake n: take n : ℕ elements from the tail
• rdropWhile p: remove all the elements from the tail of a list until it finds the first element for which p : α → Bool returns false. This element and everything before is returned.
• rtakeWhile p: Returns the longest terminal segment of a list for which p : α → Bool returns true.

Implementation detail

The two predicate-based methods operate by performing the regular "from-left" operation on List.reverse, followed by another List.reverse, so they are not the most performant. The other two rely on List.length l so they still traverse the list twice. One could construct another function that takes a L : ℕ and use L - n. Under a proof condition that L = l.length, the function would do the right thing.

def List.rdrop {α : Type u_1} (l : List α) (n : ℕ) : List α

Drop n elements from the tail end of a list.

@[simp]

theorem List.rdrop_nil {α : Type u_1} (n : ℕ) : [].rdrop n = []

@[simp]

theorem List.rdrop_zero {α : Type u_1} (l : List α) : l.rdrop 0 = l

theorem List.rdrop_eq_reverse_drop_reverse {α : Type u_1} (l : List α) (n : ℕ) : l.rdrop n = (drop n l.reverse).reverse

@[simp]

theorem List.rdrop_concat_succ {α : Type u_1} (l : List α) (n : ℕ) (x : α) : (l ++ [x]).rdrop (n + 1) = l.rdrop n

def List.rtake {α : Type u_1} (l : List α) (n : ℕ) : List α

Take n elements from the tail end of a list.

@[simp]

theorem List.rtake_nil {α : Type u_1} (n : ℕ) : [].rtake n = []

@[simp]

theorem List.rtake_zero {α : Type u_1} (l : List α) : l.rtake 0 = []

theorem List.rtake_eq_reverse_take_reverse {α : Type u_1} (l : List α) (n : ℕ) : l.rtake n = (take n l.reverse).reverse

@[simp]

theorem List.rtake_concat_succ {α : Type u_1} (l : List α) (n : ℕ) (x : α) : (l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]

def List.rdropWhile {α : Type u_1} (p : α → Bool) (l : List α) : List α

Drop elements from the tail end of a list that satisfy p : α → Bool. Implemented naively via List.reverse

@[simp]

theorem List.rdropWhile_nil {α : Type u_1} (p : α → Bool) : rdropWhile p [] = []

theorem List.rdropWhile_concat {α : Type u_1} (p : α → Bool) (l : List α) (x : α) : rdropWhile p (l ++ [x]) = if p x = true then rdropWhile p l else l ++ [x]

@[simp]

theorem List.rdropWhile_concat_pos {α : Type u_1} (p : α → Bool) (l : List α) (x : α) (h : p x = true) : rdropWhile p (l ++ [x]) = rdropWhile p l

@[simp]

theorem List.rdropWhile_concat_neg {α : Type u_1} (p : α → Bool) (l : List α) (x : α) (h : ¬p x = true) : rdropWhile p (l ++ [x]) = l ++ [x]

theorem List.rdropWhile_singleton {α : Type u_1} (p : α → Bool) (x : α) : rdropWhile p [x] = if p x = true then [] else [x]

theorem List.rdropWhile_last_not {α : Type u_1} (p : α → Bool) (l : List α) (hl : rdropWhile p l ≠ []) : ¬p ((rdropWhile p l).getLast hl) = true

theorem List.rdropWhile_prefix {α : Type u_1} (p : α → Bool) (l : List α) : rdropWhile p l <+: l

@[simp]

theorem List.rdropWhile_eq_nil_iff {α : Type u_1} {p : α → Bool} {l : List α} : rdropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

@[simp]

theorem List.rdropWhile_eq_self_iff {α : Type u_1} {p : α → Bool} {l : List α} : rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

theorem List.dropWhile_idempotent {α : Type u_1} (p : α → Bool) (l : List α) : dropWhile p (dropWhile p l) = dropWhile p l

theorem List.rdropWhile_idempotent {α : Type u_1} (p : α → Bool) (l : List α) : rdropWhile p (rdropWhile p l) = rdropWhile p l

theorem List.rdropWhile_reverse {α : Type u_1} (p : α → Bool) (l : List α) : rdropWhile p l.reverse = (dropWhile p l).reverse

def List.rtakeWhile {α : Type u_1} (p : α → Bool) (l : List α) : List α

Take elements from the tail end of a list that satisfy p : α → Bool. Implemented naively via List.reverse

@[simp]

theorem List.rtakeWhile_nil {α : Type u_1} (p : α → Bool) : rtakeWhile p [] = []

theorem List.rtakeWhile_concat {α : Type u_1} (p : α → Bool) (l : List α) (x : α) : rtakeWhile p (l ++ [x]) = if p x = true then rtakeWhile p l ++ [x] else []

@[simp]

theorem List.rtakeWhile_concat_pos {α : Type u_1} (p : α → Bool) (l : List α) (x : α) (h : p x = true) : rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]

@[simp]

theorem List.rtakeWhile_concat_neg {α : Type u_1} (p : α → Bool) (l : List α) (x : α) (h : ¬p x = true) : rtakeWhile p (l ++ [x]) = []

theorem List.rtakeWhile_suffix {α : Type u_1} (p : α → Bool) (l : List α) : rtakeWhile p l <:+ l

@[simp]

theorem List.rtakeWhile_eq_self_iff {α : Type u_1} {p : α → Bool} {l : List α} : rtakeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

@[simp]

theorem List.rtakeWhile_eq_nil_iff {α : Type u_1} {p : α → Bool} {l : List α} : rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

theorem List.mem_rtakeWhile_imp {α : Type u_1} {p : α → Bool} {l : List α} {x : α} (hx : x ∈ rtakeWhile p l) : p x = true

theorem List.rtakeWhile_idempotent {α : Type u_1} (p : α → Bool) (l : List α) : rtakeWhile p (rtakeWhile p l) = rtakeWhile p l

theorem List.rtakeWhile_reverse {α : Type u_1} {p : α → Bool} {l : List α} : rtakeWhile p l.reverse = (takeWhile p l).reverse

@[simp]

theorem List.rdropWhile_append_rtakeWhile {α : Type u_1} {p : α → Bool} {l : List α} : rdropWhile p l ++ rtakeWhile p l = l

theorem List.rdrop_add {α : Type u_1} {l : List α} (i j : ℕ) : (l.rdrop i).rdrop j = l.rdrop (i + j)

@[simp]

theorem List.rdrop_append_length {α : Type u_1} {l₁ l₂ : List α} : (l₁ ++ l₂).rdrop l₂.length = l₁

theorem List.rdrop_append_of_le_length {α : Type u_1} {l₁ l₂ : List α} (k : ℕ) : k ≤ l₂.length → (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

@[simp]

theorem List.rdrop_append_length_add {α : Type u_1} {l₁ l₂ : List α} (k : ℕ) : (l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k