# 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.

Equations
Instances For
@[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 = (List.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.

Equations
Instances For
@[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 = (List.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

Equations
Instances For
@[simp]
theorem List.rdropWhile_nil {α : Type u_1} (p : αBool) :
= []
theorem List.rdropWhile_concat {α : Type u_1} (p : αBool) (l : List α) (x : α) :
List.rdropWhile p (l ++ [x]) = if p x = true then else l ++ [x]
@[simp]
theorem List.rdropWhile_concat_pos {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : p x = true) :
List.rdropWhile p (l ++ [x]) =
@[simp]
theorem List.rdropWhile_concat_neg {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : ¬p x = true) :
List.rdropWhile p (l ++ [x]) = l ++ [x]
theorem List.rdropWhile_singleton {α : Type u_1} (p : αBool) (x : α) :
List.rdropWhile p [x] = if p x = true then [] else [x]
theorem List.rdropWhile_last_not {α : Type u_1} (p : αBool) (l : List α) (hl : []) :
¬p (().getLast hl) = true
theorem List.rdropWhile_prefix {α : Type u_1} (p : αBool) (l : List α) :
<+: l
@[simp]
theorem List.rdropWhile_eq_nil_iff {α : Type u_1} {p : αBool} {l : List α} :
= [] ∀ (x : α), x lp x = true
@[simp]
theorem List.dropWhile_eq_self_iff {α : Type u_1} {p : αBool} {l : List α} :
= l ∀ (hl : 0 < l.length), ¬p (l.get 0, hl) = true
@[simp]
theorem List.rdropWhile_eq_self_iff {α : Type u_1} {p : αBool} {l : List α} :
= l ∀ (hl : l []), ¬p (l.getLast hl) = true
theorem List.dropWhile_idempotent {α : Type u_1} (p : αBool) (l : List α) :
theorem List.rdropWhile_idempotent {α : Type u_1} (p : αBool) (l : List α) :
=
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

Equations
Instances For
@[simp]
theorem List.rtakeWhile_nil {α : Type u_1} (p : αBool) :
= []
theorem List.rtakeWhile_concat {α : Type u_1} (p : αBool) (l : List α) (x : α) :
List.rtakeWhile p (l ++ [x]) = if p x = true then ++ [x] else []
@[simp]
theorem List.rtakeWhile_concat_pos {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : p x = true) :
List.rtakeWhile p (l ++ [x]) = ++ [x]
@[simp]
theorem List.rtakeWhile_concat_neg {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : ¬p x = true) :
List.rtakeWhile p (l ++ [x]) = []
theorem List.rtakeWhile_suffix {α : Type u_1} (p : αBool) (l : List α) :
<:+ l
@[simp]
theorem List.rtakeWhile_eq_self_iff {α : Type u_1} {p : αBool} {l : List α} :
= l ∀ (x : α), x lp x = true
@[simp]
theorem List.rtakeWhile_eq_nil_iff {α : Type u_1} {p : αBool} {l : List α} :
= [] ∀ (hl : l []), ¬p (l.getLast hl) = true
theorem List.mem_rtakeWhile_imp {α : Type u_1} {p : αBool} {l : List α} {x : α} (hx : x ) :
p x = true
theorem List.rtakeWhile_idempotent {α : Type u_1} (p : αBool) (l : List α) :
=
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₁ : List α} {l₂ : List α} :
(l₁ ++ l₂).rdrop l₂.length = l₁
theorem List.rdrop_append_of_le_length {α : Type u_1} {l₁ : List α} {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₁ : List α} {l₂ : List α} (k : ) :
(l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k