Mathlib.Data.List.Infix

List.IsPrefix.take theorem

(h : l₁ <+: l₂) (n : ℕ) : l₁.take n <+: l₂.take n

Full source

@[gcongr] lemma IsPrefix.take (h : l₁ <+: l₂) (n : ℕ) : l₁.take n <+: l₂.take n := by
  simpa [prefix_take_iff, Nat.min_le_left] using (take_prefix n l₁).trans h

Prefix Preservation under List Truncation

Informal description

If a list $l₁$ is a prefix of another list $l₂$, then for any natural number $n$, the first $n$ elements of $l₁$ form a prefix of the first $n$ elements of $l₂$.

List.IsPrefix.drop theorem

(h : l₁ <+: l₂) (n : ℕ) : l₁.drop n <+: l₂.drop n

Full source

@[gcongr] lemma IsPrefix.drop (h : l₁ <+: l₂) (n : ℕ) : l₁.drop n <+: l₂.drop n := by
  rw [prefix_iff_eq_take.mp h, drop_take]; apply take_prefix

Prefix Preservation under Drop Operation

Informal description

For any two lists $l_1$ and $l_2$ such that $l_1$ is a prefix of $l_2$ (denoted $l_1 <+: l_2$), and for any natural number $n$, the list obtained by dropping the first $n$ elements of $l_1$ is a prefix of the list obtained by dropping the first $n$ elements of $l_2$.

List.isPrefix_append_of_length theorem

(h : l₁.length ≤ l₂.length) : l₁ <+: l₂ ++ l₃ ↔ l₁ <+: l₂

Full source

lemma isPrefix_append_of_length (h : l₁.length ≤ l₂.length) : l₁ <+: l₂ ++ l₃l₁ <+: l₂ ++ l₃ ↔ l₁ <+: l₂ :=
  ⟨fun h ↦ by rw [prefix_iff_eq_take] at *; nth_rw 1 [h, take_eq_left_iff]; tauto,
   fun h ↦ h.trans <| l₂.prefix_append l₃⟩

Prefix Condition for Concatenated Lists: $l_1 <+: l_2 ++ l_3 \leftrightarrow l_1 <+: l_2$ when $\text{length}(l_1) \leq \text{length}(l_2)$

Informal description

For any lists $l_1$, $l_2$, and $l_3$ of elements of type $\alpha$, if the length of $l_1$ is less than or equal to the length of $l_2$, then $l_1$ is a prefix of the concatenated list $l_2 ++ l_3$ if and only if $l_1$ is a prefix of $l_2$. In symbols: $$l_1 <+: l_2 ++ l_3 \leftrightarrow l_1 <+: l_2 \quad \text{when} \quad \text{length}(l_1) \leq \text{length}(l_2).$$

List.take_isPrefix_take theorem

{m n : ℕ} : l.take m <+: l.take n ↔ m ≤ n ∨ l.length ≤ n

Full source

@[simp] lemma take_isPrefix_take {m n : ℕ} : l.take m <+: l.take nl.take m <+: l.take n ↔ m ≤ n ∨ l.length ≤ n := by
  simp [prefix_take_iff, take_prefix]; omega

Prefix Relation Between List Prefixes: $\text{take}(m, l) \text{ is prefix of } \text{take}(n, l) \leftrightarrow m \leq n \lor \text{length}(l) \leq n$

Informal description

For any natural numbers $m$ and $n$, and any list $l$, the prefix of $l$ consisting of the first $m$ elements is a prefix of the prefix consisting of the first $n$ elements if and only if either $m \leq n$ or the length of $l$ is less than or equal to $n$.

List.IsPrefix.flatten theorem

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

Full source

@[gcongr]
protected theorem IsPrefix.flatten {l₁ l₂ : List (List α)} (h : l₁ <+: l₂) :
    l₁.flatten <+: l₂.flatten := by
  rcases h with ⟨l, rfl⟩
  simp

Prefix Preservation under List Concatenation

Informal description

For any two lists of lists $l₁$ and $l₂$ of type $\alpha$, if $l₁$ is a prefix of $l₂$, then the concatenation of all elements in $l₁$ is a prefix of the concatenation of all elements in $l₂$.

List.IsPrefix.flatMap theorem

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

Full source

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

Prefix Preservation under Flat-Mapping: $\text{flatMap}(f, l₁) <+: \text{flatMap}(f, l₂)$ when $l₁ <+: l₂$

Informal description

For any two lists $l₁$ and $l₂$ of type $\alpha$, if $l₁$ is a prefix of $l₂$ (denoted $l₁ <+: l₂$), then for any function $f : \alpha \to \text{List } \beta$, the flat-mapped list $\text{flatMap}(f, l₁)$ is a prefix of $\text{flatMap}(f, l₂)$.

List.IsSuffix.flatten theorem

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

Full source

@[gcongr]
protected theorem IsSuffix.flatten {l₁ l₂ : List (List α)} (h : l₁ <:+ l₂) :
    l₁.flatten <:+ l₂.flatten := by
  rcases h with ⟨l, rfl⟩
  simp

Suffix Preservation under List Flattening

Informal description

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

List.IsSuffix.flatMap theorem

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

Full source

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

Suffix Preservation under FlatMap Operation

Informal description

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

List.IsInfix.flatten theorem

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

Full source

@[gcongr]
protected theorem IsInfix.flatten {l₁ l₂ : List (List α)} (h : l₁ <:+: l₂) :
    l₁.flatten <:+: l₂.flatten := by
  rcases h with ⟨l, l', rfl⟩
  simp

Flattening Preserves Infix Relation on Lists of Lists

Informal description

For any two lists of lists $l₁$ and $l₂$ of type $\alpha$, if $l₁$ is an infix of $l₂$ (denoted $l₁ <:+: l₂$), then the flattened version of $l₁$ is an infix of the flattened version of $l₂$.

List.IsInfix.flatMap theorem

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

Full source

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

FlatMap Preserves Infix Relation on Lists

Informal description

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

List.dropSlice_sublist theorem

(n m : ℕ) (l : List α) : l.dropSlice n m <+ l

Full source

lemma dropSlice_sublist (n m : ℕ) (l : List α) : l.dropSlice n m <+ l :=
  calc
    l.dropSlice n m = take n l ++ drop m (drop n l) := by rw [dropSlice_eq, drop_drop, Nat.add_comm]
  _ <+ take n l ++ drop n l := (Sublist.refl _).append (drop_sublist _ _)
  _ = _ := take_append_drop _ _

`dropSlice` Preserves Sublist Relation

Informal description

For any natural numbers $n$ and $m$ and any list $l$ of elements of type $\alpha$, the list obtained by applying `dropSlice n m` to $l$ is a sublist of $l$.

List.dropSlice_subset theorem

(n m : ℕ) (l : List α) : l.dropSlice n m ⊆ l

Full source

lemma dropSlice_subset (n m : ℕ) (l : List α) : l.dropSlice n m ⊆ l :=
  (dropSlice_sublist n m l).subset

Subset Property of `dropSlice` Operation on Lists

Informal description

For any natural numbers $n$ and $m$ and any list $l$ of elements of type $\alpha$, the list obtained by applying `dropSlice n m` to $l$ is a subset of $l$.

List.mem_of_mem_dropSlice theorem

{n m : ℕ} {l : List α} {a : α} (h : a ∈ l.dropSlice n m) : a ∈ l

Full source

lemma mem_of_mem_dropSlice {n m : ℕ} {l : List α} {a : α} (h : a ∈ l.dropSlice n m) : a ∈ l :=
  dropSlice_subset n m l h

Membership Preservation under `dropSlice` Operation

Informal description

For any natural numbers $n$ and $m$, any list $l$ of elements of type $\alpha$, and any element $a \in \alpha$, if $a$ is in the list obtained by applying `dropSlice n m` to $l$, then $a$ is also in the original list $l$.

List.tail_subset theorem

(l : List α) : tail l ⊆ l

Full source

theorem tail_subset (l : List α) : tailtail l ⊆ l :=
  (tail_sublist l).subset

Tail of a List is a Subset

Informal description

For any list $l$ of elements of type $\alpha$, the tail of $l$ is a subset of $l$.

List.mem_of_mem_dropLast theorem

(h : a ∈ l.dropLast) : a ∈ l

Full source

theorem mem_of_mem_dropLast (h : a ∈ l.dropLast) : a ∈ l :=
  dropLast_subset l h

Membership Preservation in List Truncation

Informal description

For any element $a$ in a list $l$, if $a$ is in the list obtained by removing the last element of $l$ (denoted as `l.dropLast`), then $a$ is also in the original list $l$.

List.concat_get_prefix theorem

{x y : List α} (h : x <+: y) (hl : x.length < y.length) : x ++ [y.get ⟨x.length, hl⟩] <+: y

Full source

theorem concat_get_prefix {x y : List α} (h : x <+: y) (hl : x.length < y.length) :
    x ++ [y.get ⟨x.length, hl⟩] <+: y := by
  use y.drop (x.length + 1)
  nth_rw 1 [List.prefix_iff_eq_take.mp h]
  convert List.take_append_drop (x.length + 1) y using 2
  rw [← List.take_concat_get, List.concat_eq_append]; rfl

Prefix Extension by Next Element

Informal description

For any two lists $x$ and $y$ of elements of type $\alpha$, if $x$ is a prefix of $y$ (denoted $x <+: y$) and the length of $x$ is strictly less than the length of $y$, then the list obtained by appending to $x$ the element of $y$ at position $\text{length}(x)$ is also a prefix of $y$.

List.decidableInfix instance

[DecidableEq α] : ∀ l₁ l₂ : List α, Decidable (l₁ <:+: l₂)

Full source

instance decidableInfix [DecidableEq α] : ∀ l₁ l₂ : List α, Decidable (l₁ <:+: l₂)
  | [], l₂ => isTrue ⟨[], l₂, rfl⟩
  | a :: l₁, [] => isFalse fun ⟨s, t, te⟩ => by simp at te
  | l₁, b :: l₂ =>
    letI := l₁.decidableInfix l₂
    @decidable_of_decidable_of_iff (l₁ <+: b :: l₂ ∨ l₁ <:+: l₂) _ _
      infix_cons_iff.symm

Decidability of List Infix Relation

Informal description

For any type $\alpha$ with decidable equality, the infix relation $l_1 <:+: l_2$ (meaning $l_1$ is an infix of $l_2$) is decidable for any two lists $l_1, l_2$ of type $\alpha$.

List.IsPrefix.reduceOption theorem

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

Full source

protected theorem IsPrefix.reduceOption {l₁ l₂ : List (Option α)} (h : l₁ <+: l₂) :
    l₁.reduceOption <+: l₂.reduceOption :=
  h.filterMap id

Prefix Preservation under `reduceOption` Operation on Lists

Informal description

For any two lists $l₁$ and $l₂$ of type `List (Option α)`, if $l₁$ is a prefix of $l₂$, then the list obtained by removing `none` elements from $l₁$ is a prefix of the list obtained by removing `none` elements from $l₂$.

List.instIsPartialOrderIsPrefix instance

: IsPartialOrder (List α) (· <+: ·)

Full source

instance : IsPartialOrder (List α) (· <+: ·) where
  refl _ := prefix_rfl
  trans _ _ _ := IsPrefix.trans
  antisymm _ _ h₁ h₂ := h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le

Partial Order Structure of Prefix Relation on Lists

Informal description

For any type $\alpha$, the prefix relation $\cdot <+: \cdot$ on lists of $\alpha$ is a partial order. This means: 1. **Reflexivity**: Every list is a prefix of itself. 2. **Transitivity**: If $l_1$ is a prefix of $l_2$ and $l_2$ is a prefix of $l_3$, then $l_1$ is a prefix of $l_3$. 3. **Antisymmetry**: If $l_1$ is a prefix of $l_2$ and $l_2$ is a prefix of $l_1$, then $l_1 = l_2$. Here, $l_1 <+: l_2$ means $l_1$ is an initial segment of $l_2$.

List.instIsPartialOrderIsSuffix instance

: IsPartialOrder (List α) (· <:+ ·)

Full source

instance : IsPartialOrder (List α) (· <:+ ·) where
  refl _ := suffix_rfl
  trans _ _ _ := IsSuffix.trans
  antisymm _ _ h₁ h₂ := h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le

Partial Order Structure of Suffix Relation on Lists

Informal description

For any type $\alpha$, the suffix relation $\cdot <:+ \cdot$ on lists of $\alpha$ is a partial order. This means: 1. **Reflexivity**: Every list is a suffix of itself. 2. **Transitivity**: If $l_1$ is a suffix of $l_2$ and $l_2$ is a suffix of $l_3$, then $l_1$ is a suffix of $l_3$. 3. **Antisymmetry**: If $l_1$ is a suffix of $l_2$ and $l_2$ is a suffix of $l_1$, then $l_1 = l_2$. Here, $l_1 <:+ l_2$ means $l_1$ is a terminal segment of $l_2$.

List.instIsPartialOrderIsInfix instance

: IsPartialOrder (List α) (· <:+: ·)

Full source

instance : IsPartialOrder (List α) (· <:+: ·) where
  refl _ := infix_rfl
  trans _ _ _ := IsInfix.trans
  antisymm _ _ h₁ h₂ := h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le

Partial Order Structure of Infix Relation on Lists

Informal description

For any type $\alpha$, the infix relation $\cdot <:+: \cdot$ on lists of $\alpha$ is a partial order. This means: 1. **Reflexivity**: Every list is an infix of itself. 2. **Transitivity**: If $l_1$ is an infix of $l_2$ and $l_2$ is an infix of $l_3$, then $l_1$ is an infix of $l_3$. 3. **Antisymmetry**: If $l_1$ is an infix of $l_2$ and $l_2$ is an infix of $l_1$, then $l_1 = l_2$. Here, $l_1 <:+: l_2$ means $l_1$ is a contiguous sublist of $l_2$.

List.mem_inits theorem

: ∀ s t : List α, s ∈ inits t ↔ s <+: t

Full source

@[simp]
theorem mem_inits : ∀ s t : List α, s ∈ inits ts ∈ inits t ↔ s <+: t
  | s, [] =>
    suffices s = nil ↔ s <+: nil by simpa only [inits, mem_singleton]
    ⟨fun h => h.symm ▸ prefix_rfl, eq_nil_of_prefix_nil⟩
  | s, a :: t =>
    suffices (s = nil ∨ ∃ l ∈ inits t, a :: l = s) ↔ s <+: a :: t by simpa
    ⟨fun o =>
      match s, o with
      | _, Or.inl rfl => ⟨_, rfl⟩
      | s, Or.inr ⟨r, hr, hs⟩ => by
        let ⟨s, ht⟩ := (mem_inits _ _).1 hr
        rw [← hs, ← ht]; exact ⟨s, rfl⟩,
      fun mi =>
      match s, mi with
      | [], ⟨_, rfl⟩ => Or.inl rfl
      | b :: s, ⟨r, hr⟩ =>
        (List.noConfusion hr) fun ba (st : s ++ r = t) =>
          Or.inr <| by rw [ba]; exact ⟨_, (mem_inits _ _).2 ⟨_, st⟩, rfl⟩⟩

Characterization of List Prefix Membership

Informal description

For any two lists $s$ and $t$ of elements of type $\alpha$, $s$ is in the set of prefixes of $t$ if and only if $s$ is a prefix of $t$. Here, the set of prefixes of a list $t$ consists of all lists that can be obtained by taking initial segments of $t$ (including the empty list and $t$ itself), and $s$ is a prefix of $t$ (denoted $s <+: t$) means that $t$ starts with $s$.

List.mem_tails theorem

: ∀ s t : List α, s ∈ tails t ↔ s <:+ t

Full source

@[simp]
theorem mem_tails : ∀ s t : List α, s ∈ tails ts ∈ tails t ↔ s <:+ t
  | s, [] => by
    simp only [tails, mem_singleton, suffix_nil]
  | s, a :: t => by
    simp only [tails, mem_cons, mem_tails s t]
    exact
      show s = a :: t ∨ s <:+ ts = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
        ⟨fun o =>
          match s, t, o with
          | _, t, Or.inl rfl => suffix_rfl
          | s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
          fun e =>
          match s, t, e with
          | _, t, ⟨[], rfl⟩ => Or.inl rfl
          | s, t, ⟨b :: l, he⟩ => List.noConfusion he fun _ lt => Or.inr ⟨l, lt⟩⟩

Characterization of Suffix Membership in List of Suffixes

Informal description

For any two lists $s$ and $t$ of elements of type $\alpha$, the list $s$ is an element of the list of suffixes of $t$ if and only if $s$ is a suffix of $t$.

List.inits_cons theorem

(a : α) (l : List α) : inits (a :: l) = [] :: l.inits.map fun t => a :: t

Full source

theorem inits_cons (a : α) (l : List α) : inits (a :: l) = [][] :: l.inits.map fun t => a :: t := by
  simp

Prefixes of a Cons List: $\text{inits}(a :: l) = [] :: \text{map} (a :: \cdot) (\text{inits}\ l)$

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list of prefixes of the list $a :: l$ is equal to the empty list `[]` concatenated with the list obtained by mapping each prefix $t$ of $l$ to $a :: t$.

List.tails_cons theorem

(a : α) (l : List α) : tails (a :: l) = (a :: l) :: l.tails

Full source

theorem tails_cons (a : α) (l : List α) : tails (a :: l) = (a :: l) :: l.tails := by simp

Suffixes of a Cons List

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list of suffixes of the list $a :: l$ is equal to the list $(a :: l) :: \text{tails}(l)$, where $\text{tails}(l)$ denotes the list of suffixes of $l$.

List.inits_append theorem

: ∀ s t : List α, inits (s ++ t) = s.inits ++ t.inits.tail.map fun l => s ++ l

Full source

@[simp]
theorem inits_append : ∀ s t : List α, inits (s ++ t) = s.inits ++ t.inits.tail.map fun l => s ++ l
  | [], [] => by simp
  | [], a :: t => by simp
  | a :: s, t => by simp [inits_append s t, Function.comp_def]

Prefixes of Concatenated Lists

Informal description

For any two lists $s$ and $t$ of elements of type $\alpha$, the list of prefixes of the concatenated list $s \mathbin{+\!\!+} t$ is equal to the concatenation of the prefixes of $s$ with the list obtained by taking the tail of the prefixes of $t$ and prepending $s$ to each element. In other words: $$\text{inits}(s \mathbin{+\!\!+} t) = \text{inits}(s) \mathbin{+\!\!+} \text{map} (\lambda l, s \mathbin{+\!\!+} l) (\text{tail} (\text{inits}(t)))$$

List.tails_append theorem

: ∀ s t : List α, tails (s ++ t) = (s.tails.map fun l => l ++ t) ++ t.tails.tail

Full source

@[simp]
theorem tails_append :
    ∀ s t : List α, tails (s ++ t) = (s.tails.map fun l => l ++ t) ++ t.tails.tail
  | [], [] => by simp
  | [], a :: t => by simp
  | a :: s, t => by simp [tails_append s t]

Suffixes of Concatenated Lists

Informal description

For any two lists $s$ and $t$ of elements of type $\alpha$, the list of suffixes of the concatenated list $s ++ t$ is equal to the concatenation of: 1. The list obtained by appending $t$ to each suffix of $s$, and 2. The tail of the list of suffixes of $t$. In symbols: $$ \text{tails}(s \mathbin{+\kern-1.5ex+} t) = (\text{map}\ (\lambda l, l \mathbin{+\kern-1.5ex+} t)\ \text{tails}(s)) \mathbin{+\kern-1.5ex+} \text{tail}(\text{tails}(t)) $$

List.inits_eq_tails theorem

: ∀ l : List α, l.inits = (reverse <| map reverse <| tails <| reverse l)

Full source

theorem inits_eq_tails : ∀ l : List α, l.inits = (reverse <| map reverse <| tails <| reverse l)
  | [] => by simp
  | a :: l => by simp [inits_eq_tails l, map_inj_left, ← map_reverse]

Prefixes as Reversed Suffixes of Reversed List

Informal description

For any list $l$ of elements of type $\alpha$, the list of prefixes of $l$ is equal to the reverse of the list obtained by reversing each suffix of the reverse of $l$. In symbols: $$ \text{inits}(l) = \text{reverse} \left( \text{map}\ \text{reverse} \left( \text{tails} \left( \text{reverse}(l) \right) \right) \right) $$

List.tails_eq_inits theorem

: ∀ l : List α, l.tails = (reverse <| map reverse <| inits <| reverse l)

Full source

theorem tails_eq_inits : ∀ l : List α, l.tails = (reverse <| map reverse <| inits <| reverse l)
  | [] => by simp
  | a :: l => by simp [tails_eq_inits l, append_left_inj]

Suffixes as Reversed Prefixes of Reversed List

Informal description

For any list $l$ of elements of type $\alpha$, the list of suffixes of $l$ is equal to the reverse of the list obtained by mapping the reverse operation over the list of prefixes of the reverse of $l$. In symbols: $$ \text{tails}(l) = \text{reverse} \left( \text{map} \ \text{reverse} \left( \text{inits}(\text{reverse}(l)) \right) \right) $$

List.inits_reverse theorem

(l : List α) : inits (reverse l) = reverse (map reverse l.tails)

Full source

theorem inits_reverse (l : List α) : inits (reverse l) = reverse (map reverse l.tails) := by
  rw [tails_eq_inits l]
  simp [reverse_involutive.comp_self, ← map_reverse]

Prefixes of Reversed List as Reversed Reversed Suffixes

Informal description

For any list $l$ of elements of type $\alpha$, the list of prefixes of the reverse of $l$ is equal to the reverse of the list obtained by mapping the reverse operation over the list of suffixes of $l$. In symbols: $$ \text{inits}(\text{reverse}(l)) = \text{reverse}(\text{map reverse } (\text{tails } l)) $$

List.tails_reverse theorem

(l : List α) : tails (reverse l) = reverse (map reverse l.inits)

Full source

theorem tails_reverse (l : List α) : tails (reverse l) = reverse (map reverse l.inits) := by
  rw [inits_eq_tails l]
  simp [reverse_involutive.comp_self, ← map_reverse]

Suffixes of Reversed List as Reversed Reversed Prefixes

Informal description

For any list $l$ of elements of type $\alpha$, the list of suffixes of the reverse of $l$ is equal to the reverse of the list obtained by mapping the reverse operation over the list of prefixes of $l$. In symbols: $$ \text{tails}(\text{reverse}(l)) = \text{reverse}(\text{map reverse } (\text{inits } l)) $$

List.map_reverse_inits theorem

(l : List α) : map reverse l.inits = (reverse <| tails <| reverse l)

Full source

theorem map_reverse_inits (l : List α) : map reverse l.inits = (reverse <| tails <| reverse l) := by
  rw [inits_eq_tails l]
  simp [reverse_involutive.comp_self, ← map_reverse]

Reversed Prefixes as Reversed Suffixes of Reversed List

Informal description

For any list $l$ of elements of type $\alpha$, the list obtained by reversing each prefix in $\text{inits}(l)$ is equal to the reverse of the list of suffixes of the reverse of $l$. In symbols: $$ \text{map reverse (inits } l) = \text{reverse (tails (reverse } l)) $$

List.map_reverse_tails theorem

(l : List α) : map reverse l.tails = (reverse <| inits <| reverse l)

Full source

theorem map_reverse_tails (l : List α) : map reverse l.tails = (reverse <| inits <| reverse l) := by
  rw [tails_eq_inits l]
  simp [reverse_involutive.comp_self, ← map_reverse]

Reversed Suffixes as Reversed Prefixes of Reversed List

Informal description

For any list $l$ of elements of type $\alpha$, the list obtained by reversing each suffix in $\text{tails}(l)$ is equal to the reverse of the list of prefixes of the reverse of $l$. In symbols: $$ \text{map reverse (tails } l) = \text{reverse (inits (reverse } l)) $$

List.length_tails theorem

(l : List α) : length (tails l) = length l + 1

Full source

@[simp]
theorem length_tails (l : List α) : length (tails l) = length l + 1 := by
  induction' l with x l IH
  · simp
  · simpa using IH

Length of Suffixes List: $|\text{tails}(l)| = |l| + 1$

Informal description

For any list $l$ of type $\alpha$, the length of the list of suffixes `tails l` is equal to the length of $l$ plus one, i.e., $|\text{tails}(l)| = |l| + 1$.

List.length_inits theorem

(l : List α) : length (inits l) = length l + 1

Full source

@[simp]
theorem length_inits (l : List α) : length (inits l) = length l + 1 := by simp [inits_eq_tails]

Length of Prefixes List: $|\text{inits}(l)| = |l| + 1$

Informal description

For any list $l$ of elements of type $\alpha$, the length of the list of prefixes of $l$ is equal to the length of $l$ plus one, i.e., $|\text{inits}(l)| = |l| + 1$.

List.getElem_tails theorem

(l : List α) (n : Nat) (h : n < (tails l).length) : (tails l)[n] = l.drop n

Full source

@[simp]
theorem getElem_tails (l : List α) (n : Nat) (h : n < (tails l).length) :
    (tails l)[n] = l.drop n := by
  induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]

Accessing the $n$-th suffix of a list via `drop`

Informal description

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

List.get_tails theorem

(l : List α) (n : Fin (length (tails l))) : (tails l).get n = l.drop n

Full source

theorem get_tails (l : List α) (n : Fin (length (tails l))) : (tails l).get n = l.drop n := by
  simp

Suffix Access via Drop Operation

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$ (represented as a `Fin` type ensuring $n$ is less than the length of the list of suffixes of $l$), the $n$-th element of the list of suffixes of $l$ is equal to the list obtained by dropping the first $n$ elements from $l$.

List.getElem_inits theorem

(l : List α) (n : Nat) (h : n < length (inits l)) : (inits l)[n] = l.take n

Full source

@[simp]
theorem getElem_inits (l : List α) (n : Nat) (h : n < length (inits l)) :
    (inits l)[n] = l.take n := by
  induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]

$n$-th Prefix of a List is the First $n$ Elements

Informal description

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

List.get_inits theorem

(l : List α) (n : Fin (length (inits l))) : (inits l).get n = l.take n

Full source

theorem get_inits (l : List α) (n : Fin (length (inits l))) : (inits l).get n = l.take n := by
  simp

$n$-th Prefix Equals First $n$ Elements

Informal description

For any list $l$ of elements of type $\alpha$ and any natural number $n$ (represented as a finite index into the list of prefixes of $l$), the $n$-th element of the list of prefixes of $l$ is equal to the list obtained by taking the first $n$ elements of $l$.

List.map_inits theorem

{β : Type*} (g : α → β) : (l.map g).inits = l.inits.map (map g)

Full source

lemma map_inits {β : Type*} (g : α → β) : (l.map g).inits = l.inits.map (map g) := by
  induction' l using reverseRecOn <;> simp [*]

Prefixes Preserved Under List Mapping

Informal description

For any function $g : \alpha \to \beta$ and any list $l$ of elements of type $\alpha$, the list of prefixes of the mapped list $l.\text{map}(g)$ is equal to the list obtained by mapping $g$ over each prefix of $l$. In other words: $$(l.\text{map}(g)).\text{inits} = l.\text{inits}.\text{map}(\text{map}(g))$$

List.map_tails theorem

{β : Type*} (g : α → β) : (l.map g).tails = l.tails.map (map g)

Full source

lemma map_tails {β : Type*} (g : α → β) : (l.map g).tails = l.tails.map (map g) := by
  induction' l using reverseRecOn <;> simp [*]

Mapping Function Preserves List Suffixes

Informal description

For any function $g : \alpha \to \beta$ and any list $l$ of elements of type $\alpha$, the list of suffixes of the mapped list $l.\text{map}(g)$ is equal to the list obtained by applying $\text{map}(g)$ to each suffix of $l$. In symbols: $$ \text{tails}(l.\text{map}(g)) = \text{tails}(l).\text{map}(\text{map}(g)) $$

List.take_inits theorem

{n} : (l.take n).inits = l.inits.take (n + 1)

Full source

lemma take_inits {n} : (l.take n).inits = l.inits.take (n + 1) := by
  apply ext_getElem <;> (simp [take_take] <;> omega)

Prefixes of Initial Segment of List

Informal description

For any natural number $n$ and any list $l$, the list of prefixes of the first $n$ elements of $l$ is equal to the first $(n + 1)$ prefixes of $l$. That is, $$\text{inits}(l.\text{take}(n)) = \text{inits}(l).\text{take}(n + 1).$$

List.insert_eq_ite theorem

(a : α) (l : List α) : insert a l = if a ∈ l then l else a :: l

Full source

theorem insert_eq_ite (a : α) (l : List α) : insert a l = if a ∈ l then l else a :: l := by
  simp only [← elem_iff]
  rfl

Definition of List Insertion via Membership Condition

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the insertion of $a$ into $l$ is equal to $l$ if $a$ is already in $l$, and to $a$ prepended to $l$ otherwise. That is, $$\text{insert}(a, l) = \begin{cases} l & \text{if } a \in l \\ a :: l & \text{otherwise.} \end{cases}$$

List.suffix_insert theorem

(a : α) (l : List α) : l <:+ l.insert a

Full source

@[simp]
theorem suffix_insert (a : α) (l : List α) : l <:+ l.insert a := by
  by_cases h : a ∈ l
  · simp only [insert_of_mem h, insert, suffix_refl]
  · simp only [insert_of_not_mem h, suffix_cons, insert]

Insertion Preserves Suffix Property

Informal description

For any element $a$ and any list $l$, the list $l$ is a suffix of the list obtained by inserting $a$ into $l$, denoted as $l \mathbin{<:+} \operatorname{insert}(a, l)$.

List.infix_insert theorem

(a : α) (l : List α) : l <:+: l.insert a

Full source

theorem infix_insert (a : α) (l : List α) : l <:+: l.insert a :=
  (suffix_insert a l).isInfix

Insertion Preserves Infix Property

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list $l$ is an infix of the list obtained by inserting $a$ into $l$, denoted as $l \mathbin{<:+:} \operatorname{insert}(a, l)$.

List.sublist_insert theorem

(a : α) (l : List α) : l <+ l.insert a

Full source

theorem sublist_insert (a : α) (l : List α) : l <+ l.insert a :=
  (suffix_insert a l).sublist

Insertion Preserves Sublist Property

Informal description

For any element $a$ and any list $l$, the list $l$ is a sublist of the list obtained by inserting $a$ into $l$, denoted as $l \mathbin{<+} \operatorname{insert}(a, l)$.

List.subset_insert theorem

(a : α) (l : List α) : l ⊆ l.insert a

Full source

theorem subset_insert (a : α) (l : List α) : l ⊆ l.insert a :=
  (sublist_insert a l).subset

Insertion Preserves Subset Property

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list $l$ is a subset of the list obtained by inserting $a$ into $l$, denoted as $l \subseteq \operatorname{insert}(a, l)$.

Notation