List.destutter and ++

Mathlib/Data/List/Destutter.lean has no lemma relating destutter to ++. The primitive is the append decomposition List.destutter'_append: destuttering l ++ m from a destutters l from a and then m from the last element kept. Destuttering the left operand first changes nothing for any relation. When the negation of the relation is an equivalence, as for (· ≠ ·), the same holds on the right, so destutter is a congruence for ++. [UPSTREAM] candidates for that file.

Main statements

• List.head?_destutter: destutter preserves the head.
• List.destutter'_append: the append decomposition.
• List.destutter_append_left, List.destutter_append_right: absorbing a destutter of either operand, so List.destutter_append_destutter makes destutter a congruence for ++.
• List.destutter_replicate: a constant run fuses to one element.
• List.IsChain.destutter_ne_append: two (· ≠ ·)-chains concatenated and destuttered merge only at the seam.

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

@[simp]

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

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

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

theorem List.destutter'_append {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (a : α) (l m : List α) : destutter' R a (l ++ m) = destutter' R a l ++ (destutter' R ((destutter' R a l).getLastD a) m).tail

Destuttering l ++ m from a destutters l from a, then m from the last element kept.

@[simp]

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

theorem List.destutter'_replicate {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {a : α} (h : ¬R a a) (n : ℕ) : destutter' R a (replicate n a) = [a]

theorem List.destutter_replicate {α : Type u_1} {R : α → α → Prop} [DecidableRel R] {a : α} (h : ¬R a a) (n : ℕ) : destutter R (replicate (n + 1) a) = [a]

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

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

theorem List.destutter'_destutter {α : Type u_1} {R : α → α → Prop} [DecidableRel R] [IsEquiv α Rᶜ] (a : α) (m : List α) : destutter' R a (destutter R m) = destutter' R a m

@[simp]

theorem List.destutter_append_right {α : Type u_1} {R : α → α → Prop} [DecidableRel R] [IsEquiv α Rᶜ] (l m : List α) : destutter R (l ++ destutter R m) = destutter R (l ++ m)

theorem List.destutter_append_destutter {α : Type u_1} {R : α → α → Prop} [DecidableRel R] [IsEquiv α Rᶜ] (l m : List α) : destutter R (destutter R l ++ destutter R m) = destutter R (l ++ m)

theorem List.IsChain.destutter_ne_append {α : Type u_1} {l m : List α} [DecidableEq α] (h1 : IsChain (fun (x1 x2 : α) => x1 ≠ x2) l) (h2 : IsChain (fun (x1 x2 : α) => x1 ≠ x2) m) : destutter (fun (x1 x2 : α) => x1 ≠ x2) (l ++ m) = if l.getLast? = m.head? then l ++ m.tail else l ++ m

Destuttering two concatenated chains merges at most the seam, dropping the head of m exactly when it repeats the last element of l.