English
The original list L can be reconstructed by interleaving the pieces produced by splitOnP p L with the elements of L that satisfy p, then flattening.
Русский
Исходный список L можно восстановить, чередуя куски, полученные методом splitOnP p L, с элементами L, удовлетворяющими p, затем расплющивая результат.
LaTeX
$$$\\forall {\\alpha} (p: \\alpha \\to \\mathrm{Bool}) (as: \\mathrm{List}(\\alpha)),\\; \\operatorname{flatten} (\\operatorname{zipWith} (\\\\cdot \\\\ + \\\\cdot ) (\\mathrm{splitOnP}\\ p\\ as) ((as.filter p).map (\\\\lambda x. [x]) \\\\+ [[]])) = as$$$
Lean4
/-- The original list `L` can be recovered by flattening the lists produced by `splitOnP p L`,
interspersed with the elements `L.filter p`. -/
theorem splitOnP_spec (as : List α) :
flatten (zipWith (· ++ ·) (splitOnP p as) (((as.filter p).map fun x => [x]) ++ [[]])) = as := by
induction as with
| nil => rfl
| cons a as' ih =>
rw [splitOnP_cons, filter]
by_cases h : p a
· rw [if_pos h, h, map, cons_append, zipWith, nil_append, flatten, cons_append, cons_inj_right]
exact ih
· rw [if_neg h, eq_false_of_ne_true h,
flatten_zipWith (splitOnP_ne_nil _ _) (append_ne_nil_of_right_ne_nil _ (cons_ne_nil [] [])), cons_inj_right]
exact ih
where flatten_zipWith {xs ys : List (List α)} {a : α} (hxs : xs ≠ []) (hys : ys ≠ []) :
flatten (zipWith (fun x x_1 ↦ x ++ x_1) (modifyHead (cons a) xs) ys) =
a :: flatten (zipWith (fun x x_1 ↦ x ++ x_1) xs ys) :=
by
cases xs with
| nil => contradiction
| cons =>
cases ys with
| nil => contradiction
| cons => rfl
