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 #

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 : ℕ) :

Drop n elements from the tail end of a list.

Equations

l.rdrop n = list.take (l.length - n) l

@[simp]

theorem list.rdrop_nil {α : Type u_1} (n : ℕ) :

list.nil.rdrop n = list.nil

@[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 : ℕ) :

Take n elements from the tail end of a list.

Equations

l.rtake n = list.drop (l.length - n) l

@[simp]

theorem list.rtake_nil {α : Type u_1} (n : ℕ) :

list.nil.rtake n = list.nil

@[simp]

theorem list.rtake_zero {α : Type u_1} (l : list α) :

l.rtake 0 = list.nil

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.rdrop_while {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :

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

Equations

list.rdrop_while p l = (list.drop_while p l.reverse).reverse

@[simp]

theorem list.rdrop_while_nil {α : Type u_1} (p : α → Prop) [decidable_pred p] :

list.rdrop_while p list.nil = list.nil

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) :

list.rdrop_while p (l ++ [x]) = list.rdrop_while p l

@[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 : α) :

list.rdrop_while p [x] = ite (p x) list.nil [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) :

¬p ((list.rdrop_while p l).last hl)

theorem list.rdrop_while_prefix {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :

list.rdrop_while p l <+: l

@[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 α) :

list.drop_while p (list.drop_while p l) = list.drop_while p l

theorem list.rdrop_while_idempotent {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :

list.rdrop_while p (list.rdrop_while p l) = list.rdrop_while p l

def list.rtake_while {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :

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

Equations

list.rtake_while p l = (list.take_while p l.reverse).reverse

@[simp]

theorem list.rtake_while_nil {α : Type u_1} (p : α → Prop) [decidable_pred p] :

list.rtake_while p list.nil = list.nil

theorem list.rtake_while_concat {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) (x : α) :

list.rtake_while p (l ++ [x]) = ite (p x) (list.rtake_while p l ++ [x]) list.nil

@[simp]

theorem list.rtake_while_concat_pos {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) (x : α) (h : p x) :

list.rtake_while p (l ++ [x]) = list.rtake_while p l ++ [x]

@[simp]

theorem list.rtake_while_concat_neg {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) (x : α) (h : ¬p x) :

list.rtake_while p (l ++ [x]) = list.nil

theorem list.rtake_while_suffix {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :

list.rtake_while p l <:+ l

@[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 α} :

list.rtake_while p l = list.nil ↔ ∀ (hl : l ≠ list.nil), ¬p (l.last hl)

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 α) :

list.rtake_while p (list.rtake_while p l) = list.rtake_while p l