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 #
list.destutter_sublist:l.destutteris a sublist ofl.list.destutter_is_chain':l.destuttersatisfieschain' R.- Analogies of these theorems for
list.destutter', which is thedestutterequivalent ofchain.
Tags #
adjacent, chain, duplicates, remove, list, stutter, destutter
@[simp]
theorem
list.destutter'_nil
{α : Type u_1}
(R : α → α → Prop)
[decidable_rel R]
{a : α} :
list.destutter' R a list.nil = [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) :
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}
[decidable_rel R]
{a b : α}
(h : ¬R b a) :
list.destutter' R b (a :: l) = list.destutter' R b l
@[simp]
theorem
list.destutter'_sublist
{α : Type u_1}
(l : list α)
(R : α → α → Prop)
[decidable_rel R]
(a : α) :
list.destutter' R a l <+ a :: l
theorem
list.mem_destutter'
{α : Type u_1}
(l : list α)
(R : α → α → Prop)
[decidable_rel R]
(a : α) :
a ∈ list.destutter' R a l
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 : α) :
list.chain' R (list.destutter' R a l)
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 : α) :
list.destutter' R a l = a :: l ↔ list.chain R a l
theorem
list.destutter'_ne_nil
{α : Type u_1}
(l : list α)
(R : α → α → Prop)
[decidable_rel R]
{a : α} :
list.destutter' R a l ≠ list.nil
@[simp]
theorem
list.destutter_cons'
{α : Type u_1}
(l : list α)
(R : α → α → Prop)
[decidable_rel R]
{a : α} :
list.destutter R (a :: l) = list.destutter' R a l
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 : α} :
list.destutter R [a] = [a]
@[simp]
theorem
list.destutter_sublist
{α : Type u_1}
(R : α → α → Prop)
[decidable_rel R]
(l : list α) :
list.destutter R l <+ l
theorem
list.destutter_is_chain'
{α : Type u_1}
(R : α → α → Prop)
[decidable_rel R]
(l : list α) :
list.chain' R (list.destutter R l)
theorem
list.destutter_of_chain'
{α : Type u_1}
(R : α → α → Prop)
[decidable_rel R]
(l : list α) :
list.chain' R l → list.destutter R l = l
@[simp]
theorem
list.destutter_eq_self_iff
{α : Type u_1}
(R : α → α → Prop)
[decidable_rel R]
(l : list α) :
list.destutter R l = l ↔ list.chain' R l
theorem
list.destutter_idem
{α : Type u_1}
(l : list α)
(R : α → α → Prop)
[decidable_rel R] :
list.destutter R (list.destutter R l) = list.destutter R l
@[simp]