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 #

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) :
@[simp]
theorem List.destutter'_cons_neg {α : Type u_1} (l : List α) {R : ααProp} [DecidableRel R] {a : α} {b : α} (h : ¬R b a) :
@[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.destutter' R a l).Sublist (a :: l)
theorem List.mem_destutter' {α : Type u_1} (l : List α) (R : ααProp) [DecidableRel R] (a : α) :
theorem List.destutter'_is_chain {α : Type u_1} (R : ααProp) [DecidableRel R] (l : List α) {a : α} {b : α} :
R a bList.Chain R a (List.destutter' R b l)
theorem List.destutter'_is_chain' {α : Type u_1} (l : List α) (R : ααProp) [DecidableRel R] (a : α) :
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 : α) :
theorem List.destutter'_ne_nil {α : Type u_1} (l : List α) (R : ααProp) [DecidableRel R] {a : α} :
@[simp]
theorem List.destutter_nil {α : Type u_1} (R : ααProp) [DecidableRel R] :
theorem List.destutter_cons' {α : Type u_1} (l : List α) (R : ααProp) [DecidableRel R] {a : α} :
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.destutter R l).Sublist l
theorem List.destutter_is_chain' {α : Type u_1} (R : ααProp) [DecidableRel R] (l : List α) :
theorem List.destutter_of_chain' {α : Type u_1} (R : ααProp) [DecidableRel R] (l : List α) :
@[simp]
theorem List.destutter_eq_self_iff {α : Type u_1} (R : ααProp) [DecidableRel R] (l : List α) :
theorem List.destutter_idem {α : Type u_1} (l : List α) (R : ααProp) [DecidableRel R] :
@[simp]
theorem List.destutter_eq_nil {α : Type u_1} (R : ααProp) [DecidableRel R] {l : List α} :
List.destutter R l = [] l = []