Mathlib.Data.List.TakeDrop

List.take_one_drop_eq_of_lt_length theorem

{l : List α} {n : ℕ} (h : n < l.length) : (l.drop n).take 1 = [l.get ⟨n, h⟩]

Full source

theorem take_one_drop_eq_of_lt_length {l : List α} {n : ℕ} (h : n < l.length) :
    (l.drop n).take 1 = [l.get ⟨n, h⟩] := by
  rw [drop_eq_getElem_cons h, take, take]
  simp

Singleton of $n$-th element equals take-one after drop-$n$

Informal description

For any list $l$ of type $\alpha$ and natural number $n$ such that $n$ is less than the length of $l$, the list obtained by taking the first element after dropping the first $n$ elements of $l$ is equal to the singleton list containing the $n$-th element of $l$.

List.take_eq_self_iff theorem

(x : List α) {n : ℕ} : x.take n = x ↔ x.length ≤ n

Full source

@[simp] lemma take_eq_self_iff (x : List α) {n : ℕ} : x.take n = x ↔ x.length ≤ n :=
  ⟨fun h ↦ by rw [← h]; simp; omega, take_of_length_le⟩

Equality of List and its Prefix if and only if Length is Bounded

Informal description

For any list $x$ of elements of type $\alpha$ and any natural number $n$, the first $n$ elements of $x$ (denoted by $x.\text{take}\,n$) equals $x$ if and only if the length of $x$ is less than or equal to $n$. In other words, $x.\text{take}\,n = x \leftrightarrow \text{length}(x) \leq n$.

List.take_self_eq_iff theorem

(x : List α) {n : ℕ} : x = x.take n ↔ x.length ≤ n

Full source

@[simp] lemma take_self_eq_iff (x : List α) {n : ℕ} : x = x.take n ↔ x.length ≤ n := by
  rw [Eq.comm, take_eq_self_iff]

List Equals its Prefix if and only if Length is Bounded by $n$

Informal description

For any list $x$ of elements of type $\alpha$ and any natural number $n$, the list $x$ equals its first $n$ elements if and only if the length of $x$ is less than or equal to $n$. In other words, $x = x.\text{take}\,n \leftrightarrow \text{length}(x) \leq n$.

List.take_eq_left_iff theorem

{x y : List α} {n : ℕ} : (x ++ y).take n = x.take n ↔ y = [] ∨ n ≤ x.length

Full source

@[simp] lemma take_eq_left_iff {x y : List α} {n : ℕ} :
    (x ++ y).take n = x.take n ↔ y = [] ∨ n ≤ x.length := by
  simp [take_append_eq_append_take, Nat.sub_eq_zero_iff_le, Or.comm]

Equality of Prefixes in Concatenated Lists: $(x ++ y).\text{take}\, n = x.\text{take}\, n \leftrightarrow y = [] \lor n \leq \text{length}\, x$

Informal description

For any two lists $x$ and $y$ of elements of type $\alpha$ and any natural number $n$, the first $n$ elements of the concatenated list $x ++ y$ are equal to the first $n$ elements of $x$ if and only if either $y$ is the empty list or $n$ is less than or equal to the length of $x$. In symbols: $$(x ++ y).\text{take}\, n = x.\text{take}\, n \leftrightarrow y = [] \lor n \leq \text{length}\, x.$$

List.left_eq_take_iff theorem

{x y : List α} {n : ℕ} : x.take n = (x ++ y).take n ↔ y = [] ∨ n ≤ x.length

Full source

@[simp] lemma left_eq_take_iff {x y : List α} {n : ℕ} :
    x.take n = (x ++ y).take n ↔ y = [] ∨ n ≤ x.length := by
  rw [Eq.comm]; apply take_eq_left_iff

Prefix Equality in Concatenated Lists: $x.\text{take}\, n = (x ++ y).\text{take}\, n \leftrightarrow y = [] \lor n \leq \text{length}\, x$

Informal description

For any two lists $x$ and $y$ of elements of type $\alpha$ and any natural number $n$, the first $n$ elements of $x$ are equal to the first $n$ elements of the concatenated list $x ++ y$ if and only if either $y$ is the empty list or $n$ is less than or equal to the length of $x$. In symbols: $$x.\text{take}\, n = (x ++ y).\text{take}\, n \leftrightarrow y = [] \lor n \leq \text{length}\, x.$$

List.drop_take_append_drop theorem

(x : List α) (m n : ℕ) : (x.drop m).take n ++ x.drop (m + n) = x.drop m

Full source

@[simp] lemma drop_take_append_drop (x : List α) (m n : ℕ) :
    (x.drop m).take n ++ x.drop (m + n) = x.drop m := by rw [← drop_drop, take_append_drop]

List Decomposition: $(x.\text{drop}\, m).\text{take}\, n ++ x.\text{drop}\, (m + n) = x.\text{drop}\, m$

Informal description

For any list $x$ of elements of type $\alpha$ and natural numbers $m$ and $n$, the concatenation of the first $n$ elements of the list obtained by dropping the first $m$ elements of $x$ and the list obtained by dropping the first $m + n$ elements of $x$ equals the list obtained by dropping the first $m$ elements of $x$. In symbols: $$(x.\text{drop}\, m).\text{take}\, n ++ x.\text{drop}\, (m + n) = x.\text{drop}\, m.$$

List.drop_take_append_drop' theorem

(x : List α) (m n : ℕ) : (x.drop m).take n ++ x.drop (n + m) = x.drop m

Full source

/-- Compared to `drop_take_append_drop`, the order of summands is swapped. -/
@[simp] lemma drop_take_append_drop' (x : List α) (m n : ℕ) :
    (x.drop m).take n ++ x.drop (n + m) = x.drop m := by rw [Nat.add_comm, drop_take_append_drop]

List Decomposition: $(x.\text{drop}\, m).\text{take}\, n ++ x.\text{drop}\, (n + m) = x.\text{drop}\, m$

Informal description

For any list $x$ of elements of type $\alpha$ and natural numbers $m$ and $n$, the concatenation of the first $n$ elements of the list obtained by dropping the first $m$ elements of $x$ and the list obtained by dropping the first $n + m$ elements of $x$ equals the list obtained by dropping the first $m$ elements of $x$. In symbols: $$(x.\text{drop}\, m).\text{take}\, n ++ x.\text{drop}\, (n + m) = x.\text{drop}\, m.$$

List.take_concat_get' theorem

(l : List α) (i : ℕ) (h : i < l.length) : l.take i ++ [l[i]] = l.take (i + 1)

Full source

/-- `take_concat_get` in simp normal form -/
lemma take_concat_get' (l : List α) (i : ℕ) (h : i < l.length) :
  l.take i ++ [l[i]] = l.take (i + 1) := by simp

Concatenation of Initial Segment with Element Yields Extended Segment

Informal description

For any list $l$ of elements of type $\alpha$, any natural number $i$ such that $i$ is less than the length of $l$, the concatenation of the first $i$ elements of $l$ with the singleton list containing the $i$-th element of $l$ is equal to the first $i+1$ elements of $l$. In symbols: \[ \text{take}(l, i) \mathbin{+\kern-1.5ex+} [l[i]] = \text{take}(l, i+1) \]

List.cons_getElem_drop_succ theorem

{l : List α} {n : Nat} {h : n < l.length} : l[n] :: l.drop (n + 1) = l.drop n

Full source

theorem cons_getElem_drop_succ {l : List α} {n : Nat} {h : n < l.length} :
    l[n]l[n] :: l.drop (n + 1) = l.drop n :=
  (drop_eq_getElem_cons h).symm

List Decomposition via Index and Drop

Informal description

For any list $l$ of type $\alpha$ and natural number $n$ such that $n$ is less than the length of $l$, the list obtained by prepending the $n$-th element of $l$ to the result of dropping the first $n+1$ elements of $l$ is equal to the result of dropping the first $n$ elements of $l$. In symbols: \[ l[n] :: \text{drop} (n + 1) l = \text{drop} n l \]

List.cons_get_drop_succ theorem

{l : List α} {n} : l.get n :: l.drop (n.1 + 1) = l.drop n.1

Full source

theorem cons_get_drop_succ {l : List α} {n} :
    l.get n :: l.drop (n.1 + 1) = l.drop n.1 :=
  (drop_eq_getElem_cons n.2).symm

List Decomposition: $l[n] :: \text{drop}(l, n+1) = \text{drop}(l, n)$

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$ such that $n$ is a valid index for $l$, the list obtained by prepending the $n$-th element of $l$ to the result of dropping the first $(n+1)$ elements of $l$ is equal to the result of dropping the first $n$ elements of $l$. In other words, $l[n] :: \text{drop}(l, n+1) = \text{drop}(l, n)$.

List.drop_length_sub_one theorem

{l : List α} (h : l ≠ []) : l.drop (l.length - 1) = [l.getLast h]

Full source

lemma drop_length_sub_one {l : List α} (h : l ≠ []) : l.drop (l.length - 1) = [l.getLast h] := by
  induction l with
  | nil => aesop
  | cons a l ih =>
    by_cases hl : l = []
    · aesop
    rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]
    simp [getLast_cons, hl]

Dropping All But Last Element Yields Singleton List

Informal description

For any nonempty list $l$ of type $\alpha$, dropping the first $(\text{length}(l) - 1)$ elements of $l$ results in a singleton list containing the last element of $l$, i.e., $\text{drop}(l, \text{length}(l) - 1) = [\text{getLast}(l)]$.

List.takeI_length theorem

: ∀ n l, length (@takeI α _ n l) = n

Full source

@[simp]
theorem takeI_length : ∀ n l, length (@takeI α _ n l) = n
  | 0, _ => rfl
  | _ + 1, _ => congr_arg succ (takeI_length _ _)

Length of `takeI` List is Input Parameter $n$

Informal description

For any natural number $n$ and any list $l$ of type $\alpha$, the length of the list obtained by applying `takeI` to $n$ and $l$ is equal to $n$.

List.takeI_nil theorem

: ∀ n, takeI n (@nil α) = replicate n default

Full source

@[simp]
theorem takeI_nil : ∀ n, takeI n (@nil α) = replicate n default
  | 0 => rfl
  | _ + 1 => congr_arg (cons _) (takeI_nil _)

`takeI` of empty list yields default-replicated list

Informal description

For any natural number $n$ and the empty list `[]` of type `List α`, the function `takeI` applied to $n$ and the empty list returns a list consisting of $n$ copies of the default value of type `α`. That is, $\text{takeI}\,n\,[] = \text{replicate}\,n\,\text{default}$.

List.takeI_eq_take theorem

: ∀ {n} {l : List α}, n ≤ length l → takeI n l = take n l

Full source

theorem takeI_eq_take : ∀ {n} {l : List α}, n ≤ length l → takeI n l = take n l
  | 0, _, _ => rfl
  | _ + 1, _ :: _, h => congr_arg (cons _) <| takeI_eq_take <| le_of_succ_le_succ h

Equality of `takeI` and `take` when $n \leq \text{length}(l)$

Informal description

For any natural number $n$ and list $l$ of type $\alpha$, if $n$ is less than or equal to the length of $l$, then the first $n$ elements of $l$ obtained via `takeI` are equal to those obtained via `take`.

List.takeI_left theorem

(l₁ l₂ : List α) : takeI (length l₁) (l₁ ++ l₂) = l₁

Full source

@[simp]
theorem takeI_left (l₁ l₂ : List α) : takeI (length l₁) (l₁ ++ l₂) = l₁ :=
  (takeI_eq_take (by simp only [length_append, Nat.le_add_right])).trans take_left

`takeI` of concatenated list returns first list when taking its length

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the first $\text{length}(l_1)$ elements of the concatenated list $l_1 ++ l_2$ obtained via `takeI` is equal to $l_1$ itself. That is, $\text{takeI}\,(\text{length}\,l_1)\,(l_1 ++ l_2) = l_1$.

List.takeI_left' theorem

{l₁ l₂ : List α} {n} (h : length l₁ = n) : takeI n (l₁ ++ l₂) = l₁

Full source

theorem takeI_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : takeI n (l₁ ++ l₂) = l₁ := by
  rw [← h]; apply takeI_left

`takeI` of concatenated list returns first list when taking its length (generalized version)

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, and any natural number $n$ such that the length of $l_1$ equals $n$, the first $n$ elements of the concatenated list $l_1 ++ l_2$ obtained via `takeI` is equal to $l_1$ itself. That is, $\text{takeI}\,n\,(l_1 ++ l_2) = l_1$.

List.takeD_length theorem

: ∀ n l a, length (@takeD α n l a) = n

Full source

@[simp]
theorem takeD_length : ∀ n l a, length (@takeD α n l a) = n
  | 0, _, _ => rfl
  | _ + 1, _, _ => congr_arg succ (takeD_length _ _ _)

Length of `takeD` List Equals Input Parameter $n$

Informal description

For any natural number $n$, any list $l$ of elements of type $\alpha$, and any default element $a : \alpha$, the length of the list obtained by applying `takeD` to $n$, $l$, and $a$ is equal to $n$.

List.takeD_eq_take theorem

: ∀ {n} {l : List α} a, n ≤ length l → takeD n l a = take n l

Full source

theorem takeD_eq_take : ∀ {n} {l : List α} a, n ≤ length l → takeD n l a = take n l
  | 0, _, _, _ => rfl
  | _ + 1, _ :: _, a, h => congr_arg (cons _) <| takeD_eq_take a <| le_of_succ_le_succ h

Equality of `takeD` and `take` for Sufficiently Short Lists

Informal description

For any natural number $n$, any list $l$ of elements of type $\alpha$, and any default element $a$ of type $\alpha$, if $n$ is less than or equal to the length of $l$, then the function `takeD` applied to $n$, $l$, and $a$ is equal to the function `take` applied to $n$ and $l$.

List.takeD_left theorem

(l₁ l₂ : List α) (a : α) : takeD (length l₁) (l₁ ++ l₂) a = l₁

Full source

@[simp]
theorem takeD_left (l₁ l₂ : List α) (a : α) : takeD (length l₁) (l₁ ++ l₂) a = l₁ :=
  (takeD_eq_take a (by simp only [length_append, Nat.le_add_right])).trans take_left

`takeD` of concatenated lists preserves first list when taking its length

Informal description

For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, and any default element $a : \alpha$, the function `takeD` applied to the length of $l₁$, the concatenation of $l₁$ and $l₂$, and $a$ yields $l₁$.

List.takeD_left' theorem

{l₁ l₂ : List α} {n} {a} (h : length l₁ = n) : takeD n (l₁ ++ l₂) a = l₁

Full source

theorem takeD_left' {l₁ l₂ : List α} {n} {a} (h : length l₁ = n) : takeD n (l₁ ++ l₂) a = l₁ := by
  rw [← h]; apply takeD_left

`takeD` of Concatenated Lists Preserves First List When Taking Its Exact Length

Informal description

For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, any natural number $n$, and any default element $a : \alpha$, if the length of $l₁$ equals $n$, then the function `takeD` applied to $n$, the concatenation of $l₁$ and $l₂$, and $a$ yields $l₁$.

List.span_eq_takeWhile_dropWhile theorem

(l : List α) : span p l = (takeWhile p l, dropWhile p l)

Full source

@[simp]
theorem span_eq_takeWhile_dropWhile (l : List α) : span p l = (takeWhile p l, dropWhile p l) := by
  simpa using span.loop_eq_take_drop p l []

Span Equals TakeWhile-DropWhile Pair

Informal description

For any list $l$ of elements of type $\alpha$ and any predicate $p$ on $\alpha$, the operation `span p l` (which splits the list into the longest prefix satisfying $p$ and the remaining suffix) is equal to the pair consisting of `takeWhile p l` (the longest prefix of $l$ where all elements satisfy $p$) and `dropWhile p l` (the remaining suffix after removing the longest prefix satisfying $p$).

List.dropSlice_eq theorem

(xs : List α) (n m : ℕ) : dropSlice n m xs = xs.take n ++ xs.drop (n + m)

Full source

theorem dropSlice_eq (xs : List α) (n m : ℕ) : dropSlice n m xs = xs.take n ++ xs.drop (n + m) := by
  induction n generalizing xs
  · cases xs <;> simp [dropSlice]
  · cases xs <;> simp [dropSlice, *, Nat.succ_add]

Decomposition of `dropSlice` into `take` and `drop` operations

Informal description

For any list $xs$ of elements of type $\alpha$ and natural numbers $n$ and $m$, the operation `dropSlice n m xs` is equal to the concatenation of the first $n$ elements of $xs$ (obtained via `take n xs`) and the list obtained by dropping the first $n + m$ elements of $xs$ (obtained via `drop (n + m) xs$).

List.length_dropSlice theorem

(i j : ℕ) (xs : List α) : (List.dropSlice i j xs).length = xs.length - min j (xs.length - i)

Full source

@[simp]
theorem length_dropSlice (i j : ℕ) (xs : List α) :
    (List.dropSlice i j xs).length = xs.length - min j (xs.length - i) := by
  induction xs generalizing i j with
  | nil => simp
  | cons x xs xs_ih =>
    cases i <;> simp only [List.dropSlice]
    · cases j with
      | zero => simp
      | succ n => simp_all [xs_ih]; omega
    · simp [xs_ih]; omega

Length of `dropSlice` Operation on Lists

Informal description

For any natural numbers $i$ and $j$ and any list $xs$ of elements of type $\alpha$, the length of the list obtained by applying `dropSlice i j xs` is equal to the length of $xs$ minus the minimum of $j$ and the difference between the length of $xs$ and $i$. That is, $$ \text{length}(\text{dropSlice } i\, j\, xs) = \text{length}(xs) - \min(j, \text{length}(xs) - i). $$

List.length_dropSlice_lt theorem

(i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) : (List.dropSlice i j xs).length < xs.length

Full source

theorem length_dropSlice_lt (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) :
    (List.dropSlice i j xs).length < xs.length := by
  simp; omega

Strict Length Reduction Property of `dropSlice` Operation

Informal description

For any natural numbers $i$ and $j$ with $j > 0$, and any list $xs$ of elements of type $\alpha$ with $i < \text{length}(xs)$, the length of the list obtained by applying $\text{dropSlice } i\, j\, xs$ is strictly less than the length of $xs$. That is, $$ \text{length}(\text{dropSlice } i\, j\, xs) < \text{length}(xs). $$