Lemmas about List.rtake and List.rdrop

Mathlib/Data/List/DropRight.lean defines List.rtake l n and List.rdrop l n, the last n elements of l and l without them, and proves only their nil, zero, concat, and reverse characterizations, plus a few rdrop-of-append facts. This file supplies the tail mirrors of the List.take and List.drop API in Init/Data/List/Nat/TakeDrop.lean, each proved by reducing to its front counterpart through List.rtake_eq_reverse_take_reverse or List.rdrop_eq_reverse_drop_reverse. [UPSTREAM] candidates for Mathlib/Data/List/DropRight.lean.

Main results

• List.length_rtake, List.length_rtake_le, List.rtake_of_length_le, and their rdrop twins List.length_rdrop and List.rdrop_of_length_le: lengths and saturation on a short list, mirroring List.length_take, List.length_take_le, List.take_of_length_le, List.length_drop, and List.drop_of_length_le.
• List.getElem?_rtake, List.getElem?_rdrop, List.getLast?_rtake: indexing into a tail-take or tail-drop, mirroring List.getElem?_drop, List.getElem?_take, and List.head?_take.
• List.rtake_rtake, List.rtake_append, List.rdrop_append: nested tail-takes and the tail-take or tail-drop of an append, mirroring List.take_take, List.take_append, and List.drop_append. List.rtake_append_of_le_length, List.rtake_append_length, and List.rtake_append_length_add are the corollaries mirroring List.take_append_of_le_length and mathlib's List.rdrop_append_length and List.rdrop_append_length_add.
• List.rdrop_prefix, List.rtake_suffix, List.rdrop_append_rtake: a tail-drop is a prefix, a tail-take a suffix, and together they recover the list, mirroring List.take_prefix, List.drop_suffix, and List.take_append_drop.
• List.rtake_append_rtake and List.rtake_append_append_of_le_length: the last n elements are a sufficient state, so truncating before appending, or prepending anything to a block of length at least n, leaves the tail-take unchanged.

@[simp]

theorem List.length_rtake {α : Type u_1} {l : List α} {n : ℕ} : (l.rtake n).length = min n l.length

theorem List.length_rtake_le {α : Type u_1} (n : ℕ) (l : List α) : (l.rtake n).length ≤ n

@[simp]

theorem List.length_rdrop {α : Type u_1} {l : List α} {n : ℕ} : (l.rdrop n).length = l.length - n

theorem List.rtake_of_length_le {α : Type u_1} {l : List α} {n : ℕ} (h : l.length ≤ n) : l.rtake n = l

theorem List.rdrop_of_length_le {α : Type u_1} {l : List α} {n : ℕ} (h : l.length ≤ n) : l.rdrop n = []

theorem List.getElem?_rtake {α : Type u_1} {l : List α} {n i : ℕ} : (l.rtake n)[i]? = l[l.length - n + i]?

theorem List.getElem?_rdrop {α : Type u_1} {l : List α} {n i : ℕ} : (l.rdrop n)[i]? = if i < l.length - n then l[i]? else none

theorem List.getLast?_rtake {α : Type u_1} {l : List α} {n : ℕ} : (l.rtake n).getLast? = if n = 0 then none else l.getLast?

theorem List.rtake_rtake {α : Type u_1} {l : List α} {m n : ℕ} : (l.rtake n).rtake m = l.rtake (min m n)

theorem List.rtake_append {α : Type u_1} {l₁ l₂ : List α} {n : ℕ} : (l₁ ++ l₂).rtake n = l₁.rtake (n - l₂.length) ++ l₂.rtake n

theorem List.rtake_append_of_le_length {α : Type u_1} {l₁ l₂ : List α} {n : ℕ} (h : n ≤ l₂.length) : (l₁ ++ l₂).rtake n = l₂.rtake n

@[simp]

theorem List.rtake_append_length {α : Type u_1} {l₁ l₂ : List α} : (l₁ ++ l₂).rtake l₂.length = l₂

@[simp]

theorem List.rtake_append_length_add {α : Type u_1} {l₁ l₂ : List α} (k : ℕ) : (l₁ ++ l₂).rtake (l₂.length + k) = l₁.rtake k ++ l₂

theorem List.rdrop_append {α : Type u_1} {l₁ l₂ : List α} {n : ℕ} : (l₁ ++ l₂).rdrop n = l₁.rdrop (n - l₂.length) ++ l₂.rdrop n

theorem List.rdrop_prefix {α : Type u_1} (n : ℕ) (l : List α) : l.rdrop n <+: l

theorem List.rtake_suffix {α : Type u_1} (n : ℕ) (l : List α) : l.rtake n <:+ l

@[simp]

theorem List.rdrop_append_rtake {α : Type u_1} (n : ℕ) (l : List α) : l.rdrop n ++ l.rtake n = l

theorem List.rtake_append_rtake {α : Type u_1} (n : ℕ) (l₁ l₂ : List α) : (l₁.rtake n ++ l₂).rtake n = (l₁ ++ l₂).rtake n

Truncating to the last n elements before appending is the same as truncating after: the last n elements are enough state to compute the next window.

theorem List.rtake_append_append_of_le_length {α : Type u_1} {n : ℕ} (a u y : List α) (h : n ≤ u.length) : (a ++ u ++ y).rtake n = (u ++ y).rtake n

A middle block of length at least n screens off everything to its left: the last n elements of a ++ u ++ y do not depend on a.