Prefixes, suffixes, infixes

This file proves properties about

• List.isPrefix: l₁ is a prefix of l₂ if l₂ starts with l₁.
• List.isSuffix: l₁ is a suffix of l₂ if l₂ ends with l₁.
• List.isInfix: l₁ is an infix of l₂ if l₁ is a prefix of some suffix of l₂.
• List.inits: The list of prefixes of a list.
• List.tails: The list of prefixes of a list.
• insert on lists

All those (except insert) are defined in Mathlib/Data/List/Defs.lean.

Notation

• l₁ <+: l₂: l₁ is a prefix of l₂.
• l₁ <:+ l₂: l₁ is a suffix of l₂.
• l₁ <:+: l₂: l₁ is an infix of l₂.

prefix, suffix, infix

theorem List.IsPrefix.take {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <+: l₂) (n : ℕ) : List.take n l₁ <+: List.take n l₂

theorem List.IsPrefix.drop {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <+: l₂) (n : ℕ) : List.drop n l₁ <+: List.drop n l₂

theorem List.isPrefix_append_of_length {α : Type u_1} {l₁ l₂ l₃ : List α} (h : l₁.length ≤ l₂.length) : l₁ <+: l₂ ++ l₃ ↔ l₁ <+: l₂

@[simp]

theorem List.take_isPrefix_take {α : Type u_1} {l : List α} {m n : ℕ} : take m l <+: take n l ↔ m ≤ n ∨ l.length ≤ n

theorem List.IsPrefix.flatten {α : Type u_1} {l₁ l₂ : List (List α)} (h : l₁ <+: l₂) : l₁.flatten <+: l₂.flatten

theorem List.IsPrefix.flatMap {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (h : l₁ <+: l₂) (f : α → List β) : flatMap f l₁ <+: flatMap f l₂

theorem List.IsSuffix.flatten {α : Type u_1} {l₁ l₂ : List (List α)} (h : l₁ <:+ l₂) : l₁.flatten <:+ l₂.flatten

theorem List.IsSuffix.flatMap {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (h : l₁ <:+ l₂) (f : α → List β) : flatMap f l₁ <:+ flatMap f l₂

theorem List.IsInfix.flatten {α : Type u_1} {l₁ l₂ : List (List α)} (h : l₁ <:+: l₂) : l₁.flatten <:+: l₂.flatten

theorem List.IsInfix.flatMap {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} (h : l₁ <:+: l₂) (f : α → List β) : flatMap f l₁ <:+: flatMap f l₂

theorem List.dropSlice_sublist {α : Type u_1} (n m : ℕ) (l : List α) : (dropSlice n m l).Sublist l

theorem List.dropSlice_subset {α : Type u_1} (n m : ℕ) (l : List α) : dropSlice n m l ⊆ l

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

theorem List.tail_subset {α : Type u_1} (l : List α) : l.tail ⊆ l

theorem List.mem_of_mem_dropLast {α : Type u_1} {l : List α} {a : α} (h : a ∈ l.dropLast) : a ∈ l

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

theorem List.prefix_append_drop {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₂ = l₁ ++ drop l₁.length l₂

@[implicit_reducible]

instance List.decidableInfix {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <:+: l₂)

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

theorem List.singleton_infix_iff {α : Type u_1} (x : α) (xs : List α) : [x] <:+: xs ↔ x ∈ xs

@[simp]

theorem List.singleton_infix_singleton_iff {α : Type u_1} {x y : α} : [x] <:+: [y] ↔ x = y

theorem List.infix_singleton_iff {α : Type u_1} (xs : List α) (x : α) : xs <:+: [x] ↔ xs = [] ∨ xs = [x]

theorem List.infix_antisymm {α : Type u_1} {l₁ l₂ : List α} (h₁ : l₁ <:+: l₂) (h₂ : l₂ <:+: l₁) : l₁ = l₂

theorem List.IsPrefix.nodup {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <+: l₂) (hn : l₂.Nodup) : l₁.Nodup

theorem List.IsInfix.nodup {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <:+: l₂) (hn : l₂.Nodup) : l₁.Nodup

theorem List.IsSuffix.nodup {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <:+ l₂) (hn : l₂.Nodup) : l₁.Nodup

instance List.instIsPartialOrderIsPrefix {α : Type u_1} : IsPartialOrder (List α) fun (x1 x2 : List α) => x1 <+: x2

instance List.instIsPartialOrderIsSuffix {α : Type u_1} : IsPartialOrder (List α) fun (x1 x2 : List α) => x1 <:+ x2

instance List.instIsPartialOrderIsInfix {α : Type u_1} : IsPartialOrder (List α) fun (x1 x2 : List α) => x1 <:+: x2

@[simp]

theorem List.mem_inits {α : Type u_1} (s t : List α) : s ∈ t.inits ↔ s <+: t

@[simp]

theorem List.mem_tails {α : Type u_1} (s t : List α) : s ∈ t.tails ↔ s <:+ t

theorem List.inits_cons {α : Type u_1} (a : α) (l : List α) : (a :: l).inits = [] :: map (fun (t : List α) => a :: t) l.inits

theorem List.tails_cons {α : Type u_1} (a : α) (l : List α) : (a :: l).tails = (a :: l) :: l.tails

@[simp]

theorem List.inits_append {α : Type u_1} (s t : List α) : (s ++ t).inits = s.inits ++ map (fun (l : List α) => s ++ l) t.inits.tail

@[simp]

theorem List.tails_append {α : Type u_1} (s t : List α) : (s ++ t).tails = map (fun (l : List α) => l ++ t) s.tails ++ t.tails.tail

theorem List.inits_eq_tails {α : Type u_1} (l : List α) : l.inits = (map reverse l.reverse.tails).reverse

theorem List.tails_eq_inits {α : Type u_1} (l : List α) : l.tails = (map reverse l.reverse.inits).reverse

theorem List.inits_reverse {α : Type u_1} (l : List α) : l.reverse.inits = (map reverse l.tails).reverse

theorem List.tails_reverse {α : Type u_1} (l : List α) : l.reverse.tails = (map reverse l.inits).reverse

theorem List.map_reverse_inits {α : Type u_1} (l : List α) : map reverse l.inits = l.reverse.tails.reverse

theorem List.map_reverse_tails {α : Type u_1} (l : List α) : map reverse l.tails = l.reverse.inits.reverse

@[simp]

theorem List.length_tails {α : Type u_1} (l : List α) : l.tails.length = l.length + 1

@[simp]

theorem List.length_inits {α : Type u_1} (l : List α) : l.inits.length = l.length + 1

@[simp]

theorem List.getElem_tails {α : Type u_1} (l : List α) (n : ℕ) (h : n < l.tails.length) : l.tails[n] = drop n l

theorem List.get_tails {α : Type u_1} (l : List α) (n : Fin l.tails.length) : l.tails.get n = drop (↑n) l

@[simp]

theorem List.getElem_inits {α : Type u_1} (l : List α) (n : ℕ) (h : n < l.inits.length) : l.inits[n] = take n l

theorem List.get_inits {α : Type u_1} (l : List α) (n : Fin l.inits.length) : l.inits.get n = take (↑n) l

theorem List.map_inits {α : Type u_1} {l : List α} {β : Type u_3} (g : α → β) : (map g l).inits = map (map g) l.inits

theorem List.map_tails {α : Type u_1} {l : List α} {β : Type u_3} (g : α → β) : (map g l).tails = map (map g) l.tails

theorem List.take_inits {α : Type u_1} {l : List α} {n : ℕ} : (take n l).inits = take (n + 1) l.inits

insert

theorem List.insert_eq_ite {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : insert a l = if a ∈ l then l else a :: l

@[simp]

theorem List.suffix_insert {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : l <:+ List.insert a l

theorem List.infix_insert {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : l <:+: List.insert a l

theorem List.sublist_insert {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : l.Sublist (List.insert a l)

theorem List.subset_insert {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : l ⊆ List.insert a l