Lists bookended by replicate blocks

Generic facts about replicate m a ++ l ++ replicate n b — a list with a left bookend of m copies of a, a middle l, and a right bookend of n copies of b — and how take, rtake, filter, and Sublist interact with the bookends. These flesh out the replicate/append corner of the List API and are candidates for Mathlib/Data/List/.

Main results

• List.take_replicate_append / List.rtake_append_replicate — a short take/rtake reaches only into the adjacent bookend, returning its replicate.
• List.filter_replicate_append_replicate — filtering distributes over the bookends, each width collapsing to 0 when its element is filtered out.
• List.sublist_replicate_append_replicate / List.not_sublist_replicate_append_replicate — a middle-sublist embeds, and a pattern that can borrow neither bookend's element for its head or last must come from the middle.

theorem List.take_replicate_append {α : Type u_1} {k m : ℕ} {a : α} {l : List α} (h : k ≤ m) : take k (replicate m a ++ l) = replicate k a

A take no longer than the left bookend reaches only into it.

theorem List.rtake_append_replicate {α : Type u_1} {k n : ℕ} {b : α} {l : List α} (h : k ≤ n) : (l ++ replicate n b).rtake k = replicate k b

An rtake no longer than the right bookend reaches only into it.

theorem List.filter_replicate_append_replicate {α : Type u_1} (p : α → Bool) (m : ℕ) (a : α) (l : List α) (n : ℕ) (b : α) : filter p (replicate m a ++ l ++ replicate n b) = replicate (if p a = true then m else 0) a ++ filter p l ++ replicate (if p b = true then n else 0) b

Filtering distributes over both bookends; a bookend width collapses to 0 when its element fails the predicate.

theorem List.sublist_replicate_append_replicate {α : Type u_1} {pat l : List α} (h : pat.Sublist l) (m : ℕ) (a : α) (n : ℕ) (b : α) : pat.Sublist (replicate m a ++ l ++ replicate n b)

A sublist of the middle is a sublist of the bookended list.

theorem List.not_sublist_replicate_append_replicate {α : Type u_1} {pat l : List α} {a b : α} (h_head : pat.head? ≠ some a) (h_last : pat.getLast? ≠ some b) (h_mid : ¬pat.Sublist l) (m n : ℕ) : ¬pat.Sublist (replicate m a ++ l ++ replicate n b)

A pattern whose head is not a and whose last element is not b, and which is not a sublist of the middle, is not a sublist of the bookended list: the replicate blocks can supply neither its head nor its last element, so any embedding must lie in the middle.