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.

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.prefix_rfl {α : Type u_1} {l : List α} : l <+: l

theorem List.suffix_rfl {α : Type u_1} {l : List α} : l <:+ l

theorem List.infix_rfl {α : Type u_1} {l : List α} : l <:+: l

theorem List.prefix_concat {α : Type u_1} (a : α) (l : List α) : l <+: List.concat l a

theorem List.isSuffix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → List.reverse l₁ <+: List.reverse l₂

Alias of the reverse direction of List.reverse_prefix.

theorem List.isPrefix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → List.reverse l₁ <:+ List.reverse l₂

Alias of the reverse direction of List.reverse_suffix.

theorem List.isInfix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → List.reverse l₁ <:+: List.reverse l₂

Alias of the reverse direction of List.reverse_infix.

theorem List.eq_nil_of_infix_nil : ∀ {α : Type u_1} {l : List α}, l <:+: [] → l = []

Alias of the forward direction of List.infix_nil.

theorem List.eq_nil_of_prefix_nil : ∀ {α : Type u_1} {l : List α}, l <+: [] → l = []

Alias of the forward direction of List.prefix_nil.

theorem List.eq_nil_of_suffix_nil : ∀ {α : Type u_1} {l : List α}, l <:+ [] → l = []

Alias of the forward direction of List.suffix_nil.

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

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

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

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

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

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

theorem List.takeWhile_prefix {α : Type u_1} {l : List α} (p : α → Bool) : List.takeWhile p l <+: l

theorem List.dropWhile_suffix {α : Type u_1} {l : List α} (p : α → Bool) : List.dropWhile p l <:+ l

theorem List.dropLast_prefix {α : Type u_1} (l : List α) : List.dropLast l <+: l

theorem List.tail_suffix {α : Type u_1} (l : List α) : List.tail l <:+ l

theorem List.dropLast_sublist {α : Type u_1} (l : List α) : List.Sublist (List.dropLast l) l

theorem List.tail_sublist {α : Type u_1} (l : List α) : List.Sublist (List.tail l) l

theorem List.dropLast_subset {α : Type u_1} (l : List α) : List.dropLast l ⊆ l

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

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

theorem List.mem_of_mem_tail {α : Type u_1} {l : List α} {a : α} (h : a ∈ List.tail l) : a ∈ l

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

theorem List.suffix_iff_eq_append {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁ <:+ l₂ ↔ List.take (List.length l₂ - List.length l₁) l₂ ++ l₁ = l₂

theorem List.prefix_iff_eq_take {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁ <+: l₂ ↔ l₁ = List.take (List.length l₁) l₂

theorem List.suffix_iff_eq_drop {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁ <:+ l₂ ↔ l₁ = List.drop (List.length l₂ - List.length l₁) l₂

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

Equations

• List.decidablePrefix [] x = isTrue (_ : ∃ (t : List α), [] ++ t = x)
• List.decidablePrefix (a :: l₁) [] = isFalse (_ : a :: l₁ <+: [] → False)
• List.decidablePrefix (a :: l₁) (b :: l₂) = if h : a = b then decidable_of_decidable_of_iff (_ : l₁ <+: l₂ ↔ a :: l₁ <+: b :: l₂) else isFalse (_ : a :: l₁ <+: b :: l₂ → False)

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

Equations

• List.decidableSuffix [] x = isTrue (_ : ∃ (t : List α), t ++ [] = x)
• List.decidableSuffix (a :: l₁) [] = isFalse (_ : ¬a :: l₁ <:+ [])
• List.decidableSuffix x (b :: l₂) = decidable_of_decidable_of_iff (_ : x = b :: l₂ ∨ x <:+ l₂ ↔ x <:+ b :: l₂)

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

Equations

• List.decidableInfix [] x = isTrue (_ : ∃ (s : List α), ∃ (t : List α), s ++ [] ++ t = x)
• List.decidableInfix (a :: l₁) [] = isFalse (_ : a :: l₁ <:+: [] → False)
• List.decidableInfix x (b :: l₂) = decidable_of_decidable_of_iff (_ : x <+: b :: l₂ ∨ x <:+: l₂ ↔ x <:+: b :: l₂)

theorem List.prefix_take_le_iff {α : Type u_1} {m : ℕ} {n : ℕ} {L : List (List (Option α))} (hm : m < List.length L) : List.take m L <+: List.take n L ↔ m ≤ n

theorem List.cons_prefix_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} {b : α} : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂

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

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

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

instance List.instIsPartialOrderListIsPrefix {α : Type u_1} : IsPartialOrder (List α) fun (x x_1 : List α) => x <+: x_1

Equations

• (_ : IsPartialOrder (List α) fun (x x_1 : List α) => x <+: x_1) = (_ : IsPartialOrder (List α) fun (x x_1 : List α) => x <+: x_1)

instance List.instIsPartialOrderListIsSuffix {α : Type u_1} : IsPartialOrder (List α) fun (x x_1 : List α) => x <:+ x_1

Equations

• (_ : IsPartialOrder (List α) fun (x x_1 : List α) => x <:+ x_1) = (_ : IsPartialOrder (List α) fun (x x_1 : List α) => x <:+ x_1)

instance List.instIsPartialOrderListIsInfix {α : Type u_1} : IsPartialOrder (List α) fun (x x_1 : List α) => x <:+: x_1

Equations

• (_ : IsPartialOrder (List α) fun (x x_1 : List α) => x <:+: x_1) = (_ : IsPartialOrder (List α) fun (x x_1 : List α) => x <:+: x_1)

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem List.nth_le_tails {α : Type u_1} (l : List α) (n : ℕ) (hn : n < List.length (List.tails l)) : List.nthLe (List.tails l) n hn = List.drop n l

@[simp]

theorem List.nth_le_inits {α : Type u_1} (l : List α) (n : ℕ) (hn : n < List.length (List.inits l)) : List.nthLe (List.inits l) n hn = List.take n l

insert

@[simp]

theorem List.insert_nil {α : Type u_1} [DecidableEq α] (a : α) : insert a [] = [a]

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 α) : List.Sublist l (List.insert a l)

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

theorem List.mem_of_mem_suffix {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} (hx : a ∈ l₁) (hl : l₁ <:+ l₂) : a ∈ l₂