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.append_cons_inj_of_notMem_prefix: two splits of a list at an element that occurs in neither prefix coincide.
• List.exists_eq_append_cons_of_exists_mem: a list with an element satisfying p splits at its first such element.
• List.flatMap_singleton_injective: a substitution by singletons is injective on words whenever the underlying map is injective.
• 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.append_cons_inj_of_notMem_prefix {α : Type u_1} {a : α} {x₁ x₂ z₁ z₂ : List α} (h₁ : ¬a ∈ x₁) (h₂ : ¬a ∈ x₂) : x₁ ++ a :: z₁ = x₂ ++ a :: z₂ ↔ x₁ = x₂ ∧ z₁ = z₂

Two splits of a list at an element a that occurs in neither prefix coincide.

theorem List.exists_eq_append_cons_of_exists_mem {α : Type u_1} {p : α → Prop} {l : List α} (h : ∃ (x : α), x ∈ l ∧ p x) : ∃ (u : List α), ∃ (x : α), ∃ (v : List α), l = u ++ x :: v ∧ p x ∧ ∀ (y : α), y ∈ u → ¬p y

A list with an element satisfying p splits at its first such element.

theorem List.flatMap_singleton_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) : Function.Injective fun (w : List α) => flatMap (fun (a : α) => [f a]) w

A substitution by singletons is injective on words whenever the underlying map is injective.

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.