Infixes of a three-part concatenation, and prefixes

An infix of u ++ m ++ v lies within u ++ m, lies within m ++ v, or contains m. So an infix no longer than m cannot contain both an element that occurs only in u and an element that occurs only in v: this is the fact about short windows that pumping arguments use, when m is a block of the pumped word that separates two others.

The longest common prefix List.commonPrefix l₁ l₂ is the greatest list that is a prefix of both, the meet of the prefix order.

Main definitions

• List.commonPrefix: the longest common prefix of two lists.

Main results

• List.IsInfix.infix_append_or_infix_append_or_infix: an infix of u ++ m ++ v is an infix of u ++ m or of m ++ v, or contains m.
• List.IsInfix.notMem_or_notMem_of_length_le: an infix of u ++ m ++ v no longer than m misses every element occurring only in u or every element occurring only in v.
• List.pairwise_inits: the prefixes inits lists ascend in the prefix order.
• List.takeWhile_bne_prefix_of_mem: what precedes the first c is a prefix of what precedes the first d, when c comes before the first d.

Implementation notes

[UPSTREAM] candidate: Mathlib/Data/List/Infix.lean, or core Init/Data/List/Sublist.lean beside List.infix_append_iff. Neither core, Batteries nor mathlib defines a longest common prefix of lists.

theorem List.IsInfix.infix_append_or_infix_append_or_infix {α : Type u_1} {l u m v : List α} (hl : l <:+: u ++ m ++ v) : l <:+: u ++ m ∨ l <:+: m ++ v ∨ m <:+: l

An infix of u ++ m ++ v is an infix of u ++ m, an infix of m ++ v, or contains m.

theorem List.IsInfix.notMem_or_notMem_of_length_le {α : Type u_1} {l u m v : List α} {x y : α} (hl : l <:+: u ++ m ++ v) (hlen : l.length ≤ m.length) (hx : ¬x ∈ m ++ v) (hy : ¬y ∈ u ++ m) : ¬x ∈ l ∨ ¬y ∈ l

An infix of u ++ m ++ v no longer than m misses an element that occurs only in u or an element that occurs only in v.

def List.commonPrefix {α : Type u_1} [DecidableEq α] : List α → List α → List α

commonPrefix l₁ l₂ is the longest common prefix of l₁ and l₂.

Equations

• (a :: as).commonPrefix (b :: bs) = if a = b then a :: as.commonPrefix bs else []
• x✝¹.commonPrefix x✝ = []

theorem List.commonPrefix_prefix_left {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : l₁.commonPrefix l₂ <+: l₁

theorem List.commonPrefix_prefix_right {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : l₁.commonPrefix l₂ <+: l₂

theorem List.prefix_commonPrefix {α : Type u_1} [DecidableEq α] {r l₁ l₂ : List α} : r <+: l₁ → r <+: l₂ → r <+: l₁.commonPrefix l₂

theorem List.takeWhile_bne_prefix_of_mem {α : Type u_1} [DecidableEq α] {c d : α} {l : List α} : c ∈ takeWhile (fun (x : α) => x != d) l → takeWhile (fun (x : α) => x != c) l <+: takeWhile (fun (x : α) => x != d) l

An element before the first d cuts off a prefix of what comes before the first d.

theorem List.pairwise_inits {α : Type u_1} (l : List α) : Pairwise (fun (x1 x2 : List α) => x1 <+: x2) l.inits

The prefixes of a list, as inits lists them, ascend in the prefix order.