Length, saturation, and decomposition for List.rtake

A handful of facts about List.rtake (take from the tail) and List.rdrop (drop from the tail) that mathlib's Mathlib/Data/List/DropRight.lean defines but leaves without an API: the length of a tail-take, when it saturates to the whole list, how it absorbs a left append, and the rdrop/rtake decomposition. Each is the tail mirror of a front-end take lemma and is proved by reducing to it through List.rtake_eq_reverse_take_reverse — reverse, then take. These flesh out an under-developed corner of mathlib and are candidates for Mathlib/Data/List/DropRight.lean.

Main results

• List.length_rtake — (l.rtake n).length = min n l.length.
• List.length_rtake_le — (l.rtake n).length ≤ n.
• List.rtake_of_length_le — a short list is its own tail-take.
• List.rtake_append_of_le_length — a tail-take long enough to fit in the right summand ignores the left one.
• List.rdrop_append_rtake — l.rdrop n ++ l.rtake n = l, the tail analog of List.take_append_drop.

@[simp]

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

A tail-take has length min n l.length — the tail analog of List.length_take.

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

A tail-take has length at most n — the tail analog of List.length_take_le.

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

A list no longer than n is its own tail-take — the tail analog of List.take_of_length_le.

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

A tail-take that fits inside the right summand ignores the left one — the tail analog of List.take_append_of_le_length.

@[simp]

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

Splitting a list at its last n symbols — the tail analog of List.take_append_drop.

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

Taking a suffix of a suffix takes the shorter of the two.

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

A suffix long enough to swallow l₂ splits as a suffix of l₁ followed by 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 a suffix window before appending is the same as truncating after: the last n symbols 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 ≥ n screens off everything to its left: the last n symbols of a ++ u ++ y do not depend on a.