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 : α} : destutter' R a [] = [a]

theorem List.destutter'_cons {α : Type u_1} (l : List α) (R : α → α → Prop) [DecidableRel R] {a b : α} : destutter' R a (b :: l) = if R a b then a :: destutter' R b l else 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) : destutter' R b (a :: l) = b :: 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) : destutter' R b (a :: l) = destutter' R b l

@[simp]

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

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

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

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

@[irreducible]

theorem List.map_destutter {α : Type u_1} {β : Type u_2} {R : α → α → Prop} [DecidableRel R] {R₂ : β → β → Prop} [DecidableRel R₂] {f : α → β} {l : List α} : (∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → (R a b ↔ R₂ (f a) (f b))) → map f (destutter R l) = destutter R₂ (map f l)

For a relation-preserving map, destutter commutes with map.

theorem List.map_destutter_ne {α : Type u_1} {β : Type u_2} (l : List α) {f : α → β} (h : Function.Injective f) [DecidableEq α] [DecidableEq β] : map f (destutter (fun (x1 x2 : α) => x1 ≠ x2) l) = destutter (fun (x1 x2 : β) => x1 ≠ x2) (map f l)

For a injective function f, destutter' (·≠·) commutes with map f.

theorem List.length_destutter'_cotrans_ge {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {b : α} [i : IsTrans α Rᶜ] {a : α} {l : List α} : ¬R b a → (destutter' R b l).length ≤ (destutter' R a l).length

destutter' on a relation like ≠ or <, whose negation is transitive, has length monotone under a ¬R changing of the first element.

theorem List.length_destutter'_congr {α : Type u_1} (l : List α) {R : α → α → Prop} [DecidableRel R] {a b : α} [IsEquiv α Rᶜ] (hab : ¬R a b) : (destutter' R a l).length = (destutter' R b l).length

List.destutter' on a relation like ≠, whose negation is an equivalence, gives the same length if the first elements are not related.

theorem List.le_length_destutter'_cons {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {a b : α} [IsEquiv α Rᶜ] {l : List α} : (destutter' R b l).length ≤ (destutter' R a (b :: l)).length

List.destutter' on a relation like ≠, whose negation is an equivalence, has length monotonic under List.cons

theorem List.length_destutter_le_length_destutter_cons {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {a : α} [IsEquiv α Rᶜ] {l : List α} : (destutter R l).length ≤ (destutter R (a :: l)).length

List.destutter on a relation like ≠, whose negation is an equivalence, has length monotone under List.cons

theorem List.length_destutter_ne_le_length_destutter_cons {α : Type u_1} {l : List α} {a : α} [DecidableEq α] : (destutter (fun (x1 x2 : α) => x1 ≠ x2) l).length ≤ (destutter (fun (x1 x2 : α) => x1 ≠ x2) (a :: l)).length

destutter ≠ has length monotone under List.cons.

@[irreducible]

theorem List.Chain'.length_le_length_destutter {α : Type u_1} {R : α → α → Prop} [DecidableRel R] [IsEquiv α Rᶜ] {l₁ l₂ : List α} : l₁.Sublist l₂ → Chain' R l₁ → l₁.length ≤ (destutter R l₂).length

destutter of relations like ≠, whose negation is an equivalence relation, gives a list of maximal length over any chain.

In other words, l.destutter R is an R-chain sublist of l, and is at least as long as any other R-chain sublist.

theorem List.Chain'.length_le_length_destutter_ne {α : Type u_1} {l₁ l₂ : List α} [DecidableEq α] (hl : l₁.Sublist l₂) (hl₁ : Chain' (fun (x1 x2 : α) => x1 ≠ x2) l₁) : l₁.length ≤ (destutter (fun (x1 x2 : α) => x1 ≠ x2) l₂).length

destutter of ≠ gives a list of maximal length over any chain.

In other words, l.destutter (· ≠ ·) is a ≠-chain sublist of l, and is at least as long as any other ≠-chain sublist.