Mathlib.Data.List.Flatten

List.Sublist.flatten theorem

{l₁ l₂ : List (List α)} (h : l₁ <+ l₂) : l₁.flatten <+ l₂.flatten

Full source

@[gcongr]
protected theorem Sublist.flatten {l₁ l₂ : List (List α)} (h : l₁ <+ l₂) :
    l₁.flatten <+ l₂.flatten := by
  induction h with
  | slnil => simp
  | cons _ _ ih =>
    rw [flatten_cons]
    exact ih.trans (sublist_append_right _ _)
  | cons₂ _ _ ih => simpa

Sublist Preservation under List Concatenation

Informal description

For any two lists of lists $l₁$ and $l₂$ of type $\alpha$, if $l₁$ is a sublist of $l₂$ (denoted $l₁ <+ l₂$), then the concatenation of all lists in $l₁$ is a sublist of the concatenation of all lists in $l₂$.

List.Sublist.flatMap theorem

{l₁ l₂ : List α} (h : l₁ <+ l₂) (f : α → List β) : l₁.flatMap f <+ l₂.flatMap f

Full source

@[gcongr]
protected theorem Sublist.flatMap {l₁ l₂ : List α} (h : l₁ <+ l₂) (f : α → List β) :
    l₁.flatMap f <+ l₂.flatMap f :=
  (h.map f).flatten

Sublist Preservation under FlatMap Operation

Informal description

For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, if $l₁$ is a sublist of $l₂$ (denoted $l₁ <+ l₂$), then for any function $f : \alpha \to \text{List}\ \beta$, the flatMap operation applied to $f$ over $l₁$ is a sublist of the flatMap operation applied to $f$ over $l₂$. That is, $l₁.\mathtt{flatMap}\ f <+ l₂.\mathtt{flatMap}\ f$.

List.drop_take_succ_eq_cons_getElem theorem

(L : List α) (i : Nat) (h : i < L.length) : (L.take (i + 1)).drop i = [L[i]]

Full source

/-- Taking only the first `i+1` elements in a list, and then dropping the first `i` ones, one is
left with a list of length `1` made of the `i`-th element of the original list. -/
theorem drop_take_succ_eq_cons_getElem (L : List α) (i : Nat) (h : i < L.length) :
    (L.take (i + 1)).drop i = [L[i]] := by
  induction L generalizing i with
  | nil => exact (Nat.not_succ_le_zero i h).elim
  | cons head tail ih =>
    rcases i with _ | i
    · simp
    · simpa using ih _ (by simpa using h)

Extracting the $i$-th element via take and drop operations

Informal description

For any list $L$ of elements of type $\alpha$ and any natural number $i$ such that $i < \text{length}(L)$, the operation of first taking the first $i+1$ elements of $L$ and then dropping the first $i$ elements results in a singleton list containing the $i$-th element of $L$. That is, $\text{drop}\ i\ (\text{take}\ (i+1)\ L) = [L[i]]$.

List.append_flatten_map_append theorem

(L : List (List α)) (x : List α) : x ++ (L.map (· ++ x)).flatten = (L.map (x ++ ·)).flatten ++ x

Full source

/-- We can rebracket `x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x)` to
`(x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x` where `L = [l₁, l₂, ..., lₙ]`. -/
theorem append_flatten_map_append (L : List (List α)) (x : List α) :
    x ++ (L.map (· ++ x)).flatten = (L.map (x ++ ·)).flatten ++ x := by
  induction L with
  | nil => rw [map_nil, flatten, append_nil, map_nil, flatten, nil_append]
  | cons _ _ ih =>
    rw [map_cons, flatten, map_cons, flatten, append_assoc, ih, append_assoc, append_assoc]

Rebracketing Identity for List Concatenation and Flattening

Informal description

For any list of lists $L = [l_1, l_2, \dots, l_n]$ and any list $x$, the concatenation $x$ followed by the flattened list obtained by appending $x$ to each $l_i$ (i.e., $x \mathbin{+\!\!+} [l_1 \mathbin{+\!\!+} x, l_2 \mathbin{+\!\!+} x, \dots, l_n \mathbin{+\!\!+} x].\mathtt{flatten}$) is equal to the flattened list obtained by prepending $x$ to each $l_i$ (i.e., $[x \mathbin{+\!\!+} l_1, x \mathbin{+\!\!+} l_2, \dots, x \mathbin{+\!\!+} l_n].\mathtt{flatten}$) followed by $x$.