List.splitOn #
theorem
List.splitOnP.go_acc
{α : Type u_1}
(p : α → Bool)
(xs acc : List α)
:
go p xs acc = modifyHead (fun (x : List α) => acc.reverse ++ x) (splitOnP p xs)
@[simp]
theorem
List.splitOnP_cons
{α : Type u_1}
(p : α → Bool)
(x : α)
(xs : List α)
:
splitOnP p (x :: xs) = if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)
theorem
List.splitOnP_spec
{α : Type u_1}
(p : α → Bool)
(as : List α)
:
(zipWith (fun (x1 x2 : List α) => x1 ++ x2) (splitOnP p as) (map (fun (x : α) => [x]) (filter p as) ++ [[]])).flatten = as
The original list L can be recovered by flattening the lists produced by splitOnP p L,
interspersed with the elements L.filter p.
theorem
List.splitOnP_eq_single
{α : Type u_1}
(p : α → Bool)
(xs : List α)
(h : ∀ x ∈ xs, ¬p x = true)
:
splitOnP p xs = [xs]
If no element satisfies p in the list xs, then xs.splitOnP p = [xs]
theorem
List.splitOnP_append_cons
{α : Type u_1}
(p : α → Bool)
(xs as : List α)
(sep : α)
(hsep : p sep = true)
:
splitOnP p (xs ++ sep :: as) = splitOnP p xs ++ splitOnP p as
When a list of the form [...xs, sep, ...as] is split at the sep element satisfying p,
the result is the concatenation of splitOnP called on xs and as
theorem
List.splitOnP_first
{α : Type u_1}
(p : α → Bool)
(xs : List α)
(h : ∀ x ∈ xs, ¬p x = true)
(sep : α)
(hsep : p sep = true)
(as : List α)
:
splitOnP p (xs ++ sep :: as) = xs :: splitOnP p as
When a list of the form [...xs, sep, ...as] is split on p, the first element is xs,
assuming no element in xs satisfies p but sep does satisfy p
theorem
List.intercalate_splitOn
{α : Type u_1}
(xs : List α)
(x : α)
[DecidableEq α]
:
[x].intercalate (splitOn x xs) = xs
intercalate [x] is the left inverse of splitOn x
theorem
List.splitOn_intercalate
{α : Type u_1}
(ls : List (List α))
[DecidableEq α]
(x : α)
(hx : ∀ l ∈ ls, x ∉ l)
(hls : ls ≠ [])
:
splitOn x ([x].intercalate ls) = ls
splitOn x is the left inverse of intercalate [x], on the domain
consisting of each nonempty list of lists ls whose elements do not contain x