List append boundaries and unary delimiters

Main results

• 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.

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.