mathlib3 documentation

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 #

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) [decidable_pred p] (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) [decidable_pred p] :
theorem list.rdrop_while_concat {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) (x : α) :
list.rdrop_while p (l ++ [x]) = ite (p x) (list.rdrop_while p l) (l ++ [x])
@[simp]
theorem list.rdrop_while_concat_pos {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) (x : α) (h : p x) :
@[simp]
theorem list.rdrop_while_concat_neg {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) (x : α) (h : ¬p x) :
list.rdrop_while p (l ++ [x]) = l ++ [x]
theorem list.rdrop_while_singleton {α : Type u_1} (p : α Prop) [decidable_pred p] (x : α) :
theorem list.rdrop_while_last_not {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) (hl : list.rdrop_while p l list.nil) :
theorem list.rdrop_while_prefix {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) :
@[simp]
theorem list.rdrop_while_eq_nil_iff {α : Type u_1} {p : α Prop} [decidable_pred p] {l : list α} :
list.rdrop_while p l = list.nil (x : α), x l p x
@[simp]
theorem list.drop_while_eq_self_iff {α : Type u_1} {p : α Prop} [decidable_pred p] {l : list α} :
list.drop_while p l = l (hl : 0 < l.length), ¬p (l.nth_le 0 hl)
@[simp]
theorem list.rdrop_while_eq_self_iff {α : Type u_1} {p : α Prop} [decidable_pred p] {l : list α} :
list.rdrop_while p l = l (hl : l list.nil), ¬p (l.last hl)
theorem list.drop_while_idempotent {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) :
theorem list.rdrop_while_idempotent {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) :
def list.rtake_while {α : Type u_1} (p : α Prop) [decidable_pred p] (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) [decidable_pred p] :
theorem list.rtake_while_concat {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) (x : α) :
@[simp]
theorem list.rtake_while_concat_pos {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) (x : α) (h : p x) :
@[simp]
theorem list.rtake_while_concat_neg {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) (x : α) (h : ¬p x) :
theorem list.rtake_while_suffix {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) :
@[simp]
theorem list.rtake_while_eq_self_iff {α : Type u_1} {p : α Prop} [decidable_pred p] {l : list α} :
list.rtake_while p l = l (x : α), x l p x
@[simp]
theorem list.rtake_while_eq_nil_iff {α : Type u_1} {p : α Prop} [decidable_pred p] {l : list α} :
theorem list.mem_rtake_while_imp {α : Type u_1} {p : α Prop} [decidable_pred p] {l : list α} {x : α} (hx : x list.rtake_while p l) :
p x
theorem list.rtake_while_idempotent {α : Type u_1} (p : α Prop) [decidable_pred p] (l : list α) :