Split a list into contiguous runs of elements which pairwise satisfy a relation.

This file provides the basic API for List.splitBy which is defined in Core. The main results are the following:

• List.flatten_splitBy: the lists in List.splitBy join to the original list.
• List.nil_notMem_splitBy: the empty list is not contained in List.splitBy.
• List.isChain_of_mem_splitBy: any two adjacent elements in a list in List.splitBy are related by the specified relation.
• List.isChain_getLast_head_splitBy: the last element of each list in List.splitBy is not related to the first element of the next list.

@[simp]

theorem List.splitBy_nil {α : Type u_1} (r : α → α → Bool) : splitBy r [] = []

@[simp]

theorem List.flatten_splitBy {α : Type u_1} (r : α → α → Bool) (l : List α) : (splitBy r l).flatten = l

@[simp]

theorem List.splitBy_eq_nil {α : Type u_1} {r : α → α → Bool} {l : List α} : splitBy r l = [] ↔ l = []

theorem List.splitBy_ne_nil {α : Type u_1} {r : α → α → Bool} {l : List α} : splitBy r l ≠ [] ↔ l ≠ []

@[simp]

theorem List.nil_notMem_splitBy {α : Type u_1} (r : α → α → Bool) (l : List α) : ¬[] ∈ splitBy r l

theorem List.ne_nil_of_mem_splitBy {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List α} (h : m ∈ splitBy r l) : m ≠ []

theorem List.head_head_splitBy {α : Type u_1} (r : α → α → Bool) {l : List α} (hn : l ≠ []) : ((splitBy r l).head ⋯).head ⋯ = l.head hn

theorem List.getLast_getLast_splitBy {α : Type u_1} (r : α → α → Bool) {l : List α} (hn : l ≠ []) : ((splitBy r l).getLast ⋯).getLast ⋯ = l.getLast hn

theorem List.isChain_of_mem_splitBy {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List α} (h : m ∈ splitBy r l) : IsChain (fun (x y : α) => r x y = true) m

theorem List.isChain_getLast_head_splitBy {α : Type u_1} (r : α → α → Bool) (l : List α) : IsChain (fun (a b : List α) => ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) (splitBy r l)

theorem List.splitBy_of_isChain {α : Type u_1} {r : α → α → Bool} {l : List α} (hn : l ≠ []) (h : IsChain (fun (x y : α) => r x y = true) l) : splitBy r l = [l]

theorem List.splitBy_flatten {α : Type u_1} {r : α → α → Bool} {l : List (List α)} (hn : ¬[] ∈ l) (hc : ∀ (m : List α), m ∈ l → IsChain (fun (x y : α) => r x y = true) m) (hc' : IsChain (fun (a b : List α) => ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l) : splitBy r l.flatten = l

theorem List.splitBy_eq_iff {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List (List α)} : splitBy r m = l ↔ m = l.flatten ∧ ¬[] ∈ l ∧ (∀ (m : List α), m ∈ l → IsChain (fun (x y : α) => r x y = true) m) ∧ IsChain (fun (a b : List α) => ∃ (ha : a ≠ []), ∃ (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) l

A characterization of splitBy m r as the unique list l such that:

• The lists of l join to m.
• It does not contain the empty list.
• Every list in l is IsChain of r.
• The last element of each list in l is not related by r to the head of the next.

theorem List.splitBy_append {α : Type u_1} {r : α → α → Bool} {l m : List α} (ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false) : splitBy r (l ++ m) = splitBy r l ++ splitBy r m

theorem List.splitBy_append_cons {α : Type u_1} {r : α → α → Bool} {l : List α} {a : α} (m : List α) (ha : ∀ (x : α), x ∈ l.getLast? → r x a = false) : splitBy r (l ++ a :: m) = splitBy r l ++ splitBy r (a :: m)