Documentation

TauCeti.Data.List.CommonPrefix

The length of the longest common prefix of two lists #

List.commonPrefixLength l₁ l₂ is the length of the longest list that is a prefix of both l₁ and l₂. It is characterized by List.le_commonPrefixLength_iff: a number n is at most the common prefix length exactly when the first n entries of the two lists exist and agree.

Common prefix lengths satisfy the ultrametric inequality min (commonPrefixLength l₁ l₂) (commonPrefixLength l₂ l₃) ≤ commonPrefixLength l₁ l₃. For reduced words in a free group, the common prefix length is the Gromov product of word length, and this inequality is what makes word length a Lyndon length function.

source
def List.commonPrefixLength {α : Type u_1} [DecidableEq α] :
List α → List α → ℕ

The length of the longest common prefix of two lists.

Instances For
    source
    @[simp]
    theorem List.commonPrefixLength_nil_left {α : Type u_1} [DecidableEq α] (l : List α) :
    [].commonPrefixLength l = 0
    source
    @[simp]
    theorem List.commonPrefixLength_nil_right {α : Type u_1} [DecidableEq α] (l : List α) :
    l.commonPrefixLength [] = 0
    source
    @[simp]
    theorem List.commonPrefixLength_cons_cons {α : Type u_1} [DecidableEq α] (a b : α) (l₁ l₂ : List α) :
    (a :: l₁).commonPrefixLength (b :: l₂) = if a = b then l₁.commonPrefixLength l₂ + 1 else 0
    source
    theorem List.le_commonPrefixLength_iff {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} {n : ℕ} :
    n ≤ l₁.commonPrefixLength l₂ ↔ n ≤ l₁.length ∧ n ≤ l₂.length ∧ take n l₁ = take n l₂

    A number n is at most the common prefix length of two lists exactly when both lists have at least n entries and their first n entries agree.

    source
    theorem List.commonPrefixLength_comm {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
    l₁.commonPrefixLength l₂ = l₂.commonPrefixLength l₁
    source
    @[simp]
    theorem List.commonPrefixLength_self {α : Type u_1} [DecidableEq α] (l : List α) :
    l.commonPrefixLength l = l.length
    source
    theorem List.commonPrefixLength_le_length_left {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
    l₁.commonPrefixLength l₂ ≤ l₁.length
    source
    theorem List.commonPrefixLength_le_length_right {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
    l₁.commonPrefixLength l₂ ≤ l₂.length
    source
    theorem List.take_commonPrefixLength_eq {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
    take (l₁.commonPrefixLength l₂) l₁ = take (l₁.commonPrefixLength l₂) l₂

    The two lists agree up to their common prefix length.

    source
    theorem List.min_commonPrefixLength_le {α : Type u_1} [DecidableEq α] (l₁ l₂ l₃ : List α) :
    min (l₁.commonPrefixLength l₂) (l₂.commonPrefixLength l₃) ≤ l₁.commonPrefixLength l₃

    The ultrametric inequality for common prefix lengths.