Dropping or taking from lists on the right

Taking or removing element from the tail end of a list

Main defintions

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

ink

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

Drop n elements from the tail end of a list.

Equations

• List.rdrop l n = List.take (List.length l - n) l

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

Take n elements from the tail end of a list.

Equations

• List.rtake l n = List.drop (List.length l - n) l

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

• List.rdropWhile p l = List.reverse (List.dropWhile p (List.reverse l))

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[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]

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

theorem List.dropWhile_eq_self_iff {α : Type u_1} {p : α → Bool} {l : List α} : List.dropWhile p l = l ↔ ∀ (hl : 0 < List.length l), ¬p (List.nthLe l 0 hl) = true

ink

@[simp]

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

ink

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

ink

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

ink

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

• List.rtakeWhile p l = List.reverse (List.takeWhile p (List.reverse l))

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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