Init.Data.List.Nat.Sublist

List.IsSuffix.getElem theorem

 {xs ys : List α} (h : xs <:+ ys) {i} (hn : i < xs.length) :
  xs[i] = ys[ys.length - xs.length + i]'(by have := h.length_le; omega)

Full source

theorem IsSuffix.getElem {xs ys : List α} (h : xs <:+ ys) {i} (hn : i < xs.length) :
    xs[i] = ys[ys.length - xs.length + i]'(by have := h.length_le; omega) := by
  rw [getElem_eq_getElem_reverse, h.reverse.getElem, getElem_reverse]
  congr
  have := h.length_le
  omega

Suffix Lists Have Equal Elements at Corresponding Indices: $xs[i] = ys[|ys| - |xs| + i]$

Informal description

For any two lists $xs$ and $ys$ of elements of type $\alpha$, if $xs$ is a suffix of $ys$ (denoted $xs <:+ ys$), then for any index $i$ such that $i < \text{length}(xs)$, the element at position $i$ in $xs$ is equal to the element at position $\text{length}(ys) - \text{length}(xs) + i$ in $ys$, i.e., $$xs[i] = ys[|ys| - |xs| + i]$$ where $|xs|$ and $|ys|$ denote the lengths of $xs$ and $ys$ respectively.

List.isSuffix_iff theorem

 : l₁ <:+ l₂ ↔ l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]

Full source

theorem isSuffix_iff : l₁ <:+ l₂l₁ <:+ l₂ ↔
    l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i] := by
  suffices l₁.length ≤ l₂.length ∧ l₁ <:+ l₂l₁.length ≤ l₂.length ∧ l₁ <:+ l₂ ↔
      l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i] by
    constructor
    · intro h
      exact this.mp ⟨h.length_le, h⟩
    · intro h
      exact (this.mpr h).2
  simp only [and_congr_right_iff]
  intro le
  rw [← reverse_prefix, isPrefix_iff]
  simp only [length_reverse]
  constructor
  · intro w i h
    specialize w (l₁.length - 1 - i) (by omega)
    rw [getElem?_reverse (by omega)] at w
    have p : l₂.length - 1 - (l₁.length - 1 - i) = i + l₂.length - l₁.length := by omega
    rw [p] at w
    rw [w, getElem_reverse]
    congr
    omega
  · intro w i h
    rw [getElem?_reverse]
    specialize w (l₁.length - 1 - i) (by omega)
    have p : l₁.length - 1 - i + l₂.length - l₁.length = l₂.length - 1 - i := by omega
    rw [p] at w
    rw [w, getElem_reverse]
    exact Nat.lt_of_lt_of_le h le

Characterization of List Suffix via Length and Element-wise Equality

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, $l_1$ is a suffix of $l_2$ if and only if: 1. The length of $l_1$ is less than or equal to the length of $l_2$, and 2. For every index $i$ with $i < \text{length}(l_1)$, the element at position $i + \text{length}(l_2) - \text{length}(l_1)$ in $l_2$ is equal to the $i$-th element of $l_1$. In other words: $$l_1 <:+ l_2 \iff |l_1| \leq |l_2| \land \forall i < |l_1|,\ l_2[i + |l_2| - |l_1|] = l_1[i]$$ where $|l|$ denotes the length of list $l$.

List.isInfix_iff theorem

 : l₁ <:+: l₂ ↔ ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + k]? = some l₁[i]

Full source

theorem isInfix_iff : l₁ <:+: l₂l₁ <:+: l₂ ↔
    ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + k]? = some l₁[i] := by
  constructor
  · intro h
    obtain ⟨t, p, s⟩ := infix_iff_suffix_prefix.mp h
    refine ⟨t.length - l₁.length, by have := p.length_le; have := s.length_le; omega, ?_⟩
    rw [isSuffix_iff] at p
    obtain ⟨p', p⟩ := p
    rw [isPrefix_iff] at s
    intro i h
    rw [s _ (by omega)]
    specialize p i (by omega)
    rw [Nat.add_sub_assoc (by omega)] at p
    rw [← getElem?_eq_getElem, p]
  · rintro ⟨k, le, w⟩
    refine ⟨l₂.take k, l₂.drop (k + l₁.length), ?_⟩
    ext1 i
    rw [getElem?_append]
    split
    · rw [getElem?_append]
      split
      · rw [getElem?_take]; simp_all; omega
      · simp_all
        have p : i = (i - k) + k := by omega
        rw [p, w _ (by omega), getElem?_eq_getElem]
        · congr 2
          omega
        · omega
    · rw [getElem?_drop]
      congr
      simp_all
      omega

Characterization of List Infix via Offset and Element-wise Equality

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the following are equivalent: 1. $l_1$ is an infix of $l_2$ (denoted $l_1 <:+: l_2$), meaning $l_1$ appears as a contiguous subsequence in $l_2$. 2. There exists a natural number $k$ such that: - The sum of the lengths of $l_1$ and $k$ is less than or equal to the length of $l_2$ (i.e., $|l_1| + k \leq |l_2|$), and - For every index $i$ with $i < |l_1|$, the element at position $i + k$ in $l_2$ is equal to the $i$-th element of $l_1$ (i.e., $l_2[i + k] = l_1[i]$).

List.suffix_iff_eq_append theorem

: l₁ <:+ l₂ ↔ take (length l₂ - length l₁) l₂ ++ l₁ = l₂

Full source

theorem suffix_iff_eq_append : l₁ <:+ l₂l₁ <:+ l₂ ↔ take (length l₂ - length l₁) l₂ ++ l₁ = l₂ :=
  ⟨by rintro ⟨r, rfl⟩; simp only [length_append, Nat.add_sub_cancel_right, take_left], fun e =>
    ⟨_, e⟩⟩

Characterization of List Suffix via Take and Append

Informal description

For two lists $l_1$ and $l_2$ of elements of type $\alpha$, the following are equivalent: 1. $l_1$ is a suffix of $l_2$ (denoted $l_1 <:+ l_2$) 2. Taking the first $|l_2| - |l_1|$ elements of $l_2$ and appending $l_1$ results in $l_2$ itself, i.e., $$\text{take}(|l_2| - |l_1|, l_2) \mathbin{+\kern-1.5ex+} l_1 = l_2$$ where $|l|$ denotes the length of list $l$.

List.prefix_take_iff theorem

{xs ys : List α} {i : Nat} : xs <+: ys.take i ↔ xs <+: ys ∧ xs.length ≤ i

Full source

theorem prefix_take_iff {xs ys : List α} {i : Nat} : xs <+: ys.take ixs <+: ys.take i ↔ xs <+: ys ∧ xs.length ≤ i := by
  constructor
  · intro h
    constructor
    · exact List.IsPrefix.trans h <| List.take_prefix i ys
    · replace h := h.length_le
      rw [length_take, Nat.le_min] at h
      exact h.left
  · intro ⟨hp, hl⟩
    have hl' := hp.length_le
    rw [List.prefix_iff_eq_take] at *
    rw [hp, List.take_take]
    simp [Nat.min_eq_left, hl, hl']

Prefix Characterization via Take Operation: $xs <+: \text{take}(i, ys) \leftrightarrow (xs <+: ys \land |xs| \leq i)$

Informal description

For any lists $xs$ and $ys$ of elements of type $\alpha$ and any natural number $i$, the following are equivalent: 1. $xs$ is a prefix of the list obtained by taking the first $i$ elements of $ys$ (i.e., $xs <+: \text{take}(i, ys)$) 2. $xs$ is a prefix of $ys$ and the length of $xs$ is less than or equal to $i$ (i.e., $xs <+: ys \land \text{length}(xs) \leq i$).

List.suffix_iff_eq_drop theorem

: l₁ <:+ l₂ ↔ l₁ = drop (length l₂ - length l₁) l₂

Full source

theorem suffix_iff_eq_drop : l₁ <:+ l₂l₁ <:+ l₂ ↔ l₁ = drop (length l₂ - length l₁) l₂ :=
  ⟨fun h => append_cancel_left <| (suffix_iff_eq_append.1 h).trans (take_append_drop _ _).symm,
    fun e => e.symm ▸ drop_suffix _ _⟩

Characterization of List Suffix via Drop Operation: $l_1 <:+ l_2 \leftrightarrow l_1 = \text{drop}(|l_2| - |l_1|, l_2)$

Informal description

For two lists $l_1$ and $l_2$ of elements of type $\alpha$, the following are equivalent: 1. $l_1$ is a suffix of $l_2$ (denoted $l_1 <:+ l_2$) 2. $l_1$ is equal to the list obtained by dropping the first $|l_2| - |l_1|$ elements of $l_2$, i.e., $$l_1 = \text{drop}(|l_2| - |l_1|, l_2)$$ where $|l|$ denotes the length of list $l$.

List.prefix_take_le_iff theorem

{xs : List α} (hm : i < xs.length) : xs.take i <+: xs.take j ↔ i ≤ j

Full source

theorem prefix_take_le_iff {xs : List α} (hm : i < xs.length) :
    xs.take i <+: xs.take jxs.take i <+: xs.take j ↔ i ≤ j := by
  simp only [prefix_iff_eq_take, length_take]
  induction i generalizing xs j with
  | zero => simp [Nat.min_eq_left, eq_self_iff_true, Nat.zero_le, take]
  | succ i IH =>
    cases xs with
    | nil => simp_all
    | cons x xs =>
      cases j with
      | zero =>
        simp
      | succ j =>
        simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at hm
        simp [← @IH j xs hm, Nat.min_eq_left, Nat.le_of_lt hm]

Prefix Relation of List Take Operations: $\text{take}(i, xs) <+: \text{take}(j, xs) \leftrightarrow i \leq j$

Informal description

For any list $xs$ and natural numbers $i$ and $j$, if $i$ is less than the length of $xs$, then the prefix obtained by taking the first $i$ elements of $xs$ is a prefix of the prefix obtained by taking the first $j$ elements of $xs$ if and only if $i \leq j$. In other words: $$\text{take}(i, xs) <+: \text{take}(j, xs) \leftrightarrow i \leq j$$

List.append_left_sublist_self theorem

{xs : List α} (ys : List α) : xs ++ ys <+ ys ↔ xs = []

Full source

@[simp] theorem append_left_sublist_self {xs : List α} (ys : List α) : xs ++ ys <+ ysxs ++ ys <+ ys ↔ xs = [] := by
  constructor
  · intro h
    replace h := h.length_le
    simp only [length_append] at h
    have : xs.length = 0 := by omega
    simp_all
  · rintro rfl
    simp

Sublist condition for left-concatenated lists: $xs \mathbin{+\kern-1.5ex+} ys <+ ys \leftrightarrow xs = []$

Informal description

For any lists $xs$ and $ys$ of elements of type $\alpha$, the concatenated list $xs \mathbin{+\kern-1.5ex+} ys$ is a sublist of $ys$ if and only if $xs$ is the empty list. In other words: $$ xs \mathbin{+\kern-1.5ex+} ys <+ ys \leftrightarrow xs = [] $$

List.append_right_sublist_self theorem

(xs : List α) {ys : List α} : xs ++ ys <+ xs ↔ ys = []

Full source

@[simp] theorem append_right_sublist_self (xs : List α) {ys : List α} : xs ++ ys <+ xsxs ++ ys <+ xs ↔ ys = [] := by
  constructor
  · intro h
    replace h := h.length_le
    simp only [length_append] at h
    have : ys.length = 0 := by omega
    simp_all
  · rintro rfl
    simp

Concatenated List is Sublist of Left Component if and only if Right Component is Empty

Informal description

For any lists $xs$ and $ys$ of elements of type $\alpha$, the concatenation $xs \mathbin{+\kern-1.5ex+} ys$ is a sublist of $xs$ if and only if $ys$ is the empty list. In other words: $$ xs \mathbin{+\kern-1.5ex+} ys <+ xs \leftrightarrow ys = [] $$

List.append_sublist_of_sublist_left theorem

{xs ys zs : List α} (h : zs <+ xs) : xs ++ ys <+ zs ↔ ys = [] ∧ xs = zs

Full source

theorem append_sublist_of_sublist_left {xs ys zs : List α} (h : zs <+ xs) :
    xs ++ ys <+ zsxs ++ ys <+ zs ↔ ys = [] ∧ xs = zs := by
  constructor
  · intro h'
    have hl := h.length_le
    have hl' := h'.length_le
    simp only [length_append] at hl'
    have : ys.length = 0 := by omega
    simp_all only [Nat.add_zero, length_eq_zero_iff, true_and, append_nil]
    exact Sublist.eq_of_length_le h' hl
  · rintro ⟨rfl, rfl⟩
    simp

Sublist Condition for Left Concatenation: $xs \mathbin{+\kern-1.5ex+} ys <+ zs \leftrightarrow ys = [] \land xs = zs$

Informal description

For any lists $xs, ys, zs$ of elements of type $\alpha$, if $zs$ is a sublist of $xs$ (denoted $zs <+ xs$), then the concatenation $xs \mathbin{+\kern-1.5ex+} ys$ is a sublist of $zs$ if and only if $ys$ is the empty list and $xs$ is equal to $zs$. In other words: $$ xs \mathbin{+\kern-1.5ex+} ys <+ zs \leftrightarrow ys = [] \land xs = zs. $$

List.append_sublist_of_sublist_right theorem

{xs ys zs : List α} (h : zs <+ ys) : xs ++ ys <+ zs ↔ xs = [] ∧ ys = zs

Full source

theorem append_sublist_of_sublist_right {xs ys zs : List α} (h : zs <+ ys) :
    xs ++ ys <+ zsxs ++ ys <+ zs ↔ xs = [] ∧ ys = zs := by
  constructor
  · intro h'
    have hl := h.length_le
    have hl' := h'.length_le
    simp only [length_append] at hl'
    have : xs.length = 0 := by omega
    simp_all only [Nat.zero_add, length_eq_zero_iff, true_and, append_nil]
    exact Sublist.eq_of_length_le h' hl
  · rintro ⟨rfl, rfl⟩
    simp

Sublist Condition for Concatenated Lists: $xs \mathbin{+\kern-1.5ex+} ys <+ zs \leftrightarrow xs = [] \land ys = zs$ when $zs <+ ys$

Informal description

For any lists $xs$, $ys$, and $zs$ of elements of type $\alpha$, if $zs$ is a sublist of $ys$ (denoted $zs <+ ys$), then the concatenation $xs \mathbin{+\kern-1.5ex+} ys$ is a sublist of $zs$ if and only if $xs$ is the empty list and $ys$ is equal to $zs$.