mathlib3 documentation

data.list.infix

Prefixes, subfixes, infixes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves properties about

All those (except insert) are defined in data.list.defs.

Notation #

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

prefix, suffix, infix #

@[simp]
theorem list.prefix_append {α : Type u_1} (l₁ l₂ : list α) :
l₁ <+: l₁ ++ l₂
@[simp]
theorem list.suffix_append {α : Type u_1} (l₁ l₂ : list α) :
l₂ <:+ l₁ ++ l₂
theorem list.infix_append {α : Type u_1} (l₁ l₂ l₃ : list α) :
l₂ <:+: l₁ ++ l₂ ++ l₃
@[simp]
theorem list.infix_append' {α : Type u_1} (l₁ l₂ l₃ : list α) :
l₂ <:+: l₁ ++ (l₂ ++ l₃)
theorem list.is_prefix.is_infix {α : Type u_1} {l₁ l₂ : list α} :
l₁ <+: l₂ l₁ <:+: l₂
theorem list.is_suffix.is_infix {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+ l₂ l₁ <:+: l₂
theorem list.nil_prefix {α : Type u_1} (l : list α) :
theorem list.nil_suffix {α : Type u_1} (l : list α) :
theorem list.nil_infix {α : Type u_1} (l : list α) :
@[refl]
theorem list.prefix_refl {α : Type u_1} (l : list α) :
l <+: l
@[refl]
theorem list.suffix_refl {α : Type u_1} (l : list α) :
l <:+ l
@[refl]
theorem list.infix_refl {α : Type u_1} (l : list α) :
l <:+: l
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
@[simp]
theorem list.suffix_cons {α : Type u_1} (a : α) (l : list α) :
l <:+ a :: l
theorem list.prefix_concat {α : Type u_1} (a : α) (l : list α) :
l <+: l.concat a
theorem list.infix_cons {α : Type u_1} {l₁ l₂ : list α} {a : α} :
l₁ <:+: l₂ l₁ <:+: a :: l₂
theorem list.infix_concat {α : Type u_1} {l₁ l₂ : list α} {a : α} :
l₁ <:+: l₂ l₁ <:+: l₂.concat a
@[trans]
theorem list.is_prefix.trans {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <+: l₂ l₂ <+: l₃ l₁ <+: l₃
@[trans]
theorem list.is_suffix.trans {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <:+ l₂ l₂ <:+ l₃ l₁ <:+ l₃
@[trans]
theorem list.is_infix.trans {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <:+: l₂ l₂ <:+: l₃ l₁ <:+: l₃
@[protected]
theorem list.is_infix.sublist {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+: l₂ l₁ <+ l₂
@[protected]
theorem list.is_infix.subset {α : Type u_1} {l₁ l₂ : list α} (hl : l₁ <:+: l₂) :
l₁ l₂
@[protected]
theorem list.is_prefix.sublist {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <+: l₂) :
l₁ <+ l₂
@[protected]
theorem list.is_prefix.subset {α : Type u_1} {l₁ l₂ : list α} (hl : l₁ <+: l₂) :
l₁ l₂
@[protected]
theorem list.is_suffix.sublist {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+ l₂) :
l₁ <+ l₂
@[protected]
theorem list.is_suffix.subset {α : Type u_1} {l₁ l₂ : list α} (hl : l₁ <:+ l₂) :
l₁ l₂
@[simp]
theorem list.reverse_suffix {α : Type u_1} {l₁ l₂ : list α} :
l₁.reverse <:+ l₂.reverse l₁ <+: l₂
@[simp]
theorem list.reverse_prefix {α : Type u_1} {l₁ l₂ : list α} :
l₁.reverse <+: l₂.reverse l₁ <:+ l₂
@[simp]
theorem list.reverse_infix {α : Type u_1} {l₁ l₂ : list α} :
l₁.reverse <:+: l₂.reverse l₁ <:+: l₂
theorem list.is_suffix.reverse {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+ l₂ l₁.reverse <+: l₂.reverse

Alias of the reverse direction of list.reverse_prefix.

theorem list.is_prefix.reverse {α : Type u_1} {l₁ l₂ : list α} :
l₁ <+: l₂ l₁.reverse <:+ l₂.reverse

Alias of the reverse direction of list.reverse_suffix.

theorem list.is_infix.reverse {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+: l₂ l₁.reverse <:+: l₂.reverse

Alias of the reverse direction of list.reverse_infix.

theorem list.is_infix.length_le {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+: l₂) :
l₁.length l₂.length
theorem list.is_prefix.length_le {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <+: l₂) :
l₁.length l₂.length
theorem list.is_suffix.length_le {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+ l₂) :
l₁.length l₂.length
theorem list.eq_nil_of_infix_nil {α : Type u_1} {l : list α} (h : l <:+: list.nil) :
@[simp]
theorem list.infix_nil_iff {α : Type u_1} {l : list α} :
@[simp]
theorem list.prefix_nil_iff {α : Type u_1} {l : list α} :
@[simp]
theorem list.suffix_nil_iff {α : Type u_1} {l : list α} :
theorem list.eq_nil_of_prefix_nil {α : Type u_1} {l : list α} :

Alias of the forward direction of list.prefix_nil_iff.

theorem list.eq_nil_of_suffix_nil {α : Type u_1} {l : list α} :

Alias of the forward direction of list.suffix_nil_iff.

theorem list.infix_iff_prefix_suffix {α : Type u_1} (l₁ l₂ : list α) :
l₁ <:+: l₂ (t : list α), l₁ <+: t t <:+ l₂
theorem list.eq_of_infix_of_length_eq {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+: l₂) :
l₁.length = l₂.length l₁ = l₂
theorem list.eq_of_prefix_of_length_eq {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <+: l₂) :
l₁.length = l₂.length l₁ = l₂
theorem list.eq_of_suffix_of_length_eq {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+ l₂) :
l₁.length = l₂.length l₁ = l₂
theorem list.prefix_of_prefix_length_le {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <+: l₃ l₂ <+: l₃ l₁.length l₂.length l₁ <+: l₂
theorem list.prefix_or_prefix_of_prefix {α : Type u_1} {l₁ l₂ l₃ : list α} (h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) :
l₁ <+: l₂ l₂ <+: l₁
theorem list.suffix_of_suffix_length_le {α : Type u_1} {l₁ l₂ l₃ : list α} (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : l₁.length l₂.length) :
l₁ <:+ l₂
theorem list.suffix_or_suffix_of_suffix {α : Type u_1} {l₁ l₂ l₃ : list α} (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) :
l₁ <:+ l₂ l₂ <:+ l₁
theorem list.suffix_cons_iff {α : Type u_1} {l₁ l₂ : list α} {a : α} :
l₁ <:+ a :: l₂ l₁ = a :: l₂ l₁ <:+ l₂
theorem list.infix_cons_iff {α : Type u_1} {l₁ l₂ : list α} {a : α} :
l₁ <:+: a :: l₂ l₁ <+: a :: l₂ l₁ <:+: l₂
theorem list.infix_of_mem_join {α : Type u_1} {l : list α} {L : list (list α)} :
l L l <:+: L.join
theorem list.prefix_append_right_inj {α : Type u_1} {l₁ l₂ : list α} (l : list α) :
l ++ l₁ <+: l ++ l₂ l₁ <+: l₂
theorem list.prefix_cons_inj {α : Type u_1} {l₁ l₂ : list α} (a : α) :
a :: l₁ <+: a :: l₂ l₁ <+: l₂
theorem list.take_prefix {α : Type u_1} (n : ) (l : list α) :
theorem list.drop_suffix {α : Type u_1} (n : ) (l : list α) :
theorem list.take_sublist {α : Type u_1} (n : ) (l : list α) :
theorem list.drop_sublist {α : Type u_1} (n : ) (l : list α) :
theorem list.take_subset {α : Type u_1} (n : ) (l : list α) :
theorem list.drop_subset {α : Type u_1} (n : ) (l : list α) :
theorem list.mem_of_mem_take {α : Type u_1} {l : list α} {a : α} {n : } (h : a list.take n l) :
a l
theorem list.mem_of_mem_drop {α : Type u_1} {l : list α} {a : α} {n : } (h : a list.drop n l) :
a l
theorem list.slice_sublist {α : Type u_1} (n m : ) (l : list α) :
list.slice n m l <+ l
theorem list.slice_subset {α : Type u_1} (n m : ) (l : list α) :
list.slice n m l l
theorem list.mem_of_mem_slice {α : Type u_1} {n m : } {l : list α} {a : α} (h : a list.slice n m l) :
a l
theorem list.take_while_prefix {α : Type u_1} {l : list α} (p : α Prop) [decidable_pred p] :
theorem list.drop_while_suffix {α : Type u_1} {l : list α} (p : α Prop) [decidable_pred p] :
theorem list.init_prefix {α : Type u_1} (l : list α) :
l.init <+: l
theorem list.tail_suffix {α : Type u_1} (l : list α) :
l.tail <:+ l
theorem list.init_sublist {α : Type u_1} (l : list α) :
l.init <+ l
theorem list.tail_sublist {α : Type u_1} (l : list α) :
l.tail <+ l
theorem list.init_subset {α : Type u_1} (l : list α) :
l.init l
theorem list.tail_subset {α : Type u_1} (l : list α) :
l.tail l
theorem list.mem_of_mem_init {α : Type u_1} {l : list α} {a : α} (h : a l.init) :
a l
theorem list.mem_of_mem_tail {α : Type u_1} {l : list α} {a : α} (h : a l.tail) :
a l
theorem list.prefix_iff_eq_append {α : Type u_1} {l₁ l₂ : list α} :
l₁ <+: l₂ l₁ ++ list.drop l₁.length l₂ = l₂
theorem list.suffix_iff_eq_append {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+ l₂ list.take (l₂.length - l₁.length) l₂ ++ l₁ = l₂
theorem list.prefix_iff_eq_take {α : Type u_1} {l₁ l₂ : list α} :
l₁ <+: l₂ l₁ = list.take l₁.length l₂
theorem list.suffix_iff_eq_drop {α : Type u_1} {l₁ l₂ : list α} :
l₁ <:+ l₂ l₁ = list.drop (l₂.length - l₁.length) l₂
@[protected, instance]
def list.decidable_prefix {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
decidable (l₁ <+: l₂)
Equations
@[protected, instance]
def list.decidable_suffix {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
decidable (l₁ <:+ l₂)
Equations
@[protected, instance]
def list.decidable_infix {α : Type u_1} [decidable_eq α] (l₁ l₂ : list α) :
decidable (l₁ <:+: l₂)
Equations
theorem list.prefix_take_le_iff {α : Type u_1} {m n : } {L : list (list (option α))} (hm : m < L.length) :
theorem list.cons_prefix_iff {α : Type u_1} {l₁ l₂ : list α} {a b : α} :
a :: l₁ <+: b :: l₂ a = b l₁ <+: l₂
theorem list.is_prefix.map {α : Type u_1} {β : Type u_2} {l₁ l₂ : list α} (h : l₁ <+: l₂) (f : α β) :
list.map f l₁ <+: list.map f l₂
theorem list.is_prefix.filter_map {α : Type u_1} {β : Type u_2} {l₁ l₂ : list α} (h : l₁ <+: l₂) (f : α option β) :
theorem list.is_prefix.reduce_option {α : Type u_1} {l₁ l₂ : list (option α)} (h : l₁ <+: l₂) :
theorem list.is_prefix.filter {α : Type u_1} (p : α Prop) [decidable_pred p] ⦃l₁ l₂ : list α⦄ (h : l₁ <+: l₂) :
theorem list.is_suffix.filter {α : Type u_1} (p : α Prop) [decidable_pred p] ⦃l₁ l₂ : list α⦄ (h : l₁ <:+ l₂) :
theorem list.is_infix.filter {α : Type u_1} (p : α Prop) [decidable_pred p] ⦃l₁ l₂ : list α⦄ (h : l₁ <:+: l₂) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[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 = list.nil :: list.map (λ (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 ++ list.map (λ (l : list α), s ++ l) t.inits.tail
@[simp]
theorem list.tails_append {α : Type u_1} (s t : list α) :
(s ++ t).tails = list.map (λ (l : list α), l ++ t) s.tails ++ t.tails.tail
@[simp]
theorem list.length_tails {α : Type u_1} (l : list α) :
@[simp]
theorem list.length_inits {α : Type u_1} (l : list α) :
@[simp]
theorem list.nth_le_tails {α : Type u_1} (l : list α) (n : ) (hn : n < l.tails.length) :
l.tails.nth_le n hn = list.drop n l
@[simp]
theorem list.nth_le_inits {α : Type u_1} (l : list α) (n : ) (hn : n < l.inits.length) :
l.inits.nth_le n hn = list.take n l

insert #

@[simp]
theorem list.insert_nil {α : Type u_1} [decidable_eq α] (a : α) :
theorem list.insert.def {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
has_insert.insert a l = ite (a l) l (a :: l)
@[simp]
theorem list.insert_of_mem {α : Type u_1} {l : list α} {a : α} [decidable_eq α] (h : a l) :
@[simp]
theorem list.insert_of_not_mem {α : Type u_1} {l : list α} {a : α} [decidable_eq α] (h : a l) :
@[simp]
theorem list.mem_insert_iff {α : Type u_1} {l : list α} {a b : α} [decidable_eq α] :
@[simp]
theorem list.suffix_insert {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
theorem list.infix_insert {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
theorem list.sublist_insert {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
theorem list.subset_insert {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
@[simp]
theorem list.mem_insert_self {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
theorem list.mem_insert_of_mem {α : Type u_1} {l : list α} {a b : α} [decidable_eq α] (h : a l) :
theorem list.eq_or_mem_of_mem_insert {α : Type u_1} {l : list α} {a b : α} [decidable_eq α] (h : a has_insert.insert b l) :
a = b a l
@[simp]
theorem list.length_insert_of_mem {α : Type u_1} {l : list α} {a : α} [decidable_eq α] (h : a l) :
@[simp]
theorem list.length_insert_of_not_mem {α : Type u_1} {l : list α} {a : α} [decidable_eq α] (h : a l) :
theorem list.mem_of_mem_suffix {α : Type u_1} {l₁ l₂ : list α} {a : α} (hx : a l₁) (hl : l₁ <:+ l₂) :
a l₂