data.list.rdrop

# Dropping or taking from lists on the right #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
• drop_while p: remove all the elements that satisfy a decidable p : α → Prop from the tail of a list until hitting the first non-satisfying element
• take_while p: take all the elements that satisfy a decidable p : α → Prop from the tail of a list until hitting the first non-satisfying element

## 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
@[simp]
theorem list.rdrop_nil {α : Type u_1} (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 : ) :
@[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
@[simp]
theorem list.rtake_nil {α : Type u_1} (n : ) :
@[simp]
theorem list.rtake_zero {α : Type u_1} (l : list α) :
theorem list.rtake_eq_reverse_take_reverse {α : Type u_1} (l : list α) (n : ) :
@[simp]
theorem list.rtake_concat_succ {α : Type u_1} (l : list α) (n : ) (x : α) :
(l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]
def list.rdrop_while {α : Type u_1} (p : α Prop) (l : list α) :
list α

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

Equations
@[simp]
theorem list.rdrop_while_nil {α : Type u_1} (p : α Prop)  :
theorem list.rdrop_while_concat {α : Type u_1} (p : α Prop) (l : list α) (x : α) :
(l ++ [x]) = ite (p x) l) (l ++ [x])
@[simp]
theorem list.rdrop_while_concat_pos {α : Type u_1} (p : α Prop) (l : list α) (x : α) (h : p x) :
(l ++ [x]) =
@[simp]
theorem list.rdrop_while_concat_neg {α : Type u_1} (p : α Prop) (l : list α) (x : α) (h : ¬p x) :
(l ++ [x]) = l ++ [x]
theorem list.rdrop_while_singleton {α : Type u_1} (p : α Prop) (x : α) :
= ite (p x) list.nil [x]
theorem list.rdrop_while_last_not {α : Type u_1} (p : α Prop) (l : list α) (hl : list.nil) :
¬p l).last hl)
theorem list.rdrop_while_prefix {α : Type u_1} (p : α Prop) (l : list α) :
<+: l
@[simp]
theorem list.rdrop_while_eq_nil_iff {α : Type u_1} {p : α Prop} {l : list α} :
(x : α), x l p x
@[simp]
theorem list.drop_while_eq_self_iff {α : Type u_1} {p : α Prop} {l : list α} :
= l (hl : 0 < l.length), ¬p (l.nth_le 0 hl)
@[simp]
theorem list.rdrop_while_eq_self_iff {α : Type u_1} {p : α Prop} {l : list α} :
= l (hl : , ¬p (l.last hl)
theorem list.drop_while_idempotent {α : Type u_1} (p : α Prop) (l : list α) :
l) =
theorem list.rdrop_while_idempotent {α : Type u_1} (p : α Prop) (l : list α) :
l) =
def list.rtake_while {α : Type u_1} (p : α Prop) (l : list α) :
list α

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

Equations
@[simp]
theorem list.rtake_while_nil {α : Type u_1} (p : α Prop)  :
theorem list.rtake_while_concat {α : Type u_1} (p : α Prop) (l : list α) (x : α) :
(l ++ [x]) = ite (p x) l ++ [x]) list.nil
@[simp]
theorem list.rtake_while_concat_pos {α : Type u_1} (p : α Prop) (l : list α) (x : α) (h : p x) :
(l ++ [x]) = ++ [x]
@[simp]
theorem list.rtake_while_concat_neg {α : Type u_1} (p : α Prop) (l : list α) (x : α) (h : ¬p x) :
(l ++ [x]) = list.nil
theorem list.rtake_while_suffix {α : Type u_1} (p : α Prop) (l : list α) :
<:+ l
@[simp]
theorem list.rtake_while_eq_self_iff {α : Type u_1} {p : α Prop} {l : list α} :
= l (x : α), x l p x
@[simp]
theorem list.rtake_while_eq_nil_iff {α : Type u_1} {p : α Prop} {l : list α} :
(hl : , ¬p (l.last hl)
theorem list.mem_rtake_while_imp {α : Type u_1} {p : α Prop} {l : list α} {x : α} (hx : x ) :
p x
theorem list.rtake_while_idempotent {α : Type u_1} (p : α Prop) (l : list α) :
l) =