List append boundaries and unary delimiters

Main results

• List.rdropWhile_append: drop matching suffix elements across an append boundary.
• List.zip_tail_append_cons: split adjacent pairs at a shared boundary element.
• List.replicate_not_append_cons_inj, List.replicate_true_append_false_inj: a unary block followed by its delimiter determines both its length and the remaining suffix.
• List.idxOf_replicate_append_cons_of_ne, List.idxOf_false_replicate_append, List.idxOf_true_replicate_false_append: the index of a delimiter following a unary block.
• List.eq_replicate_idxOf_false, List.eq_replicate_idxOf_true: canonical decomposition of a word by its first delimiter.

theorem List.rdropWhile_append {α : Type u_1} (p : α → Bool) (l₁ l₂ : List α) : rdropWhile p (l₁ ++ l₂) = if rdropWhile p l₂ = [] then rdropWhile p l₁ else l₁ ++ rdropWhile p l₂

Dropping from the right of an appended list drops from the suffix first.

theorem List.zip_tail_append_cons {α : Type u_1} (before : List α) (middle : α) (after : List α) : (before ++ middle :: after).zip (before ++ middle :: after).tail = (before ++ [middle]).zip (before ++ [middle]).tail ++ (middle :: after).zip after

Split consecutive pairs at a boundary element shared by the two list segments.

theorem List.replicate_not_append_cons_inj {a : Bool} {m m' : ℕ} {l l' : List Bool} (h : (replicate m !a) ++ a :: l = (replicate m' !a) ++ a :: l') : m = m' ∧ l = l'

A unary block of copies of !a followed by the delimiter a determines both its length and the remaining suffix.

theorem List.replicate_true_append_false_inj {m m' : ℕ} {l l' : List Bool} (h : replicate m true ++ false :: l = replicate m' true ++ false :: l') : m = m' ∧ l = l'

A unary block of true bits followed by false determines both its length and the remaining suffix.

theorem List.idxOf_replicate_append_cons_of_ne {α : Type u_1} [DecidableEq α] {a b : α} (hab : a ≠ b) (k : ℕ) (l : List α) : idxOf b (replicate k a ++ b :: l) = k

The first occurrence of b in (replicate k a ++ b :: l) is at index k, provided a ≠ b.

@[simp]

theorem List.idxOf_false_replicate_append (k : ℕ) (l : List Bool) : idxOf false (replicate k true ++ false :: l) = k

The first occurrence of false in a list beginning with k trues is at index k.

@[simp]

theorem List.idxOf_true_replicate_false_append (k : ℕ) (l : List Bool) : idxOf true (replicate k false ++ true :: l) = k

The first occurrence of true in a list beginning with k falses is at index k.

theorem List.eq_replicate_idxOf_false {l : List Bool} (hl : false ∈ l) : l = replicate (idxOf false l) true ++ false :: drop (idxOf false l + 1) l

A Boolean word containing false decomposes into a unary run of trues up to the first false, and the remaining suffix.

theorem List.eq_replicate_idxOf_true {l : List Bool} (hl : true ∈ l) : l = replicate (idxOf true l) false ++ true :: drop (idxOf true l + 1) l

A Boolean word containing true decomposes into a unary run of falses up to the first true, and the remaining suffix.