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) [DecidableRel R] {a : α} : List.destutter' R a [] = [a]

theorem List.destutter'_cons {α : Type u_1} (l : List α) (R : α → α → Prop) [DecidableRel R] {a : α} {b : α} : List.destutter' R a (b :: l) = if R a b then a :: List.destutter' R b l else List.destutter' R a l

@[simp]

theorem List.destutter'_cons_pos {α : Type u_1} (l : List α) {R : α → α → Prop} [DecidableRel R] {a : α} {b : α} (h : R b a) : List.destutter' R b (a :: l) = b :: List.destutter' R a l

@[simp]

theorem List.destutter'_cons_neg {α : Type u_1} (l : List α) {R : α → α → Prop} [DecidableRel R] {a : α} {b : α} (h : ¬R b a) : List.destutter' R b (a :: l) = List.destutter' R b l

@[simp]

theorem List.destutter'_singleton {α : Type u_1} (R : α → α → Prop) [DecidableRel R] {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) [DecidableRel R] (a : α) : List.Sublist (List.destutter' R a l) (a :: l)

theorem List.mem_destutter' {α : Type u_1} (l : List α) (R : α → α → Prop) [DecidableRel R] (a : α) : a ∈ List.destutter' R a l

theorem List.destutter'_is_chain {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (l : List α) {a : α} {b : α} : R a b → List.Chain R a (List.destutter' R b l)

theorem List.destutter'_is_chain' {α : Type u_1} (l : List α) (R : α → α → Prop) [DecidableRel R] (a : α) : List.Chain' R (List.destutter' R a l)

theorem List.destutter'_of_chain {α : Type u_1} (l : List α) (R : α → α → Prop) [DecidableRel R] {a : α} (h : List.Chain R a l) : List.destutter' R a l = a :: l

@[simp]

theorem List.destutter'_eq_self_iff {α : Type u_1} (l : List α) (R : α → α → Prop) [DecidableRel R] (a : α) : List.destutter' R a l = a :: l ↔ List.Chain R a l

theorem List.destutter'_ne_nil {α : Type u_1} (l : List α) (R : α → α → Prop) [DecidableRel R] {a : α} : List.destutter' R a l ≠ []

@[simp]

theorem List.destutter_nil {α : Type u_1} (R : α → α → Prop) [DecidableRel R] : List.destutter R [] = []

theorem List.destutter_cons' {α : Type u_1} (l : List α) (R : α → α → Prop) [DecidableRel R] {a : α} : List.destutter R (a :: l) = List.destutter' R a l

theorem List.destutter_cons_cons {α : Type u_1} (l : List α) (R : α → α → Prop) [DecidableRel R] {a : α} {b : α} : List.destutter R (a :: b :: l) = if R a b then a :: List.destutter' R b l else List.destutter' R a l

@[simp]

theorem List.destutter_singleton {α : Type u_1} (R : α → α → Prop) [DecidableRel R] {a : α} : List.destutter R [a] = [a]

@[simp]

theorem List.destutter_pair {α : Type u_1} (R : α → α → Prop) [DecidableRel R] {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) [DecidableRel R] (l : List α) : List.Sublist (List.destutter R l) l

theorem List.destutter_is_chain' {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (l : List α) : List.Chain' R (List.destutter R l)

theorem List.destutter_of_chain' {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (l : List α) : List.Chain' R l → List.destutter R l = l

@[simp]

theorem List.destutter_eq_self_iff {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (l : List α) : List.destutter R l = l ↔ List.Chain' R l

theorem List.destutter_idem {α : Type u_1} (l : List α) (R : α → α → Prop) [DecidableRel R] : List.destutter R (List.destutter R l) = List.destutter R l

@[simp]

theorem List.destutter_eq_nil {α : Type u_1} (R : α → α → Prop) [DecidableRel R] {l : List α} : List.destutter R l = [] ↔ l = []