mathlib3 documentation

data.list.destutter

Destuttering of Lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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