English
For any xs and acc, the function go p xs acc equals modifyHead (acc.reverse ++ ·) (splitOnP p xs).
Русский
Для любых xs и acc функция go p xs acc равна modifyHead (acc.reverse ++ ·) (splitOnP p xs).
LaTeX
$$$\\forall {\\alpha} (p: \\alpha \\to \\mathrm{Bool}) (xs acc: \\mathrm{List}(\\alpha)),\\; \\mathrm{splitOnP.go}\\ p\\ xs\\ acc = \\mathrm{modifyHead}(\\mathrm{acc.reverse} ++ \\cdot)(\\mathrm{splitOnP}\\ p\\ xs)$$$
Lean4
theorem go_acc (xs acc : List α) : splitOnP.go p xs acc = modifyHead (acc.reverse ++ ·) (splitOnP p xs) := by
induction xs generalizing acc with
| nil => simp only [go, modifyHead, splitOnP_nil, append_nil]
| cons hd tl ih =>
simp only [splitOnP, go]; split
· simp only [modifyHead, reverse_nil, append_nil]
· rw [ih [hd], modifyHead_modifyHead, ih]
congr; grind
