Documentation

Mathlib.Data.List.Infix

Prefixes, suffixes, infixes #

This file proves properties about

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

Notation #

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 <+: l.concat a
theorem List.prefix_concat_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} :
l₁ <+: l₂ ++ [a] l₁ = l₂ ++ [a] l₁ <+: l₂
theorem List.isSuffix.reverse :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂l₁.reverse <+: l₂.reverse

Alias of the reverse direction of List.reverse_prefix.

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

Alias of the reverse direction of List.reverse_suffix.

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

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₂) :
l₁.length = l₂.lengthl₁ = l₂
theorem List.eq_of_prefix_of_length_eq {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ <+: l₂) :
l₁.length = l₂.lengthl₁ = l₂
theorem List.eq_of_suffix_of_length_eq {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ <:+ l₂) :
l₁.length = l₂.lengthl₁ = l₂
theorem List.dropSlice_sublist {α : Type u_1} (n : ) (m : ) (l : List α) :
(List.dropSlice n m l).Sublist l
theorem List.dropSlice_subset {α : Type u_1} (n : ) (m : ) (l : List α) :
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) :
theorem List.dropWhile_suffix {α : Type u_1} {l : List α} (p : αBool) :
theorem List.dropLast_prefix {α : Type u_1} (l : List α) :
l.dropLast <+: l
theorem List.tail_suffix {α : Type u_1} (l : List α) :
l.tail <:+ l
theorem List.dropLast_sublist {α : Type u_1} (l : List α) :
l.dropLast.Sublist l
theorem List.drop_sublist_drop_left {α : Type u_1} (l : List α) {m : } {n : } (h : m n) :
(List.drop n l).Sublist (List.drop m l)
theorem List.dropLast_subset {α : Type u_1} (l : List α) :
l.dropLast 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.mem_of_mem_tail {α : Type u_1} {l : List α} {a : α} (h : a l.tail) :
a l
theorem List.Sublist.drop {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁.Sublist l₂∀ (n : ), (List.drop n l₁).Sublist (List.drop n l₂)
theorem List.prefix_iff_eq_append {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <+: l₂ l₁ ++ List.drop l₁.length l₂ = l₂
theorem List.suffix_iff_eq_append {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <:+ l₂ List.take (l₂.length - l₁.length) l₂ ++ l₁ = l₂
theorem List.prefix_iff_eq_take {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <+: l₂ l₁ = List.take l₁.length l₂
theorem List.prefix_take_iff {α : Type u_1} {x : List α} {y : List α} {n : } :
x <+: List.take n y x <+: y x.length n
theorem List.concat_get_prefix {α : Type u_1} {x : List α} {y : List α} (h : x <+: y) (hl : x.length < y.length) :
x ++ [y.get x.length, hl] <+: y
theorem List.suffix_iff_eq_drop {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ <:+ l₂ l₁ = List.drop (l₂.length - l₁.length) l₂
instance List.decidablePrefix {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
Decidable (l₁ <+: l₂)
Equations
instance List.decidableSuffix {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
Decidable (l₁ <:+ l₂)
Equations
instance List.decidableInfix {α : Type u_1} [DecidableEq α] (l₁ : List α) (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₁ : 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.filterMap {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (h : l₁ <+: l₂) (f : αOption β) :
@[deprecated List.IsPrefix.filterMap]
theorem List.IsPrefix.filter_map {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (h : l₁ <+: l₂) (f : αOption β) :

Alias of List.IsPrefix.filterMap.

theorem List.IsPrefix.reduceOption {α : Type u_1} {l₁ : List (Option α)} {l₂ : List (Option α)} (h : l₁ <+: l₂) :
l₁.reduceOption <+: l₂.reduceOption
instance List.instIsPartialOrderIsPrefix {α : Type u_1} :
IsPartialOrder (List α) fun (x x_1 : List α) => x <+: x_1
Equations
  • =
instance List.instIsPartialOrderIsSuffix {α : Type u_1} :
IsPartialOrder (List α) fun (x x_1 : List α) => x <:+ x_1
Equations
  • =
instance List.instIsPartialOrderIsInfix {α : Type u_1} :
IsPartialOrder (List α) fun (x x_1 : List α) => x <:+: x_1
Equations
  • =
@[simp]
theorem List.mem_inits {α : Type u_1} (s : List α) (t : List α) :
s t.inits s <+: t
@[simp]
theorem List.mem_tails {α : Type u_1} (s : List α) (t : List α) :
s t.tails s <:+ t
theorem List.inits_cons {α : Type u_1} (a : α) (l : List α) :
(a :: l).inits = [] :: List.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 : List α) (t : List α) :
(s ++ t).inits = s.inits ++ List.map (fun (l : List α) => s ++ l) t.inits.tail
@[simp]
theorem List.tails_append {α : Type u_1} (s : List α) (t : List α) :
(s ++ t).tails = List.map (fun (l : List α) => l ++ t) s.tails ++ t.tails.tail
theorem List.inits_eq_tails {α : Type u_1} (l : List α) :
l.inits = (List.map List.reverse l.reverse.tails).reverse
theorem List.tails_eq_inits {α : Type u_1} (l : List α) :
l.tails = (List.map List.reverse l.reverse.inits).reverse
theorem List.inits_reverse {α : Type u_1} (l : List α) :
l.reverse.inits = (List.map List.reverse l.tails).reverse
theorem List.tails_reverse {α : Type u_1} (l : List α) :
l.reverse.tails = (List.map List.reverse l.inits).reverse
theorem List.map_reverse_inits {α : Type u_1} (l : List α) :
List.map List.reverse l.inits = l.reverse.tails.reverse
theorem List.map_reverse_tails {α : Type u_1} (l : List α) :
List.map List.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] = List.drop n l
theorem List.get_tails {α : Type u_1} (l : List α) (n : Fin l.tails.length) :
l.tails.get n = List.drop (n) l
@[simp]
theorem List.getElem_inits {α : Type u_1} (l : List α) (n : ) (h : n < l.inits.length) :
l.inits[n] = List.take n l
theorem List.get_inits {α : Type u_1} (l : List α) (n : Fin l.inits.length) :
l.inits.get n = List.take (n) l
@[simp, deprecated List.get_tails]
theorem List.nth_le_tails {α : Type u_1} (l : List α) (n : ) (hn : n < l.tails.length) :
l.tails.nthLe n hn = List.drop n l
@[simp, deprecated List.get_inits]
theorem List.nth_le_inits {α : Type u_1} (l : List α) (n : ) (hn : n < l.inits.length) :
l.inits.nthLe n hn = List.take n l

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 α) :
theorem List.infix_insert {α : Type u_1} [DecidableEq α] (a : α) (l : List α) :
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 α) :
theorem List.mem_of_mem_suffix {α : Type u_1} {l₁ : List α} {l₂ : List α} {a : α} (hx : a l₁) (hl : l₁ <:+ l₂) :
a l₂
theorem List.IsPrefix.ne_nil {α : Type u_1} {x : List α} {y : List α} (h : x <+: y) (hx : x []) :
y []
theorem List.IsPrefix.getElem {α : Type u_1} {x : List α} {y : List α} (h : x <+: y) {n : } (hn : n < x.length) :
x[n] = y[n]
theorem List.IsPrefix.get_eq {α : Type u_1} {x : List α} {y : List α} (h : x <+: y) {n : } (hn : n < x.length) :
x.get n, hn = y.get n,
theorem List.IsPrefix.head_eq {α : Type u_1} {x : List α} {y : List α} (h : x <+: y) (hx : x []) :
x.head hx = y.head