splitOn_intercalate — Mathlib

English

SplitOn x is the left inverse of intercalate [x] on the domain of nonempty lists ls with no element containing x.

Русский

SplitOn x — левая обратная функция по отношению к intercalate [x] на множестве непустых списков ls, элементы которых не содержат x.

LaTeX

$$$\\forall {\\alpha} (x: \\alpha) (ls: \\mathrm{List}(\\mathrm{List}(\\alpha)))\\; (ls \\neq []) \\land (\\forall l \\in ls, x \\notin l) \\Rightarrow \\mathrm{splitOn} x (ls.intercalate [x]) = ls$$$

Lean4

/-- `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` -/
theorem splitOn_intercalate [DecidableEq α] (x : α) (hx : ∀ l ∈ ls, x ∉ l) (hls : ls ≠ []) :
    ([x].intercalate ls).splitOn x = ls := by
  simp only [intercalate]
  induction ls with
  | nil => contradiction
  | cons hd tl ih => ?_
  cases tl
  · suffices hd.splitOn x = [hd] by simpa [flatten]
    exact splitOnP_eq_single _ _ (by grind)
  · simp only [intersperse_cons₂, singleton_append, flatten]
    specialize ih _ _
    · grind
    · grind
    simp only [splitOn] at ih ⊢
    have := splitOnP_first (· == x) hd (by grind) x (beq_self_eq_true _)
    rw [this, ih]

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