Append congruence for List.destutter

Mathlib's Mathlib/Data/List/Destutter.lean has no destutter-vs-append lemma. These fill that gap for the (· ≠ ·) relation: collapsing either operand before appending is absorbed by an outer destutter, so destutter (· ≠ ·) is a congruence for ++. The proofs go through destutter' boundary scaffolding. Candidates for Mathlib/Data/List/Destutter.lean.

Main results

• List.destutter_append_left / List.destutter_append_right — collapsing one operand before appending does not change the destuttered result.
• List.destutter_append_destutter — the congruence: destutter (· ≠ ·) of an append equals destutter (· ≠ ·) of the destuttered operands.
• List.destutter_head? — destutter preserves the head.
• List.destutter_append_length_clean — the clean-clean boundary length: two (· ≠ ·) chains concatenated and destuttered merge exactly one element iff the seam matches.
• List.destutterConcat — append then destutter; the multiplication of the destutter quotient monoid, with its associativity and unit laws (pure List facts).

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

Collapsing the left operand before appending does not change the destuttered result.

theorem List.destutter_append_right {α : 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)

Collapsing the right operand before appending does not change the destuttered result.

theorem List.destutter_append_destutter {α : 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)

The append congruence: destutter (· ≠ ·) of an append equals destutter (· ≠ ·) of the destuttered operands.

Head and the clean-clean boundary

theorem List.destutter'_replicate_self {α : 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_head? {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (l : List α) : (destutter R l).head? = l.head?

destutter preserves the head: the running element is the input's head.

theorem List.destutter_append_length_clean {α : Type u_1} [DecidableEq α] {l m : List α} (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

The clean-clean boundary length. 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. The numerical core of the autosegmental OCP quotient (Phonology/Autosegmental/Collapse.lean).

Append-then-destutter

destutterConcat — append, then collapse the single run that may form at the seam — is the multiplication of the destutter quotient monoid (built on the free monoid in Mathlib.Algebra.FreeMonoid.Destutter). Associativity and the unit laws reduce to the ++-congruences above, so they are pure List facts and live here.

def List.destutterConcat {α : Type u_1} [DecidableEq α] (x y : List α) : List α

Append then destutter: concatenate, then collapse the single run that may form at the seam. The multiplication of the destutter quotient monoid.

Equations

• x.destutterConcat y = List.destutter (fun (x1 x2 : α) => x1 ≠ x2) (x ++ y)

theorem List.isChain_destutterConcat {α : Type u_1} [DecidableEq α] (x y : List α) : IsChain (fun (x1 x2 : α) => x1 ≠ x2) (x.destutterConcat y)

destutterConcat outputs are stutter-free.

theorem List.destutterConcat_assoc {α : Type u_1} [DecidableEq α] (x y z : List α) : (x.destutterConcat y).destutterConcat z = x.destutterConcat (y.destutterConcat z)

destutterConcat is associative — inherited from ++ through destutter.

theorem List.nil_destutterConcat {α : Type u_1} [DecidableEq α] (x : List α) : [].destutterConcat x = destutter (fun (x1 x2 : α) => x1 ≠ x2) x

theorem List.destutterConcat_nil {α : Type u_1} [DecidableEq α] (x : List α) : x.destutterConcat [] = destutter (fun (x1 x2 : α) => x1 ≠ x2) x

theorem List.destutter_append_eq_destutterConcat {α : Type u_1} [DecidableEq α] (x y : List α) : destutter (fun (x1 x2 : α) => x1 ≠ x2) (x ++ y) = (destutter (fun (x1 x2 : α) => x1 ≠ x2) x).destutterConcat (destutter (fun (x1 x2 : α) => x1 ≠ x2) y)

destutter (· ≠ ·) carries (List α, ++) onto (·, destutterConcat).