mathlib documentation

data.list.infix

Prefixes, subfixes, infixes #

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 α) :
theorem list.prefix_refl {α : Type u_1} (l : list α) :
l <+: l
theorem list.suffix_refl {α : Type u_1} (l : list α) :
l <:+ l
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
theorem list.is_prefix.trans {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <+: l₂l₂ <+: l₃l₁ <+: l₃
theorem list.is_suffix.trans {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <:+ l₂l₂ <:+ l₃l₁ <:+ l₃
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_prefix.sublist {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <+: l₂) :
l₁ <+ l₂
@[protected]
theorem list.is_suffix.sublist {α : Type u_1} {l₁ l₂ : list α} (h : 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 reverse_prefix.

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

Alias of reverse_suffix.

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

Alias of 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 prefix_nil_iff.

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

Alias of 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₂.lengthl₁ = l₂
theorem list.eq_of_prefix_of_length_eq {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <+: l₂) :
l₁.length = l₂.lengthl₁ = l₂
theorem list.eq_of_suffix_of_length_eq {α : Type u_1} {l₁ l₂ : list α} (h : l₁ <:+ l₂) :
l₁.length = l₂.lengthl₁ = l₂
theorem list.prefix_of_prefix_length_le {α : Type u_1} {l₁ l₂ l₃ : list α} :
l₁ <+: l₃l₂ <+: l₃l₁.length l₂.lengthl₁ <+: 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 Ll <:+: 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.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
theorem list.inits_eq_tails {α : Type u_1} (l : list α) :
theorem list.tails_eq_inits {α : Type u_1} (l : list α) :
theorem list.inits_reverse {α : Type u_1} (l : list α) :
theorem list.tails_reverse {α : Type u_1} (l : list α) :
@[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 α) :
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) :
insert a l = l
@[simp]
theorem list.insert_of_not_mem {α : Type u_1} {l : list α} {a : α} [decidable_eq α] (h : a l) :
insert a l = a :: l
@[simp]
theorem list.mem_insert_iff {α : Type u_1} {l : list α} {a b : α} [decidable_eq α] :
a insert b l a = b a l
@[simp]
theorem list.suffix_insert {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
l <:+ insert a l
theorem list.infix_insert {α : Type u_1} [decidable_eq α] (a : α) (l : list α) :
l <:+: insert a l
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) :
a insert b l
theorem list.eq_or_mem_of_mem_insert {α : Type u_1} {l : list α} {a b : α} [decidable_eq α] (h : a 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) :
(insert a l).length = l.length + 1