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. From it, destuttering the left operand first changes nothing for any relation, and for (· ≠ ·) the same holds on the right, so destutter (· ≠ ·) is a congruence for ++. Lemmas specific to (· ≠ ·) carry the _ne suffix as in List.map_destutter_ne. [UPSTREAM] candidates for that file.

Main results

• List.head?_destutter', List.head?_destutter, List.destutter'_eq_cons: the running element stays in front, so destutter preserves the head.
• List.destutter'_append: the append decomposition.
• List.destutter_append_left, List.destutter_append_right_ne, List.destutter_append_destutter_ne: absorbing a destutter of either operand, and the ++-congruence.
• List.destutter_replicate: a constant run fuses to one element when the relation is irreflexive at it.
• List.IsChain.length_destutter_ne_append: two chains concatenated and destuttered lose exactly one element when the seam matches, the numerical core of the autosegmental OCP quotient.

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

Destuttering from a keeps a in front.

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

destutter preserves the 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

The append decomposition: destuttering l ++ m from a destutters l from a, then destutters m from the last element kept.

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)

Destuttering the left operand before appending does not change the result.

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]

destutter fuses a constant run whenever the relation is irreflexive at its element.

theorem List.destutter'_destutter_ne {α : Type u_1} [DecidableEq α] (a : α) (m : List α) : destutter' (fun (x1 x2 : α) => x1 ≠ x2) a (destutter (fun (x1 x2 : α) => x1 ≠ x2) m) = destutter' (fun (x1 x2 : α) => x1 ≠ x2) a m

Destuttering from a is insensitive to a prior destutter (· ≠ ·) of the argument: after collapsing, a either differs from the head or equals it, and both cases agree.

theorem List.destutter_append_right_ne {α : Type u_1} [DecidableEq α] (l m : List α) : destutter (fun (x1 x2 : α) => x1 ≠ x2) (l ++ destutter (fun (x1 x2 : α) => x1 ≠ x2) m) = destutter (fun (x1 x2 : α) => x1 ≠ x2) (l ++ m)

Destuttering the right operand before appending does not change the result. Unlike List.destutter_append_left, this needs (· ≠ ·): a dropped element must behave like the running one, which for (· ≠ ·) means being equal to it.

theorem List.destutter_append_destutter_ne {α : Type u_1} [DecidableEq α] (l m : List α) : destutter (fun (x1 x2 : α) => x1 ≠ x2) (l ++ m) = destutter (fun (x1 x2 : α) => x1 ≠ x2) (destutter (fun (x1 x2 : α) => x1 ≠ x2) l ++ destutter (fun (x1 x2 : α) => x1 ≠ x2) m)

destutter (· ≠ ·) is a congruence for ++.

theorem List.IsChain.length_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)).length = l.length + m.length - if l.getLast? = m.head? then 1 else 0

Two chains concatenated and destuttered merge only at the seam: the length is the sum of lengths minus one exactly when the last element of l equals the first of m.