go_ne_nil — Mathlib

English

Let p be a predicate on α and xs, acc strings of α. Then the value go p xs acc is never the empty list.

Русский

Пусть p — предикат на α и dаны xs, acc списки α. Тогда значение go p xs acc никогда не является пустым списком.

LaTeX

$$$\\forall \\alpha\\,(p: \\alpha \\to \\mathrm{Bool})\\,(xs, acc: \\mathrm{List}(\\alpha)),\\; \\splitOnP.go\\ p\\ xs\\ acc \\neq \\emptyset$$$

Lean4

theorem go_ne_nil (xs acc : List α) : splitOnP.go p xs acc ≠ [] := by induction xs generalizing acc <;> simp [go];
  split <;> simp [*]

Похожие утверждения