mathlibdocumentation

data.list.destutter

Destuttering of Lists #

This file proves theorems about list.destutter (in data.list.defs), which greedily removes all non-related items that are adjacent in a list, e.g. [2, 2, 3, 3, 2].destutter (≠) = [2, 3, 2]. Note that we make no guarantees of being the longest sublist with this property; e.g., [123, 1, 2, 5, 543, 1000].destutter (<) = [123, 543, 1000], but a longer ascending chain could be [1, 2, 5, 543, 1000].

Main statements #

• list.destutter_sublist: l.destutter is a sublist of l.
• list.destutter_is_chain': l.destutter satisfies chain' R.
• Analogies of these theorems for list.destutter', which is the destutter equivalent of chain.

Tags #

adjacent, chain, duplicates, remove, list, stutter, destutter

@[simp]
theorem list.destutter'_nil {α : Type u_1} (R : α → α → Prop) {a : α} :
= [a]
theorem list.destutter'_cons {α : Type u_1} (l : list α) (R : α → α → Prop) {a b : α} :
(b :: l) = ite (R a b) (a :: l) a l)
@[simp]
theorem list.destutter'_cons_pos {α : Type u_1} (l : list α) {R : α → α → Prop} {a b : α} (h : R b a) :
(a :: l) = b :: l
@[simp]
theorem list.destutter'_cons_neg {α : Type u_1} (l : list α) {R : α → α → Prop} {a b : α} (h : ¬R b a) :
(a :: l) = l
@[simp]
theorem list.destutter'_singleton {α : Type u_1} (R : α → α → Prop) {a b : α} :
[b] = ite (R a b) [a, b] [a]
theorem list.destutter'_sublist {α : Type u_1} (l : list α) (R : α → α → Prop) (a : α) :
l <+ a :: l
theorem list.mem_destutter' {α : Type u_1} (l : list α) (R : α → α → Prop) (a : α) :
a l
theorem list.destutter'_is_chain {α : Type u_1} (R : α → α → Prop) (l : list α) {a b : α} :
R a b a b l)
theorem list.destutter'_is_chain' {α : Type u_1} (l : list α) (R : α → α → Prop) (a : α) :
a l)
theorem list.destutter'_of_chain {α : Type u_1} (l : list α) (R : α → α → Prop) {a : α} (h : a l) :
l = a :: l
@[simp]
theorem list.destutter'_eq_self_iff {α : Type u_1} (l : list α) (R : α → α → Prop) (a : α) :
l = a :: l a l
theorem list.destutter'_ne_nil {α : Type u_1} (l : list α) (R : α → α → Prop) {a : α} :
@[simp]
theorem list.destutter_nil {α : Type u_1} (R : α → α → Prop)  :
theorem list.destutter_cons' {α : Type u_1} (l : list α) (R : α → α → Prop) {a : α} :
(a :: l) = l
theorem list.destutter_cons_cons {α : Type u_1} (l : list α) (R : α → α → Prop) {a b : α} :
(a :: b :: l) = ite (R a b) (a :: l) a l)
@[simp]
theorem list.destutter_singleton {α : Type u_1} (R : α → α → Prop) {a : α} :
[a] = [a]
@[simp]
theorem list.destutter_pair {α : Type u_1} (R : α → α → Prop) {a b : α} :
[a, b] = ite (R a b) [a, b] [a]
theorem list.destutter_sublist {α : Type u_1} (R : α → α → Prop) (l : list α) :
<+ l
theorem list.destutter_is_chain' {α : Type u_1} (R : α → α → Prop) (l : list α) :
l)
theorem list.destutter_of_chain' {α : Type u_1} (R : α → α → Prop) (l : list α) :
l = l
@[simp]
theorem list.destutter_eq_self_iff {α : Type u_1} (R : α → α → Prop) (l : list α) :
= l l
theorem list.destutter_idem {α : Type u_1} (l : list α) (R : α → α → Prop)  :
l) =
@[simp]
theorem list.destutter_eq_nil {α : Type u_1} (R : α → α → Prop) {l : list α} :