# Documentation

Mathlib.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 : α} :
List.destutter' R a [] = [a]
theorem List.destutter'_cons {α : Type u_1} (l : List α) (R : ααProp) [] {a : α} {b : α} :
List.destutter' R a (b :: l) = if R a b then a :: else
@[simp]
theorem List.destutter'_cons_pos {α : Type u_1} (l : List α) {R : ααProp} [] {a : α} {b : α} (h : R b a) :
List.destutter' R b (a :: l) = b ::
@[simp]
theorem List.destutter'_cons_neg {α : Type u_1} (l : List α) {R : ααProp} [] {a : α} {b : α} (h : ¬R b a) :
List.destutter' R b (a :: l) =
@[simp]
theorem List.destutter'_singleton {α : Type u_1} (R : ααProp) [] {a : α} {b : α} :
List.destutter' R a [b] = if R a b then [a, b] else [a]
theorem List.destutter'_sublist {α : Type u_1} (l : List α) (R : ααProp) [] (a : α) :
List.Sublist () (a :: l)
theorem List.mem_destutter' {α : Type u_1} (l : List α) (R : ααProp) [] (a : α) :
a
theorem List.destutter'_is_chain {α : Type u_1} (R : ααProp) [] (l : List α) {a : α} {b : α} :
R a bList.Chain R a ()
theorem List.destutter'_is_chain' {α : Type u_1} (l : List α) (R : ααProp) [] (a : α) :
theorem List.destutter'_of_chain {α : Type u_1} (l : List α) (R : ααProp) [] {a : α} (h : List.Chain R a l) :
= a :: l
@[simp]
theorem List.destutter'_eq_self_iff {α : Type u_1} (l : List α) (R : ααProp) [] (a : α) :
= a :: l List.Chain R 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 : α} :
theorem List.destutter_cons_cons {α : Type u_1} (l : List α) (R : ααProp) [] {a : α} {b : α} :
List.destutter R (a :: b :: l) = if R a b then a :: else
@[simp]
theorem List.destutter_singleton {α : Type u_1} (R : ααProp) [] {a : α} :
List.destutter R [a] = [a]
@[simp]
theorem List.destutter_pair {α : Type u_1} (R : ααProp) [] {a : α} {b : α} :
List.destutter R [a, b] = if R a b then [a, b] else [a]
theorem List.destutter_sublist {α : Type u_1} (R : ααProp) [] (l : List α) :
theorem List.destutter_is_chain' {α : Type u_1} (R : ααProp) [] (l : List α) :
theorem List.destutter_of_chain' {α : Type u_1} (R : ααProp) [] (l : List α) :
= l
@[simp]
theorem List.destutter_eq_self_iff {α : Type u_1} (R : ααProp) [] (l : List α) :
= l
theorem List.destutter_idem {α : Type u_1} (l : List α) (R : ααProp) [] :
@[simp]
theorem List.destutter_eq_nil {α : Type u_1} (R : ααProp) [] {l : List α} :
= [] l = []